theory Lazy_Case imports Main
keywords "lazify" :: thy_decl begin
text‹
Importing this theory adds a preprocessing step to the code generator: All case constants
(and @{const HOL.If}) are replaced by ``lazy'' versions; i.e., new constants that evaluate the
cases lazily. For example, the type of @{const case_list} is
@{typ "'a ==> ('b ==> 'b list ==> 'a) ==> 'b list ==> 'a"}. A new constant is created with the type
@{typ "(unit ==> 'a) ==> ('b ==> 'b list ==> 'a) ==> 'b list ==> 'a"}. All fully-applied occurrences of
the standard case constants are rewritten (using the [@{attribute code_unfold}] attribute). ›
text‹
The motivation for doing this is twofold:
🪙 Reconstructing match expressions is complicated. For existing target languages, this theory
reduces the amount of code that has to be trusted in the code generator, because the
transformation goes through the kernel. 🪙 It lays the groundwork to support targets that do not have syntactic constructs for case
expressions or that cannot be used for some reason, or targets where lazy evaluation of
branching constructs is not given. ›
text‹
The obvious downside is that this construction will usually degrade performance of generated code.
To some extent, an optimising compiler that performs inlining can alleviate that. ›
section‹Setup›
text‹@{const HOL.If} is just an alias for @{const case_bool}.› lemma [code_unfold]: "HOL.If P t f = case_bool t f P"by simp
ML_file ‹lazy_case.ML› setup‹Lazy_Case.setup›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-06-10)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
