src/HOL/Library/IArray.thy
author Andreas Lochbihler
Fri Sep 20 10:09:16 2013 +0200 (2013-09-20)
changeset 53745 788730ab7da4
parent 52435 6646bb548c6b
child 54459 f43ae1afd08a
permissions -rw-r--r--
prefer Code.abort over code_abort
nipkow@50138
     1
header "Immutable Arrays with Code Generation"
nipkow@50138
     2
nipkow@50138
     3
theory IArray
haftmann@51094
     4
imports Main
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
haftmann@51094
    18
primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
nipkow@50138
    19
"list_of (IArray xs) = xs"
nipkow@50138
    20
hide_const (open) list_of
nipkow@50138
    21
haftmann@51094
    22
definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
haftmann@51094
    23
[simp]: "of_fun f n = IArray (map f [0..<n])"
haftmann@51094
    24
hide_const (open) of_fun
haftmann@51094
    25
haftmann@51094
    26
definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
haftmann@51094
    27
[simp]: "as !! n = IArray.list_of as ! n"
haftmann@51094
    28
hide_const (open) sub
haftmann@51094
    29
haftmann@51094
    30
definition length :: "'a iarray \<Rightarrow> nat" where
haftmann@51094
    31
[simp]: "length as = List.length (IArray.list_of as)"
haftmann@51094
    32
hide_const (open) length
haftmann@51094
    33
haftmann@51094
    34
lemma list_of_code [code]:
haftmann@51094
    35
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
haftmann@51094
    36
by (cases as) (simp add: map_nth)
haftmann@51094
    37
nipkow@50138
    38
nipkow@50138
    39
subsection "Code Generation"
nipkow@50138
    40
haftmann@51094
    41
code_reserved SML Vector
haftmann@51094
    42
haftmann@52435
    43
code_printing
haftmann@52435
    44
  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
haftmann@52435
    45
| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
haftmann@51094
    46
haftmann@51161
    47
lemma [code]:
haftmann@51161
    48
"size (as :: 'a iarray) = 0"
haftmann@51161
    49
by (cases as) simp
haftmann@51161
    50
haftmann@51161
    51
lemma [code]:
haftmann@51161
    52
"iarray_size f as = Suc (list_size f (IArray.list_of as))"
haftmann@51161
    53
by (cases as) simp
haftmann@51161
    54
haftmann@51161
    55
lemma [code]:
haftmann@51161
    56
"iarray_rec f as = f (IArray.list_of as)"
haftmann@51161
    57
by (cases as) simp
haftmann@51161
    58
haftmann@51161
    59
lemma [code]:
haftmann@51161
    60
"iarray_case f as = f (IArray.list_of as)"
haftmann@51161
    61
by (cases as) simp
haftmann@51161
    62
haftmann@51161
    63
lemma [code]:
haftmann@51161
    64
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
haftmann@51161
    65
by (cases as, cases bs) (simp add: equal)
haftmann@51161
    66
haftmann@51143
    67
primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
haftmann@51143
    68
"tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
haftmann@51094
    69
hide_const (open) tabulate
haftmann@51094
    70
haftmann@51094
    71
lemma [code]:
haftmann@51143
    72
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
haftmann@51094
    73
by simp 
haftmann@51094
    74
haftmann@52435
    75
code_printing
haftmann@52435
    76
  constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
haftmann@51094
    77
haftmann@51143
    78
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
haftmann@51143
    79
"sub' (as, n) = IArray.list_of as ! nat_of_integer n"
haftmann@51094
    80
hide_const (open) sub'
haftmann@51094
    81
haftmann@51094
    82
lemma [code]:
haftmann@51143
    83
"as !! n = IArray.sub' (as, integer_of_nat n)"
haftmann@51094
    84
by simp
haftmann@51094
    85
haftmann@52435
    86
code_printing
haftmann@52435
    87
  constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
haftmann@51094
    88
haftmann@51143
    89
definition length' :: "'a iarray \<Rightarrow> integer" where
haftmann@51143
    90
[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
haftmann@51094
    91
hide_const (open) length'
haftmann@51094
    92
haftmann@51094
    93
lemma [code]:
haftmann@51143
    94
"IArray.length as = nat_of_integer (IArray.length' as)"
haftmann@51094
    95
by simp
haftmann@51094
    96
haftmann@52435
    97
code_printing
haftmann@52435
    98
  constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
nipkow@50138
    99
nipkow@50138
   100
end
haftmann@51094
   101