author  haftmann 
Mon, 05 Jul 2010 14:34:28 +0200  
changeset 37709  70fafefbcc98 
parent 37591  d3daea901123 
child 37724  6607ccf77946 
permissions  rwrr 
26170  1 
(* Title: HOL/Library/Heap_Monad.thy 
2 
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen 

3 
*) 

4 

5 
header {* A monad with a polymorphic heap *} 

6 

7 
theory Heap_Monad 

8 
imports Heap 

9 
begin 

10 

11 
subsection {* The monad *} 

12 

13 
subsubsection {* Monad combinators *} 

14 

15 
text {* Monadic heap actions either produce values 

16 
and transform the heap, or fail *} 

37709  17 
datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option" 
26170  18 

37709  19 
primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where 
20 
[code del]: "execute (Heap f) = f" 

26170  21 

22 
lemma Heap_execute [simp]: 

23 
"Heap (execute f) = f" by (cases f) simp_all 

24 

25 
lemma Heap_eqI: 

26 
"(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g" 

27 
by (cases f, cases g) (auto simp: expand_fun_eq) 

28 

29 
lemma Heap_eqI': 

30 
"(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g" 

31 
by (auto simp: expand_fun_eq intro: Heap_eqI) 

32 

37709  33 
definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where 
34 
[code del]: "heap f = Heap (Some \<circ> f)" 

26170  35 

36 
lemma execute_heap [simp]: 

37709  37 
"execute (heap f) = Some \<circ> f" 
26170  38 
by (simp add: heap_def) 
39 

37709  40 
lemma heap_cases [case_names succeed fail]: 
41 
fixes f and h 

42 
assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P" 

43 
assumes fail: "execute f h = None \<Longrightarrow> P" 

44 
shows P 

45 
using assms by (cases "execute f h") auto 

26170  46 

37709  47 
definition return :: "'a \<Rightarrow> 'a Heap" where 
26170  48 
[code del]: "return x = heap (Pair x)" 
49 

50 
lemma execute_return [simp]: 

37709  51 
"execute (return x) = Some \<circ> Pair x" 
26170  52 
by (simp add: return_def) 
53 

37709  54 
definition raise :: "string \<Rightarrow> 'a Heap" where  {* the string is just decoration *} 
55 
[code del]: "raise s = Heap (\<lambda>_. None)" 

26170  56 

57 
lemma execute_raise [simp]: 

37709  58 
"execute (raise s) = (\<lambda>_. None)" 
26170  59 
by (simp add: raise_def) 
60 

37709  61 
definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where 
62 
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of 

63 
Some (x, h') \<Rightarrow> execute (g x) h' 

64 
 None \<Rightarrow> None)" 

65 

66 
notation bindM (infixl "\<guillemotright>=" 54) 

67 

68 
lemma execute_bind [simp]: 

69 
"execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'" 

70 
"execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None" 

71 
by (simp_all add: bindM_def) 

72 

73 
lemma execute_bind_heap [simp]: 

74 
"execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))" 

75 
by (simp add: bindM_def split_def) 

76 

77 
lemma return_bind [simp]: "return x \<guillemotright>= f = f x" 

78 
by (rule Heap_eqI) simp 

79 

80 
lemma bind_return [simp]: "f \<guillemotright>= return = f" 

81 
by (rule Heap_eqI) (simp add: bindM_def split: option.splits) 

82 

83 
lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)" 

84 
by (rule Heap_eqI) (simp add: bindM_def split: option.splits) 

85 

86 
lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e" 

87 
by (rule Heap_eqI) simp 

88 

89 
abbreviation chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where 

90 
"f >> g \<equiv> f >>= (\<lambda>_. g)" 

91 

92 
notation chainM (infixl "\<guillemotright>" 54) 

93 

26170  94 

95 
subsubsection {* dosyntax *} 

96 

97 
text {* 

98 
We provide a convenient donotation for monadic expressions 

99 
wellknown from Haskell. @{const Let} is printed 

100 
specially in doexpressions. 

101 
*} 

