(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   listsort.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n^2*m)
 *
 * Description:
 *   Comparing lists of lists needs linear time.
 *   Since insertion sort does a quadratic number of comparisons (in the worst case) 
 *   we need cubic time to sort a list of lists using islist below.
 *
 *   We derive a tight runtime bound.
 *)



(*
eq(isortlist(R,C),1,[],[R=0]).
eq(isortlist(R,C),1,[insert(C,Rp,C),isortlist(Rp,C)],[R>=1,Rp = R-1]).
eq(insert(A,R,C),1,[],[R=0]).
eq(insert(A,R,C),1,[leq(A,C)],[R>=1]).
eq(insert(A,R,C),1,[leq(A,C),insert(A,Rs,C)],[R>=1,Rs = R-1]).
eq(leq(A,B),1,[],[A=0]).
eq(leq(A,B),1,[],[A >=1,B=0]).
eq(leq(A,B),1,[leq(Ap,Bp)],[A>=1,B>=1,Ap=A-1,Bp=B-1]).
*)

leq : (L(int),L(int)) -> bool

leq (l1,l2) = let _=tick(1) in
    match l1 with
      | nil -> true
      | (x::xs) -> match l2 with
                     | nil -> false
                     | (y::ys) -> (x L(L(int))

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



isortlist : L(L(int)) -> L(L(int))

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

main = ()