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