--- a/src/HOL/Library/IArray.thy Wed Jul 18 20:51:21 2018 +0200
+++ b/src/HOL/Library/IArray.thy Wed Jul 18 20:51:22 2018 +0200
@@ -1,5 +1,7 @@
(* 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>
@@ -32,15 +34,11 @@
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 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 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 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"
@@ -79,10 +77,18 @@
"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
@@ -107,7 +113,7 @@
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"
@@ -128,6 +134,37 @@
"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
@@ -148,4 +185,43 @@
| constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
| constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
+
+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