Email Gateway (Aug 18 2022 at 18:32): Email Gateway (Aug 18 2022 at 18:32):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hello all,
I am reporting on the continuation to remove the ancient code generator,
related to an earlier mail this July.
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
Email Gateway (Aug 18 2022 at 18:32):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
I opt for code_unfold because the code generator's preprocessor is more powerful
than mere inlining of definitions. For example, you can
write a bottom-up-rewrite optimiser for terms (very useful for automatically
generated code equations such as those by code_pred), and
use type restrictions or conditions in code_unfold theorems to redirect calls
to different implementations based on the calling context,.
Andreas
Email Gateway (Aug 18 2022 at 18:32):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
I would also vote for "code_unfold", if nothing else for consistency with the similar "nitpick_unfold" tag.
When I introduced "nitpick_unfold" I also considered "nitpick_inline", but concluded that the "unfold" terminology is from theorem proving and the "inline" terminology from the world of compilers. For the code generator, the argument swings both ways, though...
Jasmin
Email Gateway (Aug 18 2022 at 18:32):From: Makarius <makarius@sketis.net>
Good that you have answered the mail by Lukas only on one of the two
mailing list, to avoid the duplication -- isabelle-dev should be a small
subset of the larger audience of isabelle-users.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC