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