Theory HOL-Library.Code_Lazy

(* Author: Pascal Stoop, ETH Zurich
   Author: Andreas Lochbihler, Digital Asset *)

section ‹Lazy types in generated code›

theory Code_Lazy
imports Case_Converter
keywords
  "code_lazy_type"
  "activate_lazy_type"
  "deactivate_lazy_type"
  "activate_lazy_types"
  "deactivate_lazy_types"
  "print_lazy_types" :: thy_decl
begin

text ‹
  This theory and the CodeLazy tool described in \<^cite>‹"LochbihlerStoop2018"›.

  It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
  set of type constructors lazily, even in target languages with eager evaluation.
  The lazy type must be algebraic, i.e., values must be built from constructors and a
  corresponding case operator decomposes them. Every datatype and codatatype is algebraic
  and thus eligible for lazification.
›

subsection ‹The type ‹lazy››

typedef 'a lazy = "UNIV :: 'a set" ..
setup_lifting type_definition_lazy
lift_definition delay :: "(unit ⇒ 'a) ⇒ 'a lazy"  is "λf. f ()" .
lift_definition force :: "'a lazy ⇒ 'a" is "λx. x" .

code_datatype delay
lemma force_delay [code]: "force (delay f) = f ()" by transfer (rule refl)
lemma delay_force: "delay (λ_. force s) = s" by transfer (rule refl)

definition termify_lazy2 :: "'a :: typerep lazy ⇒ term"
  where "termify_lazy2 x =
  Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit ⇒ 'a) ⇒ 'a lazy)))
    (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit ⇒ 'a))))"

definition termify_lazy ::
  "(String.literal ⇒ 'typerep ⇒ 'term) ⇒
   ('term ⇒ 'term ⇒ 'term) ⇒
   (String.literal ⇒ 'typerep ⇒ 'term ⇒ 'term) ⇒
   'typerep ⇒ ('typerep ⇒ 'typerep ⇒ 'typerep) ⇒ ('typerep ⇒ 'typerep) ⇒
   ('a ⇒ 'term) ⇒ 'typerep ⇒ 'a :: typerep lazy ⇒ 'term ⇒ term"
  where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x"

declare [[code drop: "Code_Evaluation.term_of :: _ lazy ⇒ _"]]

lemma term_of_lazy_code [code]:
  "Code_Evaluation.term_of x ≡
   termify_lazy
     Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs
     TYPEREP(unit) (λT U. typerep.Typerep (STR ''fun'') [T, U]) (λT. typerep.Typerep (STR ''Code_Lazy.lazy'') [T])
     Code_Evaluation.term_of TYPEREP('a) x (Code_Evaluation.Const (STR '''') (TYPEREP(unit)))"
  for x :: "'a :: {typerep, term_of} lazy"
  by (rule term_of_anything)

text ‹
  The implementations of \<^typ>‹_ lazy› using language primitives cache forced values.

  Term reconstruction for lazy looks into the lazy value and reconstructs it to the depth it has been evaluated.
  This is not done for Haskell as we do not know of any portable way to inspect whether a lazy value
  has been evaluated to or not.
›

code_printing code_module Lazy ⇀ (SML) file "~~/src/HOL/Library/Tools/lazy.ML"
    for type_constructor lazy constant delay force termify_lazy
| type_constructor lazy ⇀ (SML) "_ Lazy.lazy"
| constant delay ⇀ (SML) "Lazy.lazy"
| constant force ⇀ (SML) "Lazy.force"
| constant termify_lazy ⇀ (SML) "Lazy.termify'_lazy"

code_reserved (SML) Lazy

code_printing ― ‹For code generation within the Isabelle environment, we reuse the thread-safe
  implementation of lazy from 🗏‹~~/src/Pure/Concurrent/lazy.ML››
  code_module Lazy ⇀ (Eval) ‹› for constant undefined
| type_constructor lazy ⇀ (Eval) "_ Lazy.lazy"
| constant delay ⇀ (Eval) "Lazy.lazy"
| constant force ⇀ (Eval) "Lazy.force"
| code_module Termify_Lazy ⇀ (Eval) file "~~/src/HOL/Library/Tools/termify_lazy.ML"
    for constant termify_lazy
| constant termify_lazy ⇀ (Eval) "Termify'_Lazy.termify'_lazy"

code_reserved (Eval) Termify_Lazy

code_printing
  type_constructor lazy ⇀ (OCaml) "_ Lazy.t"
| constant delay ⇀ (OCaml) "Lazy.from'_fun"
| constant force ⇀ (OCaml) "Lazy.force"
| code_module Termify_Lazy ⇀ (OCaml) file "~~/src/HOL/Library/Tools/termify_lazy.ocaml"
    for constant termify_lazy
| constant termify_lazy ⇀ (OCaml) "Termify'_Lazy.termify'_lazy"

code_reserved (OCaml) Lazy Termify_Lazy

code_printing
  code_module Lazy ⇀ (Haskell) file "~~/src/HOL/Library/Tools/lazy.hs"
    for type_constructor lazy constant delay force
| type_constructor lazy ⇀ (Haskell) "Lazy.Lazy _"
| constant delay ⇀ (Haskell) "Lazy.delay"
| constant force ⇀ (Haskell) "Lazy.force"

code_reserved (Haskell) Lazy

code_printing
  code_module Lazy ⇀ (Scala) file "~~/src/HOL/Library/Tools/lazy.scala"
    for type_constructor lazy constant delay force termify_lazy
| type_constructor lazy ⇀ (Scala) "Lazy.Lazy[_]"
| constant delay ⇀ (Scala) "Lazy.delay"
| constant force ⇀ (Scala) "Lazy.force"
| constant termify_lazy ⇀ (Scala) "Lazy.termify'_lazy"

code_reserved (Scala) Lazy

text ‹Make evaluation with the simplifier respect \<^term>‹delay›s.›

lemma delay_lazy_cong: "delay f = delay f" by simp
setup ‹Code_Simp.map_ss (Simplifier.add_cong @{thm delay_lazy_cong})›        

subsection ‹Implementation›

ML_file ‹code_lazy.ML›

setup ‹
  Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
›

end