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