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



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?


Lukas





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