[isabelle-dev] Code generation in Isabelle

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


Lukas