src/HOL/Library/IArray.thy
author haftmann
Wed Jul 18 20:51:22 2018 +0200 (10 months ago)
changeset 68659 db0c70767d86
parent 68658 16cc1161ad7f
child 69272 15e9ed5b28fb
permissions -rw-r--r--
setup for Haskell taken over from AFP / Gauss_Jordan
haftmann@68657
     1
(*  Title:      HOL/Library/IArray.thy
haftmann@68657
     2
    Author:     Tobias Nipkow, TU Muenchen
haftmann@68659
     3
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
haftmann@68659
     4
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
haftmann@68657
     5
*)
haftmann@68657
     6
haftmann@68654
     7
section \<open>Immutable Arrays with Code Generation\<close>
nipkow@50138
     8
nipkow@50138
     9
theory IArray
haftmann@51094
    10
imports Main
nipkow@50138
    11
begin
nipkow@50138
    12
haftmann@68657
    13
subsection \<open>Fundamental operations\<close>
haftmann@68657
    14
haftmann@68657
    15
text \<open>Immutable arrays are lists wrapped up in an additional constructor.
nipkow@50138
    16
There are no update operations. Hence code generation can safely implement
nipkow@50138
    17
this type by efficient target language arrays.  Currently only SML is
haftmann@68657
    18
provided. Could be extended to other target languages and more operations.\<close>
nipkow@50138
    19
wenzelm@61115
    20
context
wenzelm@61115
    21
begin
wenzelm@61115
    22
blanchet@58310
    23
datatype 'a iarray = IArray "'a list"
nipkow@50138
    24
wenzelm@61115
    25
qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
nipkow@50138
    26
"list_of (IArray xs) = xs"
nipkow@50138
    27
wenzelm@61115
    28
qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
haftmann@51094
    29
[simp]: "of_fun f n = IArray (map f [0..<n])"
haftmann@51094
    30
wenzelm@61115
    31
qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
haftmann@51094
    32
[simp]: "as !! n = IArray.list_of as ! n"
haftmann@51094
    33
wenzelm@61115
    34
qualified definition length :: "'a iarray \<Rightarrow> nat" where
haftmann@51094
    35
[simp]: "length as = List.length (IArray.list_of as)"
haftmann@51094
    36
haftmann@68659
    37
qualified definition all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
haftmann@68659
    38
[simp]: "all p as \<longleftrightarrow> (\<forall>a \<in> set (list_of as). p a)"
nipkow@54459
    39
haftmann@68659
    40
qualified definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
haftmann@68659
    41
[simp]: "exists p as \<longleftrightarrow> (\<exists>a \<in> set (list_of as). p a)"
haftmann@51094
    42
haftmann@68655
    43
lemma of_fun_nth:
haftmann@68655
    44
"IArray.of_fun f n !! i = f i" if "i < n"
haftmann@68655
    45
using that by (simp add: map_nth)
haftmann@68655
    46
wenzelm@61115
    47
end
wenzelm@61115
    48
nipkow@50138
    49
haftmann@68657
    50
subsection \<open>Generic code equations\<close>
haftmann@51094
    51
haftmann@51161
    52
lemma [code]:
haftmann@68658
    53
  "size (as :: 'a iarray) = Suc (IArray.length as)"
blanchet@58269
    54
  by (cases as) simp
haftmann@51161
    55
haftmann@51161
    56
lemma [code]:
blanchet@58269
    57
  "size_iarray f as = Suc (size_list f (IArray.list_of as))"
blanchet@58269
    58
  by (cases as) simp
blanchet@58269
    59
blanchet@58269
    60
lemma [code]:
blanchet@58269
    61
  "rec_iarray f as = f (IArray.list_of as)"
blanchet@58269
    62
  by (cases as) simp
blanchet@58269
    63
blanchet@58269
    64
lemma [code]:
blanchet@58269
    65
  "case_iarray f as = f (IArray.list_of as)"
blanchet@58269
    66
  by (cases as) simp
haftmann@51161
    67
haftmann@51161
    68
lemma [code]:
blanchet@58269
    69
  "set_iarray as = set (IArray.list_of as)"
wenzelm@63649
    70
  by (cases as) auto
blanchet@58269
    71
blanchet@58269
    72
lemma [code]:
blanchet@58269
    73
  "map_iarray f as = IArray (map f (IArray.list_of as))"
wenzelm@63649
    74
  by (cases as) auto
haftmann@51161
    75
haftmann@51161
    76
lemma [code]:
blanchet@58269
    77
  "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
