[
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: | 2000-12-14 (18:00) |
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 ======================================================================