author  bulwahn 
Thu, 10 Dec 2009 11:58:26 +0100  
changeset 34051  1a82e2e29d67 
parent 32069  6d28bbd33e2c 
child 35113  1a0c129bb2e0 
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 
notation (latex output) 

86 
"raise" ("\<^raw:{\textsf{raise}}>") 

87 

88 
lemma execute_raise [simp]: 

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

90 
by (simp add: raise_def) 

91 

92 

93 
subsubsection {* dosyntax *} 

94 

95 
text {* 

96 
We provide a convenient donotation for monadic expressions 

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

98 
specially in doexpressions. 

99 
*} 

100 

101 
nonterminals do_expr 

102 

103 
syntax 

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

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

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

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

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

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

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

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

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

113 
("_" [12] 12) 

114 

115 
syntax (xsymbols) 

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

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

118 
syntax (latex output) 

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

120 
("(\<^raw:{\textsf{do}}> (_))" [12] 100) 

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

122 
("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12) 

123 
notation (latex output) 

124 
"return" ("\<^raw:{\textsf{return}}>") 

125 

126 
translations 

28145  127 
"_do f" => "f" 
26170  128 
"_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)" 
129 
"_chainM f g" => "f \<guillemotright> g" 

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

131 
"_nil f" => "f" 

132 

133 
print_translation {* 

134 
let 

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

136 
let 

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

28145  138 
in (Free (v, ty), t) end 
26170  139 
 dest_abs_eta t = 
140 
let 

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

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

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

26170  147 
val v_used = fold_aterms 
28145  148 
(fn Free (w, _) => (fn s => s orelse member (op =) vs w)  _ => I) g' false; 
26170  149 
in if v_used then 
28145  150 
Const ("_bindM", dummyT) $ v $ f $ unfold_monad g' 
26170  151 
else 
152 
Const ("_chainM", dummyT) $ f $ unfold_monad g' 

153 
end 

154 
 unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) = 

155 
Const ("_chainM", dummyT) $ f $ unfold_monad g 

156 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = 

157 
let 

28145  158 
val (v, g') = dest_abs_eta g; 
159 
in Const ("_let", dummyT) $ v $ f $ unfold_monad g' end 

26170  160 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) = 
28145  161 
Const (@{const_syntax return}, dummyT) $ f 
26170  162 
 unfold_monad f = f; 
28145  163 
fun contains_bindM (Const (@{const_syntax bindM}, _) $ _ $ _) = true 
164 
 contains_bindM (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = 

165 
contains_bindM t; 

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

167 
(Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts); 

168 
fun Let_monad_tr' (f :: (g as Abs (_, _, g')) :: ts) = if contains_bindM g' then list_comb 

169 
(Const ("_do", dummyT) $ unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts) 

170 
else raise Match; 

171 
in [ 

172 
(@{const_syntax bindM}, bindM_monad_tr'), 

173 
(@{const_syntax Let}, Let_monad_tr') 

174 
] end; 

26170  175 
*} 
176 

177 

178 
subsection {* Monad properties *} 

179 

180 
subsubsection {* Monad laws *} 

181 

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

183 
by (simp add: bindM_def return_def) 

184 

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

186 
proof (rule Heap_eqI) 

187 
fix h 

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

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

190 
qed 

191 

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

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

194 

195 
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)" 

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

197 

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

199 
by (simp add: raise_def bindM_def) 

200 

201 

202 
lemmas monad_simp = return_bind bind_return bind_bind raise_bind 

203 

204 

205 
subsection {* Generic combinators *} 

206 

207 
definition 

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

209 
where 

210 
"liftM f = return o f" 

211 

212 
definition 

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

214 
where 

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

216 

217 
notation 

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

219 

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

221 
by (simp add: liftM_def) 

222 

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

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

225 

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

227 
by (simp add: compM_def monad_simp) 

228 

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

230 
by (simp add: compM_def monad_simp) 

231 

232 
lemma liftM_bind: 

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

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

235 

236 
lemma liftM_comp: 

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

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

239 

240 
lemmas monad_simp' = monad_simp liftM_compM compM_return 

241 
compM_compM liftM_bind liftM_comp 

242 

243 
primrec 

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

245 
where 

246 
"mapM f [] = return []" 

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

248 
ys \<leftarrow> mapM f xs; 

249 
return (y # ys) 

250 
done" 

251 

252 
primrec 

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

254 
where 

255 
"foldM f [] s = return s" 

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

257 

28742  258 
definition 
259 
assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" 

260 
where 

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

262 

263 
lemma assert_cong [fundef_cong]: 

264 
assumes "P = P'" 

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

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

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

268 

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

269 
subsubsection {* A monadic combinator for simple recursive functions *} 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

270 

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 
function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)") 
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 
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

273 
where 
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 
"mrec f g x 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

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

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

277 
 (Inl (Inr s), h') \<Rightarrow> 
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 
(case mrec f g s 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

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

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

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 
)" 
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 
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

284 

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 
lemma graph_implies_dom: 
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 
"mrec_graph x y \<Longrightarrow> mrec_dom 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

287 
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

288 
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

289 
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

290 
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

291 

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 
lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

293 
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

294 
by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified]) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

