nipkow@50138: header "Immutable Arrays with Code Generation"
nipkow@50138: 
nipkow@50138: theory IArray
haftmann@51094: imports Main
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: 
haftmann@51094: primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
nipkow@50138: "list_of (IArray xs) = xs"
nipkow@50138: hide_const (open) list_of
nipkow@50138: 
haftmann@51094: definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
haftmann@51094: [simp]: "of_fun f n = IArray (map f [0..<n])"
haftmann@51094: hide_const (open) of_fun
haftmann@51094: 
haftmann@51094: definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
haftmann@51094: [simp]: "as !! n = IArray.list_of as ! n"
haftmann@51094: hide_const (open) sub
haftmann@51094: 
haftmann@51094: definition length :: "'a iarray \<Rightarrow> nat" where
haftmann@51094: [simp]: "length as = List.length (IArray.list_of as)"
haftmann@51094: hide_const (open) length
haftmann@51094: 
haftmann@51094: lemma list_of_code [code]:
haftmann@51094: "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
haftmann@51094: by (cases as) (simp add: map_nth)
haftmann@51094: 
nipkow@50138: 
nipkow@50138: subsection "Code Generation"
nipkow@50138: 
haftmann@51094: code_reserved SML Vector
haftmann@51094: 
nipkow@50138: code_type iarray
nipkow@50138:   (SML "_ Vector.vector")
nipkow@50138: 
nipkow@50138: code_const IArray
nipkow@50138:   (SML "Vector.fromList")
haftmann@51094: 
haftmann@51161: lemma [code]:
haftmann@51161: "size (as :: 'a iarray) = 0"
haftmann@51161: by (cases as) simp
haftmann@51161: 
haftmann@51161: lemma [code]:
haftmann@51161: "iarray_size f as = Suc (list_size f (IArray.list_of as))"
haftmann@51161: by (cases as) simp
haftmann@51161: 
haftmann@51161: lemma [code]:
haftmann@51161: "iarray_rec f as = f (IArray.list_of as)"
haftmann@51161: by (cases as) simp
haftmann@51161: 
haftmann@51161: lemma [code]:
haftmann@51161: "iarray_case f as = f (IArray.list_of as)"
haftmann@51161: by (cases as) simp
haftmann@51161: 
haftmann@51161: lemma [code]:
haftmann@51161: "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
haftmann@51161: by (cases as, cases bs) (simp add: equal)
haftmann@51161: 
haftmann@51143: primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
haftmann@51143: "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
haftmann@51094: hide_const (open) tabulate
haftmann@51094: 
haftmann@51094: lemma [code]:
haftmann@51143: "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
haftmann@51094: by simp 
haftmann@51094: 
haftmann@51094: code_const IArray.tabulate
haftmann@51094:   (SML "Vector.tabulate")
haftmann@51094: 
haftmann@51143: primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
haftmann@51143: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
haftmann@51094: hide_const (open) sub'
haftmann@51094: 
haftmann@51094: lemma [code]:
haftmann@51143: "as !! n = IArray.sub' (as, integer_of_nat n)"
haftmann@51094: by simp
haftmann@51094: 
haftmann@51094: code_const IArray.sub'
haftmann@51094:   (SML "Vector.sub")
haftmann@51094: 
haftmann@51143: definition length' :: "'a iarray \<Rightarrow> integer" where
haftmann@51143: [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
haftmann@51094: hide_const (open) length'
haftmann@51094: 
haftmann@51094: lemma [code]:
haftmann@51143: "IArray.length as = nat_of_integer (IArray.length' as)"
haftmann@51094: by simp
haftmann@51094: 
haftmann@51094: code_const IArray.length'
nipkow@50138:   (SML "Vector.length")
nipkow@50138: 
nipkow@50138: end
haftmann@51094: