(*
   this checks that the sum of a sorted list is
   the same as that of the input list. This is
   an approximation to verifying the permutation
   invariant.
*)

datatype intlist = intNil | intCons of int * intlist

typeref intlist of int (* sum *)
with intNil <| intlist(0)
  | intCons <| {i:nat, sum:int} int(i) * intlist(sum) -> intlist(i+sum)

val quicksort =
    let
	fun intAppend(intNil, rs) = rs
	  | intAppend(intCons(l, ls), rs) = intCons(l, intAppend(ls, rs))
        where intAppend <| {sm:int, sn:int}
                           intlist(sm) * intlist(sn) -> intlist(sm+sn)

	fun qs(lst) =
	    case lst of
		intNil => intNil
	      | intCons(x,xs) =>
		    let
			fun par(x, left, right, intNil) =
			    intAppend(qs(left), intCons(x,qs(right)))
			  | par(x, left, right, intCons(y,ys))
			    = if y <= x then par(x, intCons(y,left), right, ys)
			      else par(x, left, intCons(y,right), ys)
		        where par <| {i:int, sp:int, sq:int, sr:int}
			             int(i) * intlist(sp) * intlist(sq) * intlist(sr)
                                     -> intlist(i+sp+sq+sr)
		    in par(x, intNil, intNil, xs) end
        where qs <| {sum:int} intlist(sum) -> intlist(sum)
    in
	qs
    end