(*[ datacon Nil : list(0)
    datacon Cons : -all u:nat- int * list(u) -> list(u + 1)
    datatype list with nat   ]*)
datatype list =  Nil | Cons of int * list

(*[ datasort array_op : length_op < array_op; read_op < array_op; write_op < array_op
    datacon Length : length_op
    datacon Read : read_op
    datacon Write : write_op  ]*)
datatype array_op = Length | Read | Write

(*[ datacon Array : -all n:nat- int(n) * list(n) -> array(n)
    datatype array with int  ]*)
datatype array = Array of int * list  ;

(*[ val append : -all a,b:nat- list(a) * list(b) -> list(a + b)  ]*)
fun append (xs, ys) =
  case xs of
    Nil => ys
  | Cons(x, xs') => Cons(x, append(xs', ys))

(*[ val nth : -all len:nat- list(len) -> -all n:nat- {n < len} int(n) -> int  ]*)
fun nth list n =
  case list of
    Cons(h, t) => if n=0 then h else nth t (n-1)

(*[ val replace : -all len:nat-
      list(len) -> -all n:nat- {n < len} int(n) -> int -> list(len)  ]*)
fun replace list n x =
  case list of
    Cons(h, t) => if n=0 then Cons(x, t)
                  else Cons(h, replace t (n-1) x)

(*[ val dispatch : -all len:nat-
    array(len)
 -> ((length_op -> int(len))
   & (read_op -> -all n:nat- {n < len} int(n) -> int)
   & (write_op -> -all n:nat- {n < len} int(n) -> int -> array(len)))
]*)
fun dispatch array selector =
  case array of Array(length, list) =>
    case selector of
      Length => length
    | Read => nth list
    | Write => (fn n => fn x => Array(length, replace list n x))