(*
 * 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.
 *)
structure KMP =
    struct
	assert sub <| {size:nat, i:int | 0 <= i < size} 'a array(size) * int(i) -> 'a
        and length <| {n:nat} 'a array(n) -> int(n)

	fun{slen:nat, plen:nat}
	    kmpMatch(str, pat) =
	    let
		type intShift = [i:int| 0 <= i+1 < plen ] int(i)

		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 updateShift <| {size:nat, i:int | 0 <= i < size}
                                     intShift array(size) * int(i) * intShift -> unit

		val slen = length(str)
		and plen = length(pat)

		val shiftArray = arrayShift(plen, ~1)

		fun loopShift(i, j) = (* calculate the shift array *)
		    if (j = plen) then ()
		    else
			if sub(pat, j) <> sub(pat, i+1) then
			    if (i >= 0) then loopShift(subShift(shiftArray, i), j)
			    else loopShift(~1, j)
			else ((if (i+1 < j)
				   then updateShift(shiftArray, j, i+1)
			       else ()) <| unit;
			      loopShift(subShift(shiftArray, j), j+1))
		where loopShift <| {j:int | 0 < j <= plen} intShift * int(j) -> unit

		val _ = loopShift(~1, 1)

		fun loop(s, p) = (* this the main search function *)
		    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 ~1
		    else s - plen
                where loop <| {s:nat, p:nat | s <= slen /\ p <= plen}
                                int(s) * int(p) -> int
	    in
		loop(0, 0)
	    end
        where kmpMatch <| int array(slen) * int array(plen) -> int
    end