(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 * File:
 *   rationalPotential.raml
 *
 * Author:
 *   Jan Hoffmann (2009)
 *
 * Resource Bound:
 *   O(n)
 *
 * Description: 
 *   Implementation of a zip function (zip3) that zips 3 integer lists.
 *   The resource consumption of zip3 is always payed by the shortest list.
 *
 *   A group function that groups the elements of a list into triples.
 *   This function is typed with a rational potential.
 *)


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

zip3 (l1,l2,l3) =
   match l1 with
      | nil -> nil
      | (x::xs) -> match l2 with
          | nil -> nil
          | (y::ys) -> match l3 with
               | nil -> nil
               | (z::zs) -> let _= tick(1) in (x,y,z)::zip3(xs,ys,zs);

(*
eq(zip3(L1,L2,L3),0,[],[L1=0]).
eq(zip3(L1,L2,L3),0,[],[L1>=1,L2=0]).
eq(zip3(L1,L2,L3),0,[],[L1>=1,L2>=1,L3=0]).
eq(zip3(L1,L2,L3),1,[zip3(Ls1,Ls2,Ls3)],[L1>=1,L2>=1,L3>=1,Ls1=L1-1,Ls2=L2-1,Ls3=L3-1]).
*)

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

group3 l =
   match l with
      | nil -> nil
      | (x::xs) -> match xs with
          | nil -> nil
          | (y::ys) -> match ys with
               | nil -> nil
               | (z::zs) -> let _= tick(1) in (x,y,z)::group3 zs;

(*
eq(group3(L),0,[],[L=<3]).
eq(group3(L),1,[group3(Ls)],[L>=4,Ls=L-3]).
*)

main = let x = [+1,+2,+3,+4,+5] in zip3(x,x,x)