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