src/HOL/Library/Code_Lazy.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69690 1fb204399d8d
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (* Author: Pascal Stoop, ETH Zurich
     2    Author: Andreas Lochbihler, Digital Asset *)
     3 
     4 section \<open>Lazy types in generated code\<close>
     5 
     6 theory Code_Lazy
     7 imports Case_Converter
     8 keywords
     9   "code_lazy_type"
    10   "activate_lazy_type"
    11   "deactivate_lazy_type"
    12   "activate_lazy_types"
    13   "deactivate_lazy_types"
    14   "print_lazy_types" :: thy_decl
    15 begin
    16 
    17 text \<open>
    18   This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
    19 
    20   It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
    21   set of type constructors lazily, even in target languages with eager evaluation.
    22   The lazy type must be algebraic, i.e., values must be built from constructors and a
    23   corresponding case operator decomposes them. Every datatype and codatatype is algebraic
    24   and thus eligible for lazification.
    25 \<close>
    26 
    27 subsection \<open>The type \<open>lazy\<close>\<close>
    28 
    29 typedef 'a lazy = "UNIV :: 'a set" ..
    30 setup_lifting type_definition_lazy
    31 lift_definition delay :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy"  is "\<lambda>f. f ()" .
    32 lift_definition force :: "'a lazy \<Rightarrow> 'a" is "\<lambda>x. x" .
    33 
    34 code_datatype delay
    35 lemma force_delay [code]: "force (delay f) = f ()" by transfer (rule refl)
    36 lemma delay_force: "delay (\<lambda>_. force s) = s" by transfer (rule refl)
    37 
    38 definition termify_lazy2 :: "'a :: typerep lazy \<Rightarrow> term"
    39   where "termify_lazy2 x =
    40   Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy)))
    41     (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit \<Rightarrow> 'a))))"
    42 
    43 definition termify_lazy ::
    44   "(String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term) \<Rightarrow>
    45    ('term \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
    46    (String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
    47    'typerep \<Rightarrow> ('typerep \<Rightarrow> 'typerep \<Rightarrow> 'typerep) \<Rightarrow> ('typerep \<Rightarrow> 'typerep) \<Rightarrow>
    48    ('a \<Rightarrow> 'term) \<Rightarrow> 'typerep \<Rightarrow> 'a :: typerep lazy \<Rightarrow> 'term \<Rightarrow> term"
    49   where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x"
    50 
    51 declare [[code drop: "Code_Evaluation.term_of :: _ lazy \<Rightarrow> _"]]
    52 
    53 lemma term_of_lazy_code [code]:
    54   "Code_Evaluation.term_of x \<equiv>
    55    termify_lazy
    56      Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs
    57      TYPEREP(unit) (\<lambda>T U. typerep.Typerep (STR ''fun'') [T, U]) (\<lambda>T. typerep.Typerep (STR ''Code_Lazy.lazy'') [T])
    58      Code_Evaluation.term_of TYPEREP('a) x (Code_Evaluation.Const (STR '''') (TYPEREP(unit)))"
    59   for x :: "'a :: {typerep, term_of} lazy"
    60   by (rule term_of_anything)
    61 
    62 text \<open>
    63   The implementations of \<^typ>\<open>_ lazy\<close> using language primitives cache forced values.
    64 
    65   Term reconstruction for lazy looks into the lazy value and reconstructs it to the depth it has been evaluated.
    66   This is not done for Haskell as we do not know of any portable way to inspect whether a lazy value
    67   has been evaluated to or not.
    68 \<close>
    69 
    70 code_printing code_module Lazy \<rightharpoonup> (SML)
    71 \<open>signature LAZY =
    72 sig
    73   type 'a lazy;
    74   val lazy : (unit -> 'a) -> 'a lazy;
    75   val force : 'a lazy -> 'a;
    76   val peek : 'a lazy -> 'a option
    77   val termify_lazy : 
    78    (string -> 'typerep -> 'term) -> 
    79    ('term -> 'term -> 'term) -> 
    80    (string -> 'typerep -> 'term -> 'term) ->
    81    'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
    82    ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term;
    83 end;
    84 
    85 structure Lazy : LAZY = 
    86 struct
    87 
    88 datatype 'a content =
    89    Delay of unit -> 'a
    90  | Value of 'a 
    91  | Exn of exn;
    92 
    93 datatype 'a lazy = Lazy of 'a content ref;
    94 
    95 fun lazy f = Lazy (ref (Delay f));
    96 
    97 fun force (Lazy x) = case !x of
    98    Delay f => (
    99      let val res = f (); val _ = x := Value res; in res end
   100      handle exn => (x := Exn exn; raise exn))
   101   | Value x => x
   102   | Exn exn => raise exn;
   103 
   104 fun peek (Lazy x) = case !x of
   105     Value x => SOME x
   106   | _ => NONE;
   107 
   108 fun termify_lazy const app abs unitT funT lazyT term_of T x _ =
   109   app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) 
   110     (case peek x of SOME y => abs "_" unitT (term_of y)
   111      | _ => const "Pure.dummy_pattern" (funT unitT T));
   112 
   113 end;\<close> for type_constructor lazy constant delay force termify_lazy
   114 | type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy"
   115 | constant delay \<rightharpoonup> (SML) "Lazy.lazy"
   116 | constant force \<rightharpoonup> (SML) "Lazy.force"
   117 | constant termify_lazy \<rightharpoonup> (SML) "Lazy.termify'_lazy"
   118 
   119 code_reserved SML Lazy
   120 
   121 code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe
   122   implementation of lazy from \<^file>\<open>~~/src/Pure/Concurrent/lazy.ML\<close>\<close>
   123   code_module Lazy \<rightharpoonup> (Eval) \<open>\<close> for constant undefined
   124 | type_constructor lazy \<rightharpoonup> (Eval) "_ Lazy.lazy"
   125 | constant delay \<rightharpoonup> (Eval) "Lazy.lazy"
   126 | constant force \<rightharpoonup> (Eval) "Lazy.force"
   127 | code_module Termify_Lazy \<rightharpoonup> (Eval)
   128 \<open>structure Termify_Lazy = struct
   129 fun termify_lazy
   130   (_: string -> typ -> term) (_: term -> term -> term)  (_: string -> typ -> term -> term)
   131   (_: typ) (_: typ -> typ -> typ) (_: typ -> typ)
   132   (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) =
   133   Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $
   134   (case Lazy.peek x of
   135     SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x)
   136   | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T));
   137 end;\<close> for constant termify_lazy
   138 | constant termify_lazy \<rightharpoonup> (Eval) "Termify'_Lazy.termify'_lazy"
   139 
   140 code_reserved Eval Termify_Lazy
   141 
   142 code_printing
   143   type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
   144 | constant delay \<rightharpoonup> (OCaml) "Lazy.from'_fun"
   145 | constant force \<rightharpoonup> (OCaml) "Lazy.force"
   146 | code_module Termify_Lazy \<rightharpoonup> (OCaml)
   147 \<open>module Termify_Lazy : sig
   148   val termify_lazy :
   149    (string -> 'typerep -> 'term) ->
   150    ('term -> 'term -> 'term) ->
   151    (string -> 'typerep -> 'term -> 'term) ->
   152    'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
   153    ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term
   154 end = struct
   155 
   156 let termify_lazy const app abs unitT funT lazyT term_of ty x _ =
   157   app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty)))
   158     (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x))
   159      else const "Pure.dummy_pattern" (funT unitT ty));;
   160 
   161 end;;\<close> for constant termify_lazy
   162 | constant termify_lazy \<rightharpoonup> (OCaml) "Termify'_Lazy.termify'_lazy"
   163 
   164 code_reserved OCaml Lazy Termify_Lazy
   165 
   166 
   167 code_printing
   168   code_module Lazy \<rightharpoonup> (Haskell) \<open>
   169 module Lazy(Lazy, delay, force) where
   170 
   171 newtype Lazy a = Lazy a
   172 delay f = Lazy (f ())
   173 force (Lazy x) = x\<close> for type_constructor lazy constant delay force
   174 | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
   175 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
   176 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
   177 
   178 code_reserved Haskell Lazy
   179 
   180 code_printing
   181   code_module Lazy \<rightharpoonup> (Scala) 
   182 \<open>object Lazy {
   183   final class Lazy[A] (f: Unit => A) {
   184     var evaluated = false;
   185     lazy val x: A = f ()
   186 
   187     def get() : A = {
   188       evaluated = true;
   189       return x
   190     }
   191   }
   192 
   193   def force[A] (x: Lazy[A]) : A = {
   194     return x.get()
   195   }
   196 
   197   def delay[A] (f: Unit => A) : Lazy[A] = {
   198     return new Lazy[A] (f)
   199   }
   200 
   201   def termify_lazy[Typerep, Term, A] (
   202     const: String => Typerep => Term,
   203     app: Term => Term => Term,
   204     abs: String => Typerep => Term => Term,
   205     unitT: Typerep,
   206     funT: Typerep => Typerep => Typerep,
   207     lazyT: Typerep => Typerep,
   208     term_of: A => Term,
   209     ty: Typerep,
   210     x: Lazy[A],
   211     dummy: Term) : Term = {
   212     if (x.evaluated)
   213       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get)))
   214     else
   215       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
   216   }
   217 }\<close> for type_constructor lazy constant delay force termify_lazy
   218 | type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
   219 | constant delay \<rightharpoonup> (Scala) "Lazy.delay"
   220 | constant force \<rightharpoonup> (Scala) "Lazy.force"
   221 | constant termify_lazy \<rightharpoonup> (Scala) "Lazy.termify'_lazy"
   222 
   223 code_reserved Scala Lazy
   224 
   225 text \<open>Make evaluation with the simplifier respect \<^term>\<open>delay\<close>s.\<close>
   226 
   227 lemma delay_lazy_cong: "delay f = delay f" by simp
   228 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm delay_lazy_cong})\<close>        
   229 
   230 subsection \<open>Implementation\<close>
   231 
   232 ML_file \<open>code_lazy.ML\<close>
   233 
   234 setup \<open>
   235   Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
   236 \<close>
   237 
   238 end