src/HOL/Library/IArray.thy
author Christian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516 ed6b40d15d1c
parent 50138 ca989d793b34
child 51094 84b03c49c223
permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
     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