
   0 | ||| Boyer-Moore search of ByteStrings
   1 | module Data.ByteString.Search.BoyerMoore
   2 | 
   3 | import Data.Array.Core
   4 | import Data.Array.Mutable
   5 | import Data.Bits
   6 | import Data.ByteString
   7 | import Data.ByteString.Search.BoyerMoore.Internal
   8 | import Data.Enum
   9 | import Data.Linear.Ref1
  10 | import Data.So
  11 | 
  12 | %hide Data.Buffer.Core.get
  13 | %hide Data.Buffer.Core.set
  14 | 
  15 | %default total
  16 | 
  17 | ||| Returns a list of starting positions of a pattern `ByteString`
  18 | ||| (0-based) across a target `ByteString`.
  19 | |||
  20 | ||| Boyer–Moore preprocessing is performed once before scanning begins.
  21 | ||| The bad-character table is indexed directly by `Bits8`, while the
  22 | ||| good-suffix table is indexed by bounded `PatternIndex` values.
  23 | |||
  24 | ||| Consequently, mismatch handling performs no `tryNatToFin` or equivalent
  25 | ||| dynamic array-index conversion before reading either preprocessing table.
  26 | |||
  27 | ||| Pattern positions remain represented by `Int` because the Boyer–Moore
  28 | ||| search algorithm naturally performs signed arithmetic while scanning the
  29 | ||| pattern from right to left.
  30 | |||
  31 | private
  32 | matcher :  Bool
  33 |         -> ByteString
  34 |         -> ByteString
  35 |         -> F1 s (Maybe (List Int))
  36 | matcher overlap pat target t =
  37 |   let patlen                                           := length pat
  38 |       targetlen                                        := length target
  39 |       patlenint                                        := cast {to=Int} patlen
  40 |       patend                                           := patlenint - 1
  41 |       strend                                           := (cast {to=Int} targetlen) - 1
  42 |       maxdiff                                          := cast {to=Int} (minus targetlen patlen)
  43 |       False                                            := patlen == S Z
  44 |         | True =>
  45 |             let Just patzero  := index Z pat
  46 |                   | Nothing =>
  47 |                       Nothing # t
  48 |                 Just headelem := elemIndex patzero target
  49 |                   | Nothing =>
  50 |                       Nothing # t
  51 |               in Just ((cast {to=Int} headelem) :: []) # t
  52 |       Yes patprf := decSo (not $ null pat)
  53 |         | No _ =>
  54 |             Nothing # t
  55 |       occurrencesarr                               # t := occurrences pat {prf = patprf} t
  56 |       Just occurrencesarr'                             := occurrencesarr
  57 |         | Nothing =>
  58 |             Nothing # t
  59 |       suffixshiftsarr                              # t := suffixShifts pat {prf = patprf} t
  60 |       Just (MkBMPatternTable stspace suffixshiftsarr') := suffixshiftsarr
  61 |         | Nothing =>
  62 |             Nothing # t
  63 |       zero                                             : PatternIndex stspace.size
  64 |       zero                                             := I 0 {prf = stspace.sizePositive}
  65 |       suffixzero                                   # t := bmGet suffixshiftsarr' zero t
  66 |       Just patlast                                     := index (minus patlen 1) pat
  67 |         | Nothing =>
  68 |             Nothing # t
  69 |       matches                                      # t := checkEnd stspace patend Lin patend strend maxdiff patlenint patlast suffixzero occurrencesarr' suffixshiftsarr' t
  70 |       Just matches'                                    := matches
  71 |         | Nothing =>
  72 |             Nothing # t
  73 |     in Just (matches' <>> []) # t
  74 |   where
  75 |     ||| Construct a bounded Boyer–Moore pattern-table index from a pattern
  76 |     ||| position whose bounds are already established by the matcher control
  77 |     ||| flow.
  78 |     |||
  79 |     ||| The proof is erased at runtime. This helper is used only at points
  80 |     ||| where the Boyer–Moore invariants guarantee:
  81 |     |||
  82 |     |||     0 <= idx < pattern length
  83 |     |||
  84 |     ||| and therefore performs no dynamic bounds validation.
  85 |     |||
  86 |     %inline
  87 |     patternIndex :  (stspace : BMPatternSpace)
  88 |                  -> Int
  89 |                  -> PatternIndex stspace.size
  90 |     patternIndex stspace idx =
  91 |       I (cast idx) {prf = believe_me ()}
  92 |     mutual
  93 |       ||| Examine the final byte of the pattern at the current alignment.
  94 |       |||
  95 |       ||| A mismatch on the final byte uses only the bad-character table.
  96 |       ||| Since that table is indexed directly by `Bits8`, no intermediate
  97 |       ||| `Nat` or `Fin` conversion is required.
  98 |       |||
  99 |       checkEnd :  (stspace : BMPatternSpace)
 100 |                -> (stri : Int)
 101 |                -> (final : SnocList Int)
 102 |                -> (patend : Int)
 103 |                -> (strend : Int)
 104 |                -> (maxdiff : Int)
 105 |                -> (patlen : Int)
 106 |                -> (patlast : Bits8)
 107 |                -> (suffixzero : Int)
 108 |                -> (occurrencesarr : OccurrenceTable s)
 109 |                -> (suffixshiftsarr : BMIntTable s stspace.size)
 110 |                -> F1 s (Maybe (SnocList Int))
 111 |       checkEnd stspace stri final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t =
 112 |           let False           := strend < stri
 113 |                 | True =>
 114 |                     Just final # t
 115 |               strinat         := cast {to=Nat} stri
 116 |               Just targetbyte := index strinat target
 117 |                 | Nothing =>
 118 |                     Nothing # t
 119 |               False           := targetbyte == patlast
 120 |                 | True =>
 121 |                     assert_total (findMatch stspace (stri - patend) (patend - 1) final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 122 |               occur       # t := occurrence occurrencesarr targetbyte t
 123 |               newtarget       := stri + patend + occur
 124 |             in assert_total (checkEnd stspace newtarget final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 125 |       ||| Compare pattern and target bytes from right to left at the current
 126 |       ||| Boyer–Moore alignment.
 127 |       |||
 128 |       ||| On mismatch, the bad-character shift is read directly using the
 129 |       ||| mismatched `Bits8`, while the good-suffix shift is read using a
 130 |       ||| bounded `PatternIndex`.
 131 |       |||
 132 |       ||| Neither preprocessing-table lookup requires `tryNatToFin`,
 133 |       ||| `tryIndex`, or another runtime bounds conversion.
 134 |       |||
 135 |       findMatch :  (stspace : BMPatternSpace)
 136 |                 -> (diff : Int)
 137 |                 -> (pati : Int)
 138 |                 -> (final : SnocList Int)
 139 |                 -> (patend : Int)
 140 |                 -> (strend : Int)
 141 |                 -> (maxdiff : Int)
 142 |                 -> (patlen : Int)
 143 |                 -> (patlast : Bits8)
 144 |                 -> (suffixzero : Int)
 145 |                 -> (occurrencesarr : OccurrenceTable s)
 146 |                 -> (suffixshiftsarr : BMIntTable s stspace.size)
 147 |                 -> F1 s (Maybe (SnocList Int))
 148 |       findMatch stspace diff pati final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t =
 149 |         let targetidx       := diff + pati
 150 |             targetnat       := cast {to=Nat} targetidx
 151 |             patnat          := cast {to=Nat} pati
 152 |             Just targetbyte := index targetnat target
 153 |               | Nothing =>
 154 |                   Nothing # t
 155 |             Just patbyte    := index patnat pat
 156 |               | Nothing =>
 157 |                   Nothing # t
 158 |             False           := targetbyte == patbyte
 159 |               | True =>
 160 |                   let False := pati == 0
 161 |                         | True =>
 162 |                             let final' := final :< diff
 163 |                                 False  := overlap
 164 |                                   | True =>
 165 |                                       let diff' := diff + suffixzero
 166 |                                           False := maxdiff < diff'
 167 |                                             | True =>
 168 |                                                 Just final' # t
 169 |                                           False := suffixzero == patlen
 170 |                                             | True =>
 171 |                                                 assert_total (checkEnd stspace (diff' + patend) final' patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 172 |                                         in assert_total (afterMatch stspace diff' patend final' patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 173 |                                 diff'  := diff + patlen
 174 |                                 False  := maxdiff < diff'
 175 |                                   | True =>
 176 |                                       Just final' # t
 177 |                               in assert_total (checkEnd stspace (diff' + patend) final' patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 178 |                     in assert_total (findMatch stspace diff (pati - 1) final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 179 |             occur       # t := occurrence occurrencesarr targetbyte t
 180 |             patidx          := patternIndex stspace pati
 181 |             suff        # t := bmGet suffixshiftsarr patidx t 
 182 |             shift           := max (pati + occur) suff
 183 |             diff'           := diff + shift
 184 |             False           := maxdiff < diff'
 185 |               | True =>
 186 |                   Just final # t
 187 |           in assert_total (checkEnd stspace (diff' + patend) final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 188 |       ||| Continue matching after an overlapping full match.
 189 |       |||
 190 |       ||| The already-matched suffix implied by `suffixzero` is retained and
 191 |       ||| only the remaining prefix is compared.
 192 |       |||
 193 |       ||| As in `findMatch`, bad-character lookup is directly indexed by
 194 |       ||| `Bits8`, while good-suffix lookup uses a bounded `PatternIndex`.
 195 |       |||
 196 |       afterMatch :  (stspace : BMPatternSpace)
 197 |                  -> (diff : Int)
 198 |                  -> (pati : Int)
 199 |                  -> (final : SnocList Int)
 200 |                  -> (patend : Int)
 201 |                  -> (strend : Int)
 202 |                  -> (maxdiff : Int)
 203 |                  -> (patlen : Int)
 204 |                  -> (patlast : Bits8)
 205 |                  -> (suffixzero : Int)
 206 |                  -> (occurrencesarr : OccurrenceTable s)
 207 |                  -> (suffixshiftsarr : BMIntTable s stspace.size)
 208 |                  -> F1 s (Maybe (SnocList Int))
 209 |       afterMatch stspace diff pati final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t =
 210 |           let targetidx       := diff + pati
 211 |               targetnat       := cast {to=Nat} targetidx
 212 |               patnat          := cast {to=Nat} pati
 213 |               Just targetbyte := index targetnat target
 214 |                 | Nothing =>
 215 |                     Nothing # t
 216 |               Just patbyte    := index patnat pat
 217 |                 | Nothing =>
 218 |                     Nothing # t
 219 |               False           := targetbyte == patbyte
 220 |                 | True =>
 221 |                     let kept  := patlen - suffixzero
 222 |                         False := pati == kept
 223 |                           | True =>
 224 |                               let final' := final :< diff
 225 |                                   diff'  := diff + suffixzero
 226 |                                   False  := maxdiff < diff'
 227 |                                     | True =>
 228 |                                         Just final' # t
 229 |                                 in assert_total (afterMatch stspace diff' patend final' patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 230 |                       in assert_total (afterMatch stspace diff (pati - 1) final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 231 |               False           := pati == patend
 232 |                 | True =>
 233 |                     let occur # t := occurrence occurrencesarr targetbyte t
 234 |                         nextend   := diff + (2 * patend) + occur
 235 |                       in assert_total (checkEnd stspace nextend final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 236 |               occur       # t := occurrence occurrencesarr targetbyte t
 237 |               patidx          := patternIndex stspace pati
 238 |               goodshift   # t := bmGet suffixshiftsarr patidx t
 239 |               badshift        := pati + occur
 240 |               diff'           := diff + max badshift goodshift
 241 |               False           := maxdiff < diff'
 242 |                 | True =>
 243 |                     Just final # t
 244 |             in assert_total (checkEnd stspace (diff + patend) final patend strend maxdiff patlen patlast suffixzero occurrencesarr suffixshiftsarr t)
 245 |                         
 246 | ||| Performs a string search on a `ByteString` utilizing a Boyer-Moore algorithm.
 247 | |||
 248 | ||| This function finds all (0-based) starting indices of the non-empty pattern `ByteString`
 249 | ||| pat within the non-empty target `ByteString`.
 250 | |||
 251 | ||| Example:
 252 | |||
 253 | ||| | pat  | target     |
 254 | ||| | ---- | ---------- |
 255 | ||| | "AN" | "ANPANMAN" |
 256 | |||
 257 | ||| | s | window T[s..s+1] | comparisons (right→left)      | result    |                  bad-char |     good-suffix | chosen shift | next s |
 258 | ||| | - | ---------------- | ----------------------------- | --------- | ------------------------- | --------------- | ------------ | ------ |
 259 | ||| | 0 | **AN**           | j=1: N==N ✓ → j=0: A==A ✓     | **MATCH** |                         — | (after match) 2 |            2 |      2 |
 260 | ||| | 1 | N**P**           | j=1: N vs P → mismatch at j=1 | mismatch  | lastOcc('P')=-1 → bad = 2 | suffShifts[1]=1 |        **2** |      3 |
 261 | ||| | 2 | P**A**           | j=1: N vs A → mismatch at j=1 | mismatch  |  lastOcc('A')=0 → bad = 1 |        good = 1 |        **1** |      3 |
 262 | ||| | 3 | **AN**           | j=1: N==N ✓ → j=0: A==A ✓     | **MATCH** |                         — | (after match) 2 |            2 |      5 |
 263 | ||| | 4 | N**M**           | j=1: N vs M → mismatch at j=1 | mismatch  | lastOcc('M')=-1 → bad = 2 |        good = 1 |        **2** |      6 |
 264 | ||| | 5 | M**A**           | j=1: N vs A → mismatch at j=1 | mismatch  |  lastOcc('A')=0 → bad = 1 |        good = 1 |        **1** |      6 |
 265 | ||| | 6 | **AN**           | j=1: N==N ✓ → j=0: A==A ✓     | **MATCH** |                         — | (after match) 2 |            2 |      — |
 266 | |||
 267 | ||| matchBM "AN" "ANPANMAN" => Just [0, 3, 6]
 268 | |||
 269 | export
 270 | matchBM :  (pat : ByteString)
 271 |         -> (target : ByteString)
 272 |         -> {0 prfpat : So (not $ null pat)}
 273 |         -> {0 prftarget : So (not $ null target)}
 274 |         -> {0 prflength : So ((length target) >= (length pat))}
 275 |         -> F1 s (Maybe (List Int))
 276 | matchBM pat target {prfpat} {prftarget} {prflength} t =
 277 |   let matcher' # t   := matcher False pat target t
 278 |       Just matcher'' := matcher'
 279 |         | Nothing =>
 280 |             Nothing # t
 281 |     in Just matcher'' # t
 282 | 
 283 | ||| Performs a string search on a `ByteString` utilizing a Boyer-Moore algorithm.
 284 | |||
 285 | ||| This function finds all (0-based) indices (possibly overlapping)
 286 | ||| of the non-empty pattern `ByteString` pat
 287 | ||| within the non-empty target `ByteString`.
 288 | |||
 289 | ||| Example:
 290 | |||
 291 | ||| | pat   | target      |
 292 | ||| | ----- | ----------- |
 293 | ||| | "ABC" | "ABCABCABC" |
 294 | |||
 295 | ||| | Align s   | Window       | Comparison Result                  | Chosen Shift                         | Next s   |
 296 | ||| | --------- | ------------ | ---------------------------------- | ------------------------------------ | -------- |
 297 | ||| |     0     | **ABCABC**   | MATCH                              | good-suffix after full match = 3     |     3    |
 298 | ||| |     1     | A**BCABCA**  | MISMATCH on last char (`C` vs `A`) | max(bad=2, good=1) = 2               |     3    |
 299 | ||| |     2     | AB**CABCAA** | MISMATCH on last char (`C` vs `B`) | max(bad=1, good=1) = 1               |     3    |
 300 | ||| |     3     | ABC**ABC**   | MATCH                              | (would shift 3 again)                |     —    |
 301 | ||| 
 302 | ||| indicesBM "ABCABC" "ABCABCABC" => Just [0, 3]
 303 | |||
 304 | export
 305 | indicesBM :  (pat : ByteString)
 306 |           -> (target : ByteString)
 307 |           -> {0 prfpat : So (not $ null pat)}
 308 |           -> {0 prftarget : So (not $ null target)}
 309 |           -> {0 prflength : So ((length target) >= (length pat))}
 310 |           -> F1 s (Maybe (List Int))
 311 | indicesBM pat target {prfpat} {prftarget} {prflength} t =
 312 |   let matcher'   # t := matcher True pat target t
 313 |       Just matcher'' := matcher'
 314 |         | Nothing =>
 315 |             Nothing # t
 316 |     in Just matcher'' # t
 317 | 
 318 | ||| Splits a ByteString at the first match of pat in target.
 319 | |||
 320 | ||| This function uses the Boyer–Moore matcher (with overlap = False) to
 321 | ||| locate the earliest occurrence of pat in target.  If the pattern is
 322 | ||| found at index i, the pattern ByteString pat is split at that index,
 323 | ||| returning the prefix and suffix as a pair (before, after).
 324 | |||
 325 | ||| If the pattern does not occur in the target, (pat, empty) is returned.
 326 | ||| In other words, the entire pattern becomes the “before” part and the
 327 | ||| “after” part is an empty ByteString.
 328 | |||
 329 | export
 330 | breakBM :  (pat : ByteString)
 331 |         -> (target : ByteString)
 332 |         -> {0 prfpat : So (not $ null pat)}
 333 |         -> {0 prftarget : So (not $ null target)}
 334 |         -> {0 prflength : So ((length target) >= (length pat))}
 335 |         -> F1 s (Maybe (ByteString, ByteString))
 336 | breakBM pat target {prfpat} {prftarget} {prflength} t =
 337 |    let matcher'   # t := matcher False pat target t
 338 |        Just matcher'' := matcher'
 339 |          | Nothing =>
 340 |              Nothing # t
 341 |        (i :: _)       := matcher''
 342 |          | [] =>
 343 |              Just (target, empty) # t
 344 |        target'        := splitAt (cast {to=Nat} i) target
 345 |        Just target''  := target'
 346 |          | Nothing =>
 347 |              Nothing # t
 348 |      in Just target'' # t
 349 | 
 350 | ||| Splits a ByteString after the first match of pat in target.
 351 | |||
 352 | ||| This function uses the Boyer–Moore matcher (with overlap = False) to
 353 | ||| find the earliest occurrence of pat in target.  If the pattern is
 354 | ||| found at index i, this function splits pat at position i + length pat,
 355 | ||| producing a pair (before, after) that places the entire matched region
 356 | ||| into the prefix.
 357 | |||
 358 | ||| If the pattern does not occur in target, the function returns
 359 | ||| (pat, empty), the entire pattern is the “before” substring, and the
 360 | ||| suffix is empty.
 361 | |||
 362 | export
 363 | breakAfterBM :  (pat : ByteString)
 364 |              -> (target : ByteString)
 365 |              -> {0 prfpat : So (not $ null pat)}
 366 |              -> {0 prftarget : So (not $ null target)}
 367 |              -> {0 prflength : So ((length target) >= (length pat))}
 368 |              -> F1 s (Maybe (ByteString, ByteString))
 369 | breakAfterBM pat target {prfpat} {prftarget} {prflength} t =
 370 |    let matcher'   # t := matcher False pat target t
 371 |        Just matcher'' := matcher'
 372 |          | Nothing =>
 373 |              Nothing # t
 374 |        (i :: _)       := matcher''
 375 |          | [] =>
 376 |              Just (target, empty) # t
 377 |        target'        := splitAt (plus (cast {to=Nat} i) (length pat)) target
 378 |        Just target''  := target'
 379 |          | Nothing =>
 380 |              Nothing # t
 381 |      in Just target'' # t
 382 | 
 383 | ||| Splits a ByteString into a list of pieces according to repeated
 384 | ||| matches of target, keeping the matching prefix of pat
 385 | ||| at the front of each produced chunk.
 386 | |||
 387 | ||| This function repeatedly searches target for occurrences of pat
 388 | ||| (using the Boyer–Moore matcher with overlap = False).  Each time a
 389 | ||| match is found at index i, the prefix of pat up to i + length pat
 390 | ||| is emitted as the next chunk, and the function continues processing the
 391 | ||| remaining suffix of pat.
 392 | |||
 393 | ||| Unlike breakBM or breakAfterBM, this function performs repeated
 394 | ||| splitting until the entire pattern has been consumed, producing a
 395 | ||| list of ByteStrings.
 396 | |||
 397 | export
 398 | splitKeepFrontBM :  (pat : ByteString)
 399 |                  -> (target : ByteString)
 400 |                  -> {0 prfpat : So (not $ null pat)}
 401 |                  -> {0 prftarget : So (not $ null target)}
 402 |                  -> {0 prflength : So ((length target) >= (length pat))}
 403 |                  -> F1 s (Maybe (List ByteString))
 404 | splitKeepFrontBM pat target {prfpat} {prftarget} {prflength} t =
 405 |   let splitter'   # t := splitter pat target Lin t
 406 |       Just splitter'' := splitter'
 407 |         | Nothing =>
 408 |             Nothing # t
 409 |     in Just (splitter'' <>> []) # t
 410 |   where
 411 |     psSplitter :  (pat : ByteString)
 412 |                -> (target : ByteString)
 413 |                -> (final : SnocList ByteString)
 414 |                -> F1 s (Maybe (SnocList ByteString))
 415 |     psSplitter pat target final t =
 416 |       let matcher'   # t := matcher False pat (drop (length pat) target) t
 417 |           Just matcher'' := matcher'
 418 |             | Nothing =>
 419 |                 Nothing # t
 420 |           (i :: _)       := matcher''
 421 |             | [] =>
 422 |                 let final' := final :< target
 423 |                   in Just final' # t
 424 |           length'        := plus (cast {to=Nat} i) (length pat)
 425 |           final'         := final :< (take length' target)
 426 |         in assert_total (psSplitter pat (drop length' target) final' t) 
 427 |     splitter :  (pat : ByteString)
 428 |              -> (target : ByteString)
 429 |              -> (final : SnocList ByteString)
 430 |              -> F1 s (Maybe (SnocList ByteString))
 431 |     splitter pat target final t =
 432 |       let matcher'   # t := matcher False pat target t
 433 |           Just matcher'' := matcher'
 434 |             | Nothing =>
 435 |                 Nothing # t
 436 |           (i :: _)       := matcher''
 437 |             | [] =>
 438 |                 let final' := final :< target
 439 |                   in Just final' # t
 440 |           False          := i == 0
 441 |             | True =>
 442 |                 assert_total (psSplitter pat target final t)
 443 |           final'         := final :< (take (cast {to=Nat} i) target)
 444 |         in assert_total (psSplitter pat (drop (cast {to=Nat} i) target) final' t) 
 445 | 
 446 | ||| Splits a ByteString into a list of pieces according to repeated
 447 | ||| matches of pat inside target, keeping the matching
 448 | ||| suffix of pat at the end of each produced chunk.
 449 | |||
 450 | ||| This function repeatedly searches target for occurrences of pat
 451 | ||| (using the Boyer–Moore matcher with overlap = False).  Each time a
 452 | ||| match is found at index i, the next chunk emitted is the prefix of
 453 | ||| target of length i + length pat, which includes the entire matched
 454 | ||| occurrence of pat at its end.
 455 | |||
 456 | ||| After emitting this chunk, the function continues splitting the
 457 | ||| remainder of target until all input has been consumed.
 458 | |||
 459 | ||| Unlike splitKeepFrontBM, which keeps the matched prefix of pat
 460 | ||| at the front of each chunk, splitKeepEndBM ensures the match
 461 | ||| appears at the end of each chunk.
 462 | |||
 463 | ||| If pat does not occur in target, the result is a singleton list
 464 | ||| containing the original target.
 465 | |||
 466 | export
 467 | splitKeepEndBM :  (pat : ByteString)
 468 |                -> (target : ByteString)
 469 |                -> {0 prfpat : So (not $ null pat)}
 470 |                -> {0 prftarget : So (not $ null target)}
 471 |                -> {0 prflength : So ((length target) >= (length pat))}
 472 |                -> F1 s (Maybe (List ByteString))
 473 | splitKeepEndBM pat target {prfpat} {prftarget} {prflength} t =
 474 |   let splitter'   # t := splitter pat target Lin t
 475 |       Just splitter'' := splitter'
 476 |         | Nothing =>
 477 |             Nothing # t
 478 |     in Just (splitter'' <>> []) # t
 479 |   where
 480 |     splitter :  (pat : ByteString)
 481 |              -> (target : ByteString)
 482 |              -> (final : SnocList ByteString)
 483 |              -> F1 s (Maybe (SnocList ByteString))
 484 |     splitter pat target final t =
 485 |       let matcher'   # t := matcher False pat target t
 486 |           Just matcher'' := matcher'
 487 |             | Nothing =>
 488 |                 Nothing # t
 489 |           (i :: _)       := matcher''
 490 |             | [] =>
 491 |                 let final' := final :< target
 492 |                   in Just final' # t
 493 |           length'        := plus (cast {to=Nat} i) (length pat)
 494 |           final'         := final :< (take length' target)
 495 |         in assert_total (splitter pat (drop length' target) final' t)
 496 | 
 497 | ||| Splits a ByteString into a list of pieces according to repeated
 498 | ||| matches of pat inside target, dropping each matched
 499 | ||| occurrence from the output entirely.
 500 | |||
 501 | ||| This function repeatedly searches target for occurrences of pat
 502 | ||| (using the Boyer–Moore matcher with overlap = False).  Each time a
 503 | ||| match is found at index i, the prefix of target of length i
 504 | ||| (that is, the portion preceding the match) is emitted as the next
 505 | ||| chunk.  The matched substring itself is not included.
 506 | |||
 507 | ||| After emitting this prefix, the function continues splitting the
 508 | ||| remainder of target, skipping over the full match of length
 509 | ||| i + length pat.  This process continues until the entire target
 510 | ||| has been consumed.
 511 | |||
 512 | ||| Unlike splitKeepFrontBM and splitKeepEndBM, which include the
 513 | ||| matched pattern in each emitted chunk, splitDropBM removes all
 514 | ||| occurrences of pat from the output.
 515 | |||
 516 | ||| If pat does not occur in target, the result is a singleton list
 517 | ||| containing the original target.
 518 | |||
 519 | export
 520 | splitDropBM :  (pat : ByteString)
 521 |             -> (target : ByteString)
 522 |             -> {0 prfpat : So (not $ null pat)}
 523 |             -> {0 prftarget : So (not $ null target)}
 524 |             -> {0 prflength : So ((length target) >= (length pat))}
 525 |             -> F1 s (Maybe (List ByteString))
 526 | splitDropBM pat target {prfpat} {prftarget} {prflength} t =
 527 |   let splitter' # t   := splitter pat target Lin t
 528 |       Just splitter'' := splitter'
 529 |         | Nothing =>
 530 |             Nothing # t
 531 |     in Just (splitter'' <>> []) # t
 532 |   where
 533 |     splitter :  (pat : ByteString)
 534 |              -> (target : ByteString)
 535 |              -> (final : SnocList ByteString)
 536 |              -> F1 s (Maybe (SnocList ByteString))
 537 |     splitter pat target final t =
 538 |       let matcher'   # t := matcher False pat target t
 539 |           Just matcher'' := matcher'
 540 |             | Nothing =>
 541 |                 Nothing # t
 542 |           (i :: _)       := matcher''
 543 |             | [] =>
 544 |                 let final' := final :< target
 545 |                   in Just final' # t
 546 |           length'        := plus (cast {to=Nat} i) (length pat)
 547 |           final'         := final :< (take (cast {to=Nat} i) target)
 548 |         in assert_total (splitter pat (drop length' target) final' t)
 549 | 
 550 | ||| Replaces all non-overlapping occurrences of a pattern in a ByteString
 551 | ||| using the Boyer–Moore matcher.
 552 | |||
 553 | ||| This function repeatedly searches target for occurrences of pat
 554 | ||| (using matcher False). Each time a match is found at index i:
 555 | |||
 556 | ||| * If i == 0, the match is at the current position. The matched
 557 | |||   segment is dropped and sub is appended to the result (unless
 558 | |||   sub is empty, in which case nothing is appended).
 559 | |||
 560 | ||| * If i > 0, the prefix take i target is appended to the result,
 561 | |||   followed by sub (unless sub is empty). The matched segment is
 562 | |||   then dropped and processing continues on the remaining suffix.
 563 | |||
 564 | ||| If no further matches are found, the remaining target is appended
 565 | ||| unchanged and the result is returned.
 566 | |||
 567 | ||| The result is accumulated via a `SnocList` and returned as a `List
 568 | ||| ByteString`, preserving left-to-right order of the produced chunks.
 569 | |||
 570 | export
 571 | replaceBM :  (pat : ByteString)
 572 |           -> (sub : ByteString)
 573 |           -> (target : ByteString)
 574 |           -> {0 prfpat : So (not $ null pat)}
 575 |           -> {0 prftarget : So (not $ null target)}
 576 |           -> {0 prflength : So ((length target) >= (length pat))}
 577 |           -> F1 s (Maybe (List ByteString))
 578 | replaceBM pat sub target {prfpat} {prftarget} {prflength} t =
 579 |   let replacer'   # t := replacer pat sub target Lin t
 580 |       Just replacer'' := replacer'
 581 |         | Nothing =>
 582 |             Nothing # t
 583 |     in Just (replacer'' <>> []) # t
 584 |   where
 585 |     replacer :  (pat : ByteString)
 586 |              -> (sub : ByteString)
 587 |              -> (target : ByteString)
 588 |              -> (final : SnocList ByteString)
 589 |              -> F1 s (Maybe (SnocList ByteString))
 590 |     replacer pat sub target final t =
 591 |       let matcher'   # t := matcher False pat target t
 592 |           Just matcher'' := matcher'
 593 |             | Nothing =>
 594 |                 Nothing # t
 595 |           (i :: _)       := matcher''
 596 |             | [] =>
 597 |                 let final' := final :< target
 598 |                   in Just final' # t
 599 |           Z              := cast {to=Nat} i
 600 |             | _ =>
 601 |                 let False := null sub
 602 |                       | True =>
 603 |                           let length' := plus (cast {to=Nat} i) (length pat) 
 604 |                               final'  := final :< (take (cast {to=Nat} i) target)
 605 |                             in assert_total (replacer pat sub (drop length' target) final' t)
 606 |                     length' := plus (cast {to=Nat} i) (length pat) 
 607 |                     final'  := final :< (take (cast {to=Nat} i) target) :< sub
 608 |                   in assert_total (replacer pat sub (drop length' target) final' t)
 609 |           False          := null sub
 610 |             | True =>
 611 |                 assert_total (replacer pat sub (drop (length pat) target) final t)
 612 |           final'         := final :< sub
 613 |         in assert_total (replacer pat sub (drop (length pat) target) final') t
 614 |