Theory IArray

section "Immutable Arrays with Code Generation"

theory IArray
imports Main
begin

text‹Immutable arrays are lists wrapped up in an additional constructor.
There are no update operations. Hence code generation can safely implement
this type by efficient target language arrays.  Currently only SML is
provided. Should be extended to other target languages and more operations.

Note that arrays cannot be printed directly but only by turning them into
lists first. Arrays could be converted back into lists for printing if they
were wrapped up in an additional constructor.›

context
begin

datatype 'a iarray = IArray "'a list"

qualified primrec list_of :: "'a iarray ⇒ 'a list" where
"list_of (IArray xs) = xs"

qualified definition of_fun :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a iarray" where
[simp]: "of_fun f n = IArray (map f [0..<n])"

qualified definition sub :: "'a iarray ⇒ nat ⇒ 'a" (infixl "!!" 100) where
[simp]: "as !! n = IArray.list_of as ! n"

qualified definition length :: "'a iarray ⇒ nat" where
[simp]: "length as = List.length (IArray.list_of as)"

qualified fun all :: "('a ⇒ bool) ⇒ 'a iarray ⇒ bool" where
"all p (IArray as) = (ALL a : set as. p a)"

qualified fun exists :: "('a ⇒ bool) ⇒ 'a iarray ⇒ bool" where
"exists p (IArray as) = (EX a : set as. p a)"

lemma list_of_code [code]:
"IArray.list_of as = map (λn. as !! n) [0 ..< IArray.length as]"
by (cases as) (simp add: map_nth)

end


subsection "Code Generation"

code_reserved SML Vector

code_printing
  type_constructor iarray ⇀ (SML) "_ Vector.vector"
| constant IArray ⇀ (SML) "Vector.fromList"
| constant IArray.all ⇀ (SML) "Vector.all"
| constant IArray.exists ⇀ (SML) "Vector.exists"

lemma [code]:
  "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
  by (cases as) simp

lemma [code]:
  "size_iarray f as = Suc (size_list f (IArray.list_of as))"
  by (cases as) simp

lemma [code]:
  "rec_iarray f as = f (IArray.list_of as)"
  by (cases as) simp

lemma [code]:
  "case_iarray f as = f (IArray.list_of as)"
  by (cases as) simp

lemma [code]:
  "set_iarray as = set (IArray.list_of as)"
  by (case_tac as) auto

lemma [code]:
  "map_iarray f as = IArray (map f (IArray.list_of as))"
  by (case_tac as) auto

lemma [code]:
  "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
  by (case_tac as) (case_tac bs, auto)

lemma [code]:
  "HOL.equal as bs ⟷ HOL.equal (IArray.list_of as) (IArray.list_of bs)"
  by (cases as, cases bs) (simp add: equal)

context
begin

qualified primrec tabulate :: "integer × (integer ⇒ 'a) ⇒ 'a iarray" where
  "tabulate (n, f) = IArray (map (f ∘ integer_of_nat) [0..<nat_of_integer n])"

end

lemma [code]:
  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f ∘ nat_of_integer)"
  by simp

code_printing
  constant IArray.tabulate ⇀ (SML) "Vector.tabulate"

context
begin

qualified primrec sub' :: "'a iarray × integer ⇒ 'a" where
  [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"

end

lemma [code]:
  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
  by simp

lemma [code]:
  "as !! n = IArray.sub' (as, integer_of_nat n)"
  by simp

code_printing
  constant IArray.sub' ⇀ (SML) "Vector.sub"

context
begin

qualified definition length' :: "'a iarray ⇒ integer" where
  [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"

end

lemma [code]:
  "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
  by simp

lemma [code]:
  "IArray.length as = nat_of_integer (IArray.length' as)"
  by simp

context term_syntax
begin

lemma [code]:
  "Code_Evaluation.term_of (as :: 'a::typerep iarray) =
    Code_Evaluation.Const (STR ''IArray.iarray.IArray'') (TYPEREP('a list ⇒ 'a iarray)) <⋅> (Code_Evaluation.term_of (IArray.list_of as))"
  by (subst term_of_anything) rule

end

code_printing
  constant IArray.length' ⇀ (SML) "Vector.length"

end