
   0 | ||| Fast deterministic finite automaton (DFA) search of ByteStrings
   1 | module Data.ByteString.Search.DFA
   2 | 
   3 | import Data.ByteString.Search.Internal.Utils
   4 | 
   5 | import Data.Array.Core
   6 | import Data.Array.Mutable
   7 | import Data.Bits
   8 | import Data.ByteString
   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 | private
  21 | matcher :  Bool
  22 |         -> ByteString
  23 |         -> ByteString
  24 |         -> F1 s (Maybe (List Nat))
  25 | matcher overlap pat target t =
  26 |   let False        := length pat == S Z
  27 |         | True =>
  28 |             let patzero        := index Z pat
  29 |                 Just patzero'  := patzero
  30 |                   | Nothing =>
  31 |                       Nothing # t
  32 |                 headelem       := elemIndex patzero' pat
  33 |                 Just headelem' := headelem
  34 |                   | Nothing =>
  35 |                       Nothing # t
  36 |               in Just (headelem' :: []) # t
  37 |       dfa # t      := automaton pat t
  38 |       Just dfa'    := dfa
  39 |         | Nothing =>
  40 |             Nothing # t
  41 |       match' # t   := match Z Z pat target Lin dfa' overlap t
  42 |       Just match'' := match'
  43 |         | Nothing =>
  44 |             Nothing # t
  45 |     in Just (match'' <>> []) # t
  46 |   where
  47 |     match :  (state : Nat)
  48 |           -> (idx : Nat)
  49 |           -> (pat : ByteString)
  50 |           -> (target : ByteString)
  51 |           -> (final : SnocList Nat)
  52 |           -> (dfa : MArray s (mult (plus (length pat) 1) 256) Nat)
  53 |           -> (overlap : Bool)
  54 |           -> F1 s (Maybe (SnocList Nat))
  55 |     match Z idx pat target final dfa overlap t =
  56 |       let False         := idx == length target
  57 |             | True =>
  58 |                 Just final # t
  59 |           idx'          := index idx target
  60 |           Just idx''    := idx'
  61 |             | Nothing =>
  62 |                 Nothing # t
  63 |           patzero       := index Z pat
  64 |           Just patzero' := patzero
  65 |             | Nothing =>
  66 |                 Nothing # t
  67 |           False         := idx'' == patzero'
  68 |             | True =>
  69 |                 assert_total (match (S 0) (S idx) pat target final dfa overlap t)
  70 |         in assert_total (match Z (S idx) pat target final dfa overlap t)
  71 |     match state idx pat target final dfa overlap t =
  72 |       let False           := idx == length target
  73 |             | True =>
  74 |                 Just final # t
  75 |           idx'            := index idx target
  76 |           Just idx''      := idx'
  77 |             | Nothing =>
  78 |                 Nothing # t
  79 |           nstateidx       := plus (mult state 256) (cast {to=Nat} idx'')
  80 |           Just nstateidx' := tryNatToFin nstateidx
  81 |             | Nothing =>
  82 |                 Nothing # t
  83 |           nstate      # t := get dfa nstateidx' t
  84 |           nxtidx          := S idx
  85 |           True            := nstate == length pat
  86 |             | False =>
  87 |                 assert_total (match nstate nxtidx pat target final dfa overlap t)
  88 |           final'          := minus nxtidx (length pat)
  89 |           final''         := final :< final'
  90 |           True            := overlap
  91 |             | False =>
  92 |                 assert_total (match Z nxtidx pat target final'' dfa overlap t)
  93 |           ams             := S (minus nxtidx (length pat))
  94 |         in assert_total (match Z ams pat target final'' dfa overlap t)
  95 | 
  96 | ||| Performs a string search on a `ByteString` utilizing a determinisitic-finite-automaton (DFA).
  97 | |||
  98 | ||| This function finds all (0-based) starting indices of the non-empty pattern `ByteString`
  99 | ||| pat within the non-empty target `ByteString`, using the deterministic-finite-automaton
 100 | ||| (DFA) computed by `automaton`.
 101 | |||
 102 | ||| Example:
 103 | |||
 104 | ||| | pat  | target     |
 105 | ||| | ---- | ---------- |
 106 | ||| | "AN" | "ANPANMAN" |
 107 | |||
 108 | ||| | Start | Substring      | Match? | Explanation                                      |
 109 | ||| | ----- | -------------- | ------ | ------------------------------------------------ |
 110 | ||| | 0     | **"AN"**PANMAN | Yes    | Full pattern `"AN"` matches starting at index 0. |
 111 | ||| | 1     | A**"NP"**ANMAN | No     | Mismatch after the first character.              |
 112 | ||| | 2     | AN**"PA"**NMAN | No     | No match — next candidate after suffix shift.    |
 113 | ||| | 3     | ANP**"AN"**MAN | Yes    | Match found at index 3.                          |
 114 | ||| | 4     | ANPA**"NM"**AN | No     | Mismatch.                                        |
 115 | ||| | 5     | ANPAN**"MA"**N | No     | Mismatch.                                        |
 116 | ||| | 6     | ANPANM**"AN"** | Yes    | Final match found at index 6.                    |
 117 | ||| 
 118 | |||
 119 | ||| matchDFA "AN" "ANPANMAN" => Just [0, 3, 6]
 120 | |||
 121 | export
 122 | matchDFA :  (pat : ByteString)
 123 |          -> (target : ByteString)
 124 |          -> {0 prfpat : So (not $ null pat)}
 125 |          -> {0 prftarget : So (not $ null target)}
 126 |          -> F1 s (Maybe (List Nat))
 127 | matchDFA pat target {prfpat} {prftarget} t =
 128 |   let matcher'   # t := matcher False pat target t
 129 |       Just matcher'' := matcher'
 130 |         | Nothing =>
 131 |             Nothing # t
 132 |     in Just matcher'' # t
 133 | 
 134 | ||| Performs a string search on a `ByteString` utilizing a determinisitic-finite-automaton (DFA).
 135 | |||
 136 | ||| This function finds all (0-based) indices (possibly overlapping)
 137 | ||| of the non-empty pattern `ByteString` pat
 138 | ||| within the non-empty target `ByteString`, using the deterministic-finite-automaton
 139 | ||| (DFA) computed by `automaton`.
 140 | |||
 141 | ||| Example:
 142 | |||
 143 | ||| | pat      | target      |
 144 | ||| | -------- | ----------- |
 145 | ||| | "ABCABC" | "ABCABCABC" |
 146 | |||
 147 | ||| | Start | Substring       | Match? | Explanation                                                      |
 148 | ||| | ----- | --------------- | ------ | ---------------------------------------------------------------- |
 149 | ||| | 0     | **"ABCABC"**ABC | Yes    | Full pattern matches starting at index 0.                        |
 150 | ||| | 1     | A**"BCABCA"**BC | No     | Mismatch starts immediately after first letter.                  |
 151 | ||| | 2     | AB**"CABCAA"**C | No     | Shift by suffix table → mismatch on 2nd char.                    |
 152 | ||| | 3     | ABC**"ABC"**    | Yes    | Overlapping match starting at index 3 (because `"ABC"` repeats). |
 153 | ||| 
 154 | ||| indicesDFA "ABCABC" "ABCABCABC" => Just [0, 3]
 155 | |||
 156 | export
 157 | indicesDFA :  (pat : ByteString)
 158 |            -> (target : ByteString)
 159 |            -> {0 prfpat : So (not $ null pat)}
 160 |            -> {0 prftarget : So (not $ null target)}
 161 |            -> F1 s (Maybe (List Nat))
 162 | indicesDFA pat target {prfpat} {prftarget} t =
 163 |   let matcher'   # t := matcher True pat target t
 164 |       Just matcher'' := matcher'
 165 |         | Nothing =>
 166 |             Nothing # t
 167 |     in Just matcher'' # t
 168 | 
 169 | ||| Splits a ByteString at the first match of pat in target.
 170 | |||
 171 | ||| This function uses the deterministic-finite-automaton matcher (with overlap = False) to
 172 | ||| locate the earliest occurrence of pat in target.  If the pattern is
 173 | ||| found at index i, the pattern ByteString pat is split at that index,
 174 | ||| returning the prefix and suffix as a pair (before, after).
 175 | |||
 176 | ||| If the pattern does not occur in the target, (pat, empty) is returned.
 177 | ||| In other words, the entire pattern becomes the “before” part and the
 178 | ||| “after” part is an empty ByteString.
 179 | |||
 180 | export
 181 | breakDFA :  (pat : ByteString)
 182 |          -> (target : ByteString)
 183 |          -> {0 prfpat : So (not $ null pat)}
 184 |          -> {0 prftarget : So (not $ null target)}
 185 |          -> {0 prflength : So ((length target) >= (length pat))}
 186 |          -> F1 s (Maybe (ByteString, ByteString))
 187 | breakDFA pat target {prfpat} {prftarget} {prflength} t =
 188 |    let matcher'   # t := matcher False pat target t
 189 |        Just matcher'' := matcher'
 190 |          | Nothing =>
 191 |              Nothing # t
 192 |        (i :: _)       := matcher''
 193 |          | [] =>
 194 |              Just (target, empty) # t
 195 |        target'        := splitAt (cast {to=Nat} i) target
 196 |        Just target''  := target'
 197 |          | Nothing =>
 198 |              Nothing # t
 199 |      in Just target'' # t
 200 | 
 201 | ||| Splits a ByteString after the first match of pat in target.
 202 | |||
 203 | ||| This function uses the deterministic-finite-automaton matcher (with overlap = False) to
 204 | ||| find the earliest occurrence of pat in target.  If the pattern is
 205 | ||| found at index i, this function splits pat at position i + length pat,
 206 | ||| producing a pair (before, after) that places the entire matched region
 207 | ||| into the prefix.
 208 | |||
 209 | ||| If the pattern does not occur in target, the function returns
 210 | ||| (pat, empty), the entire pattern is the “before” substring, and the
 211 | ||| suffix is empty.
 212 | |||
 213 | export
 214 | breakAfterDFA :  (pat : ByteString)
 215 |               -> (target : ByteString)
 216 |               -> {0 prfpat : So (not $ null pat)}
 217 |               -> {0 prftarget : So (not $ null target)}
 218 |               -> {0 prflength : So ((length target) >= (length pat))}
 219 |               -> F1 s (Maybe (ByteString, ByteString))
 220 | breakAfterDFA pat target {prfpat} {prftarget} {prflength} t =
 221 |    let matcher'   # t := matcher False pat target t
 222 |        Just matcher'' := matcher'
 223 |          | Nothing =>
 224 |              Nothing # t
 225 |        (i :: _)       := matcher''
 226 |          | [] =>
 227 |              Just (target, empty) # t
 228 |        target'        := splitAt (plus (cast {to=Nat} i) (length pat)) target
 229 |        Just target''  := target'
 230 |          | Nothing =>
 231 |              Nothing # t
 232 |      in Just target'' # t 
 233 | 
 234 | ||| Splits a ByteString into a list of pieces according to repeated
 235 | ||| matches of target, keeping the matching prefix of pat
 236 | ||| at the front of each produced chunk.
 237 | |||
 238 | ||| This function repeatedly searches target for occurrences of pat
 239 | ||| (using the deterministic-finite-automaton matcher with overlap = False).  Each time a
 240 | ||| match is found at index i, the prefix of pat up to i + length pat
 241 | ||| is emitted as the next chunk, and the function continues processing the
 242 | ||| remaining suffix of pat.
 243 | |||
 244 | ||| Unlike breakDFA or breakAfterDFA, this function performs repeated
 245 | ||| splitting until the entire pattern has been consumed, producing a
 246 | ||| list of ByteStrings.
 247 | |||
 248 | export
 249 | splitKeepFrontDFA :  (pat : ByteString)
 250 |                   -> (target : ByteString)
 251 |                   -> {0 prfpat : So (not $ null pat)}
 252 |                   -> {0 prftarget : So (not $ null target)}
 253 |                   -> {0 prflength : So ((length target) >= (length pat))}
 254 |                   -> F1 s (Maybe (List ByteString))
 255 | splitKeepFrontDFA pat target {prfpat} {prftarget} {prflength} t =
 256 |   let splitter'   # t := splitter pat target Lin t
 257 |       Just splitter'' := splitter'
 258 |         | Nothing =>
 259 |             Nothing # t
 260 |     in Just (splitter'' <>> []) # t
 261 |   where
 262 |     psSplitter :  (pat : ByteString)
 263 |                -> (target : ByteString)
 264 |                -> (final : SnocList ByteString)
 265 |                -> F1 s (Maybe (SnocList ByteString))
 266 |     psSplitter pat target final t =
 267 |       let matcher'   # t := matcher False pat (drop (length pat) target) t
 268 |           Just matcher'' := matcher'
 269 |             | Nothing =>
 270 |                 Nothing # t
 271 |           (i :: _)       := matcher''
 272 |             | [] =>
 273 |                 let final' := final :< target
 274 |                   in Just final' # t
 275 |           length'        := plus (cast {to=Nat} i) (length pat)
 276 |           final'         := final :< (take length' target)
 277 |         in assert_total (psSplitter pat (drop length' target) final' t)
 278 |     splitter :  (pat : ByteString)
 279 |              -> (target : ByteString)
 280 |              -> (final : SnocList ByteString)
 281 |              -> F1 s (Maybe (SnocList ByteString))
 282 |     splitter pat target final t =
 283 |       let matcher'   # t := matcher False pat target t
 284 |           Just matcher'' := matcher'
 285 |             | Nothing =>
 286 |                 Nothing # t
 287 |           (i :: _)       := matcher''
 288 |             | [] =>
 289 |                 let final' := final :< target
 290 |                   in Just final' # t
 291 |           False          := i == Z
 292 |             | True =>
 293 |                 assert_total (psSplitter pat target final t)
 294 |           final'         := final :< (take (cast {to=Nat} i) target)
 295 |         in assert_total (psSplitter pat (drop (cast {to=Nat} i) target) final' t)
 296 | 
 297 | ||| Splits a ByteString into a list of pieces according to repeated
 298 | ||| matches of pat inside target, keeping the matching
 299 | ||| suffix of pat at the end of each produced chunk.
 300 | |||
 301 | ||| This function repeatedly searches target for occurrences of pat
 302 | ||| (using the deterministic-finite-automaton matcher with overlap = False).  Each time a
 303 | ||| match is found at index i, the next chunk emitted is the prefix of
 304 | ||| target of length i + length pat, which includes the entire matched
 305 | ||| occurrence of pat at its end.
 306 | |||
 307 | ||| After emitting this chunk, the function continues splitting the
 308 | ||| remainder of target until all input has been consumed.
 309 | |||
 310 | ||| Unlike splitKeepFrontDFA, which keeps the matched prefix of pat
 311 | ||| at the front of each chunk, splitKeepEndDFA ensures the match
 312 | ||| appears at the end of each chunk.
 313 | |||
 314 | ||| If pat does not occur in target, the result is a singleton list
 315 | ||| containing the original target.
 316 | |||
 317 | export
 318 | splitKeepEndDFA :  (pat : ByteString)
 319 |                 -> (target : ByteString)
 320 |                 -> {0 prfpat : So (not $ null pat)}
 321 |                 -> {0 prftarget : So (not $ null target)}
 322 |                 -> {0 prflength : So ((length target) >= (length pat))}
 323 |                 -> F1 s (Maybe (List ByteString))
 324 | splitKeepEndDFA pat target {prfpat} {prftarget} {prflength} t =
 325 |   let splitter'   # t := splitter pat target Lin t
 326 |       Just splitter'' := splitter'
 327 |         | Nothing =>
 328 |             Nothing # t
 329 |     in Just (splitter'' <>> []) # t
 330 |   where
 331 |     splitter :  (pat : ByteString)
 332 |              -> (target : ByteString)
 333 |              -> (final : SnocList ByteString)
 334 |              -> F1 s (Maybe (SnocList ByteString))
 335 |     splitter pat target final t =
 336 |       let matcher'   # t := matcher False pat target t
 337 |           Just matcher'' := matcher'
 338 |             | Nothing =>
 339 |                 Nothing # t
 340 |           (i :: _)       := matcher''
 341 |             | [] =>
 342 |                 let final' := final :< target
 343 |                   in Just final' # t
 344 |           length'        := plus (cast {to=Nat} i) (length pat)
 345 |           final'         := final :< (take length' target)
 346 |         in assert_total (splitter pat (drop length' target) final' t)
 347 | 
 348 | ||| Splits a ByteString into a list of pieces according to repeated
 349 | ||| matches of pat inside target, dropping each matched
 350 | ||| occurrence from the output entirely.
 351 | |||
 352 | ||| This function repeatedly searches target for occurrences of pat
 353 | ||| (using the deterministic-finite-automaton matcher with overlap = False).  Each time a
 354 | ||| match is found at index i, the prefix of target of length i
 355 | ||| (that is, the portion preceding the match) is emitted as the next
 356 | ||| chunk.  The matched substring itself is not included.
 357 | |||
 358 | ||| After emitting this prefix, the function continues splitting the
 359 | ||| remainder of target, skipping over the full match of length
 360 | ||| i + length pat.  This process continues until the entire target
 361 | ||| has been consumed.
 362 | |||
 363 | ||| Unlike splitKeepFrontDFA and splitKeepEndDFA, which include the
 364 | ||| matched pattern in each emitted chunk, splitDropKMP removes all
 365 | ||| occurrences of pat from the output.
 366 | |||
 367 | ||| If pat does not occur in target, the result is a singleton list
 368 | ||| containing the original target.
 369 | |||
 370 | export
 371 | splitDropDFA :  (pat : ByteString)
 372 |              -> (target : ByteString)
 373 |              -> {0 prfpat : So (not $ null pat)}
 374 |              -> {0 prftarget : So (not $ null target)}
 375 |              -> {0 prflength : So ((length target) >= (length pat))}
 376 |              -> F1 s (Maybe (List ByteString))
 377 | splitDropDFA pat target {prfpat} {prftarget} {prflength} t =
 378 |   let splitter'   # t := splitter pat target Lin t
 379 |       Just splitter'' := splitter'
 380 |         | Nothing =>
 381 |             Nothing # t
 382 |     in Just (splitter'' <>> []) # t
 383 |   where
 384 |     splitter :  (pat : ByteString)
 385 |              -> (target : ByteString)
 386 |              -> (final : SnocList ByteString)
 387 |              -> F1 s (Maybe (SnocList ByteString))
 388 |     splitter pat target final t =
 389 |       let matcher'   # t := matcher False pat target t
 390 |           Just matcher'' := matcher'
 391 |             | Nothing =>
 392 |                 Nothing # t
 393 |           (i :: _)       := matcher''
 394 |             | [] =>
 395 |                 let final' := final :< target
 396 |                   in Just final' # t
 397 |           length'        := plus (cast {to=Nat} i) (length pat)
 398 |           final'         := final :< (take (cast {to=Nat} i) target)
 399 |         in assert_total (splitter pat (drop length' target) final' t)
 400 | 
 401 | ||| Replaces all non-overlapping occurrences of a pattern in a ByteString
 402 | ||| using the deterministic-finite-automaton matcher.
 403 | |||
 404 | ||| This function repeatedly searches target for occurrences of pat
 405 | ||| (using matcher False). Each time a match is found at index i:
 406 | |||
 407 | ||| * If i == 0, the match is at the current position. The matched
 408 | |||   segment is dropped and sub is appended to the result (unless
 409 | |||   sub is empty, in which case nothing is appended).
 410 | |||
 411 | ||| * If i > 0, the prefix take i target is appended to the result,
 412 | |||   followed by sub (unless sub is empty). The matched segment is
 413 | |||   then dropped and processing continues on the remaining suffix.
 414 | |||
 415 | ||| If no further matches are found, the remaining target is appended
 416 | ||| unchanged and the result is returned.
 417 | |||
 418 | ||| The result is accumulated via a `SnocList` and returned as a `List
 419 | ||| ByteString`, preserving left-to-right order of the produced chunks.
 420 | |||
 421 | export
 422 | replaceDFA :  (pat : ByteString)
 423 |            -> (sub : ByteString)
 424 |            -> (target : ByteString)
 425 |            -> {0 prfpat : So (not $ null pat)}
 426 |            -> {0 prftarget : So (not $ null target)}
 427 |            -> {0 prflength : So ((length target) >= (length pat))}
 428 |            -> F1 s (Maybe (List ByteString))
 429 | replaceDFA pat sub target {prfpat} {prftarget} {prflength} t =
 430 |   let replacer'   # t := replacer pat sub target Lin t
 431 |       Just replacer'' := replacer'
 432 |         | Nothing =>
 433 |             Nothing # t
 434 |     in Just (replacer'' <>> []) # t
 435 |   where
 436 |     replacer :  (pat : ByteString)
 437 |              -> (sub : ByteString)
 438 |              -> (target : ByteString)
 439 |              -> (final : SnocList ByteString)
 440 |              -> F1 s (Maybe (SnocList ByteString))
 441 |     replacer pat sub target final t =
 442 |       let matcher'   # t := matcher False pat target t
 443 |           Just matcher'' := matcher'
 444 |             | Nothing =>
 445 |                 Nothing # t
 446 |           (i :: _)       := matcher''
 447 |             | [] =>
 448 |                 let final' := final :< target
 449 |                   in Just final' # t
 450 |           Z              := i
 451 |             | _ =>
 452 |                 let False := null sub
 453 |                       | True =>
 454 |                           let length' := plus (cast {to=Nat} i) (length pat)
 455 |                               final'  := final :< (take (cast {to=Nat} i) target)
 456 |                             in assert_total (replacer pat sub (drop length' target) final' t)
 457 |                     length' := plus (cast {to=Nat} i) (length pat)
 458 |                     final'  := final :< (take (cast {to=Nat} i) target) :< sub
 459 |                   in assert_total (replacer pat sub (drop length' target) final' t)
 460 |           False          := null sub
 461 |             | True =>
 462 |                 assert_total (replacer pat sub (drop (length pat) target) final t)
 463 |           final'         := final :< sub
 464 |         in assert_total (replacer pat sub (drop (length pat) target) final') t
 465 |