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

[Florian Haftmann]

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

Good observation.  I will consider to hook up
Code.add_default_eqn_attrib with the existing Spec_Rules rather than
having it parallel.

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

It depends.  Really both forms (singleton and incremental-non-singleton)
are present, according to a quick look and Andreas Lochbihler (who is
really acquainted with code generation »in the large«).

For the moment I am pondering the following (*):

* Turn [code] into an attribute for singleton declaration (dropping
previous ones).  Introduce [code add] as means to modify an existing
code declaration by adding another equation – but unless [code] now,
make a formal declaration of *all* code equation afterwards.  Keep [code
abstype] and [code abstract] as they are now, they are always singleton
by construction.
* If this interface does not suffice, use a declaration »code_function«
as sketched above, with auxiliary syntax to distinguish literal
equations from name references to existing theorems (yes, we will need
both), and, to be a real superset of the attribute declarations above,
auxiliary syntax to introduce abstract code equations etc.  Other
auxiliary syntax would drop all equations for a particular constant,
making the funny joke »lemma [code, code del]: "f = f" .. obsolete.

This would allow to apply preprocessing after each declaration
immediately with direct error reporting etc.

Alas, I must add that this does not yet give us what we need concerning
the interpretation story: the current preprocessor does not change the
head of equations – which is normally desired since you do not want a
preprocessing rule to turn an equation for foo into an equation for bar.
 But this is exactly what we need to fold equations from locale
interpretations.  So, yet another layer still has to be added.

Nevertheless, the ideas sketched in (*) seem to be worth exploring on
their own.  What remains unsatisfactory is that two different ways are
provided.

An alternative could be to abuse meta-conjunction &&& for simultaneous
code equations, but it is doubtful whether it s a good idea to introduce
the user to that rather internal notation.

	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/20121011/74e3ba43/attachment.sig>