PUBS: A Practical Upper Bounds Solver
```
(* * * * * * * * * * *
* 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]).

*)

```