setup for Haskell taken over from AFP / Gauss_Jordan
authorhaftmann
Wed Jul 18 20:51:22 2018 +0200 (9 months ago)
changeset 68659db0c70767d86
parent 68658 16cc1161ad7f
child 68660 4ce18f389f53
setup for Haskell taken over from AFP / Gauss_Jordan
src/HOL/Library/IArray.thy
     1.1 --- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:21 2018 +0200
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:22 2018 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (*  Title:      HOL/Library/IArray.thy
     1.5      Author:     Tobias Nipkow, TU Muenchen
     1.6 +    Author:     Jose Divasón <jose.divasonm at unirioja.es>
     1.7 +    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
     1.8  *)
     1.9  
    1.10  section \<open>Immutable Arrays with Code Generation\<close>
    1.11 @@ -32,15 +34,11 @@
    1.12  qualified definition length :: "'a iarray \<Rightarrow> nat" where
    1.13  [simp]: "length as = List.length (IArray.list_of as)"
    1.14  
    1.15 -qualified primrec all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.16 -"all p (IArray as) \<longleftrightarrow> (\<forall>a \<in> set as. p a)"
    1.17 +qualified definition all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.18 +[simp]: "all p as \<longleftrightarrow> (\<forall>a \<in> set (list_of as). p a)"
    1.19  
    1.20 -qualified primrec exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.21 -"exists p (IArray as) \<longleftrightarrow> (\<exists>a \<in> set as. p a)"
    1.22 -
    1.23 -lemma list_of_code [code]:
    1.24 -"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    1.25 -by (cases as) (simp add: map_nth)
    1.26 +qualified definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.27 +[simp]: "exists p as \<longleftrightarrow> (\<exists>a \<in> set (list_of as). p a)"
    1.28  
    1.29  lemma of_fun_nth:
    1.30  "IArray.of_fun f n !! i = f i" if "i < n"
    1.31 @@ -79,10 +77,18 @@
    1.32    "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
    1.33    by (cases as, cases bs) auto
    1.34  
    1.35 +lemma list_of_code [code]:
    1.36 +  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    1.37 +  by (cases as) (simp add: map_nth)
    1.38 +
    1.39  lemma [code]:
    1.40    "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    1.41    by (cases as, cases bs) (simp add: equal)
    1.42  
    1.43 +lemma [code]:
    1.44 +  "IArray.all p = Not \<circ> IArray.exists (Not \<circ> p)"
    1.45 +  by (simp add: fun_eq_iff)
    1.46 +
    1.47  context term_syntax
    1.48  begin
    1.49  
    1.50 @@ -107,7 +113,7 @@
    1.51    by simp
    1.52  
    1.53  qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
    1.54 -  "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
    1.55 +  "sub' (as, n) = as !! nat_of_integer n"
    1.56  
    1.57  lemma [code]:
    1.58    "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
    1.59 @@ -128,6 +134,37 @@
    1.60    "IArray.length as = nat_of_integer (IArray.length' as)"
    1.61    by simp
    1.62  
    1.63 +qualified definition exists_upto :: "('a \<Rightarrow> bool) \<Rightarrow> integer \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.64 +  [simp]: "exists_upto p k as \<longleftrightarrow> (\<exists>l. 0 \<le> l \<and> l < k \<and> p (sub' (as, l)))"
    1.65 +
    1.66 +lemma exists_upto_of_nat:
    1.67 +  "exists_upto p (of_nat n) as \<longleftrightarrow> (\<exists>m<n. p (as !! m))"
    1.68 +  including integer.lifting by (simp, transfer)
    1.69 +    (metis nat_int nat_less_iff of_nat_0_le_iff)
    1.70 +
    1.71 +lemma [code]:
    1.72 +  "exists_upto p k as \<longleftrightarrow> (if k \<le> 0 then False else
    1.73 +    let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)"
    1.74 +proof (cases "k \<ge> 1")
    1.75 +  case False
    1.76 +  then show ?thesis
    1.77 +    by (auto simp add: not_le discrete)
    1.78 +next
    1.79 +  case True
    1.80 +  then have less: "k \<le> 0 \<longleftrightarrow> False"
    1.81 +    by simp
    1.82 +  define n where "n = nat_of_integer (k - 1)"
    1.83 +  with True have k: "k - 1 = of_nat n" "k = of_nat (Suc n)"
    1.84 +    by simp_all
    1.85 +  show ?thesis unfolding less Let_def k(1) unfolding k(2) exists_upto_of_nat
    1.86 +    using less_Suc_eq by auto
    1.87 +qed
    1.88 +
    1.89 +lemma [code]:
    1.90 +  "IArray.exists p as \<longleftrightarrow> exists_upto p (length' as) as"
    1.91 +  including integer.lifting by (simp, transfer)
    1.92 +   (auto, metis in_set_conv_nth less_imp_of_nat_less nat_int of_nat_0_le_iff)
    1.93 +
    1.94  end
    1.95  
    1.96  
    1.97 @@ -148,4 +185,43 @@
    1.98  | constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
    1.99  | constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   1.100  
   1.101 +
   1.102 +subsection \<open>Code Generation for Haskell\<close>
   1.103 +
   1.104 +text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to @{text Data.Array.IArray.array}
   1.105 +  in Haskell.  Performance mapping to @{text Data.Array.Unboxed.Array} and
   1.106 +  @{text Data.Array.Array} is similar.\<close>
   1.107 +
   1.108 +code_printing
   1.109 +  code_module "IArray" \<rightharpoonup> (Haskell) \<open>
   1.110 +  import Prelude (Bool(True, False), not, Maybe(Nothing, Just),
   1.111 +    Integer, (+), (-), (<), fromInteger, toInteger, map, seq, (.));
   1.112 +  import qualified Prelude;
   1.113 +  import qualified Data.Array.IArray;
   1.114 +  import qualified Data.Array.Base;
   1.115 +  import qualified Data.Ix;
   1.116 +
   1.117 +  newtype IArray e = IArray (Data.Array.IArray.Array Integer e);
   1.118 +
   1.119 +  tabulate :: (Integer, (Integer -> e)) -> IArray e;
   1.120 +  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]));
   1.121 +
   1.122 +  of_list :: [e] -> IArray e;
   1.123 +  of_list l = IArray (Data.Array.IArray.listArray (0, (toInteger . Prelude.length) l - 1) l);
   1.124 +
   1.125 +  sub :: (IArray e, Integer) -> e;
   1.126 +  sub (IArray v, i) = v `Data.Array.Base.unsafeAt` fromInteger i;
   1.127 +
   1.128 +  length :: IArray e -> Integer;
   1.129 +  length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));\<close>
   1.130 +
   1.131 +code_reserved Haskell IArray_Impl
   1.132 +
   1.133 +code_printing
   1.134 +  type_constructor iarray \<rightharpoonup> (Haskell) "IArray.IArray _"
   1.135 +| constant IArray \<rightharpoonup> (Haskell) "IArray.of'_list"
   1.136 +| constant IArray.tabulate \<rightharpoonup> (Haskell) "IArray.tabulate"
   1.137 +| constant IArray.sub' \<rightharpoonup> (Haskell)  "IArray.sub"
   1.138 +| constant IArray.length' \<rightharpoonup> (Haskell) "IArray.length"
   1.139 +
   1.140  end