src/HOL/Library/IArray.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 52435 6646bb548c6b
child 54459 f43ae1afd08a
permissions -rw-r--r--
more simplification rules on unary and binary minus
     1 header "Immutable Arrays with Code Generation"
     2 
     3 theory IArray
     4 imports Main
     5 begin
     6 
     7 text{* 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. *}
    15 
    16 datatype 'a iarray = IArray "'a list"
    17 
    18 primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
    19 "list_of (IArray xs) = xs"
    20 hide_const (open) list_of
    21 
    22 definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
    23 [simp]: "of_fun f n = IArray (map f [0..<n])"
    24 hide_const (open) of_fun
    25 
    26 definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
    27 [simp]: "as !! n = IArray.list_of as ! n"
    28 hide_const (open) sub
    29 
    30 definition length :: "'a iarray \<Rightarrow> nat" where
    31 [simp]: "length as = List.length (IArray.list_of as)"
    32 hide_const (open) length
    33 
    34 lemma list_of_code [code]:
    35 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
    36 by (cases as) (simp add: map_nth)
    37 
    38 
    39 subsection "Code Generation"
    40 
    41 code_reserved SML Vector
    42 
    43 code_printing
    44   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
    45 | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
    46 
    47 lemma [code]:
    48 "size (as :: 'a iarray) = 0"
    49 by (cases as) simp
    50 
    51 lemma [code]:
    52 "iarray_size f as = Suc (list_size f (IArray.list_of as))"
    53 by (cases as) simp
    54 
    55 lemma [code]:
    56 "iarray_rec f as = f (IArray.list_of as)"
    57 by (cases as) simp
    58 
    59 lemma [code]:
    60 "iarray_case f as = f (IArray.list_of as)"
    61 by (cases as) simp
    62 
    63 lemma [code]:
    64 "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    65 by (cases as, cases bs) (simp add: equal)
    66 
    67 primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
    68 "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
    69 hide_const (open) tabulate
    70 
    71 lemma [code]:
    72 "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
    73 by simp 
    74 
    75 code_printing
    76   constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
    77 
    78 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
    79 "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
    80 hide_const (open) sub'
    81 
    82 lemma [code]:
    83 "as !! n = IArray.sub' (as, integer_of_nat n)"
    84 by simp
    85 
    86 code_printing
    87   constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
    88 
    89 definition length' :: "'a iarray \<Rightarrow> integer" where
    90 [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
    91 hide_const (open) length'
    92 
    93 lemma [code]:
    94 "IArray.length as = nat_of_integer (IArray.length' as)"
    95 by simp
    96 
    97 code_printing
    98   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
    99 
   100 end
   101