On Sun, 22 Jul 2012, Florian Haftmann wrote:
Hi Clemens, hi Makarius,
let me resume this running thread (not necessarily gag).
Let me quote two emails by Clemens on this issue:
a) There is the mechanism for locale interpretation, which permits
arbitrary mixin morphisms
b) There is the interpretation command, which exposes the mixin
interface by taking equations as arguments.
After studying the sources a few times this year and reading again various
documents by Clemens, I think I understand at last a bit how it works,
which does not mean it would be easy nor easy to change.
My argument is (and that's what's prototyped in
Tools/interpretation_with_defs.ML) that there are alternatives for the
user interface b).
The current interface allows
c) to map derived defs in a locale under interpretation to »existing terms«
The proposal is to extend this to allow also
d) mixins to map derived defs in a locale under interpretation to newly
introduced defs
In December 2011 we were both staring at interpretation_with_defs.ML and
could not fully see the principle how it would work for complex hiearchies
of locales and interpretations. I.e. it is EXPERIMENTAL with the
capitalization that you've put there in Jan 2011 (c34415351b6d).
Are there any new insights about it in the meantime?
Just a general question: Why does the code generator require a closed
constant as a starting point? Couldn't it just take an arbitrary term,
with some decoration how it should be abstracted into a closed thing?
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
