(* * 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