author | nipkow |
Mon, 30 May 2022 20:58:45 +0200 | |
changeset 75496 | 99b37c391433 |
parent 73711 | 5833b556b3b5 |
child 76987 | 4c275405faae |
permissions | -rw-r--r-- |
68155 | 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 |
|
69567
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
69528
diff
changeset
|
7 |
imports Case_Converter |
68155 | 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 |
||
68390 | 20 |
It hooks into Isabelle's code generator such that the generated code evaluates a user-specified |
68155 | 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 |
||
69272 | 27 |
subsection \<open>The type \<open>lazy\<close>\<close> |
68155 | 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 |
|
69528 | 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" |
|
68155 | 50 |
|
69528 | 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> |
|
69593 | 63 |
The implementations of \<^typ>\<open>_ lazy\<close> using language primitives cache forced values. |
69528 | 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> |
|
68155 | 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 |
||
69528 | 113 |
end;\<close> for type_constructor lazy constant delay force termify_lazy |
114 |
| type_constructor lazy \<rightharpoonup> (SML) "_ Lazy.lazy" |
|
68155 | 115 |
| constant delay \<rightharpoonup> (SML) "Lazy.lazy" |
116 |
| constant force \<rightharpoonup> (SML) "Lazy.force" |
|
69528 | 117 |
| constant termify_lazy \<rightharpoonup> (SML) "Lazy.termify'_lazy" |
118 |
||
119 |
code_reserved SML Lazy |
|
68155 | 120 |
|
121 |
code_printing \<comment> \<open>For code generation within the Isabelle environment, we reuse the thread-safe |
|
69593 | 122 |
implementation of lazy from \<^file>\<open>~~/src/Pure/Concurrent/lazy.ML\<close>\<close> |
69528 | 123 |
code_module Lazy \<rightharpoonup> (Eval) \<open>\<close> for constant undefined |
68155 | 124 |
| type_constructor lazy \<rightharpoonup> (Eval) "_ Lazy.lazy" |
125 |
| constant delay \<rightharpoonup> (Eval) "Lazy.lazy" |
|
126 |
| constant force \<rightharpoonup> (Eval) "Lazy.force" |
|
69528 | 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 |
||
68155 | 166 |
|
167 |
code_printing |
|
69690 | 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 |
|
68155 | 174 |
| type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _" |
175 |
| constant delay \<rightharpoonup> (Haskell) "Lazy.delay" |
|
176 |
| constant force \<rightharpoonup> (Haskell) "Lazy.force" |
|
69528 | 177 |
|
68155 | 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; |
|
73711 | 185 |
lazy val x: A = f(()) |
68155 | 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) |
|
73711 | 213 |
app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(abs("_")(unitT)(term_of(x.get()))) |
68155 | 214 |
else |
215 |
app(const("Code_Lazy.delay")(funT(funT(unitT)(ty))(lazyT(ty))))(const("Pure.dummy_pattern")(funT(unitT)(ty))) |
|
216 |
} |
|
69528 | 217 |
}\<close> for type_constructor lazy constant delay force termify_lazy |
68155 | 218 |
| type_constructor lazy \<rightharpoonup> (Scala) "Lazy.Lazy[_]" |
219 |
| constant delay \<rightharpoonup> (Scala) "Lazy.delay" |
|
220 |
| constant force \<rightharpoonup> (Scala) "Lazy.force" |
|
69528 | 221 |
| constant termify_lazy \<rightharpoonup> (Scala) "Lazy.termify'_lazy" |
68155 | 222 |
|
69528 | 223 |
code_reserved Scala Lazy |
68155 | 224 |
|
69593 | 225 |
text \<open>Make evaluation with the simplifier respect \<^term>\<open>delay\<close>s.\<close> |
68155 | 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 |
||
69605 | 232 |
ML_file \<open>code_lazy.ML\<close> |
68155 | 233 |
|
234 |
setup \<open> |
|
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
68390
diff
changeset
|
235 |
Code_Preproc.add_functrans ("lazy_datatype", Code_Lazy.transform_code_eqs) |
68155 | 236 |
\<close> |
237 |
||
238 |
end |