src/HOL/Library/Code_Lazy.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 68155 8b50f29a1992
child 68390 c558a2202f32
permissions -rw-r--r--
tuned headers;
     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 Main
     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>Eliminating pattern matches\<close>
    28 
    29 definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    30   [code del]: "missing_pattern_match m f = f ()"
    31 
    32 lemma missing_pattern_match_cong [cong]:
    33   "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    34   by(rule arg_cong)
    35 
    36 lemma missing_pattern_match_code [code_unfold]:
    37   "missing_pattern_match = Code.abort"
    38   unfolding missing_pattern_match_def Code.abort_def ..
    39 
    40 ML_file "case_converter.ML"
    41 
    42 subsection \<open>The type @{text lazy}\<close>
    43 
    44 typedef 'a lazy = "UNIV :: 'a set" ..
    45 setup_lifting type_definition_lazy
    46 lift_definition delay :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy"  is "\<lambda>f. f ()" .
    47 lift_definition force :: "'a lazy \<Rightarrow> 'a" is "\<lambda>x. x" .
    48 
    49 code_datatype delay
    50 lemma force_delay [code]: "force (delay f) = f ()" by transfer(rule refl)
    51 lemma delay_force: "delay (\<lambda>_. force s) = s" by transfer(rule refl)
    52 
    53 text \<open>The implementations of @{typ "_ lazy"} using language primitives cache forced values.\<close>
    54 
    55 code_printing code_module Lazy \<rightharpoonup> (SML)
    56 \<open>signature LAZY =
    57 sig
    58   type 'a lazy;
    59   val lazy : (unit -> 'a) -> 'a lazy;
    60   val force : 'a lazy -> 'a;
    61   val peek : 'a lazy -> 'a option
    62   val termify_lazy : 
    63    (string -> 'typerep -> 'term) -> 
    64    ('term -> 'term -> 'term) -> 
    65    (string -> 'typerep -> 'term -> 'term) ->
    66    'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
    67    ('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term;
    68 end;
    69 
    70 structure Lazy : LAZY = 
    71 struct
    72 
    73 datatype 'a content =
    74    Delay of unit -> 'a
    75  | Value of 'a 
    76  | Exn of exn;
    77 
    78 datatype 'a lazy = Lazy of 'a content ref;
    79 
    80 fun lazy f = Lazy (ref (Delay f));
    81 
    82 fun force (Lazy x) = case !x of
    83    Delay f => (
    84      let val res = f (); val _ = x := Value res; in res end
    85      handle exn => (x := Exn exn; raise exn))
    86   | Value x => x
    87   | Exn exn => raise exn;
    88 
    89 fun peek (Lazy x) = case !x of
    90     Value x => SOME x
    91   | _ => NONE;
    92 
    93 fun termify_lazy const app abs unitT funT lazyT term_of T x _ =
    94   app (const "Code_Lazy.delay" (funT (funT unitT T) (lazyT T))) 
    95     (case peek x of SOME y => abs "_" unitT (term_of y)
    96      | _ => const "Pure.dummy_pattern" (funT unitT T));
    97 
    98 end;\<close>
    99 code_reserved SML Lazy
   100 
   101 code_printing
   102   type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy"
   103 | constant delay \<rightharpoonup> (SML) "Lazy.lazy"
   104 | constant force \<rightharpoonup> (SML) "Lazy.force"
   105 
   106 code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe
   107   implementation of lazy from @{file "~~/src/Pure/Concurrent/lazy.ML"}\<close>
   108   code_module Lazy \<rightharpoonup> (Eval) \<open>\<close>
   109 | type_constructor lazy \<rightharpoonup> (Eval) "_ Lazy.lazy"
   110 | constant delay \<rightharpoonup> (Eval) "Lazy.lazy"
   111 | constant force \<rightharpoonup> (Eval) "Lazy.force"
   112 
   113 code_printing
   114   code_module Lazy \<rightharpoonup> (Haskell) 
   115 \<open>newtype Lazy a = Lazy a;
   116 delay f = Lazy (f ());
   117 force (Lazy x) = x;\<close>
   118 | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
   119 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
   120 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
   121 code_reserved Haskell Lazy
   122 
   123 code_printing
   124   code_module Lazy \<rightharpoonup> (Scala) 
   125 \<open>object Lazy {
   126   final class Lazy[A] (f: Unit => A) {
   127     var evaluated = false;
   128     lazy val x: A = f ()
   129 
   130     def get() : A = {
   131       evaluated = true;
   132       return x
   133     }
   134   }
   135 
   136   def force[A] (x: Lazy[A]) : A = {
   137     return x.get()
   138   }
   139 
   140   def delay[A] (f: Unit => A) : Lazy[A] = {
   141     return new Lazy[A] (f)
   142   }
   143 
   144   def termify_lazy[Typerep, Term, A] (
   145     const: String => Typerep => Term,
   146     app: Term => Term => Term,
   147     abs: String => Typerep => Term => Term,
   148     unitT: Typerep,
   149     funT: Typerep => Typerep => Typerep,
   150     lazyT: Typerep => Typerep,
   151     term_of: A => Term,
   152     ty: Typerep,
   153     x: Lazy[A],
   154     dummy: Term) : Term = {
   155     if (x.evaluated)
   156       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get)))
   157     else
   158       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
   159   }
   160 }\<close>
   161 | type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
   162 | constant delay \<rightharpoonup> (Scala) "Lazy.delay"
   163 | constant force \<rightharpoonup> (Scala) "Lazy.force"
   164 code_reserved Scala Lazy termify_lazy
   165 
   166 code_printing
   167   type_constructor lazy \<rightharpoonup> (OCaml) "_ Lazy.t"
   168 | constant delay \<rightharpoonup> (OCaml) "Lazy.from'_fun"
   169 | constant force \<rightharpoonup> (OCaml) "Lazy.force"
   170 code_reserved OCaml Lazy
   171 
   172 text \<open>
   173   Term reconstruction for lazy looks into the lazy value and reconstructs it to the depth it has been evaluated.
   174   This is not done for Haskell and Scala as we do not know of any portable way to inspect whether a lazy value
   175   has been evaluated to or not.
   176 \<close>
   177 code_printing code_module Termify_Lazy \<rightharpoonup> (Eval) 
   178 \<open>structure Termify_Lazy = struct
   179 fun termify_lazy 
   180   (_: string -> typ -> term) (_: term -> term -> term)  (_: string -> typ -> term -> term)
   181   (_: typ) (_: typ -> typ -> typ) (_: typ -> typ)
   182   (term_of: 'a -> term) (T: typ) (x: 'a Lazy.lazy) (_: term) =
   183   Const ("Code_Lazy.delay", (HOLogic.unitT --> T) --> Type ("Code_Lazy.lazy", [T])) $ 
   184   (case Lazy.peek x of
   185     SOME (Exn.Res x) => absdummy HOLogic.unitT (term_of x)
   186   | _ => Const ("Pure.dummy_pattern", HOLogic.unitT --> T));
   187 end;\<close>
   188 code_reserved Eval Termify_Lazy TERMIFY_LAZY termify_lazy
   189 
   190 code_printing code_module Termify_Lazy \<rightharpoonup> (OCaml) 
   191 \<open>module Termify_Lazy : sig
   192   val termify_lazy :
   193    (string -> 'typerep -> 'term) -> 
   194    ('term -> 'term -> 'term) -> 
   195    (string -> 'typerep -> 'term -> 'term) ->
   196    'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
   197    ('a -> 'term) -> 'typerep -> 'a Lazy.t -> 'term -> 'term
   198 end = struct
   199 
   200 let termify_lazy const app abs unitT funT lazyT term_of ty x _ =
   201   app (const "Code_Lazy.delay" (funT (funT unitT ty) (lazyT ty))) 
   202     (if Lazy.is_val x then abs "_" unitT (term_of (Lazy.force x))
   203      else const "Pure.dummy_pattern" (funT unitT ty));;
   204 
   205 end;;\<close>
   206 code_reserved OCaml Termify_Lazy termify_lazy
   207 
   208 definition termify_lazy2 :: "'a :: typerep lazy \<Rightarrow> term"
   209 where "termify_lazy2 x =
   210   Code_Evaluation.App (Code_Evaluation.Const (STR ''Code_Lazy.delay'') (TYPEREP((unit \<Rightarrow> 'a) \<Rightarrow> 'a lazy)))
   211     (Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (TYPEREP((unit \<Rightarrow> 'a))))"
   212 
   213 definition termify_lazy :: 
   214   "(String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term) \<Rightarrow> 
   215    ('term \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow> 
   216    (String.literal \<Rightarrow> 'typerep \<Rightarrow> 'term \<Rightarrow> 'term) \<Rightarrow>
   217    'typerep \<Rightarrow> ('typerep \<Rightarrow> 'typerep \<Rightarrow> 'typerep) \<Rightarrow> ('typerep \<Rightarrow> 'typerep) \<Rightarrow>
   218    ('a \<Rightarrow> 'term) \<Rightarrow> 'typerep \<Rightarrow> 'a :: typerep lazy \<Rightarrow> 'term \<Rightarrow> term"
   219 where "termify_lazy _ _ _ _ _ _ _ _ x _ = termify_lazy2 x"
   220 
   221 declare [[code drop: "Code_Evaluation.term_of :: _ lazy \<Rightarrow> _"]]
   222 
   223 lemma term_of_lazy_code [code]:
   224   "Code_Evaluation.term_of x \<equiv> 
   225    termify_lazy 
   226      Code_Evaluation.Const Code_Evaluation.App Code_Evaluation.Abs 
   227      TYPEREP(unit) (\<lambda>T U. typerep.Typerep (STR ''fun'') [T, U]) (\<lambda>T. typerep.Typerep (STR ''Code_Lazy.lazy'') [T])
   228      Code_Evaluation.term_of TYPEREP('a) x (Code_Evaluation.Const (STR '''') (TYPEREP(unit)))"
   229   for x :: "'a :: {typerep, term_of} lazy"
   230 by(rule term_of_anything)
   231 
   232 code_printing constant termify_lazy
   233   \<rightharpoonup> (SML) "Lazy.termify'_lazy" 
   234   and (Eval) "Termify'_Lazy.termify'_lazy"
   235   and (OCaml) "Termify'_Lazy.termify'_lazy"
   236   and (Scala) "Lazy.termify'_lazy"
   237   
   238 text \<open>Make evaluation with the simplifier respect @{term delay}s.\<close>
   239 
   240 lemma delay_lazy_cong: "delay f = delay f" by simp
   241 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm delay_lazy_cong})\<close>        
   242 
   243 subsection \<open>Implementation\<close>
   244 
   245 ML_file "code_lazy.ML"
   246 
   247 setup \<open>
   248   Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs);
   249 \<close>
   250 
   251 end