[isabelle-dev] Proposal for localized interpretations

[Andreas Lochbihler]

Dear developers,

Jasmin mentioned to me that his new implementation allows to select which plugins should 
be applied. 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.

Best,
Andreas

On 05/09/14 10:36, Jasmin Christian Blanchette wrote:
> Hi all,
>
> The "interpretation" mechanism, as defined in "Pure/interpretation.ML", is used in a few places in Isabelle, including the new (co)datatype package, for allowing other tools and users to register their hooks. Unfortunately, it works at the theory level, which interacts poorly with local definitions. For example, if you try
>
>     locale A =
>      fixes a :: 'a
>      assumes "a = a"
>     begin
>
>     datatype_new 'b x = X 'b
>
>     end
>
> with Isabelle2014, you will get
>
>     Undeclared hyps:
>         A a
>     The error(s) above occurred for the goal statement⌂:
>     left_total R ⟹ left_total (A.rel_x R)
>
> This error arises in the Transfer hook. I can think of no way to solve this at the theory level.
>
> To solve this issue, I introduced my own interpretation mechanism, in "HOL/Tools/Ctr_Sugar/local_interpretation.ML", that works both on theories and local theories. If you look at it, you will see that it is mostly a copy-paste job. The key insight is that there are three scenarios (taking datatypes as our example):
>
> 1. The datatype is defined after the hook is registered.
>
> 2a. The datatype is defined before the hook is registered.
>
> 2b. The dataype and the hooks are registered in two parallel theories, which are later merged.
>
> In case 1, one can imagine having the datatype directly giving its local theory to the hook. This is what "local_interpretation.ML" does, and this is enough to solve the problem in the example above. In case 2a and 2b, things have to be done at the theory level, like before, but this is a rarer case (e.g. we have no local datatypes in "Main"). Also, the odd signature management that was necessary before to make 2a and 2b work (cf. my April 2 email to this mailing list) is now centralized (cf. e6e3b20340be).
>
> I would like to propose either replacing the old mechanism by the new one or having both live in parallel in "Pure". It is certainly not perfect, but it is IMO an improvement over the statu quo. What do you think?
>
> Jasmin
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>