author  haftmann 
Tue, 30 Jun 2009 14:53:57 +0200  
changeset 31871  cc1486840914 
parent 31724  9b5a128cdb5c 
child 31893  7d8a89390cbf 
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 

26170  269 
hide (open) const heap execute 
270 

26182  271 

272 
subsection {* Code generator setup *} 

273 

274 
subsubsection {* Logical intermediate layer *} 

275 

276 
definition 

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

277 
Fail :: "String.literal \<Rightarrow> exception" 
26182  278 
where 
28562  279 
[code del]: "Fail s = Exn" 
26182  280 

281 
definition 

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

283 
where 

28562  284 
[code del]: "raise_exc e = raise []" 
26182  285 

28562  286 
lemma raise_raise_exc [code, code inline]: 
26182  287 
"raise s = raise_exc (Fail (STR s))" 
288 
unfolding Fail_def raise_exc_def raise_def .. 

289 

290 
hide (open) const Fail raise_exc 

291 

292 

27707  293 
subsubsection {* SML and OCaml *} 
26182  294 

26752  295 
code_type Heap (SML "unit/ >/ _") 
26182  296 
code_const Heap (SML "raise/ (Fail/ \"bare Heap\")") 
27826  297 
code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())") 
27707  298 
code_const return (SML "!(fn/ ()/ =>/ _)") 
26182  299 
code_const "Heap_Monad.Fail" (SML "Fail") 
27707  300 
code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)") 
26182  301 

302 
code_type Heap (OCaml "_") 

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

27826  304 
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ >/ f'_/ (_/ ())/ ())") 
27707  305 
code_const return (OCaml "!(fun/ ()/ >/ _)") 
26182  306 
code_const "Heap_Monad.Fail" (OCaml "Failure") 
27707  307 
code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ >/ raise/ _)") 
308 

31871  309 
setup {* 
310 

311 
let 

27707  312 

31871  313 
open Code_Thingol; 
314 

315 
fun imp_program naming = 

27707  316 

31871  317 
let 
318 
fun is_const c = case lookup_const naming c 

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

320 
 NONE => K false; 

321 
val is_bindM = is_const @{const_name bindM}; 

322 
val is_return = is_const @{const_name return}; 

323 
val dummy_name = "X"; 

324 
val dummy_type = ITyVar dummy_name; 

325 
val dummy_case_term = IVar ""; 

326 
(*assumption: dummy values are not relevant for serialization*) 

327 
val unitt = case lookup_const naming @{const_name Unity} 

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

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

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

331 
 dest_abs (t, ty) = 

332 
let 

333 
val vs = fold_varnames cons t []; 

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

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

336 
in ((v, ty'), t `$ IVar v) end; 

337 
fun force (t as IConst (c, _) `$ t') = if is_return c 

338 
then t' else t `$ unitt 

339 
 force t = t `$ unitt; 

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

341 
let 

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

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

344 
and tr_bind'' t = case unfold_app t 

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

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

347 
else force t 

348 
 _ => force t; 

349 
fun imp_monad_bind'' ts = (dummy_name, dummy_type) `=> ICase (((IVar dummy_name, dummy_type), 

350 
[(unitt, tr_bind' ts)]), dummy_case_term) 

351 
and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys) 

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

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

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

355 
else IConst const `$$ map imp_monad_bind ts 

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

357 
 imp_monad_bind (t as IVar _) = t 

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

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

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

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

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

363 
(((imp_monad_bind t, ty), 

364 
(map o pairself) imp_monad_bind pats), 

365 
imp_monad_bind t0); 

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

366 

31871  367 
in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; 
27707  368 

369 
in 

370 

31871  371 
Code_Target.extend_target ("SML_imp", ("SML", imp_program)) 
372 
#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) 

27707  373 

374 
end 

31871  375 

27707  376 
*} 
377 

26182  378 
code_reserved OCaml Failure raise 
379 

380 

381 
subsubsection {* Haskell *} 

382 

383 
text {* Adaption layer *} 

384 

29793  385 
code_include Haskell "Heap" 
26182  386 
{*import qualified Control.Monad; 
387 
import qualified Control.Monad.ST; 

388 
import qualified Data.STRef; 

389 
import qualified Data.Array.ST; 

390 

27695  391 
type RealWorld = Control.Monad.ST.RealWorld; 
26182  392 
type ST s a = Control.Monad.ST.ST s a; 
393 
type STRef s a = Data.STRef.STRef s a; 

27673  394 
type STArray s a = Data.Array.ST.STArray s Int a; 
26182  395 

396 
newSTRef = Data.STRef.newSTRef; 

397 
readSTRef = Data.STRef.readSTRef; 

398 
writeSTRef = Data.STRef.writeSTRef; 

399 

27673  400 
newArray :: (Int, Int) > a > ST s (STArray s a); 
26182  401 
newArray = Data.Array.ST.newArray; 
402 

27673  403 
newListArray :: (Int, Int) > [a] > ST s (STArray s a); 
26182  404 
newListArray = Data.Array.ST.newListArray; 
405 

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

26182  408 

27673  409 
readArray :: STArray s a > Int > ST s a; 
26182  410 
readArray = Data.Array.ST.readArray; 
411 

27673  412 
writeArray :: STArray s a > Int > a > ST s (); 
26182  413 
writeArray = Data.Array.ST.writeArray;*} 
414 

29793  415 
code_reserved Haskell Heap 
26182  416 

417 
text {* Monad *} 

418 

29793  419 
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") 
27695  420 
code_const Heap (Haskell "error/ \"bare Heap\"") 
28145  421 
code_monad "op \<guillemotright>=" Haskell 
26182  422 
code_const return (Haskell "return") 
423 
code_const "Heap_Monad.Fail" (Haskell "_") 

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

425 

26170  426 
end 