(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   duplicates.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n^2*m)
 *
 * Description:
 *   The function nub removes duplicates from a list of lists.  The runtime
 *   is O(n^2*m) if n is the size of the outer list an m is the maximal
 *   size of the inner lists.
 *)




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

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

(*
eq(eq(L1,L2),1,[],[L1=0]).
eq(eq(L1,L2),1,[],[L1>=1,L2=0]).
eq(eq(L1,L2),1,[eq(Ls1,Ls2)],[L1>=1,L2>=1,Ls1=L1-1,Ls2=L2-1]).
*)
(* nub removes duplicates from a list of lists. *)
nub : L(L(int)) -> L(L(int))

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

(*
eq(nub(L1,L2),1,[],[L1=0]).
eq(nub(L1,L2),1,[remove(X,Ls1,L2),nub(L3,L2)],[L1>=1,Ls1 = L1-1, L3 =< Ls1]).
*)
remove : (L(int),L(L(int))) -> L(L(int))

remove (x,l) = let _=tick(1) in 
               match l with
                 | nil -> nil
                 | (y::ys) -> if eq (x,y) then remove(x,ys)
                                          else y::remove(x,ys);
(*
eq(remove(X,L1,L2),1,[],[L1=0]).
eq(remove(X,L1,L2),1,[eq(X,L2),remove(X,Ls1,L2)],[L1>=1,Ls1 = L1-1]).
eq(remove(X,L1,L2),1,[remove(X,Ls1,L2)],[L1>=1,Ls1 = L1-1]).
*)