Theory IArray_Syntax

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

header {* Syntax for operations on immutable arrays *}

theory IArray_Syntax
imports Main "~~/src/HOL/Library/IArray"
begin

subsection {* Tabulation *}

definition tabulate :: "nat => (nat => 'a) => 'a iarray"
where
  "tabulate n f = IArray.of_fun f n"

definition tabulate2 :: "nat => nat => (nat => nat => 'a) => 'a iarray iarray"
where
  "tabulate2 m n f = IArray.of_fun (λi .IArray.of_fun (f i) n) m "

definition tabulate3 :: "nat => nat => nat => 
  (nat => nat => nat => 'a) => 'a iarray iarray iarray" where
  "tabulate3 l m n f ≡ IArray.of_fun (λi. IArray.of_fun (λj. IArray.of_fun (λk. f i j k) n) m) l"

syntax 
 "_tabulate" :: "'a => pttrn => nat => 'a iarray"  ("([|_. _ < _|])") 
 "_tabulate2" :: "'a => pttrn => nat => pttrn => nat => 'a iarray"
   ("([|_. _ < _, _ < _|])")
 "_tabulate3" :: "'a => pttrn => nat => pttrn => nat => pttrn => nat => 'a iarray"
   ("([|_. _ < _, _ < _, _ < _ |])")

translations 
  "[|f. x < n|]" == "CONST tabulate n (λx. f)"
  "[|f. x < m, y < n|]" == "CONST tabulate2 m n (λx y. f)"
  "[|f. x < l, y < m, z < n|]" == "CONST tabulate3 l m n (λx y z. f)"


subsection {* Access *}

abbreviation sub1_syntax :: "'a iarray => nat => 'a"  ("(_[|_|])" [1000] 999)
where
  "a[|n|] ≡ IArray.sub a n"

abbreviation sub2_syntax :: "'a iarray iarray => nat => nat => 'a"  ("(_[|_,_|])" [1000] 999)
where
  "as[|m, n|] ≡ IArray.sub (IArray.sub as m) n"

abbreviation sub3_syntax :: "'a iarray iarray iarray => nat => nat => nat => 'a"  ("(_[|_,_,_|])" [1000] 999)
where
  "as[|l, m, n|] ≡ IArray.sub (IArray.sub (IArray.sub as l) m) n"

text {* examples:  @{term "[|0. i < 5|]"}, @{term "[|i. i < 5, j < 3|]"}  *}

end