14 and http://www.smlnj.org/doc/Conversion/top-level-comparison.html |
14 and http://www.smlnj.org/doc/Conversion/top-level-comparison.html |
15 *} |
15 *} |
16 |
16 |
17 subsection {* Primitive layer *} |
17 subsection {* Primitive layer *} |
18 |
18 |
19 definition |
19 definition present :: "heap \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> bool" where |
20 ref_present :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> bool" where |
20 "present h r \<longleftrightarrow> addr_of_ref r < lim h" |
21 "ref_present r h \<longleftrightarrow> addr_of_ref r < lim h" |
21 |
22 |
22 definition get :: "heap \<Rightarrow> 'a\<Colon>heap ref \<Rightarrow> 'a" where |
23 definition |
23 "get h = from_nat \<circ> refs h TYPEREP('a) \<circ> addr_of_ref" |
24 get_ref :: "'a\<Colon>heap ref \<Rightarrow> heap \<Rightarrow> 'a" where |
24 |
25 "get_ref r h = from_nat (refs h (TYPEREP('a)) (addr_of_ref r))" |
25 definition set :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
26 |
26 "set r x = refs_update |
27 definition |
27 (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r := to_nat x))))" |
28 set_ref :: "'a\<Colon>heap ref \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
28 |
29 "set_ref r x = |
29 definition alloc :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where |
30 refs_update (\<lambda>h. h(TYPEREP('a) := ((h (TYPEREP('a))) (addr_of_ref r:=to_nat x))))" |
30 "alloc x h = (let |
31 |
|
32 definition ref :: "'a \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap ref \<times> heap" where |
|
33 "ref x h = (let |
|
34 l = lim h; |
31 l = lim h; |
35 r = Ref l; |
32 r = Ref l |
36 h'' = set_ref r x (h\<lparr>lim := l + 1\<rparr>) |
33 in (r, set r x (h\<lparr>lim := l + 1\<rparr>)))" |
37 in (r, h''))" |
34 |
38 |
35 definition noteq :: "'a\<Colon>heap ref \<Rightarrow> 'b\<Colon>heap ref \<Rightarrow> bool" (infix "=!=" 70) where |
39 definition noteq_refs :: "('a\<Colon>heap) ref \<Rightarrow> ('b\<Colon>heap) ref \<Rightarrow> bool" (infix "=!=" 70) where |
|
40 "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s" |
36 "r =!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_ref r \<noteq> addr_of_ref s" |
41 |
37 |
42 lemma noteq_refs_sym: "r =!= s \<Longrightarrow> s =!= r" |
38 lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r" |
43 and unequal_refs [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!" |
39 and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!" |
44 unfolding noteq_refs_def by auto |
40 by (auto simp add: noteq_def) |
45 |
41 |
46 lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False" |
42 lemma noteq_irrefl: "r =!= r \<Longrightarrow> False" |
47 unfolding noteq_refs_def by auto |
43 by (auto simp add: noteq_def) |
48 |
44 |
49 lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)" |
45 lemma present_alloc_neq: "present h r \<Longrightarrow> r =!= fst (alloc v h)" |
50 by (simp add: ref_present_def ref_def Let_def noteq_refs_def) |
46 by (simp add: present_def alloc_def noteq_def Let_def) |
51 |
47 |
52 lemma next_ref_fresh [simp]: |
48 lemma next_fresh [simp]: |
53 assumes "(r, h') = ref x h" |
49 assumes "(r, h') = alloc x h" |
54 shows "\<not> ref_present r h" |
50 shows "\<not> present h r" |
55 using assms by (cases h) (auto simp add: ref_def ref_present_def Let_def) |
51 using assms by (cases h) (auto simp add: alloc_def present_def Let_def) |
56 |
52 |
57 lemma next_ref_present [simp]: |
53 lemma next_present [simp]: |
58 assumes "(r, h') = ref x h" |
54 assumes "(r, h') = alloc x h" |
59 shows "ref_present r h'" |
55 shows "present h' r" |
60 using assms by (cases h) (auto simp add: ref_def set_ref_def ref_present_def Let_def) |
56 using assms by (cases h) (auto simp add: alloc_def set_def present_def Let_def) |
61 |
57 |
62 lemma ref_get_set_eq [simp]: "get_ref r (set_ref r x h) = x" |
58 lemma get_set_eq [simp]: |
63 by (simp add: get_ref_def set_ref_def) |
59 "get (set r x h) r = x" |
64 |
60 by (simp add: get_def set_def) |
65 lemma ref_get_set_neq [simp]: "r =!= s \<Longrightarrow> get_ref r (set_ref s x h) = get_ref r h" |
61 |
66 by (simp add: noteq_refs_def get_ref_def set_ref_def) |
62 lemma get_set_neq [simp]: |
67 |
63 "r =!= s \<Longrightarrow> get (set s x h) r = get h r" |
68 (* FIXME: We need some infrastructure to infer that locally generated |
64 by (simp add: noteq_def get_def set_def) |
69 new refs (by new_ref(_no_init), new_array(')) are distinct |
65 |
70 from all existing refs. |
66 lemma set_same [simp]: |
71 *) |
67 "set r x (set r y h) = set r x h" |
72 |
68 by (simp add: set_def) |
73 lemma ref_set_get: "set_ref r (get_ref r h) h = h" |
69 |
74 apply (simp add: set_ref_def get_ref_def) |
70 lemma set_set_swap: |
75 oops |
71 "r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)" |
76 |
72 by (simp add: noteq_def set_def expand_fun_eq) |
77 lemma set_ref_same[simp]: |
73 |
78 "set_ref r x (set_ref r y h) = set_ref r x h" |
74 lemma alloc_set: |
79 by (simp add: set_ref_def) |
75 "fst (alloc x (set r x' h)) = fst (alloc x h)" |
80 |
76 by (simp add: alloc_def set_def Let_def) |
81 lemma ref_set_set_swap: |
77 |
82 "r =!= r' \<Longrightarrow> set_ref r x (set_ref r' x' h) = set_ref r' x' (set_ref r x h)" |
78 lemma get_alloc [simp]: |
83 by (simp add: Let_def expand_fun_eq noteq_refs_def set_ref_def) |
79 "get (snd (alloc x h)) (fst (alloc x' h)) = x" |
84 |
80 by (simp add: alloc_def Let_def) |
85 lemma ref_new_set: "fst (ref v (set_ref r v' h)) = fst (ref v h)" |
81 |
86 by (simp add: ref_def set_ref_def Let_def) |
82 lemma set_alloc [simp]: |
87 |
83 "set (fst (alloc v h)) v' (snd (alloc v h)) = snd (alloc v' h)" |
88 lemma ref_get_new [simp]: |
84 by (simp add: alloc_def Let_def) |
89 "get_ref (fst (ref v h)) (snd (ref v' h)) = v'" |
85 |
90 by (simp add: ref_def Let_def split_def) |
86 lemma get_alloc_neq: "r =!= fst (alloc v h) \<Longrightarrow> |
91 |
87 get (snd (alloc v h)) r = get h r" |
92 lemma ref_set_new [simp]: |
88 by (simp add: get_def set_def alloc_def Let_def noteq_def) |
93 "set_ref (fst (ref v h)) new_v (snd (ref v h)) = snd (ref new_v h)" |
89 |
94 by (simp add: ref_def Let_def split_def) |
90 lemma lim_set [simp]: |
95 |
91 "lim (set r v h) = lim h" |
96 lemma ref_get_new_neq: "r =!= (fst (ref v h)) \<Longrightarrow> |
92 by (simp add: set_def) |
97 get_ref r (snd (ref v h)) = get_ref r h" |
93 |
98 by (simp add: get_ref_def set_ref_def ref_def Let_def noteq_refs_def) |
94 lemma present_alloc [simp]: |
99 |
95 "present h r \<Longrightarrow> present (snd (alloc v h)) r" |
100 lemma lim_set_ref [simp]: |
96 by (simp add: present_def alloc_def Let_def) |
101 "lim (set_ref r v h) = lim h" |
97 |
102 by (simp add: set_ref_def) |
98 lemma present_set [simp]: |
103 |
99 "present (set r v h) = present h" |
104 lemma ref_present_new_ref [simp]: |
100 by (simp add: present_def expand_fun_eq) |
105 "ref_present r h \<Longrightarrow> ref_present r (snd (ref v h))" |
101 |
106 by (simp add: ref_present_def ref_def Let_def) |
102 lemma noteq_I: |
107 |
103 "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'" |
108 lemma ref_present_set_ref [simp]: |
104 by (auto simp add: noteq_def present_def) |
109 "ref_present r (set_ref r' v h) = ref_present r h" |
|
110 by (simp add: set_ref_def ref_present_def) |
|
111 |
|
112 lemma noteq_refsI: "\<lbrakk> ref_present r h; \<not>ref_present r' h \<rbrakk> \<Longrightarrow> r =!= r'" |
|
113 unfolding noteq_refs_def ref_present_def |
|
114 by auto |
|
115 |
105 |
116 |
106 |
117 subsection {* Primitives *} |
107 subsection {* Primitives *} |
118 |
108 |
119 definition |
109 definition ref :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where |
120 new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where |
110 [code del]: "ref v = Heap_Monad.heap (alloc v)" |
121 [code del]: "new v = Heap_Monad.heap (Ref.ref v)" |
111 |
122 |
112 definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where |
123 definition |
113 [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get h r, h))" |
124 lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where |
114 |
125 [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))" |
115 definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where |
126 |
116 [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))" |
127 definition |
|
128 update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where |
|
129 [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))" |
|
130 |
117 |
131 |
118 |
132 subsection {* Derivates *} |
119 subsection {* Derivates *} |
133 |
120 |
134 definition |
121 definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where |
135 change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" |
122 "change f r = (do |
136 where |
123 x \<leftarrow> ! r; |
137 "change f r = (do x \<leftarrow> ! r; |
124 let y = f x; |
138 let y = f x; |
125 r := y; |
139 r := y; |
126 return y |
140 return y |
127 done)" |
141 done)" |
|
142 |
|
143 hide_const (open) new lookup update change |
|
144 |
128 |
145 |
129 |
146 subsection {* Properties *} |
130 subsection {* Properties *} |
147 |
131 |
148 lemma lookup_chain: |
132 lemma lookup_chain: |
149 "(!r \<guillemotright> f) = f" |
133 "(!r \<guillemotright> f) = f" |
150 by (cases f) |
134 by (rule Heap_eqI) (simp add: lookup_def) |
151 (auto simp add: Let_def bindM_def lookup_def expand_fun_eq) |
|
152 |
135 |
153 lemma update_change [code]: |
136 lemma update_change [code]: |
154 "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()" |
137 "r := e = change (\<lambda>_. e) r \<guillemotright> return ()" |
155 by (auto simp add: change_def lookup_chain) |
138 by (rule Heap_eqI) (simp add: change_def lookup_chain) |
156 |
139 |
157 |
140 |
158 text {* Non-interaction between imperative array and imperative references *} |
141 text {* Non-interaction between imperative array and imperative references *} |
159 |
142 |
160 lemma get_array_set_ref [simp]: "get_array a (set_ref r v h) = get_array a h" |
143 lemma get_array_set [simp]: |
161 by (simp add: get_array_def set_ref_def) |
144 "get_array a (set r v h) = get_array a h" |
162 |
145 by (simp add: get_array_def set_def) |
163 lemma nth_set_ref [simp]: "get_array a (set_ref r v h) ! i = get_array a h ! i" |
146 |
|
147 lemma nth_set [simp]: |
|
148 "get_array a (set r v h) ! i = get_array a h ! i" |
164 by simp |
149 by simp |
165 |
150 |
166 lemma get_ref_upd [simp]: "get_ref r (Array.change a i v h) = get_ref r h" |
151 lemma get_change [simp]: |
167 by (simp add: get_ref_def set_array_def Array.change_def) |
152 "get (Array.change a i v h) r = get h r" |
168 |
153 by (simp add: get_def Array.change_def set_array_def) |
169 lemma new_ref_upd: "fst (ref v (Array.change a i v' h)) = fst (ref v h)" |
154 |
170 by (simp add: set_array_def get_array_def Let_def ref_new_set Array.change_def ref_def) |
155 lemma alloc_change: |
171 |
156 "fst (alloc v (Array.change a i v' h)) = fst (alloc v h)" |
172 lemma upd_set_ref_swap: "Array.change a i v (set_ref r v' h) = set_ref r v' (Array.change a i v h)" |
157 by (simp add: Array.change_def get_array_def set_array_def alloc_def Let_def) |
173 by (simp add: set_ref_def Array.change_def get_array_def set_array_def) |
158 |
174 |
159 lemma change_set_swap: |
175 lemma length_new_ref[simp]: |
160 "Array.change a i v (set r v' h) = set r v' (Array.change a i v h)" |
176 "length a (snd (ref v h)) = length a h" |
161 by (simp add: Array.change_def get_array_def set_array_def set_def) |
177 by (simp add: get_array_def set_ref_def length_def ref_def Let_def) |
162 |
178 |
163 lemma length_alloc [simp]: |
179 lemma get_array_new_ref [simp]: |
164 "Array.length a (snd (alloc v h)) = Array.length a h" |
180 "get_array a (snd (ref v h)) = get_array a h" |
165 by (simp add: Array.length_def get_array_def alloc_def set_def Let_def) |
181 by (simp add: ref_def set_ref_def get_array_def Let_def) |
166 |
182 |
167 lemma get_array_alloc [simp]: |
183 lemma ref_present_upd [simp]: |
168 "get_array a (snd (alloc v h)) = get_array a h" |
184 "ref_present r (Array.change a i v h) = ref_present r h" |
169 by (simp add: get_array_def alloc_def set_def Let_def) |
185 by (simp add: Array.change_def ref_present_def set_array_def get_array_def) |
170 |
186 |
171 lemma present_change [simp]: |
187 lemma array_present_set_ref [simp]: |
172 "present (Array.change a i v h) = present h" |
188 "array_present a (set_ref r v h) = array_present a h" |
173 by (simp add: Array.change_def set_array_def expand_fun_eq present_def) |
189 by (simp add: array_present_def set_ref_def) |
174 |
190 |
175 lemma array_present_set [simp]: |
191 lemma array_present_new_ref [simp]: |
176 "array_present a (set r v h) = array_present a h" |
192 "array_present a h \<Longrightarrow> array_present a (snd (ref v h))" |
177 by (simp add: array_present_def set_def) |
193 by (simp add: array_present_def ref_def Let_def) |
178 |
194 |
179 lemma array_present_alloc [simp]: |
195 lemma array_ref_set_set_swap: |
180 "array_present a h \<Longrightarrow> array_present a (snd (alloc v h))" |
196 "set_array r x (set_ref r' x' h) = set_ref r' x' (set_array r x h)" |
181 by (simp add: array_present_def alloc_def Let_def) |
197 by (simp add: Let_def expand_fun_eq set_array_def set_ref_def) |
182 |
|
183 lemma set_array_set_swap: |
|
184 "set_array a xs (set r x' h) = set r x' (set_array a xs h)" |
|
185 by (simp add: set_array_def set_def) |
|
186 |
|
187 hide_const (open) present get set alloc lookup update change |
198 |
188 |
199 |
189 |
200 subsection {* Code generator setup *} |
190 subsection {* Code generator setup *} |
201 |
191 |
202 subsubsection {* SML *} |
192 subsubsection {* SML *} |
203 |
193 |
204 code_type ref (SML "_/ Unsynchronized.ref") |
194 code_type ref (SML "_/ Unsynchronized.ref") |
205 code_const Ref (SML "raise/ (Fail/ \"bare Ref\")") |
195 code_const Ref (SML "raise/ (Fail/ \"bare Ref\")") |
206 code_const Ref.new (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)") |
196 code_const ref (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)") |
207 code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)") |
197 code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)") |
208 code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)") |
198 code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)") |
209 |
199 |
210 code_reserved SML ref |
200 code_reserved SML ref |
211 |
201 |
212 |
202 |
213 subsubsection {* OCaml *} |
203 subsubsection {* OCaml *} |
214 |
204 |
215 code_type ref (OCaml "_/ ref") |
205 code_type ref (OCaml "_/ ref") |
216 code_const Ref (OCaml "failwith/ \"bare Ref\")") |
206 code_const Ref (OCaml "failwith/ \"bare Ref\")") |
217 code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)") |
207 code_const ref (OCaml "(fn/ ()/ =>/ ref/ _)") |
218 code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)") |
208 code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)") |
219 code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)") |
209 code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)") |
220 |
210 |
221 code_reserved OCaml ref |
211 code_reserved OCaml ref |
222 |
212 |
223 |
213 |
224 subsubsection {* Haskell *} |
214 subsubsection {* Haskell *} |
225 |
215 |
226 code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _") |
216 code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _") |
227 code_const Ref (Haskell "error/ \"bare Ref\"") |
217 code_const Ref (Haskell "error/ \"bare Ref\"") |
228 code_const Ref.new (Haskell "Heap.newSTRef") |
218 code_const ref (Haskell "Heap.newSTRef") |
229 code_const Ref.lookup (Haskell "Heap.readSTRef") |
219 code_const Ref.lookup (Haskell "Heap.readSTRef") |
230 code_const Ref.update (Haskell "Heap.writeSTRef") |
220 code_const Ref.update (Haskell "Heap.writeSTRef") |
231 |
221 |
232 end |
222 end |