102 

103 
nonterminals do_expr 

104 

105 
syntax 

106 
"_do" :: "do_expr \<Rightarrow> 'a" 

107 
("(do (_)//done)" [12] 100) 

108 
"_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

109 
("_ < _;//_" [1000, 13, 12] 12) 

110 
"_chainM" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

111 
("_;//_" [13, 12] 12) 

112 
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

113 
("let _ = _;//_" [1000, 13, 12] 12) 

114 
"_nil" :: "'a \<Rightarrow> do_expr" 

115 
("_" [12] 12) 

116 

117 
syntax (xsymbols) 

118 
"_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

119 
("_ \<leftarrow> _;//_" [1000, 13, 12] 12) 

120 

121 
translations 

28145  122 
"_do f" => "f" 
26170  123 
"_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)" 
124 
"_chainM f g" => "f \<guillemotright> g" 

125 
"_let x t f" => "CONST Let t (\<lambda>x. f)" 

126 
"_nil f" => "f" 

127 

128 
print_translation {* 

129 
let 

130 
fun dest_abs_eta (Abs (abs as (_, ty, _))) = 

131 
let 

132 
val (v, t) = Syntax.variant_abs abs; 

28145  133 
in (Free (v, ty), t) end 
26170  134 
 dest_abs_eta t = 
135 
let 

136 
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0); 

28145  137 
in (Free (v, dummyT), t) end; 
26170  138 
fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) = 
139 
let 

28145  140 
val (v, g') = dest_abs_eta g; 
141 
val vs = fold_aterms (fn Free (v, _) => insert (op =) v  _ => I) v []; 

26170  142 
val v_used = fold_aterms 
28145  143 
(fn Free (w, _) => (fn s => s orelse member (op =) vs w)  _ => I) g' false; 
26170  144 
in if v_used then 
35113  145 
Const (@{syntax_const "_bindM"}, dummyT) $ v $ f $ unfold_monad g' 
26170  146 
else 
35113  147 
Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g' 
26170  148 
end 
149 
 unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) = 

35113  150 
Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g 
26170  151 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = 
152 
let 

28145  153 
val (v, g') = dest_abs_eta g; 
35113  154 
in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end 
26170  155 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) = 
28145  156 
Const (@{const_syntax return}, dummyT) $ f 
26170  157 
 unfold_monad f = f; 
28145  158 
fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true 
159 
 contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = 

160 
contains_bindM t; 

161 
fun bindM_monad_tr' (f::g::ts) = list_comb 

35113  162 
(Const (@{syntax_const "_do"}, dummyT) $ 
163 
unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts); 

164 
fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = 

165 
if contains_bindM g' then list_comb 

166 
(Const (@{syntax_const "_do"}, dummyT) $ 

167 
unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts) 

