author  krauss 
Tue, 06 Apr 2010 11:00:57 +0200  
changeset 36078  59f6773a7d1d 
parent 36057  ca6610908ae9 
child 36176  3fe7e97ccca8 
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 
datatype exception = Exn 

16 

17 
text {* Monadic heap actions either produce values 

18 
and transform the heap, or fail *} 

19 
datatype 'a Heap = Heap "heap \<Rightarrow> ('a + exception) \<times> heap" 

20 

21 
primrec 

22 
execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a + exception) \<times> heap" where 

23 
"execute (Heap f) = f" 

24 
lemmas [code del] = execute.simps 

25 

26 
lemma Heap_execute [simp]: 

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

28 

29 
lemma Heap_eqI: 

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

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

32 

33 
lemma Heap_eqI': 

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

35 
by (auto simp: expand_fun_eq intro: Heap_eqI) 

36 

37 
lemma Heap_strip: "(\<And>f. PROP P f) \<equiv> (\<And>g. PROP P (Heap g))" 

38 
proof 

39 
fix g :: "heap \<Rightarrow> ('a + exception) \<times> heap" 

40 
assume "\<And>f. PROP P f" 

41 
then show "PROP P (Heap g)" . 

42 
next 

43 
fix f :: "'a Heap" 

44 
assume assm: "\<And>g. PROP P (Heap g)" 

45 
then have "PROP P (Heap (execute f))" . 

46 
then show "PROP P f" by simp 

47 
qed 

48 

49 
definition 

50 
heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where 

51 
[code del]: "heap f = Heap (\<lambda>h. apfst Inl (f h))" 

52 

53 
lemma execute_heap [simp]: 

54 
"execute (heap f) h = apfst Inl (f h)" 

55 
by (simp add: heap_def) 

56 

57 
definition 

58 
bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where 

59 
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of 

60 
(Inl x, h') \<Rightarrow> execute (g x) h' 

61 
 r \<Rightarrow> r)" 

62 

63 
notation 

64 
bindM (infixl "\<guillemotright>=" 54) 

65 

66 
abbreviation 

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

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

69 

70 
notation 

71 
chainM (infixl "\<guillemotright>" 54) 

72 

73 
definition 

74 
return :: "'a \<Rightarrow> 'a Heap" where 

75 
[code del]: "return x = heap (Pair x)" 

76 

77 
lemma execute_return [simp]: 

78 
"execute (return x) h = apfst Inl (x, h)" 

79 
by (simp add: return_def) 

80 

81 
definition 

82 
raise :: "string \<Rightarrow> 'a Heap" where  {* the string is just decoration *} 

83 
[code del]: "raise s = Heap (Pair (Inr Exn))" 

84 

85 
lemma execute_raise [simp]: 

86 
"execute (raise s) h = (Inr Exn, h)" 

87 
by (simp add: raise_def) 

88 

89 

90 
subsubsection {* dosyntax *} 

91 

92 
text {* 

93 
We provide a convenient donotation for monadic expressions 

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

95 
specially in doexpressions. 

96 
*} 

97 

98 
nonterminals do_expr 

99 

100 
syntax 

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

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

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

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

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

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

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

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

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

110 
("_" [12] 12) 

111 

112 
syntax (xsymbols) 

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

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

115 

116 
translations 

28145  117 
"_do f" => "f" 
26170  118 
"_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)" 
119 
"_chainM f g" => "f \<guillemotright> g" 

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

121 
"_nil f" => "f" 

122 

123 
print_translation {* 

124 
let 

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

126 
let 

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

28145  128 
in (Free (v, ty), t) end 
26170  129 
 dest_abs_eta t = 
130 
let 

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

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

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

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

35113  145 
Const (@{syntax_const "_chainM"}, dummyT) $ f $ unfold_monad g 
26170  146 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = 
147 
let 

28145  148 
val (v, g') = dest_abs_eta g; 
35113  149 
in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end 
26170  150 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) = 
28145  151 
Const (@{const_syntax return}, dummyT) $ f 
26170  152 
 unfold_monad f = f; 
28145  153 
fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true 
154 
 contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = 

155 
contains_bindM t; 

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

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

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

160 
if contains_bindM g' then list_comb 

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

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

28145  163 
else raise Match; 
35113  164 
in 
165 
[(@{const_syntax bindM}, bindM_monad_tr'), 

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

167 
end; 

26170  168 
*} 
169 

170 

171 
subsection {* Monad properties *} 

172 

173 
subsubsection {* Monad laws *} 

174 

175 
lemma return_bind: "return x \<guillemotright>= f = f x" 

176 
by (simp add: bindM_def return_def) 

177 

178 
lemma bind_return: "f \<guillemotright>= return = f" 

179 
proof (rule Heap_eqI) 

180 
fix h 

181 
show "execute (f \<guillemotright>= return) h = execute f h" 

182 
by (auto simp add: bindM_def return_def split: sum.splits prod.splits) 

183 
qed 

184 

185 
lemma bind_bind: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)" 

186 
by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits) 

