[isabelle-dev] An note on code generator bookkeeping and the code generator preprocessor [was: Locale interpretation with mixins]

[Makarius]

On Thu, 4 Oct 2012, Florian Haftmann wrote:

>> The current infrastructure has only a preprocessor applied *after* the
>> internal bookkeeping (for reasons I will explain in a separate, long
>> promised mail), so this would add further complexity here.
>
> What sets the code generator apart from other tools is that theorems are
> never stand-alone but grouped according to their equation head.  E.g.
> the two theorems
> 	f (Suc n) = …
> 	f 0 = …
> belong inherently together, resulting in Haskell into something like
> 	f :: Nat -> …
> 	f (Suc n) = …
> 	f Zero = …
> Compare this e.g. to the simplifier where both theorems can stand for
> their own.

For now just some comments on this aspect that code theorems are organized 
in "packs".  (I've already made it a habit to re-read the cumulative mail 
thread on the whole topic every week, and the understanding increases 
slowly every time.)


> Internally, code theorems are declared as singleton declarations
> (typically via attributes), e.g.
> 	lemma [code]:
> 	  "f 0= …"
> 	  "f (Suc n) = …"
> 	  <proof>
> results in two separate declarations.

> Life would have been much more easier from the very beginning if the
> code generator would only have accepted simultaneous declarations. But I
> don't think this is possible. Either one would have to sacrifice the
> simple lightweight declaration
> 	lemma [code]:
> 	  "…" … "…" <proof>

Grouped declarations are not so alien, see the Spec_Rules concept that was 
introduced a few years ago. The the corresponding Morphism.fact for such 
declarations operates on thm list anyway.  It is merely a genuine 
simplification of attribute notation that it goes down to individual list 
members.

When you say "Internally" above, it probably refers to 
Code.add_default_eqn_attrib in the usual packages, which is mostly 
parallel to the slightly more modern Spec_Rules.add in the same packages.

So the question about [code] only comes up in Isar source notation.  It 
avoids an extra 'declaration' wrapper command like this:

> an instead having e.g. the more explicit
> and verbose
> 	code_function
> 	  "…"
> 	  "…"
> 	  by (fact …)+


> Or attributes would be changed to take simultaneous lists of theorems 
> instead of single ones, but I guess a such fundamental change of the 
> framework is not feasible.

This was an explicit simplification of the attribute language from the 
very beginning in 1999.  Later so many other aspects were adjoined to 
attributes that it became quite complex nonetheless.  So multi-attributes 
are off the radar to keep things manageable, and half understandable for 
the user (who already struggles to distinguish rule attributes from 
declaration attributes).

There are two ways to evade from this notational restriction:

   * explicit derivative of 'declaration' command, which is the fully
     general form (e.g. 'code_function' above)

   * additional "parameters" to attributes as part of the syntax:

       th [code th1 th2 ... thn]

     This form can then be used with 'declare' or 'lemmas'.


So how is the de-facto situation concerning [code] in the reachable 
universe of Isabelle libraries and applications? How many of [code] 
declarations are non-singleton (outside package implementations)?


 	Makarius