28145  168 
else raise Match; 
35113  169 
in 
170 
[(@{const_syntax bindM}, bindM_monad_tr'), 

171 
(@{const_syntax Let}, Let_monad_tr')] 

172 
end; 

26170  173 
*} 
174 

175 

176 
subsection {* Monad properties *} 

177 

178 
subsection {* Generic combinators *} 

179 

37709  180 
definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where 
181 
"assert P x = (if P x then return x else raise ''assert'')" 

28742  182 

183 
lemma assert_cong [fundef_cong]: 

184 
assumes "P = P'" 

185 
assumes "\<And>x. P' x \<Longrightarrow> f x = f' x" 

186 
shows "(assert P x >>= f) = (assert P' x >>= f')" 

187 
using assms by (auto simp add: assert_def return_bind raise_bind) 

188 

37709  189 
definition liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where 
190 
"liftM f = return o f" 

191 

192 
lemma liftM_collapse [simp]: 

193 
"liftM f x = return (f x)" 

194 
by (simp add: liftM_def) 

195 

196 
lemma bind_liftM: 

197 
"(f \<guillemotright>= liftM g) = (f \<guillemotright>= (\<lambda>x. return (g x)))" 

198 
by (simp add: liftM_def comp_def) 

199 

200 
primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where 

201 
"mapM f [] = return []" 

202 
 "mapM f (x#xs) = do 

203 
y \<leftarrow> f x; 

204 
ys \<leftarrow> mapM f xs; 

205 
return (y # ys) 

206 
done" 

207 

208 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

209 
subsubsection {* A monadic combinator for simple recursive functions *} 
36057  210 

211 
text {* Using a locale to fix arguments f and g of MREC *} 

212 

213 
locale mrec = 

37709  214 
fixes f :: "'a \<Rightarrow> ('b + 'a) Heap" 
215 
and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap" 

36057  216 
begin 
217 

37709  218 
function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where 
219 
"mrec x h = (case execute (f x) h of 

220 
Some (Inl r, h') \<Rightarrow> Some (r, h') 

221 
 Some (Inr s, h') \<Rightarrow> (case mrec s h' of 

222 
Some (z, h'') \<Rightarrow> execute (g x s z) h'' 

223 
 None \<Rightarrow> None) 

224 
 None \<Rightarrow> None)" 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

225 
by auto 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

226 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

227 
lemma graph_implies_dom: 
35423  228 
"mrec_graph x y \<Longrightarrow> mrec_dom x" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

229 
apply (induct rule:mrec_graph.induct) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

230 
apply (rule accpI) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

231 
apply (erule mrec_rel.cases) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

232 
by simp 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

233 

37709  234 
lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None" 
35423  235 
unfolding mrec_def 
36057  236 
by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified]) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

237 

36057  238 
lemma mrec_di_reverse: 
239 
assumes "\<not> mrec_dom (x, h)" 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

240 
shows " 
37709  241 
(case execute (f x) h of 
242 
Some (Inl r, h') \<Rightarrow> False 

243 
 Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h') 

244 
 None \<Rightarrow> False 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

245 
)" 
37709  246 
using assms apply (auto split: option.split sum.split) 
247 
apply (rule ccontr) 

248 
apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+ 

249 
done 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

250 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

251 
lemma mrec_rule: 
36057  252 
"mrec x h = 
37709  253 
(case execute (f x) h of 
254 
Some (Inl r, h') \<Rightarrow> Some (r, h') 

255 
 Some (Inr s, h') \<Rightarrow> 

36057  256 
(case mrec s h' of 
37709  257 
Some (z, h'') \<Rightarrow> execute (g x s z) h'' 
258 
 None \<Rightarrow> None) 

259 
 None \<Rightarrow> None 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

260 
)" 
36057  261 
apply (cases "mrec_dom (x,h)", simp) 
262 
apply (frule mrec_default) 

263 
apply (frule mrec_di_reverse, simp) 

37709  264 
by (auto split: sum.split option.split simp: mrec_default) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

265 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

266 
definition 
36057  267 
"MREC x = Heap (mrec x)" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

268 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

269 
lemma MREC_rule: 
36057  270 
"MREC x = 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

271 
(do y \<leftarrow> f x; 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

272 
(case y of 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

273 
Inl r \<Rightarrow> return r 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

274 
 Inr s \<Rightarrow> 
36057  275 
do z \<leftarrow> MREC s ; 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

276 
g x s z 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

277 
done) done)" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

278 
unfolding MREC_def 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

279 
unfolding bindM_def return_def 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

280 
apply simp 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

281 
apply (rule ext) 
36057  282 
apply (unfold mrec_rule[of x]) 
37709  283 
by (auto split: option.splits prod.splits sum.splits) 
36057  284 

285 
lemma MREC_pinduct: 

37709  286 
assumes "execute (MREC x) h = Some (r, h')" 
287 
assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r" 

288 
assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z 

289 
\<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r" 

36057  290 
shows "P x h h' r" 
291 
proof  

37709  292 
from assms(1) have mrec: "mrec x h = Some (r, h')" 
36057  293 
unfolding MREC_def execute.simps . 
294 
from mrec have dom: "mrec_dom (x, h)" 

295 
apply  

296 
apply (rule ccontr) 

297 
apply (drule mrec_default) by auto 

37709  298 
from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))" 
36057  299 
by auto 
37709  300 
from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))" 
36057  301 
proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom]) 
302 
case (1 x h) 

