[isabelle-dev] Locale interpretation with mixins
ballarin at in.tum.de
Sat Sep 8 21:08:17 CEST 2012
Quoting Makarius <makarius at 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
> which can be traced back here:
> (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
I'm not sure, but what you describe seems more elaborate than what I
More information about the isabelle-dev