[isabelle-dev] Proposal for localized interpretations

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140910/19bcc11b/attachment.sig>