Re: substring match like "strstr"

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>]

Hello,

I   missed  the   beginning  of   the  discussion,   but  implementing
Knuth-Morris-Pratt is quite easy. The  code is given below (26 lines),
following Sedgewick's book "Algorithms".  Notice that the function kmp
can be partially applied to  a pattern, therefore computing the offset
table only once. The complexity is N+M where N is the size of the text
and M the size of the pattern.

(The following program was proved  correct in the Coq Proof Assistant;
without the Not_found exception, however)

Hope this helps,
-- 
Jean-Christophe FILLIATRE
  mailto:Jean-Christophe.Filliatre@lri.fr
  http://www.lri.fr/~filliatr

======================================================================
let initnext p =
  let m = String.length p in
  let next = Array.create m 0 in
  let i = ref 1 and j = ref 0 in
  while !i < m-1 do
    if p.[!i] = p.[!j] then begin
      incr i; incr j; next.(!i) <- !j
    end else
      if !j = 0 then begin incr i; next.(!i) <- 0 end else j := next.(!j)
  done;
  next

let kmp p =
  let next = initnext p in
  fun a ->
    let n = String.length a
    and m = String.length p
    and i = ref 0
    and j = ref 0 in
    while !j < m & !i < n do
      if a.[!i] = p.[!j] then begin
	incr i; incr j
      end else
	if !j = 0 then incr i else j := next.(!j)
    done;
    if !j >= m then !i-m else raise Not_found
======================================================================