Quelle Lazy_Case.thy

Sprache: Isabelle

section ‹Introduction›

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.15 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.