(* * * * * * * * * * *
* Resource Aware ML *
* * * * * * * * * * *
* File:
* mergesort.raml
*
* Author:
* Jan Hoffmann (2009)
*
* Resource Bound:
* O(n^2)
*
* Description:
* An implementation of the well known sorting algorithm mergesort.
* This implementation deallocates the input list. Copy the list before
* if you want to use the unsorted list later.
*
* It is suprising that the function mergesort can be analysed. The
* type of the function looks like the result of a bug on the first
* view. But it is correct. The function mergesort is a nice
* example of a type that might be hard to find without type
* inference.
*
* There is also an out commented buggy version of mergesort
* (mergesortBuggy) that does not terminate and consumes an infinite
* ammount of heap-space and time. Thus our analysis does not work
* for mergesortBuggy. (Note that it is no general problem for our
* analysis if a function does not terminate. For example f(x) =
* f(x) consumes no heap-space and can be analysed with the
* heap-space metric.)
*)
(*
eq(mergeSort(N),1,[],[N =< 1]).
eq(mergeSort(N),1,[msplit(N), mergeSort(L1),mergeSort(L2),merge(L1,L2)],[N>=2,L1>=0,L2>=0,2*L1 =< N+1,2*L2=< N]).
eq(out2_msplit(N),0,[],[N=0]).
eq(out2_msplit(N),0,[],[N=1]).
eq(out2_msplit(N),1,[out2_msplit(Np)],[N>=2,Np = N-2]).
eq(out1_msplit(N),0,[],[N=0]).
eq(out1_msplit(N),1,[],[N=1]).
eq(out1_msplit(N),1,[out1_msplit(Np)],[N>=2,Np = N-2]).
eq(msplit(N),1,[],[N=0]).
eq(msplit(N),1,[],[N=1]).
eq(msplit(N),1,[msplit(Np)],[N>=2,Np = N-2]).
eq(merge(N1,N2),1,[],[N1=0]).
eq(merge(N1,N2),1,[],[N2=0]).
eq(merge(N1,N2),1,[merge(N1p,N2)],[N1>=1,N2>=1,N1p=N1-1]).
eq(merge(N1,N2),1,[merge(N1,N2p)],[N1>=1,N2>=1,N2p=N2-1]).
*)
mergesort: L(int) -> L(int)
(* mergesort as it is implemented in textbooks *)
mergesort l = let _=tick(1) in
match l with
| nil -> nil
| (x1::xs) -> match xs with
| nil -> x1::nil
| (x2::xs') -> let (l1,l2) = msplit (x1::x2::xs') in
merge (mergesort l1, mergesort l2);
msplit : L(int) -> (L(int),L(int))
msplit l = let _=tick(1) in
matchD l with
| nil -> (nil,nil)
| (x1::xs) -> matchD xs with
| nil -> ([x1],nil)
| (x2::xs') -> let (l1,l2) = msplit xs' in
(x1::l1,x2::l2);
merge : (L(int),L(int)) -> L(int)
merge (l1,l2) = let _=tick(1) in
matchD l1 with
| nil -> l2
| (x::xs) -> matchD l2 with
| nil -> (x::xs)
| (y::ys) -> if x