author | kuncar |
Sat, 16 Mar 2013 20:51:47 +0100 | |
changeset 51438 | a614e456870b |
parent 51161 | 6ed12ae3b3e1 |
child 52435 | 6646bb548c6b |
permissions | -rw-r--r-- |
50138 | 1 |
header "Immutable Arrays with Code Generation" |
2 |
||
3 |
theory IArray |
|
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
4 |
imports Main |
50138 | 5 |
begin |
6 |
||
7 |
text{* Immutable arrays are lists wrapped up in an additional constructor. |
|
8 |
There are no update operations. Hence code generation can safely implement |
|
9 |
this type by efficient target language arrays. Currently only SML is |
|
10 |
provided. Should be extended to other target languages and more operations. |
|
11 |
||
12 |
Note that arrays cannot be printed directly but only by turning them into |
|
13 |
lists first. Arrays could be converted back into lists for printing if they |
|
14 |
were wrapped up in an additional constructor. *} |
|
15 |
||
16 |
datatype 'a iarray = IArray "'a list" |
|
17 |
||
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
18 |
primrec list_of :: "'a iarray \<Rightarrow> 'a list" where |
50138 | 19 |
"list_of (IArray xs) = xs" |
20 |
hide_const (open) list_of |
|
21 |
||
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
22 |
definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
23 |
[simp]: "of_fun f n = IArray (map f [0..<n])" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
24 |
hide_const (open) of_fun |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
25 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
26 |
definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
27 |
[simp]: "as !! n = IArray.list_of as ! n" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
28 |
hide_const (open) sub |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
29 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
30 |
definition length :: "'a iarray \<Rightarrow> nat" where |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
31 |
[simp]: "length as = List.length (IArray.list_of as)" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
32 |
hide_const (open) length |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
33 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
34 |
lemma list_of_code [code]: |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
35 |
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
36 |
by (cases as) (simp add: map_nth) |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
37 |
|
50138 | 38 |
|
39 |
subsection "Code Generation" |
|
40 |
||
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
41 |
code_reserved SML Vector |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
42 |
|
50138 | 43 |
code_type iarray |
44 |
(SML "_ Vector.vector") |
|
45 |
||
46 |
code_const IArray |
|
47 |
(SML "Vector.fromList") |
|
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
48 |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
49 |
lemma [code]: |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
50 |
"size (as :: 'a iarray) = 0" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
51 |
by (cases as) simp |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
52 |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
53 |
lemma [code]: |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
54 |
"iarray_size f as = Suc (list_size f (IArray.list_of as))" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
55 |
by (cases as) simp |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
56 |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
57 |
lemma [code]: |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
58 |
"iarray_rec f as = f (IArray.list_of as)" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
59 |
by (cases as) simp |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
60 |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
61 |
lemma [code]: |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
62 |
"iarray_case f as = f (IArray.list_of as)" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
63 |
by (cases as) simp |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
64 |
|
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
65 |
lemma [code]: |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
66 |
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)" |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
67 |
by (cases as, cases bs) (simp add: equal) |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51143
diff
changeset
|
68 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
69 |
primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
70 |
"tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])" |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
71 |
hide_const (open) tabulate |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
72 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
73 |
lemma [code]: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
74 |
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)" |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
75 |
by simp |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
76 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
77 |
code_const IArray.tabulate |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
78 |
(SML "Vector.tabulate") |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
79 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
80 |
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
81 |
"sub' (as, n) = IArray.list_of as ! nat_of_integer n" |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
82 |
hide_const (open) sub' |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
83 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
84 |
lemma [code]: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
85 |
"as !! n = IArray.sub' (as, integer_of_nat n)" |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
86 |
by simp |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
87 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
88 |
code_const IArray.sub' |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
89 |
(SML "Vector.sub") |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
90 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
91 |
definition length' :: "'a iarray \<Rightarrow> integer" where |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
92 |
[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))" |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
93 |
hide_const (open) length' |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
94 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
95 |
lemma [code]: |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51094
diff
changeset
|
96 |
"IArray.length as = nat_of_integer (IArray.length' as)" |
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
97 |
by simp |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
98 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
99 |
code_const IArray.length' |
50138 | 100 |
(SML "Vector.length") |
101 |
||
102 |
end |
|
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
103 |