[isabelle-dev] Code generation in Isabelle
bulwahn at in.tum.de
Tue Oct 18 08:54:53 CEST 2011
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
> 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?
More information about the isabelle-dev