[isabelle-dev] Proposal for localized interpretations

[Makarius]

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
----------------------------------------------------------------------------