author | haftmann |
Wed, 13 Feb 2013 13:38:52 +0100 | |
changeset 51094 | 84b03c49c223 |
parent 50138 | ca989d793b34 |
child 51143 | 0a2371e7ced3 |
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 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
49 |
primrec tabulate :: "code_numeral \<times> (code_numeral \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
50 |
"tabulate (n, f) = IArray (map (f \<circ> Code_Numeral.of_nat) [0..<Code_Numeral.nat_of n])" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
51 |
hide_const (open) tabulate |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
52 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
53 |
lemma [code]: |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
54 |
"IArray.of_fun f n = IArray.tabulate (Code_Numeral.of_nat n, f \<circ> Code_Numeral.nat_of)" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
55 |
by simp |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
56 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
57 |
code_const IArray.tabulate |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
58 |
(SML "Vector.tabulate") |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
59 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
60 |
primrec sub' :: "'a iarray \<times> code_numeral \<Rightarrow> 'a" where |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
61 |
"sub' (as, n) = IArray.list_of as ! Code_Numeral.nat_of n" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
62 |
hide_const (open) sub' |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
63 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
64 |
lemma [code]: |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
65 |
"as !! n = IArray.sub' (as, Code_Numeral.of_nat n)" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
66 |
by simp |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
67 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
68 |
code_const IArray.sub' |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
69 |
(SML "Vector.sub") |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
70 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
71 |
definition length' :: "'a iarray \<Rightarrow> code_numeral" where |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
72 |
[simp]: "length' as = Code_Numeral.of_nat (List.length (IArray.list_of as))" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
73 |
hide_const (open) length' |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
74 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
75 |
lemma [code]: |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
76 |
"IArray.length as = Code_Numeral.nat_of (IArray.length' as)" |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
77 |
by simp |
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
78 |
|
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
79 |
code_const IArray.length' |
50138 | 80 |
(SML "Vector.length") |
81 |
||
82 |
end |
|
51094
84b03c49c223
IArray ignorant of particular representation of nat
haftmann
parents:
50138
diff
changeset
|
83 |