nipkow@50138: header "Immutable Arrays with Code Generation"
nipkow@50138: 
nipkow@50138: theory IArray
nipkow@50138: imports "~~/src/HOL/Library/Efficient_Nat"
nipkow@50138: begin
nipkow@50138: 
nipkow@50138: text{* Immutable arrays are lists wrapped up in an additional constructor.
nipkow@50138: There are no update operations. Hence code generation can safely implement
nipkow@50138: this type by efficient target language arrays.  Currently only SML is
nipkow@50138: provided. Should be extended to other target languages and more operations.
nipkow@50138: 
nipkow@50138: Note that arrays cannot be printed directly but only by turning them into
nipkow@50138: lists first. Arrays could be converted back into lists for printing if they
nipkow@50138: were wrapped up in an additional constructor. *}
nipkow@50138: 
nipkow@50138: datatype 'a iarray = IArray "'a list"
nipkow@50138: 
nipkow@50138: fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
nipkow@50138: "of_fun f n = IArray (map f [0..<n])"
nipkow@50138: hide_const (open) of_fun
nipkow@50138: 
nipkow@50138: fun length :: "'a iarray \<Rightarrow> nat" where
nipkow@50138: "length (IArray xs) = List.length xs"
nipkow@50138: hide_const (open) length
nipkow@50138: 
nipkow@50138: fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
nipkow@50138: "(IArray as) !! n = as!n"
nipkow@50138: hide_const (open) sub
nipkow@50138: 
nipkow@50138: fun list_of :: "'a iarray \<Rightarrow> 'a list" where
nipkow@50138: "list_of (IArray xs) = xs"
nipkow@50138: hide_const (open) list_of
nipkow@50138: 
nipkow@50138: 
nipkow@50138: subsection "Code Generation"
nipkow@50138: 
nipkow@50138: code_type iarray
nipkow@50138:   (SML "_ Vector.vector")
nipkow@50138: 
nipkow@50138: code_const IArray
nipkow@50138:   (SML "Vector.fromList")
nipkow@50138: code_const IArray.sub
nipkow@50138:   (SML "Vector.sub(_,_)")
nipkow@50138: code_const IArray.length
nipkow@50138:   (SML "Vector.length")
nipkow@50138: code_const IArray.of_fun
nipkow@50138:   (SML "!(fn f => fn n => Vector.tabulate(n,f))")
nipkow@50138: 
nipkow@50138: lemma list_of_code[code]:
nipkow@50138:   "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
nipkow@50138: by (cases A) (simp add: map_nth)
nipkow@50138: 
nipkow@50138: end