Lazifying case constants

Title:	Lazifying case constants
Author:	Lars Hupel
Submission date:	2017-04-18
Abstract:	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.
BibTeX:	@article{Lazy_Case-AFP, author = {Lars Hupel}, title = {Lazifying case constants}, journal = {Archive of Formal Proofs}, month = apr, year = 2017, note = {\url{http://isa-afp.org/entries/Lazy_Case.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Dict_Construction
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.