Theory IArray_Syntax

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section ‹Syntax for operations on immutable arrays›

theory IArray_Syntax
imports Main "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"
   (‹(⟦_. _ < _, _ < _, _ < _ ⟧)›)

syntax_consts
  "_tabulate" == tabulate and
  "_tabulate2" == tabulate2 and
  "_tabulate3" == tabulate3

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