(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   minsort.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n^2)
 *
 * Description:
 *   An implementation of the sorting algorithm selection sort.
 *   (See http://en.wikipedia.org/wiki/Selection_sort)
 *)


minSort : L(int) -> L(int)
 
minSort l = let _=tick(1) in 
             match findMin l with
               | nil -> nil
               | (x::xs) -> x::minSort(xs);

(*                                         
eq(minSort(N),1,[findMin(N)],[N=0]).
eq(minSort(N),1,[findMin(N),minSort(Ns)],[N>=1,Ns=N-1]).
*)

 findMin : L(int) -> L(int)
 
 findMin l =  let _=tick(1) in 
              match l with
               | nil -> nil
               | (x::xs) -> match findMin xs with
                               | nil -> [x]
                               | (y::ys) -> if x < y then x::y::ys else y::x::ys;
(*
eq(findMin(N),1,[],[N=0]).
eq(findMin(N),1,[findMin(Ns)],[N>=1,Ns=N-1]).
*)

main=()