(* 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 imports Main begin
subsection \<open>Fundamental operations\<close>
text\<open>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.\<close>
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..
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 \<open>Generic code equations\<close>
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 includes 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 \<open>Auxiliary operations for code generation\<close>
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
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 thenhave\<open>k \<le> 0\<close>
including integer.lifting by transfer simp thenshow ?thesis by simp next case True thenhave 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 \<open>Code Generation for SML\<close>
text\<open>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.\<close>
subsection \<open>Code Generation for Haskell\<close>
text\<open>We map \<^typ>\<open>'a iarray\<close>s in Isabelle/HOL to \<open>Data.Array.IArray.array\<close> in Haskell. Performance mapping to\<open>Data.Array.Unboxed.Array\<close> and \<open>Data.Array.Array\<close> is similar.\<close>
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;
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
