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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
