
   0 | ||| Fast deterministic finite automaton (DFA) search of ByteStrings
   1 | module Data.ByteString.Search.DFA
   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.Internal
   8 | import Data.ByteString.Search.DFA.Types
   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 | ||| Search for occurrences of `pat` within `target` using a precomputed
  19 | ||| deterministic finite automaton.
  20 | |||
  21 | ||| When `overlap` is `True`, overlapping occurrences are retained. When it
  22 | ||| is `False`, searching resumes after the end of each complete match.
  23 | |||
  24 | ||| A single-byte pattern is handled separately using `elemIndex`, preserving
  25 | ||| the behavior of the previous implementation.
  26 | |||
  27 | ||| For patterns longer than one byte, the DFA is constructed once and the
  28 | ||| target is scanned from left to right.
  29 | |||
  30 | ||| State zero is handled specially so that target bytes which differ from
  31 | ||| the first pattern byte do not require a DFA table lookup.
  32 | |||
  33 | ||| Nonzero DFA states are represented by `DFAState`, which is an `Index`
  34 | ||| carrying erased bounds evidence. Each call to `dfaTransition` therefore
  35 | ||| accepts an already-valid state and returns another already-valid state.
  36 | ||| No `tryNatToFin`, `tryIndex`, or equivalent DFA-table bounds check occurs
  37 | ||| in the target-scanning hot path.
  38 | |||
  39 | private
  40 | matcher :  Bool
  41 |         -> ByteString
  42 |         -> ByteString
  43 |         -> F1 s (Maybe (List Nat))
  44 | matcher overlap pat target t =
  45 |   let patlen                      := length pat
  46 |       targetlen                   := length target
  47 |       False                       := patlen == S Z
  48 |         | True =>
  49 |             let Just patzero := index Z pat
  50 |                   | Nothing =>
  51 |                       Nothing # t
  52 |                 Just headelem := elemIndex patzero target
  53 |                   | Nothing =>
  54 |                       Nothing # t
  55 |               in Just (headelem :: []) # t
  56 |       Just patzero                := index Z pat
  57 |         | Nothing =>
  58 |             Nothing # t
  59 |       dfa                     # t := automaton pat t
  60 |       Just dfa'                   := dfa
  61 |         | Nothing =>
  62 |             Nothing # t
  63 |       MkDFAutomaton stspace table := dfa'
  64 |       Just stateone               := tryIndex {r = stspace.states} 1
  65 |         | Nothing =>
  66 |             Nothing # t
  67 |       result                  # t := matchZero stspace Z Lin patlen targetlen patzero table stateone t
  68 |       Just result'                := result
  69 |         | Nothing =>
  70 |             Nothing # t
  71 |     in Just (result' <>> []) # t
  72 |   where
  73 |     mutual
  74 |       ||| Continue scanning while the DFA is in state zero.
  75 |       |||
  76 |       ||| State zero is treated specially because any byte other than the
  77 |       ||| first pattern byte necessarily leaves the automaton in state zero.
  78 |       ||| Such bytes can therefore be skipped without consulting the DFA
  79 |       ||| transition table.
  80 |       |||
  81 |       ||| When the first pattern byte is encountered, the matcher moves
  82 |       ||| directly to the prevalidated DFA state one and continues through
  83 |       ||| `matchState`.
  84 |       |||
  85 |       matchZero :  (stspace : DFAStateSpace)
  86 |                 -> (idx : Nat)
  87 |                 -> (final : SnocList Nat)
  88 |                 -> (patlen : Nat)
  89 |                 -> (targetlen : Nat)
  90 |                 -> (patzero : Bits8)
  91 |                 -> (dfa : DFATable s stspace.states)
  92 |                 -> (stateone : DFAState stspace.states)
  93 |                 -> F1 s (Maybe (SnocList Nat))
  94 |       matchZero stspace idx final patlen targetlen patzero dfa stateone t =
  95 |           let False     := idx == targetlen
  96 |                 | True =>
  97 |                     Just final # t
  98 |               Just byte := index idx target
  99 |                 | Nothing =>
 100 |                     Nothing # t
 101 |               nxtidx    := S idx
 102 |               False     := byte == patzero
 103 |                 | True =>
 104 |                     assert_total (matchState stspace stateone nxtidx final patlen targetlen patzero dfa stateone t)
 105 |             in assert_total (matchZero stspace nxtidx final patlen targetlen patzero dfa stateone t)
 106 |       ||| Continue scanning from a nonzero DFA state.
 107 |       |||
 108 |       ||| The current state is represented by `DFAState`, so it is already
 109 |       ||| known to lie within the DFA's state space. `dfaTransition` computes
 110 |       ||| the flattened transition-table position from this bounded state and
 111 |       ||| the current input byte, performs the primitive array read, and
 112 |       ||| returns another bounded `DFAState`.
 113 |       |||
 114 |       ||| Consequently, the per-byte DFA lookup performs no explicit
 115 |       ||| `tryNatToFin`, `tryIndex`, or `Maybe`-based bounds validation.
 116 |       |||
 117 |       ||| When a complete match is found, overlapping searches resume one
 118 |       ||| byte after the start of the match, while non-overlapping searches
 119 |       ||| resume immediately after the matched pattern.
 120 |       |||
 121 |       ||| If a transition returns state zero, control returns to `matchZero`
 122 |       ||| so subsequent bytes can take advantage of the state-zero fast path.
 123 |       |||
 124 |       matchState :  (stspace : DFAStateSpace)
 125 |                  -> (state : DFAState stspace.states)
 126 |                  -> (idx : Nat)
 127 |                  -> (final : SnocList Nat)
 128 |                  -> (patlen : Nat)
 129 |                  -> (targetlen : Nat)
 130 |                  -> (patzero : Bits8)
 131 |                  -> (dfa : DFATable s stspace.states)
 132 |                  -> (stateone : DFAState stspace.states)
 133 |                  -> F1 s (Maybe (SnocList Nat))
 134 |       matchState stspace state idx final patlen targetlen patzero dfa stateone t =
 135 |           let False := idx == targetlen
 136 |                 | True =>
 137 |                     Just final # t
 138 |               Just byte := index idx target
 139 |                 | Nothing =>
 140 |                     Nothing # t
 141 |               nstate # t :=
 142 |                 dfaTransition
 143 |                   {statesPrf = stspace.statesBounded}
 144 |                   dfa
 145 |                   state
 146 |                   byte
 147 |                   t
 148 |               nstateval :=
 149 |                 dfaStateValue nstate
 150 |               nxtidx :=
 151 |                 S idx
 152 |               False := nstateval == cast {to=Bits32} patlen
 153 |                 | True =>
 154 |                     let matchidx :=
 155 |                           minus nxtidx patlen
 156 |                         final' :=
 157 |                           final :< matchidx
 158 |                         False := overlap
 159 |                           | True =>
 160 |                               assert_total (matchZero stspace (S matchidx) final' patlen targetlen patzero dfa stateone t)
 161 |                       in assert_total (matchZero stspace nxtidx final' patlen targetlen patzero dfa stateone t)
 162 |               False := nstateval == 0
 163 |                 | True =>
 164 |                     assert_total (matchZero stspace nxtidx final patlen targetlen patzero dfa stateone t)
 165 |             in assert_total (matchState stspace nstate nxtidx final patlen targetlen patzero dfa stateone t)
 166 | 
 167 | ||| Performs a string search on a `ByteString` utilizing a determinisitic-finite-automaton (DFA).
 168 | |||
 169 | ||| This function finds all (0-based) starting indices of the non-empty pattern `ByteString`
 170 | ||| pat within the non-empty target `ByteString`, using the deterministic-finite-automaton
 171 | ||| (DFA) computed by `automaton`.
 172 | |||
 173 | ||| Example:
 174 | |||
 175 | ||| | pat  | target     |
 176 | ||| | ---- | ---------- |
 177 | ||| | "AN" | "ANPANMAN" |
 178 | |||
 179 | ||| | Start | Substring      | Match? | Explanation                                      |
 180 | ||| | ----- | -------------- | ------ | ------------------------------------------------ |
 181 | ||| | 0     | **"AN"**PANMAN | Yes    | Full pattern `"AN"` matches starting at index 0. |
 182 | ||| | 1     | A**"NP"**ANMAN | No     | Mismatch after the first character.              |
 183 | ||| | 2     | AN**"PA"**NMAN | No     | No match — next candidate after suffix shift.    |
 184 | ||| | 3     | ANP**"AN"**MAN | Yes    | Match found at index 3.                          |
 185 | ||| | 4     | ANPA**"NM"**AN | No     | Mismatch.                                        |
 186 | ||| | 5     | ANPAN**"MA"**N | No     | Mismatch.                                        |
 187 | ||| | 6     | ANPANM**"AN"** | Yes    | Final match found at index 6.                    |
 188 | ||| 
 189 | |||
 190 | ||| matchDFA "AN" "ANPANMAN" => Just [0, 3, 6]
 191 | |||
 192 | export
 193 | matchDFA :  (pat : ByteString)
 194 |          -> (target : ByteString)
 195 |          -> {0 prfpat : So (not $ null pat)}
 196 |          -> {0 prftarget : So (not $ null target)}
 197 |          -> F1 s (Maybe (List Nat))
 198 | matchDFA pat target {prfpat} {prftarget} t =
 199 |   let matcher'   # t := matcher False pat target t
 200 |       Just matcher'' := matcher'
 201 |         | Nothing =>
 202 |             Nothing # t
 203 |     in Just matcher'' # t
 204 | 
 205 | ||| Performs a string search on a `ByteString` utilizing a determinisitic-finite-automaton (DFA).
 206 | |||
 207 | ||| This function finds all (0-based) indices (possibly overlapping)
 208 | ||| of the non-empty pattern `ByteString` pat
 209 | ||| within the non-empty target `ByteString`, using the deterministic-finite-automaton
 210 | ||| (DFA) computed by `automaton`.
 211 | |||
 212 | ||| Example:
 213 | |||
 214 | ||| | pat      | target      |
 215 | ||| | -------- | ----------- |
 216 | ||| | "ABCABC" | "ABCABCABC" |
 217 | |||
 218 | ||| | Start | Substring       | Match? | Explanation                                                      |
 219 | ||| | ----- | --------------- | ------ | ---------------------------------------------------------------- |
 220 | ||| | 0     | **"ABCABC"**ABC | Yes    | Full pattern matches starting at index 0.                        |
 221 | ||| | 1     | A**"BCABCA"**BC | No     | Mismatch starts immediately after first letter.                  |
 222 | ||| | 2     | AB**"CABCAA"**C | No     | Shift by suffix table → mismatch on 2nd char.                    |
 223 | ||| | 3     | ABC**"ABC"**    | Yes    | Overlapping match starting at index 3 (because `"ABC"` repeats). |
 224 | ||| 
 225 | ||| indicesDFA "ABCABC" "ABCABCABC" => Just [0, 3]
 226 | |||
 227 | export
 228 | indicesDFA :  (pat : ByteString)
 229 |            -> (target : ByteString)
 230 |            -> {0 prfpat : So (not $ null pat)}
 231 |            -> {0 prftarget : So (not $ null target)}
 232 |            -> F1 s (Maybe (List Nat))
 233 | indicesDFA pat target {prfpat} {prftarget} t =
 234 |   let matcher'   # t := matcher True pat target t
 235 |       Just matcher'' := matcher'
 236 |         | Nothing =>
 237 |             Nothing # t
 238 |     in Just matcher'' # t
 239 | 
 240 | ||| Splits a ByteString at the first match of pat in target.
 241 | |||
 242 | ||| This function uses the deterministic-finite-automaton matcher (with overlap = False) to
 243 | ||| locate the earliest occurrence of pat in target.  If the pattern is
 244 | ||| found at index i, the pattern ByteString pat is split at that index,
 245 | ||| returning the prefix and suffix as a pair (before, after).
 246 | |||
 247 | ||| If the pattern does not occur in the target, (pat, empty) is returned.
 248 | ||| In other words, the entire pattern becomes the “before” part and the
 249 | ||| “after” part is an empty ByteString.
 250 | |||
 251 | export
 252 | breakDFA :  (pat : ByteString)
 253 |          -> (target : ByteString)
 254 |          -> {0 prfpat : So (not $ null pat)}
 255 |          -> {0 prftarget : So (not $ null target)}
 256 |          -> {0 prflength : So ((length target) >= (length pat))}
 257 |          -> F1 s (Maybe (ByteString, ByteString))
 258 | breakDFA pat target {prfpat} {prftarget} {prflength} t =
 259 |    let matcher'   # t := matcher False pat target t
 260 |        Just matcher'' := matcher'
 261 |          | Nothing =>
 262 |              Nothing # t
 263 |        (i :: _)       := matcher''
 264 |          | [] =>
 265 |              Just (target, empty) # t
 266 |        target'        := splitAt (cast {to=Nat} i) target
 267 |        Just target''  := target'
 268 |          | Nothing =>
 269 |              Nothing # t
 270 |      in Just target'' # t
 271 | 
 272 | ||| Splits a ByteString after the first match of pat in target.
 273 | |||
 274 | ||| This function uses the deterministic-finite-automaton matcher (with overlap = False) to
 275 | ||| find the earliest occurrence of pat in target.  If the pattern is
 276 | ||| found at index i, this function splits pat at position i + length pat,
 277 | ||| producing a pair (before, after) that places the entire matched region
 278 | ||| into the prefix.
 279 | |||
 280 | ||| If the pattern does not occur in target, the function returns
 281 | ||| (pat, empty), the entire pattern is the “before” substring, and the
 282 | ||| suffix is empty.
 283 | |||
 284 | export
 285 | breakAfterDFA :  (pat : ByteString)
 286 |               -> (target : ByteString)
 287 |               -> {0 prfpat : So (not $ null pat)}
 288 |               -> {0 prftarget : So (not $ null target)}
 289 |               -> {0 prflength : So ((length target) >= (length pat))}
 290 |               -> F1 s (Maybe (ByteString, ByteString))
 291 | breakAfterDFA pat target {prfpat} {prftarget} {prflength} t =
 292 |    let matcher'   # t := matcher False pat target t
 293 |        Just matcher'' := matcher'
 294 |          | Nothing =>
 295 |              Nothing # t
 296 |        (i :: _)       := matcher''
 297 |          | [] =>
 298 |              Just (target, empty) # t
 299 |        target'        := splitAt (plus (cast {to=Nat} i) (length pat)) target
 300 |        Just target''  := target'
 301 |          | Nothing =>
 302 |              Nothing # t
 303 |      in Just target'' # t 
 304 | 
 305 | ||| Splits a ByteString into a list of pieces according to repeated
 306 | ||| matches of target, keeping the matching prefix of pat
 307 | ||| at the front of each produced chunk.
 308 | |||
 309 | ||| This function repeatedly searches target for occurrences of pat
 310 | ||| (using the deterministic-finite-automaton matcher with overlap = False).  Each time a
 311 | ||| match is found at index i, the prefix of pat up to i + length pat
 312 | ||| is emitted as the next chunk, and the function continues processing the
 313 | ||| remaining suffix of pat.
 314 | |||
 315 | ||| Unlike breakDFA or breakAfterDFA, this function performs repeated
 316 | ||| splitting until the entire pattern has been consumed, producing a
 317 | ||| list of ByteStrings.
 318 | |||
 319 | export
 320 | splitKeepFrontDFA :  (pat : ByteString)
 321 |                   -> (target : ByteString)
 322 |                   -> {0 prfpat : So (not $ null pat)}
 323 |                   -> {0 prftarget : So (not $ null target)}
 324 |                   -> {0 prflength : So ((length target) >= (length pat))}
 325 |                   -> F1 s (Maybe (List ByteString))
 326 | splitKeepFrontDFA pat target {prfpat} {prftarget} {prflength} t =
 327 |   let splitter'   # t := splitter pat target Lin t
 328 |       Just splitter'' := splitter'
 329 |         | Nothing =>
 330 |             Nothing # t
 331 |     in Just (splitter'' <>> []) # t
 332 |   where
 333 |     psSplitter :  (pat : ByteString)
 334 |                -> (target : ByteString)
 335 |                -> (final : SnocList ByteString)
 336 |                -> F1 s (Maybe (SnocList ByteString))
 337 |     psSplitter pat target final t =
 338 |       let matcher'   # t := matcher False pat (drop (length pat) target) t
 339 |           Just matcher'' := matcher'
 340 |             | Nothing =>
 341 |                 Nothing # t
 342 |           (i :: _)       := matcher''
 343 |             | [] =>
 344 |                 let final' := final :< target
 345 |                   in Just final' # t
 346 |           length'        := plus (cast {to=Nat} i) (length pat)
 347 |           final'         := final :< (take length' target)
 348 |         in assert_total (psSplitter pat (drop length' target) final' t)
 349 |     splitter :  (pat : ByteString)
 350 |              -> (target : ByteString)
 351 |              -> (final : SnocList ByteString)
 352 |              -> F1 s (Maybe (SnocList ByteString))
 353 |     splitter pat target final t =
 354 |       let matcher'   # t := matcher False pat target t
 355 |           Just matcher'' := matcher'
 356 |             | Nothing =>
 357 |                 Nothing # t
 358 |           (i :: _)       := matcher''
 359 |             | [] =>
 360 |                 let final' := final :< target
 361 |                   in Just final' # t
 362 |           False          := i == Z
 363 |             | True =>
 364 |                 assert_total (psSplitter pat target final t)
 365 |           final'         := final :< (take (cast {to=Nat} i) target)
 366 |         in assert_total (psSplitter pat (drop (cast {to=Nat} i) target) final' t)
 367 | 
 368 | ||| Splits a ByteString into a list of pieces according to repeated
 369 | ||| matches of pat inside target, keeping the matching
 370 | ||| suffix of pat at the end of each produced chunk.
 371 | |||
 372 | ||| This function repeatedly searches target for occurrences of pat
 373 | ||| (using the deterministic-finite-automaton matcher with overlap = False).  Each time a
 374 | ||| match is found at index i, the next chunk emitted is the prefix of
 375 | ||| target of length i + length pat, which includes the entire matched
 376 | ||| occurrence of pat at its end.
 377 | |||
 378 | ||| After emitting this chunk, the function continues splitting the
 379 | ||| remainder of target until all input has been consumed.
 380 | |||
 381 | ||| Unlike splitKeepFrontDFA, which keeps the matched prefix of pat
 382 | ||| at the front of each chunk, splitKeepEndDFA ensures the match
 383 | ||| appears at the end of each chunk.
 384 | |||
 385 | ||| If pat does not occur in target, the result is a singleton list
 386 | ||| containing the original target.
 387 | |||
 388 | export
 389 | splitKeepEndDFA :  (pat : ByteString)
 390 |                 -> (target : ByteString)
 391 |                 -> {0 prfpat : So (not $ null pat)}
 392 |                 -> {0 prftarget : So (not $ null target)}
 393 |                 -> {0 prflength : So ((length target) >= (length pat))}
 394 |                 -> F1 s (Maybe (List ByteString))
 395 | splitKeepEndDFA pat target {prfpat} {prftarget} {prflength} t =
 396 |   let splitter'   # t := splitter pat target Lin t
 397 |       Just splitter'' := splitter'
 398 |         | Nothing =>
 399 |             Nothing # t
 400 |     in Just (splitter'' <>> []) # t
 401 |   where
 402 |     splitter :  (pat : ByteString)
 403 |              -> (target : ByteString)
 404 |              -> (final : SnocList ByteString)
 405 |              -> F1 s (Maybe (SnocList ByteString))
 406 |     splitter pat target final t =
 407 |       let matcher'   # t := matcher False pat target t
 408 |           Just matcher'' := matcher'
 409 |             | Nothing =>
 410 |                 Nothing # t
 411 |           (i :: _)       := matcher''
 412 |             | [] =>
 413 |                 let final' := final :< target
 414 |                   in Just final' # t
 415 |           length'        := plus (cast {to=Nat} i) (length pat)
 416 |           final'         := final :< (take length' target)
 417 |         in assert_total (splitter pat (drop length' target) final' t)
 418 | 
 419 | ||| Splits a ByteString into a list of pieces according to repeated
 420 | ||| matches of pat inside target, dropping each matched
 421 | ||| occurrence from the output entirely.
 422 | |||
 423 | ||| This function repeatedly searches target for occurrences of pat
 424 | ||| (using the deterministic-finite-automaton matcher with overlap = False).  Each time a
 425 | ||| match is found at index i, the prefix of target of length i
 426 | ||| (that is, the portion preceding the match) is emitted as the next
 427 | ||| chunk.  The matched substring itself is not included.
 428 | |||
 429 | ||| After emitting this prefix, the function continues splitting the
 430 | ||| remainder of target, skipping over the full match of length
 431 | ||| i + length pat.  This process continues until the entire target
 432 | ||| has been consumed.
 433 | |||
 434 | ||| Unlike splitKeepFrontDFA and splitKeepEndDFA, which include the
 435 | ||| matched pattern in each emitted chunk, splitDropKMP removes all
 436 | ||| occurrences of pat from the output.
 437 | |||
 438 | ||| If pat does not occur in target, the result is a singleton list
 439 | ||| containing the original target.
 440 | |||
 441 | export
 442 | splitDropDFA :  (pat : ByteString)
 443 |              -> (target : ByteString)
 444 |              -> {0 prfpat : So (not $ null pat)}
 445 |              -> {0 prftarget : So (not $ null target)}
 446 |              -> {0 prflength : So ((length target) >= (length pat))}
 447 |              -> F1 s (Maybe (List ByteString))
 448 | splitDropDFA pat target {prfpat} {prftarget} {prflength} t =
 449 |   let splitter'   # t := splitter pat target Lin t
 450 |       Just splitter'' := splitter'
 451 |         | Nothing =>
 452 |             Nothing # t
 453 |     in Just (splitter'' <>> []) # t
 454 |   where
 455 |     splitter :  (pat : ByteString)
 456 |              -> (target : ByteString)
 457 |              -> (final : SnocList ByteString)
 458 |              -> F1 s (Maybe (SnocList ByteString))
 459 |     splitter pat target final t =
 460 |       let matcher'   # t := matcher False pat target t
 461 |           Just matcher'' := matcher'
 462 |             | Nothing =>
 463 |                 Nothing # t
 464 |           (i :: _)       := matcher''
 465 |             | [] =>
 466 |                 let final' := final :< target
 467 |                   in Just final' # t
 468 |           length'        := plus (cast {to=Nat} i) (length pat)
 469 |           final'         := final :< (take (cast {to=Nat} i) target)
 470 |         in assert_total (splitter pat (drop length' target) final' t)
 471 | 
 472 | ||| Replaces all non-overlapping occurrences of a pattern in a ByteString
 473 | ||| using the deterministic-finite-automaton matcher.
 474 | |||
 475 | ||| This function repeatedly searches target for occurrences of pat
 476 | ||| (using matcher False). Each time a match is found at index i:
 477 | |||
 478 | ||| * If i == 0, the match is at the current position. The matched
 479 | |||   segment is dropped and sub is appended to the result (unless
 480 | |||   sub is empty, in which case nothing is appended).
 481 | |||
 482 | ||| * If i > 0, the prefix take i target is appended to the result,
 483 | |||   followed by sub (unless sub is empty). The matched segment is
 484 | |||   then dropped and processing continues on the remaining suffix.
 485 | |||
 486 | ||| If no further matches are found, the remaining target is appended
 487 | ||| unchanged and the result is returned.
 488 | |||
 489 | ||| The result is accumulated via a `SnocList` and returned as a `List
 490 | ||| ByteString`, preserving left-to-right order of the produced chunks.
 491 | |||
 492 | export
 493 | replaceDFA :  (pat : ByteString)
 494 |            -> (sub : ByteString)
 495 |            -> (target : ByteString)
 496 |            -> {0 prfpat : So (not $ null pat)}
 497 |            -> {0 prftarget : So (not $ null target)}
 498 |            -> {0 prflength : So ((length target) >= (length pat))}
 499 |            -> F1 s (Maybe (List ByteString))
 500 | replaceDFA pat sub target {prfpat} {prftarget} {prflength} t =
 501 |   let replacer'   # t := replacer pat sub target Lin t
 502 |       Just replacer'' := replacer'
 503 |         | Nothing =>
 504 |             Nothing # t
 505 |     in Just (replacer'' <>> []) # t
 506 |   where
 507 |     replacer :  (pat : ByteString)
 508 |              -> (sub : ByteString)
 509 |              -> (target : ByteString)
 510 |              -> (final : SnocList ByteString)
 511 |              -> F1 s (Maybe (SnocList ByteString))
 512 |     replacer pat sub target final t =
 513 |       let matcher'   # t := matcher False pat target t
 514 |           Just matcher'' := matcher'
 515 |             | Nothing =>
 516 |                 Nothing # t
 517 |           (i :: _)       := matcher''
 518 |             | [] =>
 519 |                 let final' := final :< target
 520 |                   in Just final' # t
 521 |           Z              := i
 522 |             | _ =>
 523 |                 let False := null sub
 524 |                       | True =>
 525 |                           let length' := plus (cast {to=Nat} i) (length pat)
 526 |                               final'  := final :< (take (cast {to=Nat} i) target)
 527 |                             in assert_total (replacer pat sub (drop length' target) final' t)
 528 |                     length' := plus (cast {to=Nat} i) (length pat)
 529 |                     final'  := final :< (take (cast {to=Nat} i) target) :< sub
 530 |                   in assert_total (replacer pat sub (drop length' target) final' t)
 531 |           False          := null sub
 532 |             | True =>
 533 |                 assert_total (replacer pat sub (drop (length pat) target) final t)
 534 |           final'         := final :< sub
 535 |         in assert_total (replacer pat sub (drop (length pat) target) final') t
 536 |