
   0 | ||| Fast Knuth-Morris-Pratt search of ByteStrings
   1 | module Data.ByteString.Search.KnuthMorrisPratt
   2 | 
   3 | import Data.Array.Core
   4 | import Data.Array.Mutable
   5 | import Data.Bits
   6 | import Data.ByteString
   7 | import Data.ByteString.Search.DFA.Types
   8 | import Data.ByteString.Search.KnuthMorrisPratt.Internal
   9 | import Data.Enum
  10 | import Data.Linear.Ref1
  11 | import Data.So
  12 | 
  13 | %hide Data.Buffer.Core.get
  14 | %hide Data.Buffer.Core.set
  15 | 
  16 | %default total
  17 | 
  18 | ||| Returns a list of starting positions of a pattern `ByteString`
  19 | ||| (0-based) across the list of target `ByteString`s.
  20 | |||
  21 | ||| The KMP pattern position and border values are represented by bounded
  22 | ||| `DFAState` values belonging to the state space packaged with the KMP
  23 | ||| border table.
  24 | |||
  25 | ||| Consequently, border-table lookups require no `tryNatToFin`, `Fin`
  26 | ||| conversion, or other dynamic array-bounds validation. A border lookup
  27 | ||| accepts an already-bounded state and directly returns another bounded
  28 | ||| state.
  29 | |||
  30 | ||| Target and chunk positions remain `Nat` values because they represent
  31 | ||| absolute positions in the streamed input rather than KMP states.
  32 | |||
  33 | private
  34 | matcher :  Bool
  35 |         -> ByteString
  36 |         -> List ByteString
  37 |         -> F1 s (Maybe (List Nat))
  38 | matcher overlap pat chunks t =
  39 |   let patlen                             := length pat
  40 |       Just patzero                       := index Z pat
  41 |         | Nothing =>
  42 |             Nothing # t
  43 |       bords                          # t := kmpBorders pat t
  44 |       Just (MkKMPBorders stspace bords') := bords
  45 |         | Nothing =>
  46 |             Nothing # t
  47 |       -- The complete-match state for this pattern.
  48 |       --
  49 |       -- This validation is performed once before searching begins.
  50 |       Just fullstate                     := tryIndex {r = stspace.states} (cast patlen)
  51 |         | Nothing =>
  52 |             Nothing # t
  53 |       -- DFA state one, reached after matching the first pattern byte.
  54 |       --
  55 |       -- Since `pat` is known to be nonempty at this point, state one is
  56 |       -- valid. The check is performed once outside the search loop.
  57 |       Just stateone                      := tryIndex {r = stspace.states} 1
  58 |         | Nothing =>
  59 |             Nothing # t
  60 |       fullbord                       # t := kmpBorder bords' fullstate t
  61 |       result                         # t := searcher stspace Z (zeroDFAState stspace) chunks Lin patlen patzero stateone fullbord bords' t
  62 |       Just result'                       := result
  63 |         | Nothing =>
  64 |             Nothing # t
  65 |     in Just (result' <>> []) # t
  66 |   where
  67 |     mutual
  68 |       ||| Continue searching across the remaining target chunks.
  69 |       |||
  70 |       ||| `patpos` is the current KMP pattern state. If it is state zero,
  71 |       ||| searching uses the specialized `checkHead` path; otherwise the
  72 |       ||| partial match is continued with `findMatch`.
  73 |       |||
  74 |       searcher :  (stspace : DFAStateSpace)
  75 |                -> (prior : Nat)
  76 |                -> (patpos : DFAState stspace.states)
  77 |                -> (strs : List ByteString)
  78 |                -> (final : SnocList Nat)
  79 |                -> (patlen : Nat)
  80 |                -> (patzero : Bits8)
  81 |                -> (stateone : DFAState stspace.states)
  82 |                -> (fullbord : DFAState stspace.states)
  83 |                -> (bords : KMPBorderTable s stspace.states)
  84 |                -> F1 s (Maybe (SnocList Nat))
  85 |       searcher stspace _     _      []            final _      _       _        _        _     t =
  86 |         Just final # t
  87 |       searcher stspace prior patpos (str :: rest) final patlen patzero stateone fullbord bords t =
  88 |           let strlen := length str
  89 |               False  := dfaStateValue patpos == 0
  90 |                 | True =>
  91 |                     assert_total (checkHead stspace prior Z str strlen rest final patlen patzero stateone fullbord bords t)
  92 |             in assert_total (findMatch stspace prior patpos Z str strlen rest final patlen patzero stateone fullbord bords t)
  93 |       ||| Search for the first pattern byte while the KMP state is zero.
  94 |       |||
  95 |       ||| Bytes which differ from the first pattern byte can be skipped
  96 |       ||| without consulting the KMP border table. When `patzero` is found,
  97 |       ||| searching continues directly from prevalidated state one.
  98 |       |||
  99 |       checkHead :  (stspace : DFAStateSpace)
 100 |                 -> (prior : Nat)
 101 |                 -> (stri : Nat)
 102 |                 -> (str : ByteString)
 103 |                 -> (strlen : Nat)
 104 |                 -> (rest : List ByteString)
 105 |                 -> (final : SnocList Nat)
 106 |                 -> (patlen : Nat)
 107 |                 -> (patzero : Bits8)
 108 |                 -> (stateone : DFAState stspace.states)
 109 |                 -> (fullbord : DFAState stspace.states)
 110 |                 -> (bords : KMPBorderTable s stspace.states)
 111 |                 -> F1 s (Maybe (SnocList Nat))
 112 |       checkHead stspace prior stri str strlen rest final patlen patzero stateone fullbord bords t =
 113 |         let False          := stri == strlen
 114 |               | True =>
 115 |                   assert_total (searcher stspace (plus prior strlen) (zeroDFAState stspace) rest final patlen patzero stateone fullbord bords t)
 116 |             Just strbyte := index stri str
 117 |               | Nothing =>
 118 |                   Nothing # t
 119 |             nxtstri      := S stri
 120 |             False        := strbyte == patzero
 121 |               | True =>
 122 |                   assert_total (findMatch stspace prior stateone nxtstri str strlen rest final patlen patzero stateone fullbord bords t)
 123 |           in assert_total (checkHead stspace prior nxtstri str strlen rest final patlen patzero stateone fullbord bords t)
 124 |       ||| Continue a partial KMP match.
 125 |       |||
 126 |       ||| `pati` is a bounded KMP state rather than a raw `Nat`. A complete
 127 |       ||| match is detected by comparing the underlying state value with the
 128 |       ||| pattern length.
 129 |       |||
 130 |       ||| If the current chunk ends while a partial match is active, the same
 131 |       ||| bounded pattern state is carried directly into the next chunk.
 132 |       |||
 133 |       findMatch :  (stspace : DFAStateSpace)
 134 |                 -> (prior : Nat)
 135 |                 -> (pati : DFAState stspace.states)
 136 |                 -> (stri : Nat)
 137 |                 -> (str : ByteString)
 138 |                 -> (strlen : Nat)
 139 |                 -> (rest : List ByteString)
 140 |                 -> (final : SnocList Nat)
 141 |                 -> (patlen : Nat)
 142 |                 -> (patzero : Bits8)
 143 |                 -> (stateone : DFAState stspace.states)
 144 |                 -> (fullbord : DFAState stspace.states)
 145 |                 -> (bords : KMPBorderTable s stspace.states)
 146 |                 -> F1 s (Maybe (SnocList Nat))
 147 |       findMatch stspace prior pati stri str strlen rest final patlen patzero stateone fullbord bords t =
 148 |         let patival := dfaStateValue pati
 149 |             False   := patival == cast {to=Bits32} patlen
 150 |               | True =>
 151 |                   let matchidx := minus (plus prior stri) patlen
 152 |                       final'   := final :< matchidx
 153 |                       False    := overlap
 154 |                         | True =>
 155 |                             let False := dfaStateValue fullbord == 0
 156 |                                   | True =>
 157 |                                       assert_total (checkHead stspace prior stri str strlen rest final' patlen patzero stateone fullbord bords t)
 158 |                               in assert_total (findMatch stspace prior fullbord stri str strlen rest final' patlen patzero stateone fullbord bords t)
 159 |                    in assert_total (checkHead stspace prior stri str strlen rest final' patlen patzero stateone fullbord bords t)
 160 |             False        := stri == strlen
 161 |               | True =>
 162 |                   assert_total (searcher stspace (plus prior strlen) pati rest final patlen patzero stateone fullbord bords t)
 163 |             Just strbyte := index stri str
 164 |               | Nothing =>
 165 |                   Nothing # t
 166 |          in assert_total (compareAt stspace prior pati stri strbyte str strlen rest final patlen patzero stateone fullbord bords t)
 167 |       ||| Compare the current target byte with the pattern byte represented by
 168 |       ||| the current KMP state.
 169 |       |||
 170 |       ||| On a mismatch, the fallback state is read directly from the bounded
 171 |       ||| KMP border table. No conversion through `Fin`, `tryNatToFin`, or
 172 |       ||| `Maybe` is required for the border lookup.
 173 |       |||
 174 |       ||| On a match, the pattern state advances by one. Since this function
 175 |       ||| is reached only after `findMatch` has established that `pati` is not
 176 |       ||| the complete-match state, its successor is known to remain within
 177 |       ||| the DFA state space.
 178 |       |||
 179 |       compareAt :  (stspace : DFAStateSpace)
 180 |                 -> (prior : Nat)
 181 |                 -> (pati : DFAState stspace.states)
 182 |                 -> (stri : Nat)
 183 |                 -> (strbyte : Bits8)
 184 |                 -> (str : ByteString)
 185 |                 -> (strlen : Nat)
 186 |                 -> (rest : List ByteString)
 187 |                 -> (final : SnocList Nat)
 188 |                 -> (patlen : Nat)
 189 |                 -> (patzero : Bits8)
 190 |                 -> (stateone : DFAState stspace.states)
 191 |                 -> (fullbord : DFAState stspace.states)
 192 |                 -> (bords : KMPBorderTable s stspace.states)
 193 |                 -> F1 s (Maybe (SnocList Nat))
 194 |       compareAt stspace prior pati stri strbyte str strlen rest final patlen patzero stateone fullbord bords t =
 195 |         let patidx       := cast {to=Nat} (dfaStateValue pati)
 196 |             Just patbyte := index patidx pat
 197 |               | Nothing =>
 198 |                   Nothing # t
 199 |             False        := strbyte == patbyte
 200 |               | True =>
 201 |                   let nextval : Bits32
 202 |                       nextval := dfaStateValue pati + 1
 203 |                       -- The successor is valid because `findMatch` has
 204 |                       -- already established that `pati` is not the final
 205 |                       -- pattern state.
 206 |                       nextstate : DFAState stspace.states
 207 |                       nextstate = I nextval {prf = believe_me ()}
 208 |                     in assert_total (findMatch stspace prior nextstate (S stri) str strlen rest final patlen patzero stateone fullbord bords t)
 209 |             fallback # t := kmpBorder bords pati t
 210 |             False        := dfaStateValue fallback == 0
 211 |               | True =>
 212 |                   assert_total (checkHead stspace prior (S stri) str strlen rest final patlen patzero stateone fullbord bords t)
 213 |           in assert_total (compareAt stspace prior fallback stri strbyte str strlen rest final patlen patzero stateone fullbord bords t)
 214 | 
 215 | ||| Performs a Knuth–Morris–Pratt string search on a `ByteString`.
 216 | |||
 217 | ||| This function finds all (0-based) starting indices of the non-empty pattern `ByteString`
 218 | ||| pat within the non-empty target `ByteString`, using the KMP border table
 219 | ||| computed by `kmpBorders`.
 220 | |||
 221 | ||| Example:
 222 | |||
 223 | ||| | pat  | target     |
 224 | ||| | ---- | ---------- |
 225 | ||| | "AN" | "ANPANMAN" |
 226 | |||
 227 | ||| | Start | Substring      | Match? | Explanation                                      |
 228 | ||| | ----- | -------------- | ------ | ------------------------------------------------ |
 229 | ||| | 0     | **"AN"**PANMAN | Yes    | Full pattern `"AN"` matches starting at index 0. |
 230 | ||| | 1     | A**"NP"**ANMAN | No     | Mismatch after the first character.              |
 231 | ||| | 2     | AN**"PA"**NMAN | No     | No match — next candidate after suffix shift.    |
 232 | ||| | 3     | ANP**"AN"**MAN | Yes    | Match found at index 3.                          |
 233 | ||| | 4     | ANPA**"NM"**AN | No     | Mismatch.                                        |
 234 | ||| | 5     | ANPAN**"MA"**N | No     | Mismatch.                                        |
 235 | ||| | 6     | ANPANM**"AN"** | Yes    | Final match found at index 6.                    |
 236 | ||| 
 237 | |||
 238 | ||| matchKMP "AN" "ANPANMAN" => Just [0, 3, 6]
 239 | |||
 240 | export
 241 | matchKMP :  (pat : ByteString)
 242 |          -> (target : ByteString)
 243 |          -> {0 prfpat : So (not $ null pat)}
 244 |          -> {0 prftarget : So (not $ null target)}
 245 |          -> F1 s (Maybe (List Nat))
 246 | matchKMP pat target {prfpat} {prftarget} t =
 247 |   let matcher'   # t := matcher False pat [target] t
 248 |       Just matcher'' := matcher'
 249 |         | Nothing =>
 250 |             Nothing # t
 251 |     in Just matcher'' #t
 252 | 
 253 | ||| Performs a Knuth–Morris–Pratt string search on a `ByteString`.
 254 | |||
 255 | ||| This function finds all (0-based) indices (possibly overlapping)
 256 | ||| of the non-empty pattern `ByteString` pat
 257 | ||| within the non-empty target `ByteString`, using the KMP border table
 258 | ||| computed by `kmpBorders`.
 259 | |||
 260 | ||| Example:
 261 | |||
 262 | ||| | pat   | target      |
 263 | ||| | ----- | ----------- |
 264 | ||| | "ABC" | "ABCABCABC" |
 265 | |||
 266 | ||| | Start | Substring       | Match? | Explanation                                                      |
 267 | ||| | ----- | --------------- | ------ | ---------------------------------------------------------------- |
 268 | ||| | 0     | **"ABCABC"**ABC | Yes    | Full pattern matches starting at index 0.                        |
 269 | ||| | 1     | A**"BCABCA"**BC | No     | Mismatch starts immediately after first letter.                  |
 270 | ||| | 2     | AB**"CABCAA"**C | No     | Shift by suffix table → mismatch on 2nd char.                    |
 271 | ||| | 3     | ABC**"ABC"**    | Yes    | Overlapping match starting at index 3 (because `"ABC"` repeats). |
 272 | ||| 
 273 | ||| indicesKMP "ABCABC" "ABCABCABC" => Just [0, 3]
 274 | |||
 275 | export
 276 | indicesKMP :  (pat : ByteString)
 277 |            -> (target : ByteString)
 278 |            -> {0 prfpat : So (not $ null pat)}
 279 |            -> {0 prftarget : So (not $ null target)}
 280 |            -> F1 s (Maybe (List Nat))
 281 | indicesKMP pat target {prfpat} {prftarget} t =
 282 |   let matcher'   # t := matcher True pat [target] t
 283 |       Just matcher'' := matcher'
 284 |         | Nothing =>
 285 |             Nothing # t
 286 |     in Just matcher'' # t
 287 | 
 288 | ||| Splits a ByteString at the first match of pat in target.
 289 | |||
 290 | ||| This function uses the Knuth-Morris-Pratt matcher (with overlap = False) to
 291 | ||| locate the earliest occurrence of pat in target.  If the pattern is
 292 | ||| found at index i, the pattern ByteString pat is split at that index,
 293 | ||| returning the prefix and suffix as a pair (before, after).
 294 | |||
 295 | ||| If the pattern does not occur in the target, (pat, empty) is returned.
 296 | ||| In other words, the entire pattern becomes the “before” part and the
 297 | ||| “after” part is an empty ByteString.
 298 | |||
 299 | export
 300 | breakKMP :  (pat : ByteString)
 301 |          -> (target : ByteString)
 302 |          -> {0 prfpat : So (not $ null pat)}
 303 |          -> {0 prftarget : So (not $ null target)}
 304 |          -> {0 prflength : So ((length target) >= (length pat))}
 305 |          -> F1 s (Maybe (ByteString, ByteString))
 306 | breakKMP pat target {prfpat} {prftarget} {prflength} t =
 307 |    let matcher'   # t := matcher False pat [target] t
 308 |        Just matcher'' := matcher'
 309 |          | Nothing =>
 310 |              Nothing # t
 311 |        (i :: _)       := matcher''
 312 |          | [] =>
 313 |              Just (target, empty) # t
 314 |        target'        := splitAt (cast {to=Nat} i) target
 315 |        Just target''  := target'
 316 |          | Nothing =>
 317 |              Nothing # t
 318 |      in Just target'' # t
 319 | 
 320 | ||| Splits a ByteString after the first match of pat in target.
 321 | |||
 322 | ||| This function uses the Knuth-Morris-Pratt matcher (with overlap = False) to
 323 | ||| find the earliest occurrence of pat in target.  If the pattern is
 324 | ||| found at index i, this function splits pat at position i + length pat,
 325 | ||| producing a pair (before, after) that places the entire matched region
 326 | ||| into the prefix.
 327 | |||
 328 | ||| If the pattern does not occur in target, the function returns
 329 | ||| (pat, empty), the entire pattern is the “before” substring, and the
 330 | ||| suffix is empty.
 331 | |||
 332 | export
 333 | breakAfterKMP :  (pat : ByteString)
 334 |               -> (target : ByteString)
 335 |               -> {0 prfpat : So (not $ null pat)}
 336 |               -> {0 prftarget : So (not $ null target)}
 337 |               -> {0 prflength : So ((length target) >= (length pat))}
 338 |               -> F1 s (Maybe (ByteString, ByteString))
 339 | breakAfterKMP pat target {prfpat} {prftarget} {prflength} t =
 340 |    let matcher'   # t := matcher False pat [target] t
 341 |        Just matcher'' := matcher'
 342 |          | Nothing =>
 343 |              Nothing # t
 344 |        (i :: _)       := matcher''
 345 |          | [] =>
 346 |              Just (target, empty) # t
 347 |        target'        := splitAt (plus (cast {to=Nat} i) (length pat)) target
 348 |        Just target''  := target'
 349 |          | Nothing =>
 350 |              Nothing # t
 351 |      in Just target'' # t
 352 | 
 353 | ||| Splits a ByteString into a list of pieces according to repeated
 354 | ||| matches of target, keeping the matching prefix of pat
 355 | ||| at the front of each produced chunk.
 356 | |||
 357 | ||| This function repeatedly searches target for occurrences of pat
 358 | ||| (using the Knuth-Morris-Pratt matcher with overlap = False).  Each time a
 359 | ||| match is found at index i, the prefix of pat up to i + length pat
 360 | ||| is emitted as the next chunk, and the function continues processing the
 361 | ||| remaining suffix of pat.
 362 | |||
 363 | ||| Unlike breakKMP or breakAfterKMP, this function performs repeated
 364 | ||| splitting until the entire pattern has been consumed, producing a
 365 | ||| list of ByteStrings.
 366 | |||
 367 | export
 368 | splitKeepFrontKMP :  (pat : ByteString)
 369 |                   -> (target : ByteString)
 370 |                   -> {0 prfpat : So (not $ null pat)}
 371 |                   -> {0 prftarget : So (not $ null target)}
 372 |                   -> {0 prflength : So ((length target) >= (length pat))}
 373 |                   -> F1 s (Maybe (List ByteString))
 374 | splitKeepFrontKMP pat target {prfpat} {prftarget} {prflength} t =
 375 |   let splitter'   # t := splitter pat target Lin t
 376 |       Just splitter'' := splitter'
 377 |         | Nothing =>
 378 |             Nothing # t
 379 |     in Just (splitter'' <>> []) # t
 380 |   where
 381 |     psSplitter :  (pat : ByteString)
 382 |                -> (target : ByteString)
 383 |                -> (final : SnocList ByteString)
 384 |                -> F1 s (Maybe (SnocList ByteString))
 385 |     psSplitter pat target final t =
 386 |       let matcher'   # t := matcher False pat [(drop (length pat) target)] t
 387 |           Just matcher'' := matcher'
 388 |             | Nothing =>
 389 |                 Nothing # t
 390 |           (i :: _)       := matcher''
 391 |             | [] =>
 392 |                 let final' := final :< target
 393 |                   in Just final' # t
 394 |           length'        := plus (cast {to=Nat} i) (length pat)
 395 |           final'         := final :< (take length' target)
 396 |         in assert_total (psSplitter pat (drop length' target) final' t)
 397 |     splitter :  (pat : ByteString)
 398 |              -> (target : ByteString)
 399 |              -> (final : SnocList ByteString)
 400 |              -> F1 s (Maybe (SnocList ByteString))
 401 |     splitter pat target final t =
 402 |       let matcher'   # t := matcher False pat [target] t
 403 |           Just matcher'' := matcher'
 404 |             | Nothing =>
 405 |                 Nothing # t
 406 |           (i :: _)       := matcher''
 407 |             | [] =>
 408 |                 let final' := final :< target
 409 |                   in Just final' # t
 410 |           False          := i == Z
 411 |             | True =>
 412 |                 assert_total (psSplitter pat target final t)
 413 |           final'         := final :< (take (cast {to=Nat} i) target)
 414 |         in assert_total (psSplitter pat (drop (cast {to=Nat} i) target) final' t)
 415 | 
 416 | ||| Splits a ByteString into a list of pieces according to repeated
 417 | ||| matches of pat inside target, keeping the matching
 418 | ||| suffix of pat at the end of each produced chunk.
 419 | |||
 420 | ||| This function repeatedly searches target for occurrences of pat
 421 | ||| (using the Knuth-Morris-Pratt matcher with overlap = False).  Each time a
 422 | ||| match is found at index i, the next chunk emitted is the prefix of
 423 | ||| target of length i + length pat, which includes the entire matched
 424 | ||| occurrence of pat at its end.
 425 | |||
 426 | ||| After emitting this chunk, the function continues splitting the
 427 | ||| remainder of target until all input has been consumed.
 428 | |||
 429 | ||| Unlike splitKeepFrontKMP, which keeps the matched prefix of pat
 430 | ||| at the front of each chunk, splitKeepEndKMP ensures the match
 431 | ||| appears at the end of each chunk.
 432 | |||
 433 | ||| If pat does not occur in target, the result is a singleton list
 434 | ||| containing the original target.
 435 | |||
 436 | export
 437 | splitKeepEndKMP :  (pat : ByteString)
 438 |                 -> (target : ByteString)
 439 |                 -> {0 prfpat : So (not $ null pat)}
 440 |                 -> {0 prftarget : So (not $ null target)}
 441 |                 -> {0 prflength : So ((length target) >= (length pat))}
 442 |                 -> F1 s (Maybe (List ByteString))
 443 | splitKeepEndKMP pat target {prfpat} {prftarget} {prflength} t =
 444 |   let splitter'   # t := splitter pat target Lin t
 445 |       Just splitter'' := splitter'
 446 |         | Nothing =>
 447 |             Nothing # t
 448 |     in Just (splitter'' <>> []) # t
 449 |   where
 450 |     splitter :  (pat : ByteString)
 451 |              -> (target : ByteString)
 452 |              -> (final : SnocList ByteString)
 453 |              -> F1 s (Maybe (SnocList ByteString))
 454 |     splitter pat target final t =
 455 |       let matcher'   # t := matcher False pat [target] t
 456 |           Just matcher'' := matcher'
 457 |             | Nothing =>
 458 |                 Nothing # t
 459 |           (i :: _)       := matcher''
 460 |             | [] =>
 461 |                 let final' := final :< target
 462 |                   in Just final' # t
 463 |           length'        := plus (cast {to=Nat} i) (length pat)
 464 |           final'         := final :< (take length' target)
 465 |         in assert_total (splitter pat (drop length' target) final' t)
 466 | 
 467 | ||| Splits a ByteString into a list of pieces according to repeated
 468 | ||| matches of pat inside target, dropping each matched
 469 | ||| occurrence from the output entirely.
 470 | |||
 471 | ||| This function repeatedly searches target for occurrences of pat
 472 | ||| (using the Knuth-Morris-Pratt matcher with overlap = False).  Each time a
 473 | ||| match is found at index i, the prefix of target of length i
 474 | ||| (that is, the portion preceding the match) is emitted as the next
 475 | ||| chunk.  The matched substring itself is not included.
 476 | |||
 477 | ||| After emitting this prefix, the function continues splitting the
 478 | ||| remainder of target, skipping over the full match of length
 479 | ||| i + length pat.  This process continues until the entire target
 480 | ||| has been consumed.
 481 | |||
 482 | ||| Unlike splitKeepFrontKMP and splitKeepEndKMP, which include the
 483 | ||| matched pattern in each emitted chunk, splitDropKMP removes all
 484 | ||| occurrences of pat from the output.
 485 | |||
 486 | ||| If pat does not occur in target, the result is a singleton list
 487 | ||| containing the original target.
 488 | |||
 489 | export
 490 | splitDropKMP :  (pat : ByteString)
 491 |              -> (target : ByteString)
 492 |              -> {0 prfpat : So (not $ null pat)}
 493 |              -> {0 prftarget : So (not $ null target)}
 494 |              -> {0 prflength : So ((length target) >= (length pat))}
 495 |              -> F1 s (Maybe (List ByteString))
 496 | splitDropKMP pat target {prfpat} {prftarget} {prflength} t =
 497 |   let splitter'   # t := splitter pat target Lin t
 498 |       Just splitter'' := splitter'
 499 |         | Nothing =>
 500 |             Nothing # t
 501 |     in Just (splitter'' <>> []) # t 
 502 |   where
 503 |     splitter :  (pat : ByteString)
 504 |              -> (target : ByteString)
 505 |              -> (final : SnocList ByteString)
 506 |              -> F1 s (Maybe (SnocList ByteString))
 507 |     splitter pat target final t =
 508 |       let matcher'   # t := matcher False pat [target] t
 509 |           Just matcher'' := matcher'
 510 |             | Nothing =>
 511 |                 Nothing # t
 512 |           (i :: _)       := matcher''
 513 |             | [] =>
 514 |                 let final' := final :< target
 515 |                   in Just final' # t
 516 |           length'        := plus (cast {to=Nat} i) (length pat)
 517 |           final'         := final :< (take (cast {to=Nat} i) target)
 518 |         in assert_total (splitter pat (drop length' target) final' t)
 519 | 
 520 | ||| Replaces all non-overlapping occurrences of a pattern in a ByteString
 521 | ||| using the Knuth-Morris-Pratt matcher.
 522 | |||
 523 | ||| This function repeatedly searches target for occurrences of pat
 524 | ||| (using matcher False). Each time a match is found at index i:
 525 | |||
 526 | ||| * If i == 0, the match is at the current position. The matched
 527 | |||   segment is dropped and sub is appended to the result (unless
 528 | |||   sub is empty, in which case nothing is appended).
 529 | |||
 530 | ||| * If i > 0, the prefix take i target is appended to the result,
 531 | |||   followed by sub (unless sub is empty). The matched segment is
 532 | |||   then dropped and processing continues on the remaining suffix.
 533 | |||
 534 | ||| If no further matches are found, the remaining target is appended
 535 | ||| unchanged and the result is returned.
 536 | |||
 537 | ||| The result is accumulated via a `SnocList` and returned as a `List
 538 | ||| ByteString`, preserving left-to-right order of the produced chunks.
 539 | |||
 540 | export
 541 | replaceKMP :  (pat : ByteString)
 542 |            -> (sub : ByteString)
 543 |            -> (target : ByteString)
 544 |            -> {0 prfpat : So (not $ null pat)}
 545 |            -> {0 prftarget : So (not $ null target)}
 546 |            -> {0 prflength : So ((length target) >= (length pat))}
 547 |            -> F1 s (Maybe (List ByteString))
 548 | replaceKMP pat sub target {prfpat} {prftarget} {prflength} t =
 549 |   let replacer'   # t := replacer pat sub target Lin t
 550 |       Just replacer'' := replacer'
 551 |         | Nothing =>
 552 |             Nothing # t
 553 |     in Just (replacer'' <>> []) # t
 554 |   where
 555 |     replacer :  (pat : ByteString)
 556 |              -> (sub : ByteString)
 557 |              -> (target : ByteString)
 558 |              -> (final : SnocList ByteString)
 559 |              -> F1 s (Maybe (SnocList ByteString))
 560 |     replacer pat sub target final t =
 561 |       let matcher'   # t := matcher False pat [target] t
 562 |           Just matcher'' := matcher'
 563 |             | Nothing =>
 564 |                 Nothing # t
 565 |           (i :: _)       := matcher''
 566 |             | [] =>
 567 |                 let final' := final :< target
 568 |                   in Just final' # t
 569 |           Z              := i
 570 |             | _ =>
 571 |                let False := null sub
 572 |                      | True =>
 573 |                          let length' := plus (cast {to=Nat} i) (length pat)
 574 |                              final'  := final :< (take (cast {to=Nat} i) target)
 575 |                            in assert_total (replacer pat sub (drop length' target) final' t)
 576 |                    length' := plus (cast {to=Nat} i) (length pat)
 577 |                    final'  := final :< (take (cast {to=Nat} i) target) :< sub
 578 |                  in assert_total (replacer pat sub (drop length' target) final' t)
 579 |           False          := null sub
 580 |             | True =>
 581 |                  assert_total (replacer pat sub (drop (length pat) target) final t)
 582 |           final' := final :< sub
 583 |         in assert_total (replacer pat sub (drop (length pat) target) final') t
 584 |