haftmann@37787
|
1 |
(* Title: HOL/Imperative_HOL/Heap_Monad.thy
|
haftmann@26170
|
2 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
|
haftmann@26170
|
3 |
*)
|
haftmann@26170
|
4 |
|
haftmann@37771
|
5 |
header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
|
haftmann@26170
|
6 |
|
haftmann@26170
|
7 |
theory Heap_Monad
|
wenzelm@41661
|
8 |
imports
|
wenzelm@41661
|
9 |
Heap
|
wenzelm@41661
|
10 |
"~~/src/HOL/Library/Monad_Syntax"
|
wenzelm@41661
|
11 |
"~~/src/HOL/Library/Code_Natural"
|
haftmann@26170
|
12 |
begin
|
haftmann@26170
|
13 |
|
haftmann@26170
|
14 |
subsection {* The monad *}
|
haftmann@26170
|
15 |
|
haftmann@37757
|
16 |
subsubsection {* Monad construction *}
|
haftmann@26170
|
17 |
|
haftmann@26170
|
18 |
text {* Monadic heap actions either produce values
|
haftmann@26170
|
19 |
and transform the heap, or fail *}
|
haftmann@37709
|
20 |
datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
|
haftmann@26170
|
21 |
|
haftmann@40509
|
22 |
lemma [code, code del]:
|
haftmann@40509
|
23 |
"(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
|
haftmann@40509
|
24 |
..
|
haftmann@40509
|
25 |
|
haftmann@37709
|
26 |
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
|
haftmann@37709
|
27 |
[code del]: "execute (Heap f) = f"
|
haftmann@26170
|
28 |
|
haftmann@37757
|
29 |
lemma Heap_cases [case_names succeed fail]:
|
haftmann@37757
|
30 |
fixes f and h
|
haftmann@37757
|
31 |
assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
|
haftmann@37757
|
32 |
assumes fail: "execute f h = None \<Longrightarrow> P"
|
haftmann@37757
|
33 |
shows P
|
haftmann@37757
|
34 |
using assms by (cases "execute f h") auto
|
haftmann@37757
|
35 |
|
haftmann@26170
|
36 |
lemma Heap_execute [simp]:
|
haftmann@26170
|
37 |
"Heap (execute f) = f" by (cases f) simp_all
|
haftmann@26170
|
38 |
|
haftmann@26170
|
39 |
lemma Heap_eqI:
|
haftmann@26170
|
40 |
"(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
|
nipkow@39535
|
41 |
by (cases f, cases g) (auto simp: fun_eq_iff)
|
haftmann@26170
|
42 |
|
wenzelm@46165
|
43 |
ML {* structure Execute_Simps = Named_Thms
|
wenzelm@46165
|
44 |
(
|
wenzelm@46165
|
45 |
val name = @{binding execute_simps}
|
haftmann@37757
|
46 |
val description = "simplification rules for execute"
|
haftmann@37757
|
47 |
) *}
|
haftmann@37757
|
48 |
|
haftmann@37757
|
49 |
setup Execute_Simps.setup
|
haftmann@37757
|
50 |
|
haftmann@37787
|
51 |
lemma execute_Let [execute_simps]:
|
haftmann@37757
|
52 |
"execute (let x = t in f x) = (let x = t in execute (f x))"
|
haftmann@37757
|
53 |
by (simp add: Let_def)
|
haftmann@37757
|
54 |
|
haftmann@37757
|
55 |
|
haftmann@37757
|
56 |
subsubsection {* Specialised lifters *}
|
haftmann@37757
|
57 |
|
haftmann@37757
|
58 |
definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
|
haftmann@37757
|
59 |
[code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
|
haftmann@37757
|
60 |
|
haftmann@37787
|
61 |
lemma execute_tap [execute_simps]:
|
haftmann@37757
|
62 |
"execute (tap f) h = Some (f h, h)"
|
haftmann@37757
|
63 |
by (simp add: tap_def)
|
haftmann@26170
|
64 |
|
haftmann@37709
|
65 |
definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
|
haftmann@37709
|
66 |
[code del]: "heap f = Heap (Some \<circ> f)"
|
haftmann@26170
|
67 |
|
haftmann@37787
|
68 |
lemma execute_heap [execute_simps]:
|
haftmann@37709
|
69 |
"execute (heap f) = Some \<circ> f"
|
haftmann@26170
|
70 |
by (simp add: heap_def)
|
haftmann@26170
|
71 |
|
haftmann@37753
|
72 |
definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
|
haftmann@37753
|
73 |
[code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
|
haftmann@37753
|
74 |
|
haftmann@37757
|
75 |
lemma execute_guard [execute_simps]:
|
haftmann@37753
|
76 |
"\<not> P h \<Longrightarrow> execute (guard P f) h = None"
|
haftmann@37753
|
77 |
"P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
|
haftmann@37753
|
78 |
by (simp_all add: guard_def)
|
haftmann@37753
|
79 |
|
haftmann@37757
|
80 |
|
haftmann@37757
|
81 |
subsubsection {* Predicate classifying successful computations *}
|
haftmann@37757
|
82 |
|
haftmann@37757
|
83 |
definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
|
haftmann@37757
|
84 |
"success f h \<longleftrightarrow> execute f h \<noteq> None"
|
haftmann@37757
|
85 |
|
haftmann@37757
|
86 |
lemma successI:
|
haftmann@37757
|
87 |
"execute f h \<noteq> None \<Longrightarrow> success f h"
|
haftmann@37757
|
88 |
by (simp add: success_def)
|
haftmann@37757
|
89 |
|
haftmann@37757
|
90 |
lemma successE:
|
haftmann@37757
|
91 |
assumes "success f h"
|
haftmann@37771
|
92 |
obtains r h' where "r = fst (the (execute c h))"
|
haftmann@37771
|
93 |
and "h' = snd (the (execute c h))"
|
haftmann@37771
|
94 |
and "execute f h \<noteq> None"
|
haftmann@37771
|
95 |
using assms by (simp add: success_def)
|
haftmann@37757
|
96 |
|
wenzelm@46165
|
97 |
ML {* structure Success_Intros = Named_Thms
|
wenzelm@46165
|
98 |
(
|
wenzelm@46165
|
99 |
val name = @{binding success_intros}
|
haftmann@37757
|
100 |
val description = "introduction rules for success"
|
haftmann@37757
|
101 |
) *}
|
haftmann@37757
|
102 |
|
haftmann@37757
|
103 |
setup Success_Intros.setup
|
haftmann@37757
|
104 |
|
haftmann@37787
|
105 |
lemma success_tapI [success_intros]:
|
haftmann@37757
|
106 |
"success (tap f) h"
|
haftmann@37787
|
107 |
by (rule successI) (simp add: execute_simps)
|
haftmann@37757
|
108 |
|
haftmann@37787
|
109 |
lemma success_heapI [success_intros]:
|
haftmann@37757
|
110 |
"success (heap f) h"
|
haftmann@37787
|
111 |
by (rule successI) (simp add: execute_simps)
|
haftmann@37757
|
112 |
|
haftmann@37757
|
113 |
lemma success_guardI [success_intros]:
|
haftmann@37757
|
114 |
"P h \<Longrightarrow> success (guard P f) h"
|
haftmann@37757
|
115 |
by (rule successI) (simp add: execute_guard)
|
haftmann@37757
|
116 |
|
haftmann@37757
|
117 |
lemma success_LetI [success_intros]:
|
haftmann@37757
|
118 |
"x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
|
haftmann@37757
|
119 |
by (simp add: Let_def)
|
haftmann@37757
|
120 |
|
haftmann@37771
|
121 |
lemma success_ifI:
|
haftmann@37771
|
122 |
"(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
|
haftmann@37771
|
123 |
success (if c then t else e) h"
|
haftmann@37771
|
124 |
by (simp add: success_def)
|
haftmann@37771
|
125 |
|
haftmann@37771
|
126 |
|
haftmann@37771
|
127 |
subsubsection {* Predicate for a simple relational calculus *}
|
haftmann@37771
|
128 |
|
haftmann@37771
|
129 |
text {*
|
haftmann@40919
|
130 |
The @{text effect} predicate states that when a computation @{text c}
|
haftmann@37771
|
131 |
runs with the heap @{text h} will result in return value @{text r}
|
haftmann@37771
|
132 |
and a heap @{text "h'"}, i.e.~no exception occurs.
|
haftmann@37771
|
133 |
*}
|
haftmann@37771
|
134 |
|
haftmann@40919
|
135 |
definition effect :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
|
haftmann@40919
|
136 |
effect_def: "effect c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
|
haftmann@37771
|
137 |
|
haftmann@40919
|
138 |
lemma effectI:
|
haftmann@40919
|
139 |
"execute c h = Some (r, h') \<Longrightarrow> effect c h h' r"
|
haftmann@40919
|
140 |
by (simp add: effect_def)
|
haftmann@37771
|
141 |
|
haftmann@40919
|
142 |
lemma effectE:
|
haftmann@40919
|
143 |
assumes "effect c h h' r"
|
haftmann@37771
|
144 |
obtains "r = fst (the (execute c h))"
|
haftmann@37771
|
145 |
and "h' = snd (the (execute c h))"
|
haftmann@37771
|
146 |
and "success c h"
|
haftmann@37771
|
147 |
proof (rule that)
|
haftmann@40919
|
148 |
from assms have *: "execute c h = Some (r, h')" by (simp add: effect_def)
|
haftmann@37771
|
149 |
then show "success c h" by (simp add: success_def)
|
haftmann@37771
|
150 |
from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
|
haftmann@37771
|
151 |
by simp_all
|
haftmann@37771
|
152 |
then show "r = fst (the (execute c h))"
|
haftmann@37771
|
153 |
and "h' = snd (the (execute c h))" by simp_all
|
haftmann@37771
|
154 |
qed
|
haftmann@37771
|
155 |
|
haftmann@40919
|
156 |
lemma effect_success:
|
haftmann@40919
|
157 |
"effect c h h' r \<Longrightarrow> success c h"
|
haftmann@40919
|
158 |
by (simp add: effect_def success_def)
|
haftmann@37771
|
159 |
|
haftmann@40919
|
160 |
lemma success_effectE:
|
haftmann@37771
|
161 |
assumes "success c h"
|
haftmann@40919
|
162 |
obtains r h' where "effect c h h' r"
|
haftmann@40919
|
163 |
using assms by (auto simp add: effect_def success_def)
|
haftmann@37771
|
164 |
|
haftmann@40919
|
165 |
lemma effect_deterministic:
|
haftmann@40919
|
166 |
assumes "effect f h h' a"
|
haftmann@40919
|
167 |
and "effect f h h'' b"
|
haftmann@37771
|
168 |
shows "a = b" and "h' = h''"
|
haftmann@40919
|
169 |
using assms unfolding effect_def by auto
|
haftmann@37771
|
170 |
|
haftmann@46900
|
171 |
ML {* structure Effect_Intros = Named_Thms
|
wenzelm@46165
|
172 |
(
|
wenzelm@46165
|
173 |
val name = @{binding effect_intros}
|
haftmann@40919
|
174 |
val description = "introduction rules for effect"
|
haftmann@37771
|
175 |
) *}
|
haftmann@37771
|
176 |
|
haftmann@46900
|
177 |
ML {* structure Effect_Elims = Named_Thms
|
wenzelm@46165
|
178 |
(
|
wenzelm@46165
|
179 |
val name = @{binding effect_elims}
|
haftmann@40919
|
180 |
val description = "elimination rules for effect"
|
haftmann@37771
|
181 |
) *}
|
haftmann@37771
|
182 |
|
haftmann@46900
|
183 |
setup "Effect_Intros.setup #> Effect_Elims.setup"
|
haftmann@37771
|
184 |
|
haftmann@40919
|
185 |
lemma effect_LetI [effect_intros]:
|
haftmann@40919
|
186 |
assumes "x = t" "effect (f x) h h' r"
|
haftmann@40919
|
187 |
shows "effect (let x = t in f x) h h' r"
|
haftmann@37771
|
188 |
using assms by simp
|
haftmann@37771
|
189 |
|
haftmann@40919
|
190 |
lemma effect_LetE [effect_elims]:
|
haftmann@40919
|
191 |
assumes "effect (let x = t in f x) h h' r"
|
haftmann@40919
|
192 |
obtains "effect (f t) h h' r"
|
haftmann@37771
|
193 |
using assms by simp
|
haftmann@37771
|
194 |
|
haftmann@40919
|
195 |
lemma effect_ifI:
|
haftmann@40919
|
196 |
assumes "c \<Longrightarrow> effect t h h' r"
|
haftmann@40919
|
197 |
and "\<not> c \<Longrightarrow> effect e h h' r"
|
haftmann@40919
|
198 |
shows "effect (if c then t else e) h h' r"
|
haftmann@37771
|
199 |
by (cases c) (simp_all add: assms)
|
haftmann@37771
|
200 |
|
haftmann@40919
|
201 |
lemma effect_ifE:
|
haftmann@40919
|
202 |
assumes "effect (if c then t else e) h h' r"
|
haftmann@40919
|
203 |
obtains "c" "effect t h h' r"
|
haftmann@40919
|
204 |
| "\<not> c" "effect e h h' r"
|
haftmann@37771
|
205 |
using assms by (cases c) simp_all
|
haftmann@37771
|
206 |
|
haftmann@40919
|
207 |
lemma effect_tapI [effect_intros]:
|
haftmann@37771
|
208 |
assumes "h' = h" "r = f h"
|
haftmann@40919
|
209 |
shows "effect (tap f) h h' r"
|
haftmann@40919
|
210 |
by (rule effectI) (simp add: assms execute_simps)
|
haftmann@37771
|
211 |
|
haftmann@40919
|
212 |
lemma effect_tapE [effect_elims]:
|
haftmann@40919
|
213 |
assumes "effect (tap f) h h' r"
|
haftmann@37771
|
214 |
obtains "h' = h" and "r = f h"
|
haftmann@40919
|
215 |
using assms by (rule effectE) (auto simp add: execute_simps)
|
haftmann@37771
|
216 |
|
haftmann@40919
|
217 |
lemma effect_heapI [effect_intros]:
|
haftmann@37771
|
218 |
assumes "h' = snd (f h)" "r = fst (f h)"
|
haftmann@40919
|
219 |
shows "effect (heap f) h h' r"
|
haftmann@40919
|
220 |
by (rule effectI) (simp add: assms execute_simps)
|
haftmann@37771
|
221 |
|
haftmann@40919
|
222 |
lemma effect_heapE [effect_elims]:
|
haftmann@40919
|
223 |
assumes "effect (heap f) h h' r"
|
haftmann@37771
|
224 |
obtains "h' = snd (f h)" and "r = fst (f h)"
|
haftmann@40919
|
225 |
using assms by (rule effectE) (simp add: execute_simps)
|
haftmann@37771
|
226 |
|
haftmann@40919
|
227 |
lemma effect_guardI [effect_intros]:
|
haftmann@37771
|
228 |
assumes "P h" "h' = snd (f h)" "r = fst (f h)"
|
haftmann@40919
|
229 |
shows "effect (guard P f) h h' r"
|
haftmann@40919
|
230 |
by (rule effectI) (simp add: assms execute_simps)
|
haftmann@37771
|
231 |
|
haftmann@40919
|
232 |
lemma effect_guardE [effect_elims]:
|
haftmann@40919
|
233 |
assumes "effect (guard P f) h h' r"
|
haftmann@37771
|
234 |
obtains "h' = snd (f h)" "r = fst (f h)" "P h"
|
haftmann@40919
|
235 |
using assms by (rule effectE)
|
haftmann@37771
|
236 |
(auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
|
haftmann@37771
|
237 |
|
haftmann@37757
|
238 |
|
haftmann@37757
|
239 |
subsubsection {* Monad combinators *}
|
haftmann@26170
|
240 |
|
haftmann@37709
|
241 |
definition return :: "'a \<Rightarrow> 'a Heap" where
|
haftmann@26170
|
242 |
[code del]: "return x = heap (Pair x)"
|
haftmann@26170
|
243 |
|
haftmann@37787
|
244 |
lemma execute_return [execute_simps]:
|
haftmann@37709
|
245 |
"execute (return x) = Some \<circ> Pair x"
|
haftmann@37787
|
246 |
by (simp add: return_def execute_simps)
|
haftmann@26170
|
247 |
|
haftmann@37787
|
248 |
lemma success_returnI [success_intros]:
|
haftmann@37757
|
249 |
"success (return x) h"
|
haftmann@37787
|
250 |
by (rule successI) (simp add: execute_simps)
|
haftmann@37757
|
251 |
|
haftmann@40919
|
252 |
lemma effect_returnI [effect_intros]:
|
haftmann@40919
|
253 |
"h = h' \<Longrightarrow> effect (return x) h h' x"
|
haftmann@40919
|
254 |
by (rule effectI) (simp add: execute_simps)
|
haftmann@37771
|
255 |
|
haftmann@40919
|
256 |
lemma effect_returnE [effect_elims]:
|
haftmann@40919
|
257 |
assumes "effect (return x) h h' r"
|
haftmann@37771
|
258 |
obtains "r = x" "h' = h"
|
haftmann@40919
|
259 |
using assms by (rule effectE) (simp add: execute_simps)
|
haftmann@37771
|
260 |
|
haftmann@37709
|
261 |
definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
|
haftmann@37709
|
262 |
[code del]: "raise s = Heap (\<lambda>_. None)"
|
haftmann@26170
|
263 |
|
haftmann@37787
|
264 |
lemma execute_raise [execute_simps]:
|
haftmann@37709
|
265 |
"execute (raise s) = (\<lambda>_. None)"
|
haftmann@26170
|
266 |
by (simp add: raise_def)
|
haftmann@26170
|
267 |
|
haftmann@40919
|
268 |
lemma effect_raiseE [effect_elims]:
|
haftmann@40919
|
269 |
assumes "effect (raise x) h h' r"
|
haftmann@37771
|
270 |
obtains "False"
|
haftmann@40919
|
271 |
using assms by (rule effectE) (simp add: success_def execute_simps)
|
haftmann@37771
|
272 |
|
krauss@37792
|
273 |
definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
|
krauss@37792
|
274 |
[code del]: "bind f g = Heap (\<lambda>h. case execute f h of
|
haftmann@37709
|
275 |
Some (x, h') \<Rightarrow> execute (g x) h'
|
haftmann@37709
|
276 |
| None \<Rightarrow> None)"
|
haftmann@37709
|
277 |
|
krauss@37792
|
278 |
setup {*
|
krauss@37792
|
279 |
Adhoc_Overloading.add_variant
|
haftmann@37816
|
280 |
@{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind}
|
krauss@37792
|
281 |
*}
|
krauss@37792
|
282 |
|
haftmann@37757
|
283 |
lemma execute_bind [execute_simps]:
|
haftmann@37709
|
284 |
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
|
haftmann@37709
|
285 |
"execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
|
haftmann@37755
|
286 |
by (simp_all add: bind_def)
|
haftmann@37709
|
287 |
|
haftmann@38635
|
288 |
lemma execute_bind_case:
|
haftmann@38635
|
289 |
"execute (f \<guillemotright>= g) h = (case (execute f h) of
|
haftmann@38635
|
290 |
Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"
|
haftmann@38635
|
291 |
by (simp add: bind_def)
|
haftmann@38635
|
292 |
|
haftmann@37771
|
293 |
lemma execute_bind_success:
|
haftmann@37771
|
294 |
"success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
|
haftmann@37771
|
295 |
by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
|
haftmann@37771
|
296 |
|
haftmann@37771
|
297 |
lemma success_bind_executeI:
|
haftmann@37771
|
298 |
"execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
|
haftmann@37757
|
299 |
by (auto intro!: successI elim!: successE simp add: bind_def)
|
haftmann@37757
|
300 |
|
haftmann@40919
|
301 |
lemma success_bind_effectI [success_intros]:
|
haftmann@40919
|
302 |
"effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
|
haftmann@40919
|
303 |
by (auto simp add: effect_def success_def bind_def)
|
haftmann@37771
|
304 |
|
haftmann@40919
|
305 |
lemma effect_bindI [effect_intros]:
|
haftmann@40919
|
306 |
assumes "effect f h h' r" "effect (g r) h' h'' r'"
|
haftmann@40919
|
307 |
shows "effect (f \<guillemotright>= g) h h'' r'"
|
haftmann@37771
|
308 |
using assms
|
haftmann@40919
|
309 |
apply (auto intro!: effectI elim!: effectE successE)
|
haftmann@37771
|
310 |
apply (subst execute_bind, simp_all)
|
haftmann@37771
|
311 |
done
|
haftmann@37771
|
312 |
|
haftmann@40919
|
313 |
lemma effect_bindE [effect_elims]:
|
haftmann@40919
|
314 |
assumes "effect (f \<guillemotright>= g) h h'' r'"
|
haftmann@40919
|
315 |
obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
|
haftmann@40919
|
316 |
using assms by (auto simp add: effect_def bind_def split: option.split_asm)
|
haftmann@37771
|
317 |
|
haftmann@37771
|
318 |
lemma execute_bind_eq_SomeI:
|
haftmann@37851
|
319 |
assumes "execute f h = Some (x, h')"
|
haftmann@37851
|
320 |
and "execute (g x) h' = Some (y, h'')"
|
haftmann@37851
|
321 |
shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
|
haftmann@37755
|
322 |
using assms by (simp add: bind_def)
|
haftmann@37753
|
323 |
|
haftmann@37709
|
324 |
lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
|
haftmann@37787
|
325 |
by (rule Heap_eqI) (simp add: execute_bind execute_simps)
|
haftmann@37709
|
326 |
|
haftmann@37709
|
327 |
lemma bind_return [simp]: "f \<guillemotright>= return = f"
|
haftmann@37787
|
328 |
by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
|
haftmann@37709
|
329 |
|
haftmann@37828
|
330 |
lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: 'a Heap) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
|
haftmann@37787
|
331 |
by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
|
haftmann@37709
|
332 |
|
haftmann@37709
|
333 |
lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
|
haftmann@37787
|
334 |
by (rule Heap_eqI) (simp add: execute_simps)
|
haftmann@37709
|
335 |
|
haftmann@26170
|
336 |
|
haftmann@37757
|
337 |
subsection {* Generic combinators *}
|
haftmann@26170
|
338 |
|
haftmann@37757
|
339 |
subsubsection {* Assertions *}
|
haftmann@26170
|
340 |
|
haftmann@37709
|
341 |
definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
|
haftmann@37709
|
342 |
"assert P x = (if P x then return x else raise ''assert'')"
|
haftmann@28742
|
343 |
|
haftmann@37757
|
344 |
lemma execute_assert [execute_simps]:
|
haftmann@37753
|
345 |
"P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
|
haftmann@37753
|
346 |
"\<not> P x \<Longrightarrow> execute (assert P x) h = None"
|
haftmann@37787
|
347 |
by (simp_all add: assert_def execute_simps)
|
haftmann@37753
|
348 |
|
haftmann@37757
|
349 |
lemma success_assertI [success_intros]:
|
haftmann@37757
|
350 |
"P x \<Longrightarrow> success (assert P x) h"
|
haftmann@37757
|
351 |
by (rule successI) (simp add: execute_assert)
|
haftmann@37757
|
352 |
|
haftmann@40919
|
353 |
lemma effect_assertI [effect_intros]:
|
haftmann@40919
|
354 |
"P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> effect (assert P x) h h' r"
|
haftmann@40919
|
355 |
by (rule effectI) (simp add: execute_assert)
|
haftmann@37771
|
356 |
|
haftmann@40919
|
357 |
lemma effect_assertE [effect_elims]:
|
haftmann@40919
|
358 |
assumes "effect (assert P x) h h' r"
|
haftmann@37771
|
359 |
obtains "P x" "r = x" "h' = h"
|
haftmann@40919
|
360 |
using assms by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)
|
haftmann@37771
|
361 |
|
haftmann@28742
|
362 |
lemma assert_cong [fundef_cong]:
|
haftmann@28742
|
363 |
assumes "P = P'"
|
haftmann@28742
|
364 |
assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
|
haftmann@28742
|
365 |
shows "(assert P x >>= f) = (assert P' x >>= f')"
|
haftmann@37753
|
366 |
by (rule Heap_eqI) (insert assms, simp add: assert_def)
|
haftmann@28742
|
367 |
|
haftmann@37757
|
368 |
|
haftmann@37757
|
369 |
subsubsection {* Plain lifting *}
|
haftmann@37757
|
370 |
|
haftmann@37753
|
371 |
definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
|
haftmann@37753
|
372 |
"lift f = return o f"
|
haftmann@37709
|
373 |
|
haftmann@37753
|
374 |
lemma lift_collapse [simp]:
|
haftmann@37753
|
375 |
"lift f x = return (f x)"
|
haftmann@37753
|
376 |
by (simp add: lift_def)
|
haftmann@37709
|
377 |
|
haftmann@37753
|
378 |
lemma bind_lift:
|
haftmann@37753
|
379 |
"(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
|
haftmann@37753
|
380 |
by (simp add: lift_def comp_def)
|
haftmann@37709
|
381 |
|
haftmann@37757
|
382 |
|
haftmann@37757
|
383 |
subsubsection {* Iteration -- warning: this is rarely useful! *}
|
haftmann@37757
|
384 |
|
haftmann@37755
|
385 |
primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
|
haftmann@37755
|
386 |
"fold_map f [] = return []"
|
krauss@37792
|
387 |
| "fold_map f (x # xs) = do {
|
haftmann@37709
|
388 |
y \<leftarrow> f x;
|
haftmann@37755
|
389 |
ys \<leftarrow> fold_map f xs;
|
haftmann@37709
|
390 |
return (y # ys)
|
krauss@37792
|
391 |
}"
|
haftmann@37709
|
392 |
|
haftmann@37755
|
393 |
lemma fold_map_append:
|
haftmann@37755
|
394 |
"fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
|
haftmann@37753
|
395 |
by (induct xs) simp_all
|
haftmann@37753
|
396 |
|
haftmann@37757
|
397 |
lemma execute_fold_map_unchanged_heap [execute_simps]:
|
haftmann@37753
|
398 |
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
|
haftmann@37755
|
399 |
shows "execute (fold_map f xs) h =
|
haftmann@37753
|
400 |
Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
|
haftmann@37753
|
401 |
using assms proof (induct xs)
|
haftmann@37787
|
402 |
case Nil show ?case by (simp add: execute_simps)
|
haftmann@37753
|
403 |
next
|
haftmann@37753
|
404 |
case (Cons x xs)
|
haftmann@37753
|
405 |
from Cons.prems obtain y
|
haftmann@37753
|
406 |
where y: "execute (f x) h = Some (y, h)" by auto
|
haftmann@37755
|
407 |
moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
|
haftmann@37753
|
408 |
Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
|
haftmann@37787
|
409 |
ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
|
haftmann@37753
|
410 |
qed
|
haftmann@37753
|
411 |
|
haftmann@40510
|
412 |
|
haftmann@40510
|
413 |
subsection {* Partial function definition setup *}
|
haftmann@40510
|
414 |
|
haftmann@40510
|
415 |
definition Heap_ord :: "'a Heap \<Rightarrow> 'a Heap \<Rightarrow> bool" where
|
haftmann@40510
|
416 |
"Heap_ord = img_ord execute (fun_ord option_ord)"
|
haftmann@40510
|
417 |
|
huffman@45045
|
418 |
definition Heap_lub :: "'a Heap set \<Rightarrow> 'a Heap" where
|
haftmann@40510
|
419 |
"Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
|
haftmann@40510
|
420 |
|
haftmann@40510
|
421 |
interpretation heap!: partial_function_definitions Heap_ord Heap_lub
|
haftmann@40510
|
422 |
proof -
|
haftmann@40510
|
423 |
have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
|
haftmann@40510
|
424 |
by (rule partial_function_lift) (rule flat_interpretation)
|
haftmann@40510
|
425 |
then have "partial_function_definitions (img_ord execute (fun_ord option_ord))
|
haftmann@40510
|
426 |
(img_lub execute Heap (fun_lub (flat_lub None)))"
|
haftmann@40510
|
427 |
by (rule partial_function_image) (auto intro: Heap_eqI)
|
haftmann@40510
|
428 |
then show "partial_function_definitions Heap_ord Heap_lub"
|
haftmann@40510
|
429 |
by (simp only: Heap_ord_def Heap_lub_def)
|
haftmann@40510
|
430 |
qed
|
haftmann@40510
|
431 |
|
krauss@43790
|
432 |
declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
|
krauss@43921
|
433 |
@{term heap.mono_body} @{thm heap.fixp_rule_uc} NONE *}
|
krauss@43790
|
434 |
|
krauss@43790
|
435 |
|
haftmann@40510
|
436 |
abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
|
haftmann@40510
|
437 |
|
haftmann@40510
|
438 |
lemma Heap_ordI:
|
haftmann@40510
|
439 |
assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
|
haftmann@40510
|
440 |
shows "Heap_ord x y"
|
haftmann@40510
|
441 |
using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
|
haftmann@40510
|
442 |
by blast
|
haftmann@40510
|
443 |
|
haftmann@40510
|
444 |
lemma Heap_ordE:
|
haftmann@40510
|
445 |
assumes "Heap_ord x y"
|
haftmann@40510
|
446 |
obtains "execute x h = None" | "execute x h = execute y h"
|
haftmann@40510
|
447 |
using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
|
haftmann@40510
|
448 |
by atomize_elim blast
|
haftmann@40510
|
449 |
|
haftmann@46900
|
450 |
lemma bind_mono [partial_function_mono]:
|
haftmann@40510
|
451 |
assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
|
haftmann@40510
|
452 |
shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
|
haftmann@40510
|
453 |
proof (rule monotoneI)
|
haftmann@40510
|
454 |
fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
|
haftmann@40510
|
455 |
from mf
|
haftmann@40510
|
456 |
have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg)
|
haftmann@40510
|
457 |
from mg
|
haftmann@40510
|
458 |
have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
|
haftmann@40510
|
459 |
|
haftmann@40510
|
460 |
have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
|
haftmann@40510
|
461 |
(is "Heap_ord ?L ?R")
|
haftmann@40510
|
462 |
proof (rule Heap_ordI)
|
haftmann@40510
|
463 |
fix h
|
haftmann@40510
|
464 |
from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"
|
haftmann@40510
|
465 |
by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
|
haftmann@40510
|
466 |
qed
|
haftmann@40510
|
467 |
also
|
haftmann@40510
|
468 |
have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
|
haftmann@40510
|
469 |
(is "Heap_ord ?L ?R")
|
haftmann@40510
|
470 |
proof (rule Heap_ordI)
|
haftmann@40510
|
471 |
fix h
|
haftmann@40510
|
472 |
show "execute ?L h = None \<or> execute ?L h = execute ?R h"
|
haftmann@40510
|
473 |
proof (cases "execute (B g) h")
|
haftmann@40510
|
474 |
case None
|
haftmann@40510
|
475 |
then have "execute ?L h = None" by (auto simp: execute_bind_case)
|
haftmann@40510
|
476 |
thus ?thesis ..
|
haftmann@40510
|
477 |
next
|
haftmann@40510
|
478 |
case Some
|
haftmann@40510
|
479 |
then obtain r h' where "execute (B g) h = Some (r, h')"
|
haftmann@40510
|
480 |
by (metis surjective_pairing)
|
haftmann@40510
|
481 |
then have "execute ?L h = execute (C r f) h'"
|
haftmann@40510
|
482 |
"execute ?R h = execute (C r g) h'"
|
haftmann@40510
|
483 |
by (auto simp: execute_bind_case)
|
haftmann@40510
|
484 |
with 2[of r] show ?thesis by (auto elim: Heap_ordE)
|
haftmann@40510
|
485 |
qed
|
haftmann@40510
|
486 |
qed
|
haftmann@40510
|
487 |
finally (heap.leq_trans)
|
haftmann@40510
|
488 |
show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
|
haftmann@40510
|
489 |
qed
|
haftmann@40510
|
490 |
|
haftmann@40510
|
491 |
|
haftmann@26182
|
492 |
subsection {* Code generator setup *}
|
haftmann@26182
|
493 |
|
haftmann@26182
|
494 |
subsubsection {* Logical intermediate layer *}
|
haftmann@26182
|
495 |
|
bulwahn@39477
|
496 |
definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
|
bulwahn@39477
|
497 |
[code del]: "raise' s = raise (explode s)"
|
bulwahn@39477
|
498 |
|
haftmann@46900
|
499 |
lemma [code_abbrev]: "raise' (STR s) = raise s"
|
haftmann@46900
|
500 |
unfolding raise'_def by (simp add: STR_inverse)
|
haftmann@26182
|
501 |
|
haftmann@46900
|
502 |
lemma raise_raise': (* FIXME delete candidate *)
|
haftmann@37709
|
503 |
"raise s = raise' (STR s)"
|
bulwahn@39477
|
504 |
unfolding raise'_def by (simp add: STR_inverse)
|
haftmann@26182
|
505 |
|
haftmann@37709
|
506 |
code_datatype raise' -- {* avoid @{const "Heap"} formally *}
|
haftmann@26182
|
507 |
|
haftmann@26182
|
508 |
|
haftmann@27707
|
509 |
subsubsection {* SML and OCaml *}
|
haftmann@26182
|
510 |
|
haftmann@26752
|
511 |
code_type Heap (SML "unit/ ->/ _")
|
haftmann@37828
|
512 |
code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
|
haftmann@27707
|
513 |
code_const return (SML "!(fn/ ()/ =>/ _)")
|
haftmann@37709
|
514 |
code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
|
haftmann@26182
|
515 |
|
haftmann@37753
|
516 |
code_type Heap (OCaml "unit/ ->/ _")
|
haftmann@37828
|
517 |
code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
|
haftmann@27707
|
518 |
code_const return (OCaml "!(fun/ ()/ ->/ _)")
|
haftmann@37828
|
519 |
code_const Heap_Monad.raise' (OCaml "failwith")
|
haftmann@27707
|
520 |
|
haftmann@37838
|
521 |
|
haftmann@37838
|
522 |
subsubsection {* Haskell *}
|
haftmann@37838
|
523 |
|
haftmann@37838
|
524 |
text {* Adaption layer *}
|
haftmann@37838
|
525 |
|
haftmann@37838
|
526 |
code_include Haskell "Heap"
|
haftmann@37838
|
527 |
{*import qualified Control.Monad;
|
haftmann@37838
|
528 |
import qualified Control.Monad.ST;
|
haftmann@37838
|
529 |
import qualified Data.STRef;
|
haftmann@37838
|
530 |
import qualified Data.Array.ST;
|
haftmann@37838
|
531 |
|
haftmann@38201
|
532 |
import Natural;
|
haftmann@38201
|
533 |
|
haftmann@37838
|
534 |
type RealWorld = Control.Monad.ST.RealWorld;
|
haftmann@37838
|
535 |
type ST s a = Control.Monad.ST.ST s a;
|
haftmann@37838
|
536 |
type STRef s a = Data.STRef.STRef s a;
|
haftmann@38201
|
537 |
type STArray s a = Data.Array.ST.STArray s Natural a;
|
haftmann@37838
|
538 |
|
haftmann@37838
|
539 |
newSTRef = Data.STRef.newSTRef;
|
haftmann@37838
|
540 |
readSTRef = Data.STRef.readSTRef;
|
haftmann@37838
|
541 |
writeSTRef = Data.STRef.writeSTRef;
|
haftmann@37838
|
542 |
|
haftmann@38201
|
543 |
newArray :: Natural -> a -> ST s (STArray s a);
|
haftmann@37838
|
544 |
newArray k = Data.Array.ST.newArray (0, k);
|
haftmann@37838
|
545 |
|
haftmann@37838
|
546 |
newListArray :: [a] -> ST s (STArray s a);
|
haftmann@38201
|
547 |
newListArray xs = Data.Array.ST.newListArray (0, (fromInteger . toInteger . length) xs) xs;
|
haftmann@37838
|
548 |
|
haftmann@38201
|
549 |
newFunArray :: Natural -> (Natural -> a) -> ST s (STArray s a);
|
haftmann@37838
|
550 |
newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
|
haftmann@37838
|
551 |
|
haftmann@38201
|
552 |
lengthArray :: STArray s a -> ST s Natural;
|
haftmann@37838
|
553 |
lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
|
haftmann@37838
|
554 |
|
haftmann@38201
|
555 |
readArray :: STArray s a -> Natural -> ST s a;
|
haftmann@37838
|
556 |
readArray = Data.Array.ST.readArray;
|
haftmann@37838
|
557 |
|
haftmann@38201
|
558 |
writeArray :: STArray s a -> Natural -> a -> ST s ();
|
haftmann@37838
|
559 |
writeArray = Data.Array.ST.writeArray;*}
|
haftmann@37838
|
560 |
|
haftmann@37838
|
561 |
code_reserved Haskell Heap
|
haftmann@37838
|
562 |
|
haftmann@37838
|
563 |
text {* Monad *}
|
haftmann@37838
|
564 |
|
haftmann@37838
|
565 |
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
|
haftmann@37838
|
566 |
code_monad bind Haskell
|
haftmann@37838
|
567 |
code_const return (Haskell "return")
|
haftmann@37838
|
568 |
code_const Heap_Monad.raise' (Haskell "error")
|
haftmann@37838
|
569 |
|
haftmann@37838
|
570 |
|
haftmann@37838
|
571 |
subsubsection {* Scala *}
|
haftmann@37838
|
572 |
|
haftmann@37842
|
573 |
code_include Scala "Heap"
|
haftmann@39194
|
574 |
{*object Heap {
|
haftmann@39194
|
575 |
def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
|
haftmann@39194
|
576 |
}
|
haftmann@37842
|
577 |
|
haftmann@37842
|
578 |
class Ref[A](x: A) {
|
haftmann@37842
|
579 |
var value = x
|
haftmann@37842
|
580 |
}
|
haftmann@37842
|
581 |
|
haftmann@37842
|
582 |
object Ref {
|
haftmann@39004
|
583 |
def apply[A](x: A): Ref[A] =
|
haftmann@39004
|
584 |
new Ref[A](x)
|
haftmann@39004
|
585 |
def lookup[A](r: Ref[A]): A =
|
haftmann@39004
|
586 |
r.value
|
haftmann@39004
|
587 |
def update[A](r: Ref[A], x: A): Unit =
|
haftmann@39004
|
588 |
{ r.value = x }
|
haftmann@37842
|
589 |
}
|
haftmann@37842
|
590 |
|
haftmann@38201
|
591 |
object Array {
|
haftmann@39194
|
592 |
import collection.mutable.ArraySeq
|
haftmann@39194
|
593 |
def alloc[A](n: Natural)(x: A): ArraySeq[A] =
|
haftmann@39004
|
594 |
ArraySeq.fill(n.as_Int)(x)
|
haftmann@39194
|
595 |
def make[A](n: Natural)(f: Natural => A): ArraySeq[A] =
|
haftmann@39194
|
596 |
ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
|
haftmann@39194
|
597 |
def len[A](a: ArraySeq[A]): Natural =
|
haftmann@39194
|
598 |
Natural(a.length)
|
haftmann@39194
|
599 |
def nth[A](a: ArraySeq[A], n: Natural): A =
|
haftmann@39004
|
600 |
a(n.as_Int)
|
haftmann@39194
|
601 |
def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit =
|
haftmann@39004
|
602 |
a.update(n.as_Int, x)
|
haftmann@39004
|
603 |
def freeze[A](a: ArraySeq[A]): List[A] =
|
haftmann@39004
|
604 |
a.toList
|
haftmann@39194
|
605 |
}
|
haftmann@39194
|
606 |
*}
|
haftmann@37842
|
607 |
|
haftmann@39194
|
608 |
code_reserved Scala Heap Ref Array
|
haftmann@37838
|
609 |
|
haftmann@37838
|
610 |
code_type Heap (Scala "Unit/ =>/ _")
|
haftmann@39004
|
611 |
code_const bind (Scala "Heap.bind")
|
haftmann@37842
|
612 |
code_const return (Scala "('_: Unit)/ =>/ _")
|
haftmann@37845
|
613 |
code_const Heap_Monad.raise' (Scala "!error((_))")
|
haftmann@37838
|
614 |
|
haftmann@37838
|
615 |
|
haftmann@37838
|
616 |
subsubsection {* Target variants with less units *}
|
haftmann@37838
|
617 |
|
haftmann@31870
|
618 |
setup {*
|
haftmann@27707
|
619 |
|
haftmann@31870
|
620 |
let
|
haftmann@27707
|
621 |
|
haftmann@31870
|
622 |
open Code_Thingol;
|
haftmann@27707
|
623 |
|
haftmann@31870
|
624 |
fun imp_program naming =
|
haftmann@31870
|
625 |
let
|
haftmann@31870
|
626 |
fun is_const c = case lookup_const naming c
|
haftmann@31870
|
627 |
of SOME c' => (fn c'' => c' = c'')
|
haftmann@31870
|
628 |
| NONE => K false;
|
haftmann@37755
|
629 |
val is_bind = is_const @{const_name bind};
|
haftmann@31870
|
630 |
val is_return = is_const @{const_name return};
|
haftmann@31893
|
631 |
val dummy_name = "";
|
haftmann@31893
|
632 |
val dummy_case_term = IVar NONE;
|
haftmann@31870
|
633 |
(*assumption: dummy values are not relevant for serialization*)
|
haftmann@38303
|
634 |
val (unitt, unitT) = case lookup_const naming @{const_name Unity}
|
bulwahn@45662
|
635 |
of SOME unit' =>
|
haftmann@49087
|
636 |
let
|
haftmann@49087
|
637 |
val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
|
haftmann@49087
|
638 |
in
|
haftmann@49087
|
639 |
(IConst { name = unit', typargs = [], dicts = [], dom = [],
|
haftmann@49087
|
640 |
range = unitT, annotate = false }, unitT)
|
haftmann@49087
|
641 |
end
|
haftmann@31870
|
642 |
| NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
|
haftmann@31870
|
643 |
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
|
haftmann@31870
|
644 |
| dest_abs (t, ty) =
|
haftmann@31870
|
645 |
let
|
haftmann@31870
|
646 |
val vs = fold_varnames cons t [];
|
wenzelm@44206
|
647 |
val v = singleton (Name.variant_list vs) "x";
|
haftmann@31870
|
648 |
val ty' = (hd o fst o unfold_fun) ty;
|
haftmann@31893
|
649 |
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
|
haftmann@49087
|
650 |
fun force (t as IConst { name = c, ... } `$ t') = if is_return c
|
haftmann@31870
|
651 |
then t' else t `$ unitt
|
haftmann@31870
|
652 |
| force t = t `$ unitt;
|
haftmann@38611
|
653 |
fun tr_bind'' [(t1, _), (t2, ty2)] =
|
haftmann@31870
|
654 |
let
|
haftmann@31870
|
655 |
val ((v, ty), t) = dest_abs (t2, ty2);
|
haftmann@49087
|
656 |
in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
|
haftmann@38611
|
657 |
and tr_bind' t = case unfold_app t
|
haftmann@49087
|
658 |
of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
|
haftmann@38612
|
659 |
then tr_bind'' [(x1, ty1), (x2, ty2)]
|
haftmann@38612
|
660 |
else force t
|
haftmann@38612
|
661 |
| _ => force t;
|
haftmann@49087
|
662 |
fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
|
haftmann@49087
|
663 |
ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
|
haftmann@49087
|
664 |
fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
|
haftmann@31870
|
665 |
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
|
haftmann@31870
|
666 |
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
|
haftmann@31870
|
667 |
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
|
haftmann@31870
|
668 |
else IConst const `$$ map imp_monad_bind ts
|
haftmann@31870
|
669 |
and imp_monad_bind (IConst const) = imp_monad_bind' const []
|
haftmann@31870
|
670 |
| imp_monad_bind (t as IVar _) = t
|
haftmann@31870
|
671 |
| imp_monad_bind (t as _ `$ _) = (case unfold_app t
|
haftmann@31870
|
672 |
of (IConst const, ts) => imp_monad_bind' const ts
|
haftmann@31870
|
673 |
| (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
|
haftmann@31870
|
674 |
| imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
|
haftmann@49087
|
675 |
| imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
|
haftmann@49087
|
676 |
ICase { term = imp_monad_bind t, typ = ty,
|
haftmann@49087
|
677 |
clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
|
haftmann@31870
|
678 |
|
haftmann@39265
|
679 |
in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
|
haftmann@27707
|
680 |
|
haftmann@27707
|
681 |
in
|
haftmann@27707
|
682 |
|
haftmann@31870
|
683 |
Code_Target.extend_target ("SML_imp", ("SML", imp_program))
|
haftmann@31870
|
684 |
#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
|
haftmann@37838
|
685 |
#> Code_Target.extend_target ("Scala_imp", ("Scala", imp_program))
|
haftmann@27707
|
686 |
|
haftmann@27707
|
687 |
end
|
haftmann@31870
|
688 |
|
haftmann@27707
|
689 |
*}
|
haftmann@27707
|
690 |
|
haftmann@37757
|
691 |
hide_const (open) Heap heap guard raise' fold_map
|
haftmann@37721
|
692 |
|
haftmann@26170
|
693 |
end
|
haftmann@49087
|
694 |
|