On Thu, 18 Sep 2014, Andreas Lochbihler wrote:
Currently, the code generator has its own manager of plugins
(Code.datatype_interpretation) and I would be very happy if certain
plugins could be disabled selectively upon code_datatype commands. For
example, in AFP/Coinductive, I would like code_datatype to not change
the code equations for the partial_term_of instantiations, because it
does not (and cannot in general) adapt the equations for narrowing, but
the two should be in sync. At present (AFP/222773085523), I have to undo
the effect of the partial_term_of plugin in Lazy_LList.thy and
Lazy_TLList.thy by writing ugly code equations. It would be much easier
to disable the plugin locally for this declaration.
I would expect that if Jasmin's plugin manager is also used in the code
generator, it would be easy to implement plugin selection for
code_datatype, too.
This should work out easily with the unified Plugin_Name and Plugin
concept of
http://isabelle.in.tum.de/repos/isabelle/file/1891f17c6124/src/Pure/Tools/plugin.ML
Plugin_Name.declare and related operations manage a name space of plugins
for commands, with semantic completion etc. The operations around
Plugin_Name.filter allow a command to restrict the use of plugins
systematically.
(A potential source of user confusion is the unchecked combination of all
plugins with all commands in the name space, i.e. the semantic completion
may offer a plugin for a command that is not known to it. On the other
hand, commands may be built on top of each other, and I did not want to
add further complexity for some inheritance system of plugins.)
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org 738,307 people so far
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
