1 (* Title: HOL/Library/Ref.thy |
|
2 ID: $Id$ |
|
3 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Monadic references *} |
|
7 |
|
8 theory Ref |
|
9 imports Heap_Monad |
|
10 begin |
|
11 |
|
12 text {* |
|
13 Imperative reference operations; modeled after their ML counterparts. |
|
14 See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html |
|
15 and http://www.smlnj.org/doc/Conversion/top-level-comparison.html |
|
16 *} |
|
17 |
|
18 subsection {* Primitives *} |
|
19 |
|
20 definition |
|
21 new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where |
|
22 [code del]: "new v = Heap_Monad.heap (Heap.ref v)" |
|
23 |
|
24 definition |
|
25 lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where |
|
26 [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))" |
|
27 |
|
28 definition |
|
29 update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where |
|
30 [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))" |
|
31 |
|
32 |
|
33 subsection {* Derivates *} |
|
34 |
|
35 definition |
|
36 change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" |
|
37 where |
|
38 "change f r = (do x \<leftarrow> ! r; |
|
39 let y = f x; |
|
40 r := y; |
|
41 return y |
|
42 done)" |
|
43 |
|
44 hide (open) const new lookup update change |
|
45 |
|
46 |
|
47 subsection {* Properties *} |
|
48 |
|
49 lemma lookup_chain: |
|
50 "(!r \<guillemotright> f) = f" |
|
51 by (cases f) |
|
52 (auto simp add: Let_def bindM_def lookup_def expand_fun_eq) |
|
53 |
|
54 lemma update_change [code]: |
|
55 "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()" |
|
56 by (auto simp add: monad_simp change_def lookup_chain) |
|
57 |
|
58 |
|
59 subsection {* Code generator setup *} |
|
60 |
|
61 subsubsection {* SML *} |
|
62 |
|
63 code_type ref (SML "_/ ref") |
|
64 code_const Ref (SML "raise/ (Fail/ \"bare Ref\")") |
|
65 code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)") |
|
66 code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)") |
|
67 code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)") |
|
68 |
|
69 code_reserved SML ref |
|
70 |
|
71 |
|
72 subsubsection {* OCaml *} |
|
73 |
|
74 code_type ref (OCaml "_/ ref") |
|
75 code_const Ref (OCaml "failwith/ \"bare Ref\")") |
|
76 code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)") |
|
77 code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)") |
|
78 code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)") |
|
79 |
|
80 code_reserved OCaml ref |
|
81 |
|
82 |
|
83 subsubsection {* Haskell *} |
|
84 |
|
85 code_type ref (Haskell "STRef/ RealWorld/ _") |
|
86 code_const Ref (Haskell "error/ \"bare Ref\"") |
|
87 code_const Ref.new (Haskell "newSTRef") |
|
88 code_const Ref.lookup (Haskell "readSTRef") |
|
89 code_const Ref.update (Haskell "writeSTRef") |
|
90 |
|
91 end |
|