37709  303 
obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp 
36057  304 
show ?case 
37709  305 
proof (cases "execute (f x) h") 
306 
case (Some result) 

307 
then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp 

36057  308 
note Inl' = this 
309 
show ?thesis 

310 
proof (cases a) 

311 
case (Inl aa) 

312 
from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis 

313 
by auto 

314 
next 

315 
case (Inr b) 

316 
note Inr' = this 

37709  317 
show ?thesis 
318 
proof (cases "mrec b h1") 

319 
case (Some result) 

320 
then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp 

321 
moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" 

322 
apply (intro 1(2)) 

323 
apply (auto simp add: Inr Inl') 

324 
done 

325 
moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3) 

326 
ultimately show ?thesis 

327 
apply auto 

328 
apply (rule rec_case) 

329 
apply auto 

330 
unfolding MREC_def by auto 

36057  331 
next 
37709  332 
case None 
333 
from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto 

36057  334 
qed 
335 
qed 

336 
next 

37709  337 
case None 
338 
from this 1(1) mrec 1(3) show ?thesis by simp 

36057  339 
qed 
340 
qed 

341 
from this h'_r show ?thesis by simp 

342 
qed 

343 

344 
end 

345 

346 
text {* Providing global versions of the constant and the theorems *} 

347 

348 
abbreviation "MREC == mrec.MREC" 

349 
lemmas MREC_rule = mrec.MREC_rule 

350 
lemmas MREC_pinduct = mrec.MREC_pinduct 

351 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
36078
diff
changeset

352 
hide_const (open) heap execute 
26170  353 

26182  354 

355 
subsection {* Code generator setup *} 

356 

357 
subsubsection {* Logical intermediate layer *} 

358 

37709  359 
primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where 
360 
[code del, code_post]: "raise' (STR s) = raise s" 

26182  361 

37709  362 
lemma raise_raise' [code_inline]: 
363 
"raise s = raise' (STR s)" 

364 
by simp 

26182  365 

37709  366 
code_datatype raise'  {* avoid @{const "Heap"} formally *} 
26182  367 

37709  368 
hide_const (open) raise' 
26182  369 

370 

27707  371 
subsubsection {* SML and OCaml *} 
26182  372 

26752  373 
code_type Heap (SML "unit/ >/ _") 
27826  374 
code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())") 
27707  375 
code_const return (SML "!(fn/ ()/ =>/ _)") 
37709  376 
code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)") 
26182  377 

378 
code_type Heap (OCaml "_") 

27826  379 
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ >/ f'_/ (_/ ())/ ())") 
27707  380 
code_const return (OCaml "!(fun/ ()/ >/ _)") 
37709  381 
code_const Heap_Monad.raise' (OCaml "failwith/ _") 
27707  382 

31871  383 
setup {* 
384 

385 
let 

27707  386 

31871  387 
open Code_Thingol; 
388 

389 
fun imp_program naming = 

27707  390 

31871  391 
let 
392 
fun is_const c = case lookup_const naming c 

393 
of SOME c' => (fn c'' => c' = c'') 

394 
 NONE => K false; 

395 
val is_bindM = is_const @{const_name bindM}; 

396 
val is_return = is_const @{const_name return}; 

31893  397 
val dummy_name = ""; 
31871  398 
val dummy_type = ITyVar dummy_name; 
31893  399 
val dummy_case_term = IVar NONE; 
31871  400 
(*assumption: dummy values are not relevant for serialization*) 
401 
val unitt = case lookup_const naming @{const_name Unity} 

402 
of SOME unit' => IConst (unit', (([], []), [])) 

403 
 NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants."); 

