author  haftmann 
Fri, 09 Jul 2010 09:48:53 +0200  
changeset 37754  683d1e1bc234 
parent 37724  6607ccf77946 
child 37756  59caa6180fff 
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 

37754  40 
definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where 
41 
[code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)" 

42 

43 
lemma execute_guard [simp]: 

44 
"\<not> P h \<Longrightarrow> execute (guard P f) h = None" 

45 
"P h \<Longrightarrow> execute (guard P f) h = Some (f h)" 

46 
by (simp_all add: guard_def) 

47 

37709  48 
lemma heap_cases [case_names succeed fail]: 
49 
fixes f and h 

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

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

52 
shows P 

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

26170  54 

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

58 
lemma execute_return [simp]: 

37709  59 
"execute (return x) = Some \<circ> Pair x" 
26170  60 
by (simp add: return_def) 
61 

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

26170  64 

65 
lemma execute_raise [simp]: 

37709  66 
"execute (raise s) = (\<lambda>_. None)" 
26170  67 
by (simp add: raise_def) 
68 

37754  69 
definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where (*FIXME just bind*) 
37709  70 
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of 
71 
Some (x, h') \<Rightarrow> execute (g x) h' 

72 
 None \<Rightarrow> None)" 

73 

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

75 

76 
lemma execute_bind [simp]: 

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

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

79 
by (simp_all add: bindM_def) 

80 

81 
lemma execute_bind_heap [simp]: 

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

83 
by (simp add: bindM_def split_def) 

84 

37754  85 
lemma execute_eq_SomeI: 
86 
assumes "Heap_Monad.execute f h = Some (x, h')" 

87 
and "Heap_Monad.execute (g x) h' = Some (y, h'')" 

88 
shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')" 

89 
using assms by (simp add: bindM_def) 

90 

37709  91 
lemma return_bind [simp]: "return x \<guillemotright>= f = f x" 
92 
by (rule Heap_eqI) simp 

93 

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

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

96 

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

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

99 

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

101 
by (rule Heap_eqI) simp 

102 

37754  103 
abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where 
37709  104 
"f >> g \<equiv> f >>= (\<lambda>_. g)" 
105 

37754  106 
notation chain (infixl "\<guillemotright>" 54) 
37709  107 

26170  108 

109 
subsubsection {* dosyntax *} 

110 

111 
text {* 

112 
We provide a convenient donotation for monadic expressions 

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

114 
specially in doexpressions. 

115 
*} 

116 

117 
nonterminals do_expr 

118 

119 
syntax 

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

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

37754  122 
"_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 
26170  123 
("_ < _;//_" [1000, 13, 12] 12) 
37754  124 
"_chain" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 
26170  125 
("_;//_" [13, 12] 12) 
126 
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 

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

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

129 
("_" [12] 12) 

130 

131 
syntax (xsymbols) 

37754  132 
"_bind" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr" 
26170  133 
("_ \<leftarrow> _;//_" [1000, 13, 12] 12) 
134 

135 
translations 

28145  136 
"_do f" => "f" 
37754  137 
"_bind x f g" => "f \<guillemotright>= (\<lambda>x. g)" 
138 
"_chain f g" => "f \<guillemotright> g" 

26170  139 
"_let x t f" => "CONST Let t (\<lambda>x. f)" 
140 
"_nil f" => "f" 

141 

142 
print_translation {* 

143 
let 

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

145 
let 

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

28145  147 
in (Free (v, ty), t) end 
26170  148 
 dest_abs_eta t = 
149 
let 

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

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

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

26170  156 
val v_used = fold_aterms 
28145  157 
(fn Free (w, _) => (fn s => s orelse member (op =) vs w)  _ => I) g' false; 
26170  158 
in if v_used then 
37754  159 
Const (@{syntax_const "_bind"}, dummyT) $ v $ f $ unfold_monad g' 
26170  160 
else 
37754  161 
Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g' 
26170  162 
end 
37754  163 
 unfold_monad (Const (@{const_syntax chain}, _) $ f $ g) = 
164 
Const (@{syntax_const "_chain"}, dummyT) $ f $ unfold_monad g 

26170  165 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) = 
166 
let 

