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