(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   insertionsort.raml
 *
 * Author:
 *   Jan Hoffmann (2009)
 *
 * Resource Bound:
 *   O(n^2)
 *
 * Description:
 *   Two implementations of the sorting algorithm insertion sort.
 *
 *   insertionsort admits a quatratic heap-space and time consumption.
 *
 *   insertionssortD uses the destructive insert function insertD.
 *   Thus it has linear heap-space consumption while having still
 *   quadratic run time.
 *)


insertionsort : L(int) -> L(int)

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

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

insert(x,l) =   let _=tick(1) in
                match l with
                | nil -> [x]
                | (y::ys) -> if y < x then y::insert(x,ys)
                                      else x::y::ys;





insertionsortD : L(int) -> L(int)

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

(*
eq(insertionsortD(A),1,[],[A=0]).
eq(insertionsortD(A),1,[insertD(X,Ap),insertionsortD(Ap)],[A>=1,Ap=A-1]).
*)


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

insertD(x,l) =  let _=tick(1) in
                matchD l with
                | nil -> [x]
                | (y::ys) -> if y < x then y::insertD(x,ys)
                                      else x::y::ys;

(*
eq(insertD(A,B),1,[],[B=0]).
eq(insertD(A,B),1,[],[B>=1]).
eq(insertD(A,B),1,[insertD(A,Bp)],[B>=1,Bp = B-1]).
*)