(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   matrix.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n*m*k)
 *
 * Description:
 *   A clever way of matrix multiplication for matrices that are
 *   represented as lists of lists.  It does not need to transpose
 *   the second matrix.  (Thanks to Helmut Seidl for suggesting this
 *   algorithm.)
 *)


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

matrixMult (m1,m2) = let _=tick(1) in
    match m1 with
      | [] -> []
      | (l::ls) -> (computeLine(l,m2,[])) :: matrixMult(ls,m2);

(*
eq(matrixMult(L1r,L1c,L2r,L2c),1,[],[L1r=0]).
eq(matrixMult(L1r,L1c,L2r,L2c),1,[computeLine(L1c,L2r,L2c,L3),matrixMult(L1rp,L1c,L2r,L2c)],[L1r>=1,L3=0,L1rp
= L1r-1]).
*)



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

computeLine (line,m,acc) = let _=tick(1) in
    match line with
      | [] -> acc
      | (x::xs) -> match m with
                     | [] -> []
                     | (l::ls) ->
    computeLine(xs,ls,lineMult(x,l,acc));

(*
eq(computeLine(L,Mr,Mc,Acc),1,[],[L=0]).
eq(computeLine(L,Mr,Mc,Acc),1,[],[L>=1,Mr=0]).
eq(computeLine(L,Mr,Mc,Acc),1,[lineMult(X,Mc,Acc),computeLine(Lp,Mrp,Mc,Acc)],[L>=1,Mr>=1,Lp=L-1,Mrp=Mr-1]).
*)

lineMult : (int,L(int),L(int)) -> L(int)
                
lineMult (n,l1,l2) =  let _=tick(1) in
                       match l1 with
                       | [] -> []
                       | (x::xs) -> match l2 with
                                      | [] -> x*n::lineMult(n,xs,[])
                                      | (y::ys) -> x*n + y ::
				      lineMult(n,xs,ys);

(*
eq(size_lineMult(A,L1,L2),0,[],[L1=0]).
eq(size_lineMult(A,L1,L2),1,[size_lineMult(A,L1p,L2p)],[L1>=1,L2=0,L1p =
L1-1,L2p=0]).
eq(size_lineMult(A,L1,L2),1,[size_lineMult(A,L1p,L2p)],[L1>=1,L2=0,L1p = L1-1,L2p=L2-1]).


eq(lineMult(A,L1,L2),1,[],[L1=0]).
eq(lineMult(A,L1,L2),1,[lineMult(A,L1p,L2p)],[L1>=1,L2=0,L1p =
L1-1,L2p=0]).
eq(lineMult(A,L1,L2),1,[lineMult(A,L1p,L2p)],[L1>=1,L2=0,L1p = L1-1,L2p=L2-1]).

*)