|
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.
|
|