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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
