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