295 

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 
lemma f_di_reverse: 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

297 
assumes "\<not> mrec_dom (f, g, x, 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

298 
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

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

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

301 
 (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, 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

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

303 
)" 
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 
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

305 
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

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

307 

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 
lemma mrec_rule: 
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 
"mrec f g x 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

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

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

313 
 (Inl (Inr s), h') \<Rightarrow> 
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 
(case mrec f g s 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

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

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

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 
)" 
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 
apply (cases "mrec_dom (f,g,x,h)", 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

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

321 
apply (frule f_di_reverse, 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

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

323 

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 
definition 
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 
"MREC f g x = Heap (mrec f g 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

327 

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 
lemma MREC_rule: 
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 
"MREC f g 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

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

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

332 
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

333 
 Inr s \<Rightarrow> 
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 
do z \<leftarrow> MREC f g s ; 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
32069
diff
changeset

335 
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

336 
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

337 
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

338 
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

339 
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

340 
apply (rule ext) 
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 (unfold mrec_rule[of f g 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

342 
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

343 

26170  344 
hide (open) const heap execute 
345 

26182  346 

347 
subsection {* Code generator setup *} 

348 

349 
subsubsection {* Logical intermediate layer *} 

350 

351 
definition 

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

352 
Fail :: "String.literal \<Rightarrow> exception" 
26182  353 
where 
28562  354 
[code del]: "Fail s = Exn" 
26182  355 

356 
definition 

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

358 
where 

28562  359 
[code del]: "raise_exc e = raise []" 
26182  360 

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

361 
lemma raise_raise_exc [code, code_unfold]: 
26182  362 
"raise s = raise_exc (Fail (STR s))" 
363 
unfolding Fail_def raise_exc_def raise_def .. 

364 

365 
hide (open) const Fail raise_exc 

366 

367 

27707  368 
subsubsection {* SML and OCaml *} 
26182  369 

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

377 
code_type Heap (OCaml "_") 

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

27826  379 
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ >/ f'_/ (_/ ())/ ())") 
27707  380 
code_const return (OCaml "!(fun/ ()/ >/ _)") 
26182  381 
code_const "Heap_Monad.Fail" (OCaml "Failure") 
27707  382 
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ >/ raise/ _)") 
383 

31871  384 
setup {* 
385 

386 
let 

27707  387 

31871  388 
open Code_Thingol; 
389 

390 
fun imp_program naming = 

27707  391 

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

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

395 
 NONE => K false; 

396 
val is_bindM = is_const @{const_name bindM}; 

397 
val is_return = is_const @{const_name return}; 

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

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

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

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

406 
 dest_abs (t, ty) = 

407 
let 

408 
val vs = fold_varnames cons t []; 

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

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

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

414 
 force t = t `$ unitt; 

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

416 
let 

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

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

419 
and tr_bind'' t = case unfold_app t 

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

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

422 
else force t 

423 
 _ => force t; 

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

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

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

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

430 
else IConst const `$$ map imp_monad_bind ts 

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

432 
 imp_monad_bind (t as IVar _) = t 

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

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

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

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

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

438 
(((imp_monad_bind t, ty), 

439 
(map o pairself) imp_monad_bind pats), 

440 
imp_monad_bind t0); 

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

441 

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

444 
in 

445 

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

27707  448 

449 
end 

31871  450 

27707  451 
*} 
452 

26182  453 
code_reserved OCaml Failure raise 
454 

455 

456 
subsubsection {* Haskell *} 

457 

458 
text {* Adaption layer *} 

459 

29793  460 
code_include Haskell "Heap" 
26182  461 
{*import qualified Control.Monad; 
462 
import qualified Control.Monad.ST; 

463 
import qualified Data.STRef; 

464 
import qualified Data.Array.ST; 

465 

27695  466 
type RealWorld = Control.Monad.ST.RealWorld; 
26182  467 
type ST s a = Control.Monad.ST.ST s a; 
468 
type STRef s a = Data.STRef.STRef s a; 

27673  469 
type STArray s a = Data.Array.ST.STArray s Int a; 
26182  470 

471 
newSTRef = Data.STRef.newSTRef; 

472 
readSTRef = Data.STRef.readSTRef; 

473 
writeSTRef = Data.STRef.writeSTRef; 

474 

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

27673  478 
newListArray :: (Int, Int) > [a] > ST s (STArray s a); 
26182  479 
newListArray = Data.Array.ST.newListArray; 
480 

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

26182  483 

27673  484 
readArray :: STArray s a > Int > ST s a; 
26182  485 
readArray = Data.Array.ST.readArray; 
486 

27673  487 
writeArray :: STArray s a > Int > a > ST s (); 
26182  488 
writeArray = Data.Array.ST.writeArray;*} 
489 

29793  490 
code_reserved Haskell Heap 
26182  491 

492 
text {* Monad *} 

493 

29793  494 
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") 
27695  495 
code_const Heap (Haskell "error/ \"bare Heap\"") 
28145  496 
code_monad "op \<guillemotright>=" Haskell 
26182  497 
code_const return (Haskell "return") 
498 
code_const "Heap_Monad.Fail" (Haskell "_") 

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

500 

26170  501 
end 