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