50138
|
1 |
header "Immutable Arrays with Code Generation"
|
|
2 |
|
|
3 |
theory IArray
|
|
4 |
imports "~~/src/HOL/Library/Efficient_Nat"
|
|
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 |
|
|
18 |
fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
|
|
19 |
"of_fun f n = IArray (map f [0..<n])"
|
|
20 |
hide_const (open) of_fun
|
|
21 |
|
|
22 |
fun length :: "'a iarray \<Rightarrow> nat" where
|
|
23 |
"length (IArray xs) = List.length xs"
|
|
24 |
hide_const (open) length
|
|
25 |
|
|
26 |
fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
|
|
27 |
"(IArray as) !! n = as!n"
|
|
28 |
hide_const (open) sub
|
|
29 |
|
|
30 |
fun list_of :: "'a iarray \<Rightarrow> 'a list" where
|
|
31 |
"list_of (IArray xs) = xs"
|
|
32 |
hide_const (open) list_of
|
|
33 |
|
|
34 |
|
|
35 |
subsection "Code Generation"
|
|
36 |
|
|
37 |
code_type iarray
|
|
38 |
(SML "_ Vector.vector")
|
|
39 |
|
|
40 |
code_const IArray
|
|
41 |
(SML "Vector.fromList")
|
|
42 |
code_const IArray.sub
|
|
43 |
(SML "Vector.sub(_,_)")
|
|
44 |
code_const IArray.length
|
|
45 |
(SML "Vector.length")
|
|
46 |
code_const IArray.of_fun
|
|
47 |
(SML "!(fn f => fn n => Vector.tabulate(n,f))")
|
|
48 |
|
|
49 |
lemma list_of_code[code]:
|
|
50 |
"IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
|
|
51 |
by (cases A) (simp add: map_nth)
|
|
52 |
|
|
53 |
end
|