/* union <'a> list with nat { Nil(0); {n:nat} Cons(n+1) of 'a * <'a> list(n) } */ 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 ("::"); } } } ('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] ( list(p1) * list(q1)) partition (x: int, left: list(p), right: list(q), rest: list(r)) { var: int y;; invariant: [p1:nat,q1:nat,r1:nat | p1+q1+r1 = p+q+r] (left: list(p1), right: list(q1), rest: 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} list(n) quicksort (xs: list(n)) { var: int x; 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: 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 (); }