(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   dyade.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n*m)
 *
 * Description:
 *   The function dyade computes the (nxm)-matrix that results from the
 *   multiplication of two vectors (integer lists) of length n and
 *   length m, respectively.
 *
 *   The computed bounds are tight.
 *)

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

dyade (l1,l2) = let _=tick(1) in 
                 match l1 with
                  | nil -> nil
                  | (x::xs) -> (mult(x,l2))::dyade(xs,l2);
(*
eq(dyade(N,M),1,[],[N =0]).
eq(dyade(N,M),1,[mult(X,M),dyade(Np,M)],[N >=1,Np = N-1]).
*)
mult : (int,L(int)) -> L(int)

mult (n,l) =  let _=tick(1) in 
              match l with 
               | nil -> nil
               | (x::xs) -> n*x::mult(n,xs);
(*
eq(mult(N,M),1,[],[M=0]).
eq(mult(N,M),1,[mult(N,Mp)],[M>=1,Mp = M-1]).
*)

main = ()