Email Gateway (Aug 22 2022 at 15:25): Email Gateway (Aug 22 2022 at 15:25):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new tool in the AFP.
Lazifying case constants
by Lars Hupel
Isabelle's code generator performs various adaptations for target languages.
Among others, case statements are printed as match expressions. Internally,
this is a sophisticated procedure, because in HOL, case statements are
represented as nested calls to the case combinators as generated by the
datatype package. Furthermore, the procedure relies on laziness of match
expressions in the target language, i.e., that branches guarded by patterns
that fail to match are not evaluated. Similarly, if-then-else is printed to
the corresponding construct in the target language. This entry provides
tooling to replace these special cases in the code generator by ignoring these
target language features, instead printing case expressions and if-then-else
as functions.
https://www.isa-afp.org/entries/Lazy_Case.shtml
Enjoy,
René
Last updated: Apr 26 2024 at 08:19 UTC