(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 * File:
 *   appendAll.raml
 *
 * Author:
 *   Jan Hoffmann (2009)
 *
 * Resource Bound:
 *   O(n)
 *
 * Description:
 *   Implementations of functions that append lists (of lists (of lists)):
 *   appendAll appends lists of lists, appendAll2 appends lists of lists of lists, ...
 * 
 *   The example should show how RAML deals with inner lists.
 *)



appendAll3 : L(L(L(L(int)))) -> L(int)

appendAll3 l =  let _=tick(1) in
                match l with
                | nil -> nil
                | (l1::ls) -> append(appendAll2 l1,appendAll3 ls);

(*
eq(appendall3(H1,H2,R,C),1,[],[H1 =< 0]).
eq(appendall3(H1,H2,R,C),1,[inst([L1,L2],[out_appendall2(H2,R,C),out_appendall3(Hs,H2,R,C)],append(L1,L2)),append(L1,L2),out_appendall3(Hs,H2,R,C),out_appendall2(H2,R,C),appendall2(H2,R,C),appendall3(Hs,H2,R,C)],[H1>=1,Hs=H1-1]).

eq(out_appendall3(H1,H2,R,C),0,[],[H1 =< 0]).
eq(out_appendall3(H1,H2,R,C),0,[out_appendall2(H2,R,C),out_appendall3(Hs,H2,R,C)],[H1>=1,Hs=H1-1]).
*)

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

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

(*
eq(append(N,M),1,[],[N =< 0]).
eq(append(N,M),1,[append(Np,M)],[N >= 1,Np = N-1]).
eq(inst(N,M,O),0,[],[]).
*)
appendAll : L(L(int)) -> L(int)

appendAll l =  let _=tick(1) in
               match l with
               | nil -> nil
               | (l1::ls) -> append(l1,appendAll ls);

(*
eq(appendall(N,M),1,[],[N =< 0]).
eq(appendall(N,M),1,[inst([L],[out_appendall(NP,M)],append(M,L)),out_appendall(NP,M),append(M,L),appendall(Np,M)],[N >=1,Np=N-1]).
eq(out_appendall(N,M),0,[],[N =< 0]).
eq(out_appendall(N,M),nat(M),[out_appendall(Np,M)],[N >= 1,Np=N-1]).
*)

appendAll2 : L(L(L(int))) -> L(int)

appendAll2 l =  let _=tick(1) in
                match l with
                | nil -> nil
                | (l1::ls) -> append(appendAll l1,appendAll2 ls);

(*
eq(appendall2(H,R,C),1,[],[H =< 0]).
eq(appendall2(H,R,C),1,[inst([L1,L2],[out_appendall(R,C),out_appendall2(H,R,C)],append(L1,L2)),append(L1,L2),out_appendall(R,C),out_appendall2(H,R,C),appendall(R,C),appendall2(Hs,R,C)],[H>=1,Hs=H-1,L >=0]).

eq(out_appendall2(H,R,C),0,[],[H =< 0]).
eq(out_appendall2(H,R,C),0,[out_appendall(R,C),out_appendall2(Hs,R,C)],[H>=1,Hs=H-1]).

*)

main = ()