Vector.fm

T Vector <A: Type>                                ~ (size: Nat)
| Vector.nil                                      ~ (Nat.zero);
| Vector.ext<size: Nat>(head: A, tail: Vector(A,size)) ~ (Nat.succ(size));

Vector.indl<A: Type, P: Nat -> Type, m: Nat>
(nil  : P(Nat.zero))
(ext   : <size: Nat> -> (a: A) -> (tail: P(size)) -> P(Nat.succ(size)))
(vector : Vector(A, m))
: P(m)
  case vector:
  | nil;
  | def P   = (n) P(Nat.succ(n))
    def nil = ext<Nat.zero>(vector.head, nil)
    def ext  = <x> ext<Nat.succ(x)>
    Vector.indl<A, P, vector.size>(nil, ext, vector.tail);
  : P(vector.size);

Vector.size_0_is_nil(vec: Vector(Nat, Nat.zero)): Equal(_, vec, Vector.nil<Nat>)
  case vec:
  with e : Equal(Nat, vec.size, Nat.zero) = Equal.to<Nat, Nat.zero>;
  | def P0 = ((x) Vector(Nat, Nat.zero)) :: Nat -> Type
    def x0 = Equal.rewrite<_,_,_, P0>(e, Vector.nil<Nat>)
    Equal.to<Vector(Nat, Nat.zero), x0>;
  | Empty.absurd<>(Nat.succ_isnt_zero<vec.size>(e));
  : def P0 = ((x) Vector(Nat, x)) :: Nat -> Type
    def P1 = ((x) Vector(Nat, Nat.zero)) :: Nat -> Type
    let x0 = Equal.rewrite<_, vec.size, Nat.zero, P0>(e, vec.self)
    let x1 = Equal.rewrite<_, vec.size, Nat.zero, P1>(e, Vector.nil<Nat>)
    Equal(_, x0, x1);

Vector.extract<A: Type, n: Nat>(xs: Vector(A, Nat.succ(n))): Pair(A, Vector(A, n))
  case xs:
  | Unit.new;
  | Pair.new<A, Vector(A, xs.size)>(xs.head, xs.tail);
  : Bool.if<Type>(Nat.eql(0, xs.size), Unit, Pair(A, Vector(A, Nat.pred(xs.size))));

Vector.split_at<A: Type, n: Nat>(xs: Vector(A, n)): (m: Nat) -> Pair(Vector(A, Nat.min(n, m)), Vector(A, Nat.sub(n, m)))
  case xs:
  | (m) Pair.new<Vector(A, 0), Vector(A, 0)>(Vector.nil<A>, Vector.nil<A>);
  | (m)
    case m:
    | Pair.new<,>(Vector.nil<A>, Vector.ext<A, xs.size>(xs.head, xs.tail));
    | get x y = Vector.split_at<A, xs.size>(xs.tail, m.pred)
      let x = Vector.ext<A, Nat.min(xs.size, m.pred)>(xs.head, x)
      Pair.new<_,_>(x, y);
    : Pair(Vector(A, Nat.min(Nat.succ(xs.size), m.self)), Vector(A, Nat.sub(Nat.succ(xs.size), m.self)));;
  : (m: Nat) -> Pair(Vector(A, Nat.min(xs.size, m)), Vector(A, Nat.sub(xs.size, m)));

Vector.reverse<A: Type, size: Nat>(xs: Vector(A, size)): Vector(A, size)
  Vector.indl<A, Vector(A), size>(Vector.nil<A>, Vector.ext<A>, xs)

Vector.concat<A: Type, n: Nat, m: Nat>(as: Vector(A, n), bs: Vector(A, m)): Vector(A, Nat.add(n, m))
  case as:
  | bs;
  | Vector.ext<A, Nat.add(as.size, m)>(as.head, Vector.concat<A, as.size, m>(as.tail, bs));
  : Vector(A, Nat.add(as.size, m));

Vector.fill<A: Type>(n: Nat, a: A): Vector(A, n)
  case n:
  | Vector.nil<A>;
  | Vector.ext<A, n.pred>(a, Vector.fill<A>(n.pred, a));
  : Vector(A, n.self);