PUBS: A Practical Upper Bounds Solver

(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 * File:
 *   quicksort.raml
 *
 * Author:
 *   Jan Hoffmann (2009)
 *
 * Resource Bound:
 *   O(n^2)
 *
 * Description:
 *   Two implementations of the well known sorting algorithm quicksort.
 *   
 *   The function quicksort does not use a destructive pattern match
 *   and thus consumes quadratic heap-space and quadratic time.
 *
 *   quicksortD uses the destructive pattern matching to delete
 *   intermediate results.  This leads to a linear heap-space and
 *   quadratic time consumption.
 *)


quicksort : L(int) -> L(int)  
(* works out of the box as implemented in textbooks *)

quicksort l = let _=tick(1) in
              match l with
              | nil -> nil
              | (z::zs) -> let (xs,ys) = split (z,zs) in
                           append(quicksort xs, z::(quicksort ys));


split : (int,L(int)) -> (L(int),L(int))

split(pivot,l) = let _=tick(1) in
                  match l with
                    | nil     -> (nil,nil)
                    | (x::xs) -> let (ls,rs) = split (pivot,xs) in
                                 if x > pivot then (ls,x::rs) else (x::ls,rs);



append : (L(int),L(int)) -> L(int)

append(l,ys) = let _=tick(1) in
                match l with
                | nil -> ys
                | (x::xs) -> x::append(xs,ys);

main = ()