src/HOL/Library/IArray.thy
author haftmann
Tue Feb 19 19:44:10 2013 +0100 (2013-02-19)
changeset 51188 9b5bf1a9a710
parent 51161 6ed12ae3b3e1
child 52435 6646bb548c6b
permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
     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_type iarray
    44   (SML "_ Vector.vector")
    45 
    46 code_const IArray
    47   (SML "Vector.fromList")
    48 
    49 lemma [code]:
    50 "size (as :: 'a iarray) = 0"
    51 by (cases as) simp
    52 
    53 lemma [code]:
    54 "iarray_size f as = Suc (list_size f (IArray.list_of as))"
    55 by (cases as) simp
    56 
    57 lemma [code]:
    58 "iarray_rec f as = f (IArray.list_of as)"
    59 by (cases as) simp
    60 
    61 lemma [code]:
    62 "iarray_case f as = f (IArray.list_of as)"
    63 by (cases as) simp
    64 
    65 lemma [code]:
    66 "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
    67 by (cases as, cases bs) (simp add: equal)
    68 
    69 primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
    70 "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
    71 hide_const (open) tabulate
    72 
    73 lemma [code]:
    74 "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
    75 by simp 
    76 
    77 code_const IArray.tabulate
    78   (SML "Vector.tabulate")
    79 
    80 primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
    81 "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
    82 hide_const (open) sub'
    83 
    84 lemma [code]:
    85 "as !! n = IArray.sub' (as, integer_of_nat n)"
    86 by simp
    87 
    88 code_const IArray.sub'
    89   (SML "Vector.sub")
    90 
    91 definition length' :: "'a iarray \<Rightarrow> integer" where
    92 [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
    93 hide_const (open) length'
    94 
    95 lemma [code]:
    96 "IArray.length as = nat_of_integer (IArray.length' as)"
    97 by simp
    98 
    99 code_const IArray.length'
   100   (SML "Vector.length")
   101 
   102 end
   103