28145  167 
val (v, g') = dest_abs_eta g; 
35113  168 
in Const (@{syntax_const "_let"}, dummyT) $ v $ f $ unfold_monad g' end 
26170  169 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) = 
28145  170 
Const (@{const_syntax return}, dummyT) $ f 
26170  171 
 unfold_monad f = f; 
37754  172 
fun contains_bind (Const (@{const_syntax bindM}, _) $ _ $ _) = true 
173 
 contains_bind (Const (@{const_syntax Let}, _) $ _ $ Abs (_, _, t)) = 

174 
contains_bind t; 

28145  175 
fun bindM_monad_tr' (f::g::ts) = list_comb 
35113  176 
(Const (@{syntax_const "_do"}, dummyT) $ 
177 
unfold_monad (Const (@{const_syntax bindM}, dummyT) $ f $ g), ts); 

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

37754  179 
if contains_bind g' then list_comb 
35113  180 
(Const (@{syntax_const "_do"}, dummyT) $ 
181 
unfold_monad (Const (@{const_syntax Let}, dummyT) $ f $ g), ts) 

28145  182 
else raise Match; 
35113  183 
in 
184 
[(@{const_syntax bindM}, bindM_monad_tr'), 

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

186 
end; 

26170  187 
*} 
188 

189 

190 
subsection {* Monad properties *} 

191 

192 
subsection {* Generic combinators *} 

193 

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

28742  196 

37754  197 
lemma execute_assert [simp]: 
198 
"P x \<Longrightarrow> execute (assert P x) h = Some (x, h)" 

199 
"\<not> P x \<Longrightarrow> execute (assert P x) h = None" 

200 
by (simp_all add: assert_def) 

201 

28742  202 
lemma assert_cong [fundef_cong]: 
203 
assumes "P = P'" 

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

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

37754  206 
by (rule Heap_eqI) (insert assms, simp add: assert_def) 
28742  207 

37754  208 
definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where 
209 
"lift f = return o f" 

37709  210 

37754  211 
lemma lift_collapse [simp]: 
212 
"lift f x = return (f x)" 

213 
by (simp add: lift_def) 

37709  214 

37754  215 
lemma bind_lift: 
216 
"(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))" 

217 
by (simp add: lift_def comp_def) 

37709  218 

37754  219 
primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where (*FIXME just map?*) 
37709  220 
"mapM f [] = return []" 
37754  221 
 "mapM f (x # xs) = do 
37709  222 
y \<leftarrow> f x; 
223 
ys \<leftarrow> mapM f xs; 

224 
return (y # ys) 

225 
done" 

226 

37754  227 
lemma mapM_append: 
228 
"mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))" 

229 
by (induct xs) simp_all 

230 

231 
lemma execute_mapM_unchanged_heap: 

232 
assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)" 

233 
shows "execute (mapM f xs) h = 

234 
Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" 

235 
using assms proof (induct xs) 

236 
case Nil show ?case by simp 

237 
next 

238 
case (Cons x xs) 

239 
from Cons.prems obtain y 

240 
where y: "execute (f x) h = Some (y, h)" by auto 

241 
moreover from Cons.prems Cons.hyps have "execute (mapM f xs) h = 

242 
Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto 

243 
ultimately show ?case by (simp, simp only: execute_bind(1), simp) 

244 
qed 

245 

37709  246 

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

247 
subsubsection {* A monadic combinator for simple recursive functions *} 
36057  248 

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

250 

251 
locale mrec = 

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

36057  254 
begin 
255 

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

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

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

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

261 
 None \<Rightarrow> None) 

262 
 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

263 
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

264 

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

267 
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

268 
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

269 
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

270 
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

271 

37709  272 
lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None" 
35423  273 
unfolding mrec_def 
36057  274 
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

275 

36057  276 
lemma mrec_di_reverse: 
277 
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

