src/HOL/Library/IArray.thy
author wenzelm
Sat, 12 Jan 2013 14:53:56 +0100
changeset 50843 1465521b92a1
parent 50138 ca989d793b34
child 51094 84b03c49c223
permissions -rw-r--r--
removed unused/non-portable bash_output_fifo;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50138
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     1
header "Immutable Arrays with Code Generation"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     2
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     3
theory IArray
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     4
imports "~~/src/HOL/Library/Efficient_Nat"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     5
begin
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     6
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     7
text{* Immutable arrays are lists wrapped up in an additional constructor.
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     8
There are no update operations. Hence code generation can safely implement
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
     9
this type by efficient target language arrays.  Currently only SML is
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    10
provided. Should be extended to other target languages and more operations.
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    11
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    12
Note that arrays cannot be printed directly but only by turning them into
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    13
lists first. Arrays could be converted back into lists for printing if they
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    14
were wrapped up in an additional constructor. *}
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    15
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    16
datatype 'a iarray = IArray "'a list"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    17
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    18
fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    19
"of_fun f n = IArray (map f [0..<n])"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    20
hide_const (open) of_fun
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    21
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    22
fun length :: "'a iarray \<Rightarrow> nat" where
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    23
"length (IArray xs) = List.length xs"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    24
hide_const (open) length
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    25
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    26
fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    27
"(IArray as) !! n = as!n"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    28
hide_const (open) sub
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    29
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    30
fun list_of :: "'a iarray \<Rightarrow> 'a list" where
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    31
"list_of (IArray xs) = xs"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    32
hide_const (open) list_of
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    33
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    34
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    35
subsection "Code Generation"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    36
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    37
code_type iarray
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    38
  (SML "_ Vector.vector")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    39
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    40
code_const IArray
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    41
  (SML "Vector.fromList")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    42
code_const IArray.sub
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    43
  (SML "Vector.sub(_,_)")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    44
code_const IArray.length
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    45
  (SML "Vector.length")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    46
code_const IArray.of_fun
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    47
  (SML "!(fn f => fn n => Vector.tabulate(n,f))")
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    48
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    49
lemma list_of_code[code]:
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    50
  "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    51
by (cases A) (simp add: map_nth)
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    52
ca989d793b34 new theory of immutable arrays
nipkow
parents:
diff changeset
    53
end