404 
fun dest_abs ((v, ty) `=> t, _) = ((v, ty), t) 

405 
 dest_abs (t, ty) = 

406 
let 

407 
val vs = fold_varnames cons t []; 

408 
val v = Name.variant vs "x"; 

409 
val ty' = (hd o fst o unfold_fun) ty; 

31893  410 
in ((SOME v, ty'), t `$ IVar (SOME v)) end; 
31871  411 
fun force (t as IConst (c, _) `$ t') = if is_return c 
412 
then t' else t `$ unitt 

413 
 force t = t `$ unitt; 

414 
fun tr_bind' [(t1, _), (t2, ty2)] = 

415 
let 

416 
val ((v, ty), t) = dest_abs (t2, ty2); 

417 
in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end 

418 
and tr_bind'' t = case unfold_app t 

419 
of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c 

420 
then tr_bind' [(x1, ty1), (x2, ty2)] 

421 
else force t 

422 
 _ => force t; 

31893  423 
fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `=> ICase (((IVar (SOME dummy_name), dummy_type), 
31871  424 
[(unitt, tr_bind' ts)]), dummy_case_term) 
425 
and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys) 

426 
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] 

427 
 ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 

428 
 (ts, _) => imp_monad_bind (eta_expand 2 (const, ts)) 

429 
else IConst const `$$ map imp_monad_bind ts 

430 
and imp_monad_bind (IConst const) = imp_monad_bind' const [] 

431 
 imp_monad_bind (t as IVar _) = t 

432 
 imp_monad_bind (t as _ `$ _) = (case unfold_app t 

433 
of (IConst const, ts) => imp_monad_bind' const ts 

434 
 (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts) 

435 
 imp_monad_bind (v_ty `=> t) = v_ty `=> imp_monad_bind t 

436 
 imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase 

437 
(((imp_monad_bind t, ty), 

438 
(map o pairself) imp_monad_bind pats), 

439 
imp_monad_bind t0); 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28562
diff
changeset

440 

31871  441 
in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; 
27707  442 

443 
in 

444 

31871  445 
Code_Target.extend_target ("SML_imp", ("SML", imp_program)) 
446 
#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) 

27707  447 

448 
end 

31871  449 

27707  450 
*} 
451 

26182  452 

453 
subsubsection {* Haskell *} 

454 

455 
text {* Adaption layer *} 

456 

29793  457 
code_include Haskell "Heap" 
26182  458 
{*import qualified Control.Monad; 
459 
import qualified Control.Monad.ST; 

460 
import qualified Data.STRef; 

461 
import qualified Data.Array.ST; 

462 

27695  463 
type RealWorld = Control.Monad.ST.RealWorld; 
26182  464 
type ST s a = Control.Monad.ST.ST s a; 
465 
type STRef s a = Data.STRef.STRef s a; 

27673  466 
type STArray s a = Data.Array.ST.STArray s Int a; 
26182  467 

468 
newSTRef = Data.STRef.newSTRef; 

469 
readSTRef = Data.STRef.readSTRef; 

470 
writeSTRef = Data.STRef.writeSTRef; 

471 

27673  472 
newArray :: (Int, Int) > a > ST s (STArray s a); 
26182  473 
newArray = Data.Array.ST.newArray; 
474 

27673  475 
newListArray :: (Int, Int) > [a] > ST s (STArray s a); 
26182  476 
newListArray = Data.Array.ST.newListArray; 
477 

27673  478 
lengthArray :: STArray s a > ST s Int; 
479 
lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a); 

26182  480 

27673  481 
readArray :: STArray s a > Int > ST s a; 
26182  482 
readArray = Data.Array.ST.readArray; 
483 

27673  484 
writeArray :: STArray s a > Int > a > ST s (); 
26182  485 
writeArray = Data.Array.ST.writeArray;*} 
486 

29793  487 
code_reserved Haskell Heap 
26182  488 

489 
text {* Monad *} 

490 

29793  491 
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") 
28145  492 
code_monad "op \<guillemotright>=" Haskell 
26182  493 
code_const return (Haskell "return") 
37709  494 
code_const Heap_Monad.raise' (Haskell "error/ _") 
26182  495 

26170  496 
end 