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