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

('a){m:nat,n:nat}
<'a> list(m+n) merge
(order: ('a, 'a) -> bool, xs: <'a> list(m), ys: <'a> list(n)) {
   var: 'a x, y;;
 
   switch (xs, ys) {
     case (Nil, _): return ys;
     case (_, Nil): return xs;    
     case (Cons(x, xs), Cons(y, ys)):
       if (order(x, y)) {
	 return Cons(x, merge(order, xs, Cons(y, ys)));
       } else {
	 return Cons(y, merge(order, Cons(x, xs), ys));
       }       
   }
}

union <'a> listlist with nat {
  ListNil(0);
  {m:nat,n:nat} ListCons(m+n) of <'a> list(m) * <'a> listlist(n)
}

('a){n:nat}
<'a> listlist(n) initlist(order: ('a, 'a) -> bool, xs: <'a> list(n)) {
   var: 'a x, y;;

   switch (xs) {
     case Nil: return ListNil;
     case Cons(_, Nil): return ListCons(xs, ListNil);
     case Cons(x, Cons(y, xs)):
       if (order(x, y)) {
         return ListCons(Cons(x, Cons(y, Nil)), initlist(order, xs));
       } else {
         return ListCons(Cons(y, Cons(x, Nil)), initlist(order, xs));
       }
   }
}

('a){n:nat}
<'a> listlist(n) listmerge(order: ('a, 'a) -> bool, xss: <'a> listlist(n)) {
  var: <'a> list xs, ys;;

  switch (xss) {
    case ListCons(xs, ListCons(ys, xss)):
      return ListCons(merge(order, xs, ys), listmerge(order, xss));
    default: return xss;
  }
}

('a){n:nat}
<'a> list(n) mergeall(order: ('a, 'a) -> bool, xss: <'a> listlist(n)) {
   var: <'a> list xs;;

   invariant: (xss: <'a> listlist(n))
   while (true) {   
     switch (xss) {
       case ListNil: return Nil;
       case ListCons(xs, ListNil): return xs;
       default: xss = listmerge(order, xss);
     }
   }
   exit;
}

('a){n:nat}
<'a> list(n) mergesort(order: ('a, 'a) -> bool, xs: <'a> list(n)) {
    return mergeall(order, initlist(order, xs));
}

bool lessthan (x:int, y:int) {
  if (x < y) return true; else return false;
}

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

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

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

  l = mergesort (lessthan, l);
  print_list (l);
  print_newline ();
}