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___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
