[isabelle-dev] Locale interpretation with mixins

[Clemens Ballarin]

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
>      
> 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