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

unit print_list (l: <int> list) {
  var: int x;;

  while (true) {
    switch (l) {
      case Nil: print_string ("[]"); break;
      case Cons (x, l): print_int (x); print_string ("::");
    }
  }
}

('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));
   }
}

{p:nat,q:nat,r:nat}
[p1:nat,q1:nat | p1+q1=p+q+r] (<int> list(p1) * <int> list(q1))
partition (x: int,
           left: <int> list(p),
           right: <int> list(q),
           rest: <int> list(r)) {
  var: int y;;

  invariant:
    [p1:nat,q1:nat,r1:nat | p1+q1+r1 = p+q+r]
    (left: <int> list(p1), right: <int> list(q1), rest: <int> list(r1))
  while (true) {
    switch (rest) {
    case Nil: return (left, right);
    case Cons(y, rest):
      if (y < x) { left = Cons (y, left); }
      else { right = Cons (y, right); }
    }
  }
  exit;
}

{n:nat}
<int> list(n) quicksort (xs: <int> list(n)) {
  var: int x;
       <int> list left, right;;

  switch (xs) {
  case Nil: return Nil;
  case Cons (x, xs):
    switch (partition (x, Nil, Nil, xs)) {
    case (left, right):
      return append(quicksort(left), Cons(x, quicksort(right)));
    }
  }
}

unit main () {
  var: l: <int> list;;

  l = Cons (3, Cons(5, Cons (2, Nil)));
  l = append (l, l);
  l = append (l, l);
  l = append (l, l);
  print_list (l);
  print_newline ();

  l = quicksort (l);
  print_list (l);
  print_newline ();
}