Quoting Makarius <makar...@sketis.net>:
It means that a "constant" c that depends on context parameters x y
z is turned into a fountational constant "loc.c" in the background,
and then re-imported into the local context as "loc.c x y z. Later
it might get re-interpreted such that its dependency on former
context parameters is turned into terms (by intepretation) or the
whole thing "loc.c t1 t2 t3" is replaced by something else
(rewriting via mixins etc.).
If we can mark 'loc.c x y z' to make it atomic in tools like the
simplifier (or, for uniformity, the entire system) I believe we are
much better off. Let's use angular brackets to mark the atomic part:
<loc.c x y z>. When parameters are instantiated, the thing should
remain atomic: <loc.c t1 t2 t3>, because it denotes a constant in some
other context. If a rewrite morphism is applied, say <loc.c t1 t2 t3>
= t4, then it should not remain atomic, for it is now the compound
term the user turned it into.
So when the code generator sees an interpreted function application
"loc.c t1 t2 t3 x y z" it should somehow do the right thing, in
taking it as "(loc.c t1 t2 t3) x y z", and considering the inner
part as "atomic entity" (and instance of c defined earlier in the
abstract context).
On our running gag list with have at least these related issues:
* codgeneration as sketched above
* behaviour of the Simplifier on seemingly atomic "constants" c (due
to abbreviations) that are actually of the form "loc.c x y z"
* stability and expectedness of abbreviations, as they are printed
* the Haftmann/Wenzel educated guess here
http://isabelle.in.tum.de/repos/isabelle/file/38af9102ee75/src/Pure/Isar/named_target.ML#l56
which can be traced back here:
http://isabelle.in.tum.de/repos/isabelle/rev/9dd61cb753ae
(Fall/Winter 2007 was the time where we desparately tried to recover
from the 2006/2007 gap in the Isabelle release chain).
Is there any nice, sane, simple approach to all that?
My impression it that this would address the first two points; I don't
have enough insight to judge the others.
Some months ago I mentally experimented with a notion of explicit
"boundaries" for locale contexts and somehow follow the structure of
interpretations.
I'm not sure, but what you describe seems more elaborate than what I
sketched above.
Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
