src/HOL/Library/Code_Lazy.thy
author wenzelm
Sun Jan 06 15:04:34 2019 +0100 (7 months ago)
changeset 69605 a96320074298
parent 69593 3dda49e08b9d
child 69690 1fb204399d8d
permissions -rw-r--r--
isabelle update -u path_cartouches;
     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) 
   169 \<open>newtype Lazy a = Lazy a;
   170 delay f = Lazy (f ());
   171 force (Lazy x) = x;\<close> for type_constructor lazy constant delay force
   172 | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
   173 | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
   174 | constant force \<rightharpoonup> (Haskell) "Lazy.force"
   175 
   176 code_reserved Haskell Lazy
   177 
   178 code_printing
   179   code_module Lazy \<rightharpoonup> (Scala) 
   180 \<open>object Lazy {
   181   final class Lazy[A] (f: Unit => A) {
   182     var evaluated = false;
   183     lazy val x: A = f ()
   184 
   185     def get() : A = {
   186       evaluated = true;
   187       return x
   188     }
   189   }
   190 
   191   def force[A] (x: Lazy[A]) : A = {
   192     return x.get()
   193   }
   194 
   195   def delay[A] (f: Unit => A) : Lazy[A] = {
   196     return new Lazy[A] (f)
   197   }
   198 
   199   def termify_lazy[Typerep, Term, A] (
   200     const: String => Typerep => Term,
   201     app: Term => Term => Term,
   202     abs: String => Typerep => Term => Term,
   203     unitT: Typerep,
   204     funT: Typerep => Typerep => Typerep,
   205     lazyT: Typerep => Typerep,
   206     term_of: A => Term,
   207     ty: Typerep,
   208     x: Lazy[A],
   209     dummy: Term) : Term = {
   210     if (x.evaluated)
   211       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get)))
   212     else
   213       app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty)))
   214   }
   215 }\<close> for type_constructor lazy constant delay force termify_lazy
   216 | type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]"
   217 | constant delay \<rightharpoonup> (Scala) "Lazy.delay"
   218 | constant force \<rightharpoonup> (Scala) "Lazy.force"
   219 | constant termify_lazy \<rightharpoonup> (Scala) "Lazy.termify'_lazy"
   220 
   221 code_reserved Scala Lazy
   222 
   223 text \<open>Make evaluation with the simplifier respect \<^term>\<open>delay\<close>s.\<close>
   224 
   225 lemma delay_lazy_cong: "delay f = delay f" by simp
   226 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm delay_lazy_cong})\<close>        
   227 
   228 subsection \<open>Implementation\<close>
   229 
   230 ML_file \<open>code_lazy.ML\<close>
   231 
   232 setup \<open>
   233   Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs)
   234 \<close>
   235 
   236 end