[isabelle-dev] An note on code generator bookkeeping and the code generator preprocessor [was: Locale interpretation with mixins]
makarius at sketis.net
Fri Oct 5 16:03:49 CEST 2012
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) = …"
> 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
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
> 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
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)?
More information about the isabelle-dev