(* * This example shows that mergeSort on a list * always yields a list of the same length. * This code is basically copied from SML/NJ lib. *) (* 8 type annotations, which occupy about 15 lines *) structure Merge_Sort = struct datatype 'a listlist = Nil | Cons of 'a list * 'a listlist typeref 'a listlist of nat * nat with Nil <| 'a listlist(0,0) | Cons <| {l:nat,m:nat,n:nat} 'a list(l) * 'a listlist(m,n) -> 'a listlist(m+1,n+l) assert not <| bool -> bool and rev <| {n:nat} 'a list(n) -> 'a list(n) and hd <| { n:nat | n > 0 } 'a list(n) -> 'a fun('a) sort cmp ls = let fun merge([],ys) = ys | merge(xs,[]) = xs | merge(x::xs,y::ys) = if cmp(x,y) then y::merge(x::xs,ys) else x::merge(xs,y::ys) where merge <| {m:nat, n:nat} 'a list(m) * 'a list(n) -> 'a list(m+n) fun mergepairs'(ls as Cons(l,Nil)) = l | mergepairs'(Cons(l1,Cons(l2,ls))) = mergepairs'(Cons(merge(l1,l2),ls)) where mergepairs' <| {m:nat, n:nat | m > 0} 'a listlist(m,n) -> 'a list(n) fun mergepairs(ls as Cons(l,Nil), k) = ls | mergepairs(Cons(l1,Cons(l2,ls)),k) = if k mod 2 = 1 then Cons(l1,Cons(l2,ls)) else mergepairs(Cons(merge(l1,l2),ls), k div 2) where mergepairs <| {m:nat, n:nat | m > 0} 'a listlist(m,n) * int -> [m:nat | m > 0] 'a listlist(m,n) fun nextrun(run,[]) = (rev run,[]) | nextrun(run,x::xs) = if cmp(x,hd(run)) then nextrun(x::run,xs) else (rev run,x::xs) where nextrun <| {m:nat, n:nat | m > 0 } 'a list(m) * 'a list(n) -> [p:nat, q:nat | p+q = m+n] ('a list(p) * 'a list(q)) fun samsorting([], ls, k) = mergepairs'(ls) | samsorting(x::xs, ls, k) = let val (run,tail) = nextrun([x],xs) in samsorting(tail, mergepairs(Cons(run,ls),k+1), k+1) end where samsorting <| {l:nat,m:nat,n:nat | m+l > 0} 'a list(l) * 'a listlist(m,n) * int -> 'a list(n+l) in case ls of [] => [] | _::_ => samsorting(ls, Nil, 0) end where sort <| {n:nat} ('a * 'a -> bool) -> 'a list(n) -> 'a list(n) fun('a) sorted (cmp) = let fun s (x::(rest as (y::_))) = not(cmp(x, y)) andalso s rest | s l = true where s <| 'a list -> bool in s end where sorted <| ('a * 'a -> bool) -> 'a list -> bool end (* end of mergeSort *)