src/HOL/Library/IArray.thy

 (*  Title:      HOL/Library/IArray.thy
     Author:     Tobias Nipkow, TU Muenchen
+    Author:     Jose Divasón <jose.divasonm at unirioja.es>
+    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
 *)
 
 section \<open>Immutable Arrays with Code Generation\<close>
 
 theory IArray

 [simp]: "as !! n = IArray.list_of as ! n"
 
 qualified definition length :: "'a iarray \<Rightarrow> nat" where
 [simp]: "length as = List.length (IArray.list_of as)"
 
-qualified primrec all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"all p (IArray as) \<longleftrightarrow> (\<forall>a \<in> set as. p a)"
-
-qualified primrec exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"exists p (IArray as) \<longleftrightarrow> (\<exists>a \<in> set as. p a)"
-
-lemma list_of_code [code]:
-"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
-by (cases as) (simp add: map_nth)
+qualified definition all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+[simp]: "all p as \<longleftrightarrow> (\<forall>a \<in> set (list_of as). p a)"
+
+qualified definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+[simp]: "exists p as \<longleftrightarrow> (\<exists>a \<in> set (list_of as). p a)"
 
 lemma of_fun_nth:
 "IArray.of_fun f n !! i = f i" if "i < n"
 using that by (simp add: map_nth)
 

 
 lemma [code]:
   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
   by (cases as, cases bs) auto
 
+lemma list_of_code [code]:
+  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
+  by (cases as) (simp add: map_nth)
+
 lemma [code]:
   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
   by (cases as, cases bs) (simp add: equal)
+
+lemma [code]:
+  "IArray.all p = Not \<circ> IArray.exists (Not \<circ> p)"
+  by (simp add: fun_eq_iff)
 
 context term_syntax
 begin
 
 lemma [code]:

 lemma [code]:
   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
   by simp
 
 qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
-  "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
+  "sub' (as, n) = as !! nat_of_integer n"
 
 lemma [code]:
   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
   by simp
 

   by simp
 
 lemma [code]:
   "IArray.length as = nat_of_integer (IArray.length' as)"
   by simp
+
+qualified definition exists_upto :: "('a \<Rightarrow> bool) \<Rightarrow> integer \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+  [simp]: "exists_upto p k as \<longleftrightarrow> (\<exists>l. 0 \<le> l \<and> l < k \<and> p (sub' (as, l)))"
+
+lemma exists_upto_of_nat:
+  "exists_upto p (of_nat n) as \<longleftrightarrow> (\<exists>m<n. p (as !! m))"
+  including integer.lifting by (simp, transfer)
+    (metis nat_int nat_less_iff of_nat_0_le_iff)
+
+lemma [code]:
+  "exists_upto p k as \<longleftrightarrow> (if k \<le> 0 then False else
+    let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)"
+proof (cases "k \<ge> 1")
+  case False
+  then show ?thesis
+    by (auto simp add: not_le discrete)
+next
+  case True
+  then have less: "k \<le> 0 \<longleftrightarrow> False"
+    by simp
+  define n where "n = nat_of_integer (k - 1)"
+  with True have k: "k - 1 = of_nat n" "k = of_nat (Suc n)"
+    by simp_all
+  show ?thesis unfolding less Let_def k(1) unfolding k(2) exists_upto_of_nat
+    using less_Suc_eq by auto
+qed
+
+lemma [code]:
+  "IArray.exists p as \<longleftrightarrow> exists_upto p (length' as) as"
+  including integer.lifting by (simp, transfer)
+   (auto, metis in_set_conv_nth less_imp_of_nat_less nat_int of_nat_0_le_iff)
 
 end
 
 
 subsection \<open>Code Generation for SML\<close>

 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
 | constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
 | constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
 | constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
 
-end
+
+subsection \<open>Code Generation for Haskell\<close>
+
+text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to @{text Data.Array.IArray.array}
+  in Haskell.  Performance mapping to @{text Data.Array.Unboxed.Array} and
+  @{text Data.Array.Array} is similar.\<close>
+
+code_printing
+  code_module "IArray" \<rightharpoonup> (Haskell) \<open>
+  import Prelude (Bool(True, False), not, Maybe(Nothing, Just),
+    Integer, (+), (-), (<), fromInteger, toInteger, map, seq, (.));
+  import qualified Prelude;
+  import qualified Data.Array.IArray;
+  import qualified Data.Array.Base;
+  import qualified Data.Ix;
+
+  newtype IArray e = IArray (Data.Array.IArray.Array Integer e);
+
+  tabulate :: (Integer, (Integer -> e)) -> IArray e;
+  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]));
+
+  of_list :: [e] -> IArray e;
+  of_list l = IArray (Data.Array.IArray.listArray (0, (toInteger . Prelude.length) l - 1) l);
+
+  sub :: (IArray e, Integer) -> e;
+  sub (IArray v, i) = v `Data.Array.Base.unsafeAt` fromInteger i;
+
+  length :: IArray e -> Integer;
+  length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));\<close>
+
+code_reserved Haskell IArray_Impl
+
+code_printing
+  type_constructor iarray \<rightharpoonup> (Haskell) "IArray.IArray _"
+| constant IArray \<rightharpoonup> (Haskell) "IArray.of'_list"
+| constant IArray.tabulate \<rightharpoonup> (Haskell) "IArray.tabulate"
+| constant IArray.sub' \<rightharpoonup> (Haskell)  "IArray.sub"
+| constant IArray.length' \<rightharpoonup> (Haskell) "IArray.length"
+
+end