Hi Jasmin, […]
> 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?
when we started this hook business, the situation was as follows:
a) Hook clients were all for adding type class instances, i.e.
inherently working a the theory level.
b) Hooks were a bootstrap device, e.g. after a certain point in the
theory hierarchy they were considered to be »sealed« (by convention, not
by implementation).
c) There were a few experimental theories which would add further hooks
– these theories are gone nowadays.
So, the questions IMHO are:
1. Is a) still valid today? Maybe not, since the error in questions
seems related to transfer.
2. What is the matter with b)?
I am not sure where to go from here. Of course to fully generalize we
would need a concept of »reconstructable« local theory, i.e. each
target would provide an operation reenter :: local_theory -> (theory ->
local_theory) option. Is it worth the effort? It appears very similar
to the ancient infamous reinit operation.
So far a few rough considerations.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
