src/HOL/Library/IArray.thy
author haftmann
Wed Jul 18 20:51:20 2018 +0200 (9 months ago)
changeset 68657 65ad2bfc19d2
parent 68656 297ca38c7da5
child 68658 16cc1161ad7f
permissions -rw-r--r--
restructured for future incorporation of Haskell
     1 (*  Title:      HOL/Library/IArray.thy
     2     Author:     Tobias Nipkow, TU Muenchen
     3 *)
     4 
     5 section \<open>Immutable Arrays with Code Generation\<close>
     6 
     7 theory IArray
     8 imports Main
     9 begin
    10 
    11 subsection \<open>Fundamental operations\<close>
    12 
    13 text \<open>Immutable arrays are lists wrapped up in an additional constructor.
    14 There are no update operations. Hence code generation can safely implement
    15 this type by efficient target language arrays.  Currently only SML is
    16 provided. Could be extended to other target languages and more operations.\<close>
    17 
    18 context
    19 begin
    20 
    21 datatype 'a iarray = IArray "'a list"
    22 
    23 qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
    24 "list_of (IArray xs) = xs"
    25 
    26 qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    27 [simp]: "of_fun f n = IArray (map f [0..<n])"
    28 
    29 qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    30 [simp]: "as !! n = IArray.list_of as ! n"
    31 
    32 qualified definition length :: "'a iarray \<Rightarrow> nat" where
    33 [simp]: "length as = List.length (IArray.list_of as)"
    34 
    35 qualified primrec all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    36 "all p (IArray as) \<longleftrightarrow> (\<forall>a \<in> set as. p a)"
    37 
    38 qualified primrec exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    39 "exists p (IArray as) \<longleftrightarrow> (\<exists>a \<in> set as. p a)"
    40 
    41 lemma list_of_code [code]:
    42 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    43 by (cases as) (simp add: map_nth)
    44 
    45 lemma of_fun_nth:
    46 "IArray.of_fun f n !! i = f i" if "i < n"
    47 using that by (simp add: map_nth)
    48 
    49 end
    50 
    51 
    52 subsection \<open>Generic code equations\<close>
    53 
    54 lemma [code]:
    55   "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
    56   by (cases as) simp
    57 
    58 lemma [code]:
    59   "size_iarray f as = Suc (size_list f (IArray.list_of as))"
    60   by (cases as) simp
    61 
    62 lemma [code]:
    63   "rec_iarray f as = f (IArray.list_of as)"
    64   by (cases as) simp
    65 
    66 lemma [code]:
    67   "case_iarray f as = f (IArray.list_of as)"
    68   by (cases as) simp
    69 
    70 lemma [code]:
    71   "set_iarray as = set (IArray.list_of as)"
    72   by (cases as) auto
    73 
    74 lemma [code]:
    75   "map_iarray f as = IArray (map f (IArray.list_of as))"
    76   by (cases as) auto
    77 
    78 lemma [code]:
    79   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
    80   by (cases as, cases bs) auto
    81 
    82 lemma [code]:
    83   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    84   by (cases as, cases bs) (simp add: equal)
    85 
    86 context term_syntax
    87 begin
    88 
    89 lemma [code]:
    90   "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
    91     Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list \<Rightarrow> 'a iarray)) <\<cdot>> (Code_Evaluation.term_of (IArray.list_of as))"
    92   by (subst term_of_anything) rule
    93 
    94 end
    95 
    96 
    97 subsection \<open>Auxiliary operations for code generation\<close>
    98 
    99 context
   100 begin
   101 
   102 qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
   103   "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
   104 
   105 lemma [code]:
   106   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
   107   by simp
   108 
   109 qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   110   "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
   111 
   112 lemma [code]:
   113   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
   114   by simp
   115 
   116 lemma [code]:
   117   "as !! n = IArray.sub' (as, integer_of_nat n)"
   118   by simp
   119 
   120 qualified definition length' :: "'a iarray \<Rightarrow> integer" where
   121   [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
   122 
   123 lemma [code]:
   124   "IArray.length' (IArray as) = integer_of_nat (List.length as)"
   125   by simp
   126 
   127 lemma [code]:
   128   "IArray.length as = nat_of_integer (IArray.length' as)"
   129   by simp
   130 
   131 end
   132 
   133 
   134 subsection \<open>Code Generation for SML\<close>
   135 
   136 text \<open>Note that arrays cannot be printed directly but only by turning them into
   137 lists first. Arrays could be converted back into lists for printing if they
   138 were wrapped up in an additional constructor.\<close>
   139 
   140 code_reserved SML Vector
   141 
   142 code_printing
   143   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
   144 | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
   145 | constant IArray.all \<rightharpoonup> (SML) "Vector.all"
   146 | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
   147 | constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
   148 | constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
   149 | constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   150 
   151 end