src/HOL/Library/IArray.thy
author haftmann
Wed Jan 28 08:29:08 2015 +0100 (2015-01-28)
changeset 59457 c4f044389c28
parent 58881 b9556a055632
child 60500 903bb1495239
permissions -rw-r--r--
proper term_of for iarray
wenzelm@58881
     1
section "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
blanchet@58310
    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
nipkow@54459
    34
fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
nipkow@54459
    35
"all p (IArray as) = (ALL a : set as. p a)"
nipkow@54459
    36
hide_const (open) all
nipkow@54459
    37
nipkow@54459
    38
fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
nipkow@54459
    39
"exists p (IArray as) = (EX a : set as. p a)"
nipkow@54459
    40
hide_const (open) exists
nipkow@54459
    41
haftmann@51094
    42
lemma list_of_code [code]:
haftmann@51094
    43
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
haftmann@51094
    44
by (cases as) (simp add: map_nth)
haftmann@51094
    45
nipkow@50138
    46
nipkow@50138
    47
subsection "Code Generation"
nipkow@50138
    48
haftmann@51094
    49
code_reserved SML Vector
haftmann@51094
    50
haftmann@52435
    51
code_printing
haftmann@52435
    52
  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
haftmann@52435
    53
| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
nipkow@54459
    54
| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
nipkow@54459
    55
| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
haftmann@51094
    56
haftmann@51161
    57
lemma [code]:
blanchet@58269
    58
  "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
blanchet@58269
    59
  by (cases as) simp
haftmann@51161
    60
haftmann@51161
    61
lemma [code]:
blanchet@58269
    62
  "size_iarray f as = Suc (size_list f (IArray.list_of as))"
blanchet@58269
    63
  by (cases as) simp
blanchet@58269
    64
blanchet@58269
    65
lemma [code]:
blanchet@58269
    66
  "rec_iarray f as = f (IArray.list_of as)"
blanchet@58269
    67
  by (cases as) simp
blanchet@58269
    68
blanchet@58269
    69
lemma [code]:
blanchet@58269
    70
  "case_iarray f as = f (IArray.list_of as)"
blanchet@58269
    71
  by (cases as) simp
haftmann@51161
    72
haftmann@51161
    73
lemma [code]:
blanchet@58269
    74
  "set_iarray as = set (IArray.list_of as)"
blanchet@58269
    75
  by (case_tac as) auto
blanchet@58269
    76
blanchet@58269
    77
lemma [code]:
blanchet@58269
    78
  "map_iarray f as = IArray (map f (IArray.list_of as))"
blanchet@58269
    79
  by (case_tac as) auto
haftmann@51161
    80
haftmann@51161
    81
lemma [code]:
blanchet@58269
    82
  "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
blanchet@58269
    83
  by (case_tac as) (case_tac bs, auto)
haftmann@51161
    84
haftmann@51161
    85
lemma [code]:
blanchet@58269
    86
  "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
blanchet@58269
    87
  by (cases as, cases bs) (simp add: equal)
haftmann@51161
    88
haftmann@51143
    89
primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
blanchet@58269
    90
  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
blanchet@58269
    91
haftmann@51094
    92
hide_const (open) tabulate
haftmann@51094
    93
haftmann@51094
    94
lemma [code]:
blanchet@58269
    95
  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
blanchet@58269
    96
  by simp
haftmann@51094
    97
haftmann@52435
    98
code_printing
haftmann@52435
    99
  constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
haftmann@51094
   100
haftmann@51143
   101
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
blanchet@58269
   102
  [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
blanchet@58269
   103
haftmann@51094
   104
hide_const (open) sub'
haftmann@51094
   105
haftmann@51094
   106
lemma [code]:
haftmann@57117
   107
  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
haftmann@57117
   108
  by simp
haftmann@57117
   109
haftmann@57117
   110
lemma [code]:
blanchet@58269
   111
  "as !! n = IArray.sub' (as, integer_of_nat n)"
blanchet@58269
   112
  by simp
haftmann@51094
   113
haftmann@52435
   114
code_printing
haftmann@52435
   115
  constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
haftmann@51094
   116
haftmann@51143
   117
definition length' :: "'a iarray \<Rightarrow> integer" where
blanchet@58269
   118
  [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
blanchet@58269
   119
haftmann@51094
   120
hide_const (open) length'
haftmann@51094
   121
haftmann@51094
   122
lemma [code]:
haftmann@57117
   123
  "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
haftmann@57117
   124
  by simp
haftmann@57117
   125
haftmann@57117
   126
lemma [code]:
blanchet@58269
   127
  "IArray.length as = nat_of_integer (IArray.length' as)"
blanchet@58269
   128
  by simp
haftmann@51094
   129
haftmann@59457
   130
context term_syntax
haftmann@59457
   131
begin
haftmann@59457
   132
haftmann@59457
   133
lemma [code]:
haftmann@59457
   134
  "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
haftmann@59457
   135
    Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list \<Rightarrow> 'a iarray)) <\<cdot>> (Code_Evaluation.term_of (IArray.list_of as))"
haftmann@59457
   136
  by (subst term_of_anything) rule
haftmann@59457
   137
haftmann@59457
   138
end
haftmann@59457
   139
haftmann@52435
   140
code_printing
haftmann@52435
   141
  constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
nipkow@50138
   142
nipkow@50138
   143
end