author | haftmann |
Fri, 08 May 2009 08:00:11 +0200 | |
changeset 31065 | d87465cbfc9e |
parent 29822 | c45845743f04 |
child 31203 | 5c8fb4fd67e0 |
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 |
definition |
|
36 |
upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" |
|
37 |
where |
|
38 |
[code del]: "upd i x a = (do len \<leftarrow> length a; |
|
39 |
(if i < len |
|
26719 | 40 |
then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h)) |
41 |
else raise (''array update: index out of range'')) |
|
26170 | 42 |
done)" |
43 |
||
44 |
lemma upd_return: |
|
45 |
"upd i x a \<guillemotright> return a = upd i x a" |
|
26719 | 46 |
proof (rule Heap_eqI) |
47 |
fix h |
|
48 |
obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')" |
|
49 |
by (cases "Heap_Monad.execute (Array.length a) h") |
|
50 |
then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h" |
|
28145 | 51 |
by (auto simp add: upd_def bindM_def split: sum.split) |
26719 | 52 |
qed |
26170 | 53 |
|
54 |
||
55 |
subsection {* Derivates *} |
|
56 |
||
57 |
definition |
|
58 |
map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
|
59 |
where |
|
60 |
"map_entry i f a = (do |
|
61 |
x \<leftarrow> nth a i; |
|
62 |
upd i (f x) a |
|
63 |
done)" |
|
64 |
||
65 |
definition |
|
66 |
swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" |
|
67 |
where |
|
68 |
"swap i x a = (do |
|
69 |
y \<leftarrow> nth a i; |
|
70 |
upd i x a; |
|
27596 | 71 |
return y |
26170 | 72 |
done)" |
73 |
||
74 |
definition |
|
75 |
make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" |
|
76 |
where |
|
77 |
"make n f = of_list (map f [0 ..< n])" |
|
78 |
||
79 |
definition |
|
80 |
freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" |
|
81 |
where |
|
82 |
"freeze a = (do |
|
83 |
n \<leftarrow> length a; |
|
84 |
mapM (nth a) [0..<n] |
|
85 |
done)" |
|
86 |
||
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
87 |
definition |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
88 |
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
|
89 |
where |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
90 |
"map f a = (do |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
91 |
n \<leftarrow> length a; |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
92 |
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
|
93 |
return a |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
94 |
done)" |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
95 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset
|
96 |
hide (open) const new map -- {* avoid clashed with some popular names *} |
26170 | 97 |
|
98 |
||
99 |
subsection {* Properties *} |
|
100 |
||
28562 | 101 |
lemma array_make [code]: |
26170 | 102 |
"Array.new n x = make n (\<lambda>_. x)" |
103 |
by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def |
|
104 |
monad_simp array_of_list_replicate [symmetric] |
|
105 |
map_replicate_trivial replicate_append_same |
|
106 |
of_list_def) |
|
107 |
||
28562 | 108 |
lemma array_of_list_make [code]: |
26170 | 109 |
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" |
110 |
unfolding make_def map_nth .. |
|
111 |
||
26182 | 112 |
|
113 |
subsection {* Code generator setup *} |
|
114 |
||
115 |
subsubsection {* Logical intermediate layer *} |
|
116 |
||
117 |
definition new' where |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
118 |
[code del]: "new' = Array.new o Code_Index.nat_of" |
26182 | 119 |
hide (open) const new' |
28562 | 120 |
lemma [code]: |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
121 |
"Array.new = Array.new' o Code_Index.of_nat" |
26182 | 122 |
by (simp add: new'_def o_def) |
123 |
||
124 |
definition of_list' where |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
125 |
[code del]: "of_list' i xs = Array.of_list (take (Code_Index.nat_of i) xs)" |
26182 | 126 |
hide (open) const of_list' |
28562 | 127 |
lemma [code]: |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
128 |
"Array.of_list xs = Array.of_list' (Code_Index.of_nat (List.length xs)) xs" |
26182 | 129 |
by (simp add: of_list'_def) |
130 |
||
131 |
definition make' where |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
132 |
[code del]: "make' i f = Array.make (Code_Index.nat_of i) (f o Code_Index.of_nat)" |
26182 | 133 |
hide (open) const make' |
28562 | 134 |
lemma [code]: |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
135 |
"Array.make n f = Array.make' (Code_Index.of_nat n) (f o Code_Index.nat_of)" |
26182 | 136 |
by (simp add: make'_def o_def) |
137 |
||
138 |
definition length' where |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
139 |
[code del]: "length' = Array.length \<guillemotright>== liftM Code_Index.of_nat" |
26182 | 140 |
hide (open) const length' |
28562 | 141 |
lemma [code]: |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
142 |
"Array.length = Array.length' \<guillemotright>== liftM Code_Index.nat_of" |
26182 | 143 |
by (simp add: length'_def monad_simp', |
144 |
simp add: liftM_def comp_def monad_simp, |
|
145 |
simp add: monad_simp') |
|
146 |
||
147 |
definition nth' where |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
148 |
[code del]: "nth' a = Array.nth a o Code_Index.nat_of" |
26182 | 149 |
hide (open) const nth' |
28562 | 150 |
lemma [code]: |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
151 |
"Array.nth a n = Array.nth' a (Code_Index.of_nat n)" |
26182 | 152 |
by (simp add: nth'_def) |
153 |
||
154 |
definition upd' where |
|
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
155 |
[code del]: "upd' a i x = Array.upd (Code_Index.nat_of i) x a \<guillemotright> return ()" |
26182 | 156 |
hide (open) const upd' |
28562 | 157 |
lemma [code]: |
29815
9e94b7078fa5
mandatory prefix for index conversion operations
haftmann
parents:
29793
diff
changeset
|
158 |
"Array.upd i x a = Array.upd' a (Code_Index.of_nat i) x \<guillemotright> return a" |
26743 | 159 |
by (simp add: upd'_def monad_simp upd_return) |
26182 | 160 |
|
161 |
||
162 |
subsubsection {* SML *} |
|
163 |
||
164 |
code_type array (SML "_/ array") |
|
165 |
code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
|
26752 | 166 |
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
167 |
code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
|
168 |
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") |
|
169 |
code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)") |
|
170 |
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
|
171 |
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
|
26182 | 172 |
|
173 |
code_reserved SML Array |
|
174 |
||
175 |
||
176 |
subsubsection {* OCaml *} |
|
177 |
||
178 |
code_type array (OCaml "_/ array") |
|
179 |
code_const Array (OCaml "failwith/ \"bare Array\"") |
|
27673 | 180 |
code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ _/ _)") |
181 |
code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)") |
|
182 |
code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ _/ _)") |
|
183 |
code_const Array.length' (OCaml "(fun/ ()/ ->/ Array.length/ _)") |
|
184 |
code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ _)") |
|
185 |
code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ _/ _)") |
|
26182 | 186 |
|
187 |
code_reserved OCaml Array |
|
188 |
||
189 |
||
190 |
subsubsection {* Haskell *} |
|
191 |
||
29793 | 192 |
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") |
26182 | 193 |
code_const Array (Haskell "error/ \"bare Array\"") |
29793 | 194 |
code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)") |
195 |
code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)") |
|
196 |
code_const Array.length' (Haskell "Heap.lengthArray") |
|
197 |
code_const Array.nth' (Haskell "Heap.readArray") |
|
198 |
code_const Array.upd' (Haskell "Heap.writeArray") |
|
26182 | 199 |
|
26170 | 200 |
end |