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