(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   longestCommonSubsequence.raml
 *
 * Author:
 *   Jan Hoffmann (2010)
 *
 * Resource Bound:
 *   O(n*m)
 *
 * Description:
 *   A standard example of dynamic programming that can be found in
 *   many textbooks (see e.g. Cormen/Leiserson/Rivest/Stein:
 *   Introduction to Algorithms) is the computation of the length of
 *   the longest common subsequence (LCS) of two given lists
 *   (sequences).  Given two sequences a_1,...,a_n and b_1,...,b_m, one
 *   successively fills an nxm-matrix (here a list of lists) A such
 *   that A(i,j) contains the length of the LCS of a_1,...,a_i and
 *   b_1,...,b_j.  It is the case that
 *
 *            { 0                      if i=0 or j=0
 *   A(i,j) = { A(i-1,j-1) + 1         if i,j > 0 and a_i = b_j 
 *            { max(A(i,j-1),A(i-1,j)) if i,j > 0 and a_i \= b_j
 *
 *   This algorithm can be analyzed in our system and is exemplary for
 *   similar algorithms that use dynamic programming.
 *)


lcs : (L(int),L(int)) -> int
(* computes the length of the longest common subsequence *)

lcs(l1,l2) = let _=tick(1) in
             let m = lcstable(l1,l2) in 
             match m with 
               | nil -> +0
               | (l1::_) -> match l1 with
                                    | nil -> +0
                                    | (len::_) -> len;

(*
eq(lcs(A,B),1,[lcstable(A,B)],[A>=0,B>=0]).
*)

lcstable : (L(int),L(int)) -> L(L(int))
(* computes the table of lengths *)

lcstable (l1,l2) = let _=tick(1) in
                    match l1 with
                    | nil -> [firstline l2]
                    | (x::xs) -> let m = lcstable (xs,l2) in
                                 match m with
                                   | nil -> nil
                                   | (l::ls) -> (newline (x,l,l2))::l::ls;

(* 
eq(lcstable(A,B),1,[firstline(B)],[A=0]). 
eq(lcstable(A,B),1,[newline(X,B,B),lcstable(Ap,B)],[A>=1,Ap=A-1]). 

eq(out1_lcstable(A,B),1,[],[A=0]). 
eq(out1_lcstable(A,B),1,[out1_lcstable(Ap,B)],[A>=1,Ap=A-1]). 

eq(out2_lcstable(A,B),nat(B),[],[A=0]). 
eq(out2_lcstable(A,B),0,[out2_lcstable(Ap,B)],[A>=1,Ap=A-1]). 
*)

firstline : L(int) -> L(int)
(* Returns the first line of zeros *)

firstline(l) =  let _=tick(1) in
                match l with 
                 | nil -> nil
                 | (x::xs) -> +0::firstline xs;

(*
eq(firstline(A),1,[],[A=0]).
eq(firstline(A),1,[firstline(Ap)],[A >=1,Ap=A-1]).
*)

newline : (int,L(int),L(int)) -> L(int)
(* computes a new line according to the recursive definition above
 * y is the element of the second list
 * lastline the the previously computed line in the matrix
 * l contains elements of the first list *)

newline (y,lastline,l) = let _=tick(1) in
   match l with 
     | nil     -> nil
     | (x::xs) -> match lastline with
                   | nil -> nil
                   | (belowVal::lastline') -> 
		       let nl = newline(y,lastline',xs) in
                       let rightVal = right nl in
                       let diagVal =  right lastline' in
                       let elem = if x == y then diagVal+1 else max(belowVal,rightVal)
                       in elem::nl;

(*
eq(newline(A,B,C),1,[],[C=0]).
eq(newline(A,B,C),1,[],[C>=1,B=0]).
eq(newline(A,B,C),1,[right(Cp),right(Bp),max(E,F),newline(A,Bp,Cp)],[C>=1,B>=1,Bp=B-1,Cp=C-1]).
eq(newline(A,B,C),1,[right(Cp),right(Bp),newline(A,Bp,Cp)],[C>=1,B>=1,Bp=B-1,Cp=C-1]).

eq(out_newline(A,B,C),0,[],[C=0]).
eq(out_newline(A,B,C),0,[],[C>=1,B=0]).
eq(out_newline(A,B,C),1,[out_newline(A,Bp,Cp)],[C>=1,B>=1,Bp=B-1,Cp=C-1]).
*)

right : L(int) -> int

right l =  let _=tick(1) in
            match l with
            | nil -> +0
            | (x::xs) -> x;
(*
eq(right(A),1,[],[]).
*)
max : (int,int) -> (int)

max (a,b) = let _=tick(1) in
             if a>b then a else b;
(*
eq(max(A,B),1,[],[]).
*)