[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Jean-Christophe Filliatre <Jean-Christophe.Filliatre@l...> |
| Subject: | Re: substring match like "strstr" |
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
======================================================================