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

[Florian Haftmann]

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

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.

When code generation is issued, theorems are grouped together according
to their equation head and only then passed to the preprocesser, which
already requires the grouped view since it must be able to transform
e.g. the equations from above into
	f n = (if n = 0 … else …)
in Efficient_Nat.thy.

This also means that some checks which are only valid on the grouped
view are only to be carried out after preprocessing, not immediately
after declaration. The singleton declaration / grouped equations
mismatch has also some other funny consequences, e.g. non-standard
add/del behaviour and own ideas how the order of equations is determined
etc.

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>
(which can also be annotated to theorems which make sense as »normal«
theorem beyond code generation) 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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121004/3415fb31/attachment.sig>