wenzelm@63649
    78
  by (cases as, cases bs) auto
haftmann@51161
    79
haftmann@68659
    80
lemma list_of_code [code]:
haftmann@68659
    81
  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
haftmann@68659
    82
  by (cases as) (simp add: map_nth)
haftmann@68659
    83
haftmann@51161
    84
lemma [code]:
blanchet@58269
    85
  "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
blanchet@58269
    86
  by (cases as, cases bs) (simp add: equal)
haftmann@51161
    87
haftmann@68659
    88
lemma [code]:
haftmann@68659
    89
  "IArray.all p = Not \<circ> IArray.exists (Not \<circ> p)"
haftmann@68659
    90
  by (simp add: fun_eq_iff)
haftmann@68659
    91
haftmann@59457
    92
context term_syntax
haftmann@59457
    93
begin
haftmann@59457
    94
haftmann@59457
    95
lemma [code]:
haftmann@59457
    96
  "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
haftmann@59457
    97
    Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list \<Rightarrow> 'a iarray)) <\<cdot>> (Code_Evaluation.term_of (IArray.list_of as))"
haftmann@59457
    98
  by (subst term_of_anything) rule
haftmann@59457
    99
haftmann@59457
   100
end
haftmann@59457
   101
haftmann@68657
   102
haftmann@68657
   103
subsection \<open>Auxiliary operations for code generation\<close>
haftmann@68657
   104
haftmann@68657
   105
context
haftmann@68657
   106
begin
haftmann@68657
   107
haftmann@68657
   108
qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
haftmann@68657
   109
  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
haftmann@68657
   110
haftmann@68657
   111
lemma [code]:
haftmann@68657
   112
  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
haftmann@68657
   113
  by simp
haftmann@68657
   114
haftmann@68657
   115
qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
haftmann@68659
   116
  "sub' (as, n) = as !! nat_of_integer n"
haftmann@68657
   117
haftmann@68657
   118
lemma [code]:
haftmann@68657
   119
  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
haftmann@68657
   120
  by simp
haftmann@68657
   121
haftmann@68657
   122
lemma [code]:
haftmann@68657
   123
  "as !! n = IArray.sub' (as, integer_of_nat n)"
haftmann@68657
   124
  by simp
haftmann@68657
   125
haftmann@68657
   126
qualified definition length' :: "'a iarray \<Rightarrow> integer" where
haftmann@68657
   127
  [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
haftmann@68657
   128
haftmann@68657
   129
lemma [code]:
haftmann@68657
   130
  "IArray.length' (IArray as) = integer_of_nat (List.length as)"
haftmann@68657
   131
  by simp
haftmann@68657
   132
haftmann@68657
   133
lemma [code]:
haftmann@68657
   134
  "IArray.length as = nat_of_integer (IArray.length' as)"
haftmann@68657
   135
  by simp
nipkow@50138
   136
haftmann@68659
   137
qualified definition exists_upto :: "('a \<Rightarrow> bool) \<Rightarrow> integer \<Rightarrow> 'a iarray \<Rightarrow> bool" where
haftmann@68659
   138
  [simp]: "exists_upto p k as \<longleftrightarrow> (\<exists>l. 0 \<le> l \<and> l < k \<and> p (sub' (as, l)))"
haftmann@68659
   139
haftmann@68659
   140
lemma exists_upto_of_nat:
haftmann@68659
   141
  "exists_upto p (of_nat n) as \<longleftrightarrow> (\<exists>m<n. p (as !! m))"
haftmann@68659
   142
  including integer.lifting by (simp, transfer)
haftmann@68659
   143
    (metis nat_int nat_less_iff of_nat_0_le_iff)
haftmann@68659
   144
haftmann@68659
   145
lemma [code]:
haftmann@68659
   146
  "exists_upto p k as \<longleftrightarrow> (if k \<le> 0 then False else
haftmann@68659
   147
    let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)"
haftmann@68659
   148
proof (cases "k \<ge> 1")
haftmann@68659
   149
  case False
haftmann@68659
   150
  then show ?thesis
haftmann@68659
   151
    by (auto simp add: not_le discrete)
haftmann@68659
   152
next
haftmann@68659
   153
  case True
haftmann@68659
   154
  then have less: "k \<le> 0 \<longleftrightarrow> False"
haftmann@68659
   155
    by simp
haftmann@68659
   156
  define n where "n = nat_of_integer (k - 1)"
haftmann@68659
   157
  with True have k: "k - 1 = of_nat n" "k = of_nat (Suc n)"