278 
shows " 
37709  279 
(case execute (f x) h of 
280 
Some (Inl r, h') \<Rightarrow> False 

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

282 
 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

283 
)" 
37709  284 
using assms apply (auto split: option.split sum.split) 
285 
apply (rule ccontr) 

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

287 
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

288 

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 
lemma mrec_rule: 
36057  290 
"mrec x h = 
37709  291 
(case execute (f x) h of 
292 
Some (Inl r, h') \<Rightarrow> Some (r, h') 

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

36057  294 
(case mrec s h' of 
37709  295 
Some (z, h'') \<Rightarrow> execute (g x s z) h'' 
296 
 None \<Rightarrow> None) 

297 
 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

298 
)" 
36057  299 
apply (cases "mrec_dom (x,h)", simp) 
300 
apply (frule mrec_default) 

301 
apply (frule mrec_di_reverse, simp) 

37709  302 
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

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 
definition 
36057  305 
"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

306 

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

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

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

311 
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

312 
 Inr s \<Rightarrow> 
36057  313 
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

314 
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

315 
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

316 
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

317 
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

318 
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

319 
apply (rule ext) 
36057  320 
apply (unfold mrec_rule[of x]) 
37709  321 
by (auto split: option.splits prod.splits sum.splits) 
36057  322 

323 
lemma MREC_pinduct: 

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

326 
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 

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

36057  328 
shows "P x h h' r" 
329 
proof  

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

333 
apply  

334 
apply (rule ccontr) 

335 
apply (drule mrec_default) by auto 

37709  336 
from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))" 
36057  337 
by auto 
37709  338 
from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))" 
36057  339 
proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom]) 
340 
case (1 x h) 

37709  341 
obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp 
36057  342 
show ?case 
37709  343 
proof (cases "execute (f x) h") 
344 
case (Some result) 

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

36057  346 
note Inl' = this 
347 
show ?thesis 

348 
proof (cases a) 

349 
case (Inl aa) 

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

351 
by auto 

352 
next 

353 
case (Inr b) 

354 
note Inr' = this 

37709  355 
show ?thesis 
356 
proof (cases "mrec b h1") 

357 
case (Some result) 

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

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

360 
apply (intro 1(2)) 

361 
apply (auto simp add: Inr Inl') 

362 
done 

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

364 
ultimately show ?thesis 

365 
apply auto 

366 
apply (rule rec_case) 

367 
apply auto 

368 
unfolding MREC_def by auto 

36057  369 
next 
37709  370 
case None 
371 
from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto 

36057  372 
qed 
373 
qed 

374 
next 

37709  375 
case None 
376 
from this 1(1) mrec 1(3) show ?thesis by simp 

36057  377 
qed 
378 
qed 

379 
from this h'_r show ?thesis by simp 

380 
qed 

381 

382 
end 

383 

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

385 

386 
abbreviation "MREC == mrec.MREC" 

387 
lemmas MREC_rule = mrec.MREC_rule 

388 
lemmas MREC_pinduct = mrec.MREC_pinduct 

389 

26182  390 

391 
subsection {* Code generator setup *} 

392 

393 
subsubsection {* Logical intermediate layer *} 

394 

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

26182  397 

37709  398 
lemma raise_raise' [code_inline]: 
399 
"raise s = raise' (STR s)" 

400 
by simp 

26182  401 

37709  402 
code_datatype raise'  {* avoid @{const "Heap"} formally *} 
26182  403 

404 

27707  405 
subsubsection {* SML and OCaml *} 
26182  406 

26752  407 
code_type Heap (SML "unit/ >/ _") 
27826  408 
code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())") 
27707  409 
code_const return (SML "!(fn/ ()/ =>/ _)") 
37709  410 
code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)") 
26182  411 

37754  412 
code_type Heap (OCaml "unit/ >/ _") 
27826  413 
code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ >/ f'_/ (_/ ())/ ())") 
27707  414 
code_const return (OCaml "!(fun/ ()/ >/ _)") 
37709  415 
code_const Heap_Monad.raise' (OCaml "failwith/ _") 
27707  416 

