src/HOL/Library/IArray.thy
changeset 50138 ca989d793b34
child 51094 84b03c49c223
equal deleted inserted replaced
50137:0226d408058b 50138:ca989d793b34
       
     1 header "Immutable Arrays with Code Generation"
       
     2 
       
     3 theory IArray
       
     4 imports "~~/src/HOL/Library/Efficient_Nat"
       
     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 fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
       
    19 "of_fun f n = IArray (map f [0..<n])"
       
    20 hide_const (open) of_fun
       
    21 
       
    22 fun length :: "'a iarray \<Rightarrow> nat" where
       
    23 "length (IArray xs) = List.length xs"
       
    24 hide_const (open) length
       
    25 
       
    26 fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
       
    27 "(IArray as) !! n = as!n"
       
    28 hide_const (open) sub
       
    29 
       
    30 fun list_of :: "'a iarray \<Rightarrow> 'a list" where
       
    31 "list_of (IArray xs) = xs"
       
    32 hide_const (open) list_of
       
    33 
       
    34 
       
    35 subsection "Code Generation"
       
    36 
       
    37 code_type iarray
       
    38   (SML "_ Vector.vector")
       
    39 
       
    40 code_const IArray
       
    41   (SML "Vector.fromList")
       
    42 code_const IArray.sub
       
    43   (SML "Vector.sub(_,_)")
       
    44 code_const IArray.length
       
    45   (SML "Vector.length")
       
    46 code_const IArray.of_fun
       
    47   (SML "!(fn f => fn n => Vector.tabulate(n,f))")
       
    48 
       
    49 lemma list_of_code[code]:
       
    50   "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
       
    51 by (cases A) (simp add: map_nth)
       
    52 
       
    53 end