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: 
blanchet@58249: datatype_new '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: 
nipkow@54459: fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
nipkow@54459: "all p (IArray as) = (ALL a : set as. p a)"
nipkow@54459: hide_const (open) all
nipkow@54459: 
nipkow@54459: fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
nipkow@54459: "exists p (IArray as) = (EX a : set as. p a)"
nipkow@54459: hide_const (open) exists
nipkow@54459: 
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: 
haftmann@52435: code_printing
haftmann@52435:   type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
haftmann@52435: | constant IArray \<rightharpoonup> (SML) "Vector.fromList"
nipkow@54459: | constant IArray.all \<rightharpoonup> (SML) "Vector.all"
nipkow@54459: | constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
haftmann@51094: 
haftmann@51161: lemma [code]:
blanchet@58269:   "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
blanchet@58269:   by (cases as) simp
haftmann@51161: 
haftmann@51161: lemma [code]:
blanchet@58269:   "size_iarray f as = Suc (size_list f (IArray.list_of as))"
blanchet@58269:   by (cases as) simp
blanchet@58269: 
blanchet@58269: lemma [code]:
blanchet@58269:   "rec_iarray f as = f (IArray.list_of as)"
blanchet@58269:   by (cases as) simp
blanchet@58269: 
blanchet@58269: lemma [code]:
blanchet@58269:   "case_iarray f as = f (IArray.list_of as)"
blanchet@58269:   by (cases as) simp
haftmann@51161: 
haftmann@51161: lemma [code]:
blanchet@58269:   "set_iarray as = set (IArray.list_of as)"
blanchet@58269:   by (case_tac as) auto
blanchet@58269: 
blanchet@58269: lemma [code]:
blanchet@58269:   "map_iarray f as = IArray (map f (IArray.list_of as))"
blanchet@58269:   by (case_tac as) auto
haftmann@51161: 
haftmann@51161: lemma [code]:
blanchet@58269:   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
blanchet@58269:   by (case_tac as) (case_tac bs, auto)
haftmann@51161: 
haftmann@51161: lemma [code]:
blanchet@58269:   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
blanchet@58269:   by (cases as, cases bs) (simp add: equal)
haftmann@51161: 
haftmann@51143: primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
blanchet@58269:   "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
blanchet@58269: 
haftmann@51094: hide_const (open) tabulate
haftmann@51094: 
haftmann@51094: lemma [code]:
blanchet@58269:   "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
blanchet@58269:   by simp
haftmann@51094: 
haftmann@52435: code_printing
haftmann@52435:   constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
haftmann@51094: 
haftmann@51143: primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
blanchet@58269:   [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
blanchet@58269: 
haftmann@51094: hide_const (open) sub'
haftmann@51094: 
haftmann@51094: lemma [code]:
haftmann@57117:   "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
haftmann@57117:   by simp
haftmann@57117: 
haftmann@57117: lemma [code]:
blanchet@58269:   "as !! n = IArray.sub' (as, integer_of_nat n)"
blanchet@58269:   by simp
haftmann@51094: 
haftmann@52435: code_printing
haftmann@52435:   constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
haftmann@51094: 
haftmann@51143: definition length' :: "'a iarray \<Rightarrow> integer" where
blanchet@58269:   [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
blanchet@58269: 
haftmann@51094: hide_const (open) length'
haftmann@51094: 
haftmann@51094: lemma [code]:
haftmann@57117:   "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
haftmann@57117:   by simp
haftmann@57117: 
haftmann@57117: lemma [code]:
blanchet@58269:   "IArray.length as = nat_of_integer (IArray.length' as)"
blanchet@58269:   by simp
haftmann@51094: 
haftmann@52435: code_printing
haftmann@52435:   constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
nipkow@50138: 
nipkow@50138: end