187 

188 
lemma bind_bind': "f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h x) = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= (\<lambda>y. return (x, y))) \<guillemotright>= (\<lambda>(x, y). h x y)" 

189 
by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits) 

190 

191 
lemma raise_bind: "raise e \<guillemotright>= f = raise e" 

192 
by (simp add: raise_def bindM_def) 

193 

194 

195 
lemmas monad_simp = return_bind bind_return bind_bind raise_bind 

196 

197 

198 
subsection {* Generic combinators *} 

199 

200 
definition 

201 
liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" 

202 
where 

203 
"liftM f = return o f" 

204 

205 
definition 

206 
compM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> ('b \<Rightarrow> 'c Heap) \<Rightarrow> 'a \<Rightarrow> 'c Heap" (infixl ">>==" 54) 

207 
where 

208 
"(f >>== g) = (\<lambda>x. f x \<guillemotright>= g)" 

209 

210 
notation 

211 
compM (infixl "\<guillemotright>==" 54) 

212 

213 
lemma liftM_collapse: "liftM f x = return (f x)" 

214 
by (simp add: liftM_def) 

215 

216 
lemma liftM_compM: "liftM f \<guillemotright>== g = g o f" 

217 
by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def) 

218 

219 
lemma compM_return: "f \<guillemotright>== return = f" 

220 
by (simp add: compM_def monad_simp) 

221 

222 
lemma compM_compM: "(f \<guillemotright>== g) \<guillemotright>== h = f \<guillemotright>== (g \<guillemotright>== h)" 

223 
by (simp add: compM_def monad_simp) 

224 

225 
lemma liftM_bind: 

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

227 
by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def) 

228 

229 
lemma liftM_comp: 

230 
"liftM f o g = liftM (f o g)" 

231 
by (rule Heap_eqI') (simp add: liftM_def) 

232 

233 
lemmas monad_simp' = monad_simp liftM_compM compM_return 

234 
compM_compM liftM_bind liftM_comp 

235 

236 
primrec 

237 
mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" 

238 
where 

239 
"mapM f [] = return []" 

240 
 "mapM f (x#xs) = do y \<leftarrow> f x; 

241 
ys \<leftarrow> mapM f xs; 

242 
return (y # ys) 

243 
done" 

244 

245 
primrec 

246 
foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap" 

247 
where 

248 
"foldM f [] s = return s" 

249 
 "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs" 

250 

28742  251 
definition 
252 
assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" 

253 
where 

254 
"assert P x = (if P x then return x else raise (''assert''))" 

255 

256 
lemma assert_cong [fundef_cong]: 

257 
assumes "P = P'" 

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

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

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

261 

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

262 
subsubsection {* A monadic combinator for simple recursive functions *} 
36057  263 

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

265 

266 
locale mrec = 

267 
fixes 

268 
f :: "'a => ('b + 'a) Heap" 

269 
and g :: "'a => 'a => 'b => 'b Heap" 

270 
begin 

271 

272 
function (default "\<lambda>(x,h). (Inr Exn, undefined)") 

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

273 
mrec 
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 
where 
36057  275 
"mrec 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

276 
(case Heap_Monad.execute (f x) h 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

277 
(Inl (Inl r), h') \<Rightarrow> (Inl r, h') 
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 
 (Inl (Inr s), h') \<Rightarrow> 
36057  279 
(case mrec s h' of 
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

280 
(Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h'' 
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 
 (Inr e, h'') \<Rightarrow> (Inr e, h'')) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

282 
 (Inr e, h') \<Rightarrow> (Inr e, h') 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

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

284 
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

285 

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

286 
lemma graph_implies_dom: 
35423  287 
"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

288 
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

289 
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

290 
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

291 
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

292 

36057  293 
lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)" 
35423  294 
unfolding mrec_def 
36057  295 
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

296 

36057  297 
lemma mrec_di_reverse: 
298 
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

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

300 
(case Heap_Monad.execute (f x) h of 
36057  301 
(Inl (Inl r), h') \<Rightarrow> False 
302 
 (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h') 

303 
 (Inr e, h') \<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

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

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

306 
by (auto split:prod.splits sum.splits) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

307 
(erule notE, rule accpI, elim mrec_rel.cases, 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

308 

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

309 

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

310 
lemma mrec_rule: 
36057  311 
"mrec 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

312 
(case Heap_Monad.execute (f x) h 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

313 
(Inl (Inl r), h') \<Rightarrow> (Inl r, h') 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

314 
 (Inl (Inr s), h') \<Rightarrow> 
36057  315 
(case mrec s h' of 
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

316 
(Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h'' 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

317 
 (Inr e, h'') \<Rightarrow> (Inr e, h'')) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

318 
 (Inr e, h') \<Rightarrow> (Inr e, h') 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

319 
)" 
36057  320 
apply (cases "mrec_dom (x,h)", simp) 
321 
apply (frule mrec_default) 

322 
apply (frule mrec_di_reverse, simp) 

323 
by (auto split: sum.split prod.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

324 

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

325 

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

326 
definition 
36057  327 
"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

328 

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

329 
lemma MREC_rule: 
36057  330 
"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

331 
(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

332 
(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

333 
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

334 
 Inr s \<Rightarrow> 
36057  335 
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

336 
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

337 
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

338 
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

339 
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

340 
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

341 
apply (rule ext) 
36057  342 
apply (unfold mrec_rule[of 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

343 
by (auto split:prod.splits sum.splits) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

344 

36057  345 

346 
lemma MREC_pinduct: 

347 
assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')" 

348 
assumes non_rec_case: "\<And> x h h' r. Heap_Monad.execute (f x) h = (Inl (Inl r), h') \<Longrightarrow> P x h h' r" 

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

350 
\<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r" 

351 
shows "P x h h' r" 

352 
proof  

353 
from assms(1) have mrec: "mrec x h = (Inl r, h')" 

354 
unfolding MREC_def execute.simps . 

355 
from mrec have dom: "mrec_dom (x, h)" 

356 
apply  

357 
apply (rule ccontr) 

358 
apply (drule mrec_default) by auto 

359 
from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))" 

360 
by auto 

361 
from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))" 

362 
proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom]) 

363 
case (1 x h) 

364 
obtain rr h' where "mrec x h = (rr, h')" by fastsimp 

365 
obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp 

366 
show ?case 

367 
proof (cases fret) 

368 
case (Inl a) 

369 
note Inl' = this 

370 
show ?thesis 

371 
proof (cases a) 

372 
case (Inl aa) 

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

374 
by auto 

375 
next 

376 
case (Inr b) 

377 
note Inr' = this 

378 
obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp 

379 
from this Inl 1(1) exec_f mrec show ?thesis 

380 
proof (cases "ret_mrec") 

381 
case (Inl aaa) 

382 
from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3) 

383 
show ?thesis 

384 
apply auto 

385 
apply (rule rec_case) 

386 
unfolding MREC_def by auto 

387 
next 

388 
case (Inr b) 

389 
from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto 

390 
qed 

391 
qed 

392 
next 

393 
case (Inr b) 

394 
from this 1(1) mrec exec_f 1(3) show ?thesis by simp 

395 
qed 

396 
qed 

397 
from this h'_r show ?thesis by simp 

398 
qed 

399 

400 
end 

401 

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

403 

404 
abbreviation "MREC == mrec.MREC" 

405 
lemmas MREC_rule = mrec.MREC_rule 

406 
lemmas MREC_pinduct = mrec.MREC_pinduct 

407 

26170  408 
hide (open) const heap execute 
409 

26182  410 

411 
subsection {* Code generator setup *} 

412 

413 
subsubsection {* Logical intermediate layer *} 

414 

415 
definition 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31058
diff
changeset

416 
Fail :: "String.literal \<Rightarrow> exception" 
26182  417 
where 
28562  418 
[code del]: "Fail s = Exn" 
26182  419 

420 
definition 

421 
raise_exc :: "exception \<Rightarrow> 'a Heap" 

422 
where 

28562  423 
[code del]: "raise_exc e = raise []" 
26182  424 

32069
6d28bbd33e2c
prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents:
31998
diff
changeset

425 
lemma raise_raise_exc [code, code_unfold]: 
26182  426 
"raise s = raise_exc (Fail (STR s))" 
427 
unfolding Fail_def raise_exc_def raise_def .. 

428 

429 
hide (open) const Fail raise_exc 

430 

431 

27707  432 
subsubsection {* SML and OCaml *} 
26182  433 

26752  434 
code_type Heap (SML "unit/ >/ _") 
26182  435 
code_const Heap (SML "raise/ (Fail/ \"bare Heap\")") 
27826  436 
code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())") 
27707  437 
code_const return (SML "!(fn/ ()/ =>/ _)") 
26182  438 
code_const "Heap_Monad.Fail" (SML "Fail") 
27707  439 
code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)") 
26182  440 

441 
code_type Heap (OCaml "_") 

442 
code_const Heap (OCaml "failwith/ \"bare Heap\"") 

27826  443 
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ >/ f'_/ (_/ ())/ ())") 
27707  444 
code_const return (OCaml "!(fun/ ()/ >/ _)") 
26182  445 
code_const "Heap_Monad.Fail" (OCaml "Failure") 
27707  446 
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ >/ raise/ _)") 
447 

31871  448 
setup {* 
449 

450 
let 

27707  451 

31871  452 
open Code_Thingol; 
453 

454 
fun imp_program naming = 

27707  455 

31871  456 
let 
457 
fun is_const c = case lookup_const naming c 

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

459 
 NONE => K false; 

460 
val is_bindM = is_const @{const_name bindM}; 

461 
val is_return = is_const @{const_name return}; 

31893  462 
val dummy_name = ""; 
31871  463 
val dummy_type = ITyVar dummy_name; 
31893  464 
val dummy_case_term = IVar NONE; 
31871  465 
(*assumption: dummy values are not relevant for serialization*) 
466 
val unitt = case lookup_const naming @{const_name Unity} 

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

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

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

470 
 dest_abs (t, ty) = 

471 
let 

472 
val vs = fold_varnames cons t []; 

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

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

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

478 
 force t = t `$ unitt; 

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

480 
let 

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

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

483 
and tr_bind'' t = case unfold_app t 

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

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

486 
else force t 

487 
 _ => force t; 

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

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

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

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

494 
else IConst const `$$ map imp_monad_bind ts 

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

496 
 imp_monad_bind (t as IVar _) = t 

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

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

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

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

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

502 
(((imp_monad_bind t, ty), 

503 
(map o pairself) imp_monad_bind pats), 

504 
imp_monad_bind t0); 

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

505 

31871  506 
in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; 
27707  507 

508 
in 

509 

31871  510 
Code_Target.extend_target ("SML_imp", ("SML", imp_program)) 
511 
#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) 

27707  512 

513 
end 

31871  514 

27707  515 
*} 
516 

26182  517 
code_reserved OCaml Failure raise 
518 

519 

520 
subsubsection {* Haskell *} 

521 

522 
text {* Adaption layer *} 

523 

29793  524 
code_include Haskell "Heap" 
26182  525 
{*import qualified Control.Monad; 
526 
import qualified Control.Monad.ST; 

527 
import qualified Data.STRef; 

528 
import qualified Data.Array.ST; 

529 

27695  530 
type RealWorld = Control.Monad.ST.RealWorld; 
26182  531 
type ST s a = Control.Monad.ST.ST s a; 
532 
type STRef s a = Data.STRef.STRef s a; 

27673  533 
type STArray s a = Data.Array.ST.STArray s Int a; 
26182  534 

535 
newSTRef = Data.STRef.newSTRef; 

536 
readSTRef = Data.STRef.readSTRef; 

537 
writeSTRef = Data.STRef.writeSTRef; 

538 

27673  539 
newArray :: (Int, Int) > a > ST s (STArray s a); 
26182  540 
newArray = Data.Array.ST.newArray; 
541 

27673  542 
newListArray :: (Int, Int) > [a] > ST s (STArray s a); 
26182  543 
newListArray = Data.Array.ST.newListArray; 
544 

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

26182  547 

27673  548 
readArray :: STArray s a > Int > ST s a; 
26182  549 
readArray = Data.Array.ST.readArray; 
550 

27673  551 
writeArray :: STArray s a > Int > a > ST s (); 
26182  552 
writeArray = Data.Array.ST.writeArray;*} 
553 

29793  554 
code_reserved Haskell Heap 
26182  555 

556 
text {* Monad *} 

557 

29793  558 
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") 
27695  559 
code_const Heap (Haskell "error/ \"bare Heap\"") 
28145  560 
code_monad "op \<guillemotright>=" Haskell 
26182  561 
code_const return (Haskell "return") 
562 
code_const "Heap_Monad.Fail" (Haskell "_") 

563 
code_const "Heap_Monad.raise_exc" (Haskell "error") 

564 

26170  565 
end 