[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

There is a series of minimal invasive patches to generalize
»interpretation« / »sublocale« to »interpretation« in arbitrary targets,
not just theories and locales. The patches are inspectible at

	http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation

Explanations follow. It is good tradition not to muddle with the module
system code arbitrarily, therefore this rather unconventional approach
to gain feedback.

1.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5
	Identity juggling to prepare following steps.

2.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/aee4c6577ff7

	Ironing out a FIXME in the code. This already gives a hint how the
existing code base naturally converges to unify »interpretation« and
»sublocale«.

3.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f6bc704b5cd6

	In order to let »interpretation« and »sublocale« converge, the close
marriage of »interpretation« and »interpret« must be given up. This is a
step back only in the first instance – it would still be possible to
factor out common code of the resulting unified »interpretation« and
»interpret« in a separate step afterwards. In the same breath the
(operationally void!) switch from »ctxt« to »lthy« yields the key clue
of the whole story.

4.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/9d5c8a5251d5

	This establishes sharing of »interpretation« and »sublocale« as far as
appropriate.

5.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/1d3a62ef74dd

	Identity juggling to prepare following steps.

6.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/dd6dd81381fb

	This is the key step: »subscription« as target operation to make
»interpretation« work regardless of the underlying target.
	The »potential_reinit« is a wart: when interpreting locales into
locales, the new facts must be provided in the local theory context of
this locale also, and I have up after a few experiments with
Locale.activate_facts etc. Note the same situation has been occuring in
»subclass« for years now. Here it is more critical since interpretation
should be fully target-ignorant (unlike subclass which always knows that
it operates on classes). However I have let it stand for the moment as a
conceptual preview. I'm thankful for any hints how to resolve this.
	In this change the clone in src/Tools/ has been changed accordingly –
its future is still not so clear yet.

7.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f48553718a7a

	Some examples. Note that I have experienced that »interpretation« does
sometimes not work inside »instantiation« (something in connection with
abbreviations), but this indicates a weakness of the instantiation
target rather than a conceptual mistake in interpretation. This needs to
be amended separately.

The next steps after those would be something like
* Amend the wart mentioned in (6).
* Add documentation.
* One round trip over the whole sources to avoid references to (then
legacy) »sublocale«.
* Amend the instantiation target not to choke on abbreviations stemming
from interpretations.
* Examine whether this code basis already allows to have confined
interpretations inside context … begin … end blocks.

I'm looking forward to responses.

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: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130324/e07b1393/attachment.asc>