author | haftmann |
Mon, 21 Jul 2008 15:26:24 +0200 | |
changeset 27673 | 52056ddac194 |
parent 27656 | d4f6e64ee7cc |
child 27695 | 033732c90ebd |
permissions | -rw-r--r-- |
26170 | 1 |
(* Title: HOL/Library/Array.thy |
2 |
ID: $Id$ |
|
3 |
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Monadic arrays *} |
|
7 |
||
8 |
theory Array |
|
26182 | 9 |
imports Heap_Monad Code_Index |
26170 | 10 |
begin |
11 |
||
12 |
subsection {* Primitives *} |
|
13 |
||
14 |
definition |
|
15 |
new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
|
16 |
[code del]: "new n x = Heap_Monad.heap (Heap.array n x)" |
|
17 |
||
18 |
definition |
|
19 |
of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
|
20 |
[code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)" |
|
21 |
||
22 |
definition |
|
23 |
length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
|
24 |
[code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))" |
|
25 |
||
26 |
definition |
|
27 |
nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" |
|
28 |
where |
|
29 |
[code del]: "nth a i = (do len \<leftarrow> length a; |
|
30 |
(if i < len |
|
31 |
then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h)) |
|
32 |
else raise (''array lookup: index out of range'')) |
|
33 |
done)" |
|
34 |
||
35 |
-- {* FIXME adjustion for List theory *} |
|
36 |
no_syntax |
|
37 |
nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100) |
|
38 |
||
39 |
abbreviation |
|
40 |
nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100) |
|
41 |
where |
|
42 |
"nth_list \<equiv> List.nth" |
|
43 |
||
44 |
definition |
|
45 |
upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" |
|
46 |
where |
|
47 |
[code del]: "upd i x a = (do len \<leftarrow> length a; |
|
48 |
(if i < len |
|
26719 | 49 |
then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h)) |
50 |
else raise (''array update: index out of range'')) |
|
26170 | 51 |
done)" |
52 |
||
53 |
lemma upd_return: |
|
54 |
"upd i x a \<guillemotright> return a = upd i x a" |
|
26719 | 55 |
proof (rule Heap_eqI) |
56 |
fix h |
|
57 |
obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')" |
|
58 |
by (cases "Heap_Monad.execute (Array.length a) h") |
|
59 |
then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h" |
|
60 |
by (auto simp add: upd_def bindM_def run_drop split: sum.split) |
|
61 |
qed |
|
26170 | 62 |
|
63 |
||
64 |
subsection {* Derivates *} |
|
65 |
||
66 |
definition |
|
67 |
map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
|
68 |
where |
|
69 |
"map_entry i f a = (do |
|
70 |
x \<leftarrow> nth a i; |
|
71 |
upd i (f x) a |
|
72 |
done)" |
|
73 |
||
74 |
definition |
|
75 |
swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" |
|
76 |
where |
|
77 |
"swap i x a = (do |
|
78 |
y \<leftarrow> nth a i; |
|
79 |
upd i x a; |
|
27596 | 80 |
return y |
26170 | 81 |
done)" |
82 |
||
83 |
definition |
|
84 |
make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" |
|
85 |
where |
|
86 |
"make n f = of_list (map f [0 ..< n])" |
|
87 |
||
88 |
definition |
|
89 |
freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" |
|
90 |
where |
|
91 |
"freeze a = (do |
|
92 |
n \<leftarrow> length a; |
|
93 |
mapM (nth a) [0..<n] |
|
94 |
done)" |
|
95 |
||
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
96 |
definition |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
97 |
map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
98 |
where |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
99 |
"map f a = (do |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
100 |
n \<leftarrow> length a; |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
101 |
mapM (\<lambda>n. map_entry n f a) [0..<n]; |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
102 |
return a |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
103 |
done)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
104 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
105 |
hide (open) const new map -- {* avoid clashed with some popular names *} |
26170 | 106 |
|
107 |
||
108 |
subsection {* Properties *} |
|
109 |
||
110 |
lemma array_make [code func]: |
|
111 |
"Array.new n x = make n (\<lambda>_. x)" |
|
112 |
by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def |
|
113 |
monad_simp array_of_list_replicate [symmetric] |
|
114 |
map_replicate_trivial replicate_append_same |
|
115 |
of_list_def) |
|
116 |
||
117 |
lemma array_of_list_make [code func]: |
|
118 |
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" |
|
119 |
unfolding make_def map_nth .. |
|
120 |
||
26182 | 121 |
|
122 |
subsection {* Code generator setup *} |
|
123 |
||
124 |
subsubsection {* Logical intermediate layer *} |
|
125 |
||
126 |
definition new' where |
|
127 |
[code del]: "new' = Array.new o nat_of_index" |
|
128 |
hide (open) const new' |
|
129 |
lemma [code func]: |
|
130 |
"Array.new = Array.new' o index_of_nat" |
|
131 |
by (simp add: new'_def o_def) |
|
132 |
||
133 |
definition of_list' where |
|
134 |
[code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)" |
|
135 |
hide (open) const of_list' |
|
136 |
lemma [code func]: |
|
137 |
"Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs" |
|
138 |
by (simp add: of_list'_def) |
|
139 |
||
140 |
definition make' where |
|
141 |
[code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)" |
|
142 |
hide (open) const make' |
|
143 |
lemma [code func]: |
|
144 |
"Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)" |
|
145 |
by (simp add: make'_def o_def) |
|
146 |
||
147 |
definition length' where |
|
148 |
[code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat" |
|
149 |
hide (open) const length' |
|
150 |
lemma [code func]: |
|
151 |
"Array.length = Array.length' \<guillemotright>== liftM nat_of_index" |
|
152 |
by (simp add: length'_def monad_simp', |
|
153 |
simp add: liftM_def comp_def monad_simp, |
|
154 |
simp add: monad_simp') |
|
155 |
||
156 |
definition nth' where |
|
157 |
[code del]: "nth' a = Array.nth a o nat_of_index" |
|
158 |
hide (open) const nth' |
|
159 |
lemma [code func]: |
|
160 |
"Array.nth a n = Array.nth' a (index_of_nat n)" |
|
161 |
by (simp add: nth'_def) |
|
162 |
||
163 |
definition upd' where |
|
164 |
[code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()" |
|
165 |
hide (open) const upd' |
|
166 |
lemma [code func]: |
|
167 |
"Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a" |
|
26743 | 168 |
by (simp add: upd'_def monad_simp upd_return) |
26182 | 169 |
|
170 |
||
171 |
subsubsection {* SML *} |
|
172 |
||
173 |
code_type array (SML "_/ array") |
|
174 |
code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
|
26752 | 175 |
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
176 |
code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
|
177 |
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") |
|
178 |
code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)") |
|
179 |
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
|
180 |
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
|
26182 | 181 |
|
182 |
code_reserved SML Array |
|
183 |
||
184 |
||
185 |
subsubsection {* OCaml *} |
|
186 |
||
187 |
code_type array (OCaml "_/ array") |
|
188 |
code_const Array (OCaml "failwith/ \"bare Array\"") |
|
27673 | 189 |
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)") |
190 |
code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)") |
|
191 |
code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)") |
|
192 |
code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)") |
|
193 |
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)") |
|
194 |
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)") |
|
26182 | 195 |
|
196 |
code_reserved OCaml Array |
|
197 |
||
198 |
||
199 |
subsubsection {* Haskell *} |
|
200 |
||
201 |
code_type array (Haskell "STArray '_s _") |
|
202 |
code_const Array (Haskell "error/ \"bare Array\"") |
|
203 |
code_const Array.new' (Haskell "newArray/ (0,/ _)") |
|
204 |
code_const Array.of_list' (Haskell "newListArray/ (0,/ _)") |
|
27673 | 205 |
code_const Array.length' (Haskell "lengthArray") |
26182 | 206 |
code_const Array.nth' (Haskell "readArray") |
207 |
code_const Array.upd' (Haskell "writeArray") |
|
208 |
||
26170 | 209 |
end |