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