(* 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 ‹Immutable Arrays with Code Generation› theory IArray imports Main begin subsection ‹Fundamental operations› text ‹Immutable arrays are lists wrapped up in an additional constructor. There are no update operations. Hence code generation can safely implement this type by efficient target language arrays. Currently only SML is provided. Could be extended to other target languages and more operations.› context begin datatype 'a iarray = IArray "'a list" qualified primrec list_of :: "'a iarray ⇒ 'a list" where "list_of (IArray xs) = xs" qualified definition of_fun :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a iarray" where [simp]: "of_fun f n = IArray (map f [0..<n])" qualified definition sub :: "'a iarray ⇒ nat ⇒ 'a" (infixl "!!" 100) where [simp]: "as !! n = IArray.list_of as ! n" qualified definition length :: "'a iarray ⇒ nat" where [simp]: "length as = List.length (IArray.list_of as)" qualified definition all :: "('a ⇒ bool) ⇒ 'a iarray ⇒ bool" where [simp]: "all p as ⟷ (∀a ∈ set (list_of as). p a)" qualified definition exists :: "('a ⇒ bool) ⇒ 'a iarray ⇒ bool" where [simp]: "exists p as ⟷ (∃a ∈ 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) end subsection ‹Generic code equations› lemma [code]: "size (as :: 'a iarray) = Suc (IArray.length as)" by (cases as) simp lemma [code]: "size_iarray f as = Suc (size_list f (IArray.list_of as))" by (cases as) simp lemma [code]: "rec_iarray f as = f (IArray.list_of as)" by (cases as) simp lemma [code]: "case_iarray f as = f (IArray.list_of as)" by (cases as) simp lemma [code]: "set_iarray as = set (IArray.list_of as)" by (cases as) auto lemma [code]: "map_iarray f as = IArray (map f (IArray.list_of as))" by (cases as) auto 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 (λn. as !! n) [0 ..< IArray.length as]" by (cases as) (simp add: map_nth) lemma [code]: "HOL.equal as bs ⟷ HOL.equal (IArray.list_of as) (IArray.list_of bs)" by (cases as, cases bs) (simp add: equal) lemma [code]: "IArray.all p = Not ∘ IArray.exists (Not ∘ p)" by (simp add: fun_eq_iff) context term_syntax begin lemma [code]: "Code_Evaluation.term_of (as :: 'a::typerep iarray) = Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list ⇒ 'a iarray)) <⋅> (Code_Evaluation.term_of (IArray.list_of as))" by (subst term_of_anything) rule end subsection ‹Auxiliary operations for code generation› context begin qualified primrec tabulate :: "integer × (integer ⇒ 'a) ⇒ 'a iarray" where "tabulate (n, f) = IArray (map (f ∘ integer_of_nat) [0..<nat_of_integer n])" lemma [code]: "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f ∘ nat_of_integer)" by simp qualified primrec sub' :: "'a iarray × integer ⇒ 'a" where "sub' (as, n) = as !! nat_of_integer n" lemma [code]: "IArray.sub' (IArray as, n) = as ! nat_of_integer n" by simp lemma [code]: "as !! n = IArray.sub' (as, integer_of_nat n)" by simp qualified definition length' :: "'a iarray ⇒ integer" where [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))" lemma [code]: "IArray.length' (IArray as) = integer_of_nat (List.length as)" by simp lemma [code]: "IArray.length as = nat_of_integer (IArray.length' as)" by simp qualified definition exists_upto :: "('a ⇒ bool) ⇒ integer ⇒ 'a iarray ⇒ bool" where [simp]: "exists_upto p k as ⟷ (∃l. 0 ≤ l ∧ l < k ∧ p (sub' (as, l)))" lemma exists_upto_of_nat: "exists_upto p (of_nat n) as ⟷ (∃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 ⟷ (if k ≤ 0 then False else let l = k - 1 in p (sub' (as, l)) ∨ exists_upto p l as)" proof (cases "k ≥ 1") case False then show ?thesis by (auto simp add: not_le discrete) next case True then have less: "k ≤ 0 ⟷ 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 ⟷ 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 ‹Code Generation for SML› text ‹Note that arrays cannot be printed directly but only by turning them into lists first. Arrays could be converted back into lists for printing if they were wrapped up in an additional constructor.› code_reserved SML Vector code_printing type_constructor iarray ⇀ (SML) "_ Vector.vector" | constant IArray ⇀ (SML) "Vector.fromList" | constant IArray.all ⇀ (SML) "Vector.all" | constant IArray.exists ⇀ (SML) "Vector.exists" | constant IArray.tabulate ⇀ (SML) "Vector.tabulate" | constant IArray.sub' ⇀ (SML) "Vector.sub" | constant IArray.length' ⇀ (SML) "Vector.length" subsection ‹Code Generation for Haskell› text ‹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.› code_printing code_module "IArray" ⇀ (Haskell) ‹ 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));› code_reserved Haskell IArray_Impl code_printing type_constructor iarray ⇀ (Haskell) "IArray.IArray _" | constant IArray ⇀ (Haskell) "IArray.of'_list" | constant IArray.tabulate ⇀ (Haskell) "IArray.tabulate" | constant IArray.sub' ⇀ (Haskell) "IArray.sub" | constant IArray.length' ⇀ (Haskell) "IArray.length" end