Re: [isabelle] [isabelle-dev] Code generation in Isabelle

I opt for code_unfold because the code generator's preprocessor is more powerful than mere inlining of definitions. For example, you can

1. write a bottom-up-rewrite optimiser for terms (very useful for automatically generated code equations such as those by code_pred), and

2. use type restrictions or conditions in code_unfold theorems to redirect calls to different implementations based on the calling context,.


Am 18.10.2011 08:54, schrieb Lukas Bulwahn:
Hello all,

I am reporting on the continuation to remove the ancient code generator, related
to an earlier mail this July.

at the moment, we have two code generators in Isabelle:

1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML
without supporting type classes.
Commands to invoke it were code_module and code_library.

2. A generic code generator in Isabelle by Florian Haftmann - extenible to
multiple target languages, supporting type classes, basic integration of
reflection and abstraction mechanisms
Commands to invoke it are export_code, value, code_reflect, and some others.

The second subsumes the first, so we intend to remove the first code generator
from the next Isabelle distribution if there are not any strong defenders of
the ancient code generator.

We are getting closer to remove the ancient code generator.
In this process, the preprocessing attributes of the code generator code_unfold
and code_inline now have the same semantics. Hence, only one has to be kept.

At the moment, there are four attributes related to code generation
preprocessing, code_unfold and code_inline, code_post and code_unfold_post.

Florian and I are not sure if code_inline or code_unfold fit better to the
intended behaviour of "rewriting a code equation by some simplifying equation"
(unfolding a term by its definition, or inlining the definition).

Does anyone have a suggestion?


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.