Theory Lazy_Case

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