haftmann@68659
   158
    by simp_all
haftmann@68659
   159
  show ?thesis unfolding less Let_def k(1) unfolding k(2) exists_upto_of_nat
haftmann@68659
   160
    using less_Suc_eq by auto
haftmann@68659
   161
qed
haftmann@68659
   162
haftmann@68659
   163
lemma [code]:
haftmann@68659
   164
  "IArray.exists p as \<longleftrightarrow> exists_upto p (length' as) as"
haftmann@68659
   165
  including integer.lifting by (simp, transfer)
haftmann@68659
   166
   (auto, metis in_set_conv_nth less_imp_of_nat_less nat_int of_nat_0_le_iff)
haftmann@68659
   167
nipkow@50138
   168
end
haftmann@68657
   169
haftmann@68657
   170
haftmann@68657
   171
subsection \<open>Code Generation for SML\<close>
haftmann@68657
   172
haftmann@68657
   173
text \<open>Note that arrays cannot be printed directly but only by turning them into
haftmann@68657
   174
lists first. Arrays could be converted back into lists for printing if they
haftmann@68657
   175
were wrapped up in an additional constructor.\<close>
haftmann@68657
   176
haftmann@68657
   177
code_reserved SML Vector
haftmann@68657
   178
haftmann@68657
   179
code_printing
haftmann@68657
   180
  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
haftmann@68657
   181
| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
haftmann@68657
   182
| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
haftmann@68657
   183
| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
haftmann@68657
   184
| constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
haftmann@68657
   185
| constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
haftmann@68657
   186
| constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
haftmann@68657
   187
haftmann@68659
   188
haftmann@68659
   189
subsection \<open>Code Generation for Haskell\<close>
haftmann@68659
   190
haftmann@68659
   191
text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to @{text Data.Array.IArray.array}
haftmann@68659
   192
  in Haskell.  Performance mapping to @{text Data.Array.Unboxed.Array} and
haftmann@68659
   193
  @{text Data.Array.Array} is similar.\<close>
haftmann@68659
   194
haftmann@68659
   195
code_printing
haftmann@68659
   196
  code_module "IArray" \<rightharpoonup> (Haskell) \<open>
haftmann@68659
   197
  import Prelude (Bool(True, False), not, Maybe(Nothing, Just),
haftmann@68659
   198
    Integer, (+), (-), (<), fromInteger, toInteger, map, seq, (.));
haftmann@68659
   199
  import qualified Prelude;
haftmann@68659
   200
  import qualified Data.Array.IArray;
haftmann@68659
   201
  import qualified Data.Array.Base;
haftmann@68659
   202
  import qualified Data.Ix;
haftmann@68659
   203
haftmann@68659
   204
  newtype IArray e = IArray (Data.Array.IArray.Array Integer e);
haftmann@68659
   205
haftmann@68659
   206
  tabulate :: (Integer, (Integer -> e)) -> IArray e;
haftmann@68659
   207
  tabulate (k, f) = IArray (Data.Array.IArray.array (0, k - 1) (map (\i -> let fi = f i in fi `seq` (i, fi)) [0..k - 1]));
haftmann@68659
   208
haftmann@68659
   209
  of_list :: [e] -> IArray e;
haftmann@68659
   210
  of_list l = IArray (Data.Array.IArray.listArray (0, (toInteger . Prelude.length) l - 1) l);
haftmann@68659
   211
haftmann@68659
   212
  sub :: (IArray e, Integer) -> e;
haftmann@68659
   213
  sub (IArray v, i) = v `Data.Array.Base.unsafeAt` fromInteger i;
haftmann@68659
   214
haftmann@68659
   215
  length :: IArray e -> Integer;
haftmann@68659
   216
  length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));\<close>
haftmann@68659
   217
haftmann@68659
   218
code_reserved Haskell IArray_Impl
haftmann@68659
   219
haftmann@68659
   220
code_printing
haftmann@68659
   221
  type_constructor iarray \<rightharpoonup> (Haskell) "IArray.IArray _"
haftmann@68659
   222
| constant IArray \<rightharpoonup> (Haskell) "IArray.of'_list"
haftmann@68659
   223
| constant IArray.tabulate \<rightharpoonup> (Haskell) "IArray.tabulate"
haftmann@68659
   224
| constant IArray.sub' \<rightharpoonup> (Haskell)  "IArray.sub"
haftmann@68659
   225
| constant IArray.length' \<rightharpoonup> (Haskell) "IArray.length"
haftmann@68659
   226
haftmann@68657
   227
end