(* This is an implementation of the Knuth-Morris-Pratt string matching algorithm
 * in standard ML. Also this demonstrates some interesting questions involved
 * with array bounds checks. Note that some array bound checks are still needed.
 *)
structure KMP =
    struct
	(* sub needs NO bound checking, but subW needs bound checking *)

	assert sub <| {size:nat, i:int | 0 <= i < size} 'a array(size) * int(i) -> 'a
        and subW <| 'a array * int -> 'a
        and length <| {n:nat} 'a array(n) -> int(n)

	type intShift = [i:int| 0 <= i+1] int(i)

       (* subShift and updateShift need NO bound checking *)
       (* subShiftW needs bound checking *)

	assert arrayShift <| {size:nat} int(size) * intShift -> intShift array(size)
        and subShift <| {size:nat, i:int | 0 <= i < size} 
	                  intShift array(size) * int(i) -> intShift
        and subShiftW <| intShift array * int -> intShift
        and updateShift <| {size:nat, i:int | 0 <= i < size}
                             intShift array(size) * int(i) * intShift -> unit

	fun makeShift(pat) = (* generate the table for shifts when matching fails *)
	    let
		val plen = length(pat)
		val shiftArray = arrayShift(plen, ~1)
		
		fun loop(i, j) = (* calculate the shift array *)
		    if (j >= plen) then ()
		    else
			if sub(pat, j) <> subW(pat, i+1) then
			    if (i >= 0) then loop(subShiftW(shiftArray, i), j)
			    else loop(~1, j+1)
			else (updateShift(shiftArray, j, i+1);
                              loop(subShift(shiftArray, j), j+1))
		where loop <| {j:nat} intShift * int(j) -> unit
	    in
		(loop(~1, 1); shiftArray)
	    end
        where makeShift <| {plen:nat} int array(plen) -> intShift array(plen)

	fun kmpMatch(str, pat) =
	    let
		val slen = length(str)
		and plen = length(pat)

		val shiftArray = makeShift(pat)

		fun loop(s, p) = 
		    if s < slen then
			if p < plen then
			    if sub(str, s) = sub(pat, p) then loop(s+1, p+1)
			    else
				if (p = 0) then loop(s+1, p)
				else loop(s, subShift(shiftArray, p-1)+1)
			else (s - plen)
		    else ~1
                where loop <| {s:nat, p:nat} int(s) * int(p) -> int
	    in
		loop(0, 0)
	    end
        where kmpMatch <| {slen:nat, plen:nat} int array(slen) * int array(plen) -> int
    end