31871  417 
setup {* 
418 

419 
let 

27707  420 

31871  421 
open Code_Thingol; 
422 

423 
fun imp_program naming = 

27707  424 

31871  425 
let 
426 
fun is_const c = case lookup_const naming c 

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

428 
 NONE => K false; 

37754  429 
val is_bind = is_const @{const_name bindM}; 
31871  430 
val is_return = is_const @{const_name return}; 
31893  431 
val dummy_name = ""; 
31871  432 
val dummy_type = ITyVar dummy_name; 
31893  433 
val dummy_case_term = IVar NONE; 
31871  434 
(*assumption: dummy values are not relevant for serialization*) 
435 
val unitt = case lookup_const naming @{const_name Unity} 

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

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

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

439 
 dest_abs (t, ty) = 

440 
let 

441 
val vs = fold_varnames cons t []; 

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

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

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

447 
 force t = t `$ unitt; 

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

449 
let 

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

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

452 
and tr_bind'' t = case unfold_app t 

37754  453 
of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c 
31871  454 
then tr_bind' [(x1, ty1), (x2, ty2)] 
455 
else force t 

456 
 _ => force t; 

31893  457 
fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `=> ICase (((IVar (SOME dummy_name), dummy_type), 
31871  458 
[(unitt, tr_bind' ts)]), dummy_case_term) 
37754  459 
and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys) 
31871  460 
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] 
461 
 ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 

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

463 
else IConst const `$$ map imp_monad_bind ts 

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

465 
 imp_monad_bind (t as IVar _) = t 

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

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

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

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

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

471 
(((imp_monad_bind t, ty), 

472 
(map o pairself) imp_monad_bind pats), 

473 
imp_monad_bind t0); 

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

474 

31871  475 
in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; 
27707  476 

477 
in 

478 

31871  479 
Code_Target.extend_target ("SML_imp", ("SML", imp_program)) 
480 
#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) 

27707  481 

482 
end 

31871  483 

27707  484 
*} 
485 

26182  486 

487 
subsubsection {* Haskell *} 

488 

489 
text {* Adaption layer *} 

490 

29793  491 
code_include Haskell "Heap" 
26182  492 
{*import qualified Control.Monad; 
493 
import qualified Control.Monad.ST; 

494 
import qualified Data.STRef; 

495 
import qualified Data.Array.ST; 

496 

27695  497 
type RealWorld = Control.Monad.ST.RealWorld; 
26182  498 
type ST s a = Control.Monad.ST.ST s a; 
499 
type STRef s a = Data.STRef.STRef s a; 

27673  500 
type STArray s a = Data.Array.ST.STArray s Int a; 
26182  501 

502 
newSTRef = Data.STRef.newSTRef; 

503 
readSTRef = Data.STRef.readSTRef; 

504 
writeSTRef = Data.STRef.writeSTRef; 

505 

27673  506 
newArray :: (Int, Int) > a > ST s (STArray s a); 
26182  507 
newArray = Data.Array.ST.newArray; 
508 

27673  509 
newListArray :: (Int, Int) > [a] > ST s (STArray s a); 
26182  510 
newListArray = Data.Array.ST.newListArray; 
511 

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

26182  514 

27673  515 
readArray :: STArray s a > Int > ST s a; 
26182  516 
readArray = Data.Array.ST.readArray; 
517 

27673  518 
writeArray :: STArray s a > Int > a > ST s (); 
26182  519 
writeArray = Data.Array.ST.writeArray;*} 
520 

29793  521 
code_reserved Haskell Heap 
26182  522 

523 
text {* Monad *} 

524 

29793  525 
code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") 
28145  526 
code_monad "op \<guillemotright>=" Haskell 
26182  527 
code_const return (Haskell "return") 
37709  528 
code_const Heap_Monad.raise' (Haskell "error/ _") 
26182  529 

37754  530 
hide_const (open) Heap heap guard execute raise' 
37724  531 

26170  532 
end 