/*
union <'a> list with nat {
 Nil(0);
 {n:nat} Cons(n+1) of 'a * <'a> list(n)
}
*/

('a){n:nat} int(n) length (xs: <'a> list(n)) {
  var: int x;;
  x = 0;
  invariant:
  [i:nat,j:nat | i+j=n] (xs: <'a> list(i), x: int(j))
  while (true) {
    switch(xs) {
      case Nil: return x;
      case Cons(_, xs): x = x + 1;
    }
  }
  exit;
}

('a){m:nat,n:nat}
<'a> list(m+n) append (xs: <'a> list(m), ys: <'a> list(n)) {
   var: 'a x;;
 
   switch (xs) {
     case Nil: return ys;
     case Cons(x, xs): return Cons(x, append(xs, ys));
   }
}


('a){m:nat,n:nat}
<'a> list(m+n) rev_append (xs: <'a> list(m), ys: <'a> list(n)) {
   var: 'a x;;
  
   invariant:
     [m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1))
   while (true) {
     switch (xs) {
       case Nil: return ys;
       case Cons(x, xs): ys = Cons(x, ys);
     }
   }
   exit;
}

('a){n:nat}
<'a> list(n) reverse (xs: <'a> list(n)) {
   return rev_append(xs, Nil);
}

('a,'b){n:nat}
<'b> list(n) map (f: 'a -> 'b, xs: <'a> list(n)) {
  var: 'a x;;

  switch (xs) {
    case Nil: return Nil;
    case Cons(x, xs): return Cons(f(x), map(f, xs));
  }
}

('a,'b){n:nat}
<'a> list(n) * <'b> list(n) split (xs: <'a *'b> list(n)) {
  var: 'a y; 'b z; <'a> list ys; <'b> list zs;;

  switch (xs) {
    case Nil: return (Nil, Nil);
    case Cons((y, z), xs):
      switch (split(xs)) {
        case (ys, zs): return(Cons(y, ys), Cons(z, zs));
      }
  }
}

('a,'b){n:nat}
<'a * 'b> list(n) zip (xs: <'a> list(n), ys: <'b> list(n)) {
  var: 'a x; 'b y;;

  switch (xs, ys) {
    case (Nil, Nil): return Nil;
    case (Cons(x, xs), Cons(y, ys)):
      return Cons((x, y), zip (xs, ys));
  }
}

('a,'b){m:nat,n:nat}
<'a * 'b> list(min(m,n)) zip1 (xs: <'a> list(m), ys: <'b> list(n)) {
  var: 'a x; 'b y;;

  switch (xs, ys) {
    case (Nil, _): return Nil;
    case (_, Nil): return Nil;
    case (Cons(x, xs), Cons(y, ys)):
      return Cons((x, y), zip1 (xs, ys));
  }
}

('a){n:nat}
'a head (xs: <'a> list(n+1)) {
  var: 'a x;;
  Cons(x, xs) = xs; return x;
}

('a){n:nat}
<'a> list(n) tail (xs: <'a> list(n+1)) {
  Cons(_, xs) = xs; return xs;
}

('a){n:nat}
int(n) length (xs: <'a> list(n)) {
  var: int x;;
  x = 0;

  invariant: [p:nat, q:nat | p + q = n] (xs: <'a> list(p), x: int(q))
  while (true) {
    switch(xs) {
      case Nil: return x;
      case Cons(_, xs): x = x + 1;
    }
  }
  exit;
}

('a){m:nat,n:nat | n < m}
'a nth (xs: <'a> list(m), n: int(n)) {
   var: 'a x;;

   invariant: [m:nat, n:nat | n < m] (xs: <'a> list(m), n: int(n))
   while (true) {     
     Cons(x, xs) = xs;
     if (n > 0) n = n - 1; else return x;
   }
   exit;
}

('a){n:nat}
unit iterate (f: 'a -> unit, xs: <'a> list(n)) {
  var: 'a x;;

  invariant: [n:nat] (xs: <'a> list(n))
  while (true) {
    switch (xs) {
      case Nil: return;
      case Cons(x, xs): f(x);
    }
  }
}

('a)
bool exists(p: 'a -> bool, xs: <'a> list) {
  var: 'a x;;

  while (true) {
    switch (xs) {
      case Nil: break;
      case Cons(x, xs): if (p(x)) return true;
    }
  }
  return false;
}

('a)
bool forall(p: 'a -> bool, xs: <'a> list) {
  var: 'a x;;

  while (true) {
    switch (xs) {
      case Nil: break;
      case Cons(x, xs): if (p(x)) ; else return false;
    }
  }
  return true;
}

('a)
<'a> list flatten (xss: <<'a> list> list) {
   var: <'a> list xs, ys;;

   switch (xss) {
     case Nil: return Nil;
     case Cons(xs, xss): ys = flatten (xss); return append(xs, ys);
   }
}