[isabelle-dev] Locale interpretation with mixins

[Makarius]

On Thu, 6 Sep 2012, Florian Haftmann wrote:

> Hi Clemens, hi Makarius,
>
> (sorry for being so little reactive on this imminent thread, but it 
> requires considerable preheating to catch the critical points)

The preheating is definitely a problem.  We somehow need to try to get a 
critical mass of insight into this issue, to address it eventually.

In some sense it is a leftover from our "national debts" from 2006/2007. 
Already back then, I was very abstractly wondering together with Clemens 
about the question, how certain codgeneration issues could be fully 
integrated into the locale + interpretation concepts, without subtraction 
from either side or adding just workarounds.


>> 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?
>
> Well, it can accomplish anything you tell it to do (cf. 
> http://dilbert.com/strips/comic/2006-01-29/).  But the idea has always 
> been to rely as closely as possible on the foundation without doing more 
> extralogical things than necessary.

The term "foundation" was actually introduced formally in one of the local 
theory target reforms by yourself, e.g. see 
http://isabelle.in.tum.de/repos/isabelle/file/38af9102ee75/src/Pure/Isar/generic_target.ML#l292

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

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?

Some months ago I mentally experimented with a notion of explicit 
"boundaries" for locale contexts and somehow follow the structure of 
interpretations.  This could help here, although in the first and second 
round of testing the hypothesis against the real system, I got deflected.
It might also turn out to be too complicated as a concept.


 	Makarius