0 | ||| Utilities for string searching algorithms
  1 | module Data.ByteString.Search.Internal.Utils
  2 |
  3 | import Data.Array.Core
  4 | import Data.Array.Mutable
  5 | import Data.Bits
  6 | import Data.ByteString
  7 | import Data.Linear.Ref1
  8 | import Data.So
  9 |
 10 | %hide Data.Buffer.Core.get
 11 | %hide Data.Buffer.Core.set
 12 |
 13 | %default total
 14 |
 15 | --------------------------------------------------------------------------------
 16 | --          Preprocessing
 17 | --------------------------------------------------------------------------------
 18 |
 19 | ||| Computes the suffix-oriented KMP border table for a given pattern.
 20 | |||
 21 | ||| Each entry at index i (0 ≤ i ≤ length pattern) stores the length of the
 22 | ||| longest proper prefix of the prefix pattern[0..i-1] that is also a
 23 | ||| suffix. This “border” is used to determine how far to backtrack in
 24 | ||| pattern matching when a mismatch occurs.
 25 | |||
 26 | ||| Unlike the standard KMP table, this table is suffix-oriented and
 27 | ||| built in a descending, structurally recursive manner.
 28 | |||
 29 | ||| The table helps efficiently skip positions in the pattern during
 30 | ||| substring search, while descending from longer prefixes to shorter ones.
 31 | |||
 32 | ||| Example: ANPANMAN"
 33 | |||
 34 | ||| Indices: 0..8
 35 | |||
 36 | ||| Prefixes: ""   "A"   "AN"   "ANP"  "ANPA"  "ANPAN"  "ANPANM"  "ANPANMA"  "ANPANMAN"
 37 | ||| Borders:  0    0     0      0      1       2        0         1          2
 38 | |||
 39 | export
 40 | kmpBorders :  (bs : ByteString)
 41 |            -> F1 s (Maybe (MArray s (S (length bs)) Nat))
 42 | kmpBorders bs t =
 43 |   let arr   # t := unsafeMArray1 (S (length bs)) t
 44 |       Just zero := tryNatToFin Z
 45 |         | Nothing => Nothing # t
 46 |       ()    # t := set arr zero Z t
 47 |     in go (S Z) Z bs arr t
 48 |   where
 49 |     mutual
 50 |       advance :  (i : Nat)
 51 |               -> (j : Nat)
 52 |               -> (wi : Nat)
 53 |               -> (bs : ByteString)
 54 |               -> (arr : MArray s (S (length bs)) Nat)
 55 |               -> F1 s (Maybe (MArray s (S (length bs)) Nat))
 56 |       advance i j wi bs arr t =
 57 |         let Just wj := index j bs
 58 |               | Nothing => Nothing # t
 59 |             wj' := cast {to=Nat} wj
 60 |             False := wi == wj'
 61 |               | True =>
 62 |                   let j'       := S j
 63 |                       Just fi' := tryNatToFin (S i)
 64 |                         | Nothing => Nothing # t
 65 |                       ()   # t := set arr fi' j' t
 66 |                     in assert_total (go (S i) j' bs arr t)
 67 |             False := j == 0
 68 |               | True =>
 69 |                   let Just fi' := tryNatToFin (S i)
 70 |                         | Nothing => Nothing # t
 71 |                       ()   # t := set arr fi' Z t
 72 |                     in assert_total (go (S i) Z bs arr t)
 73 |             Just fj := tryNatToFin j
 74 |               | Nothing => Nothing # t
 75 |             j' # t := get arr fj t
 76 |           in assert_total (advance i j' wi bs arr t)
 77 |       go :  (i : Nat)
 78 |          -> (j : Nat)
 79 |          -> (bs : ByteString)
 80 |          -> (arr : MArray s (S (length bs)) Nat)
 81 |          -> F1 s (Maybe (MArray s (S (length bs)) Nat))
 82 |       go i j bs arr t =
 83 |         let False   := i == length bs
 84 |               | True =>
 85 |                   Just arr # t
 86 |             Just wi := index i bs
 87 |               | Nothing => Nothing # t
 88 |             wi'     := cast {to=Nat} wi
 89 |           in advance i j wi' bs arr t
 90 |
 91 |
 92 | ||| Builds a deterministic finite automaton (DFA) for pattern matching over a `ByteString`.
 93 | |||
 94 | ||| The automaton encodes transitions from (state, input byte) → next state,
 95 | ||| allowing efficient streaming search for the pattern within input data.
 96 | |||
 97 | ||| It produces a flattened transition table of size `((length pattern) + 1) * 256`,
 98 | ||| where 256 corresponds to all possible byte values (0–255).
 99 | |||
100 | ||| States correspond to pattern prefixes:
101 | ||| - State 0: no match (empty prefix)
102 | ||| - State i: matched the first i bytes of the pattern
103 | ||| - State (length pattern): full match
104 | |||
105 | ||| Transition behavior is derived from the KMP border table (`kmpBorders`),
106 | ||| ensuring correct fallback transitions and eliminating redundant backtracking.
107 | |||
108 | ||| Example: "ANPANMAN"
109 | |||
110 | ||| These following equation is used to determine the "flat" index to build the automaton:
111 | |||
112 | ||| flatindex = (state ∗ alphabetsize) + charcode
113 | |||
114 | ||| Where:
115 | ||| - state : Range from 0 to length of the input pattern
116 | ||| - alphabetsize : All possible input characters (in this case extended ASCII, 8-bit range from 0 to 255)
117 | ||| - charcode : Characters are interpreted via its ASCII code ('A' = 65, 'M' = 77, 'N' = 78, 'P' = 80, and so on)
118 | |||
119 | ||| | Flat index | State | Char code | Char | Meaning       |
120 | ||| | ---------- | ----- | --------- | ---- | ------------- |
121 | ||| | 65         | 0     | 65        | 'A'  | δ(0, 'A') = 1 |
122 | ||| | 321        | 1     | 65        | 'A'  | δ(1, 'A') = 1 |
123 | ||| | 334        | 1     | 78        | 'N'  | δ(1, 'N') = 2 |
124 | ||| | 577        | 2     | 65        | 'A'  | δ(2, 'A') = 1 |
125 | ||| | 592        | 2     | 80        | 'P'  | δ(2, 'P') = 3 |
126 | ||| | 833        | 3     | 65        | 'A'  | δ(3, 'A') = 4 |
127 | ||| | 1089       | 4     | 65        | 'A'  | δ(4, 'A') = 1 |
128 | ||| | 1102       | 4     | 78        | 'N'  | δ(4, 'N') = 5 |
129 | ||| | 1345       | 5     | 65        | 'A'  | δ(5, 'A') = 1 |
130 | ||| | 1357       | 5     | 77        | 'M'  | δ(5, 'M') = 6 |
131 | ||| | 1601       | 6     | 65        | 'A'  | δ(6, 'A') = 7 |
132 | ||| | 1857       | 7     | 65        | 'A'  | δ(7, 'A') = 1 |
133 | ||| | 1870       | 7     | 78        | 'N'  | δ(7, 'N') = 8 |
134 | ||| | 2113       | 8     | 65        | 'A'  | δ(8, 'A') = 1 |
135 | |||
136 | export
137 | automaton :  (bs : ByteString)
138 |           -> F1 s (Maybe (MArray s (mult (plus (length bs) 1) 256) Nat))
139 | automaton bs t =
140 |   let arr  # t := unsafeMArray1 (mult (plus (length bs) 1) 256) t
141 |       bord # t := kmpBorders bs t
142 |       Just bord' := bord
143 |         | Nothing => Nothing # t
144 |     in go Z arr bord' t
145 |   where
146 |     fillState :  (state : Nat)
147 |               -> (byte : Nat)
148 |               -> (patbyte : Maybe Nat)
149 |               -> (bordcur : Nat)
150 |               -> (statebase : Nat)
151 |               -> (arr : MArray s (mult (plus (length bs) 1) 256) Nat)
152 |               -> F1 s (Maybe (MArray s (mult (plus (length bs) 1) 256) Nat))
153 |     fillState state byte patbyte bordcur statebase arr t =
154 |       let idx           := plus statebase byte
155 |           Just idx'     := the (Maybe (Fin (mult (plus (length bs) 1) 256))) (tryNatToFin idx)
156 |             | Nothing =>
157 |                 Nothing # t
158 |           Just patbyte' := patbyte
159 |             | Nothing =>
160 |                 let False        := state == Z
161 |                       | True =>
162 |                           let () # t := set arr idx' Z t
163 |                               False  := byte == Z
164 |                                 | True =>
165 |                                     Just arr # t
166 |                             in assert_total (fillState state (minus byte 1) patbyte bordcur statebase arr t)
167 |                     fidx         := plus (mult bordcur 256) byte
168 |                     Just fidx'   := tryNatToFin fidx
169 |                       | Nothing => Nothing # t
170 |                     bordcur' # t := get arr fidx' t
171 |                     ()       # t := set arr idx' bordcur' t
172 |                     False  := byte == Z
173 |                       | True =>
174 |                           Just arr # t
175 |                   in assert_total (fillState state (minus byte 1) patbyte bordcur' statebase arr t)
176 |           False         := byte == patbyte'
177 |             | True =>
178 |                 let () # t := set arr idx' (S state) t
179 |                     False  := byte == Z
180 |                       | True =>
181 |                           Just arr # t
182 |                   in assert_total (fillState state (minus byte 1) patbyte bordcur statebase arr t)
183 |           False         := state == Z
184 |             | True =>
185 |                 let () # t := set arr idx' Z t
186 |                     False  := byte == Z
187 |                       | True =>
188 |                           Just arr # t
189 |                   in assert_total (fillState state (minus byte 1) patbyte bordcur statebase arr t)
190 |           fidx          := plus (mult bordcur 256) byte
191 |           Just fidx'    := tryNatToFin fidx
192 |             | Nothing =>
193 |                 Nothing # t
194 |           bordcur' # t  := get arr fidx' t
195 |           ()       # t  := set arr idx' bordcur' t
196 |           False         := byte == Z
197 |             | True =>
198 |                 Just arr # t
199 |         in assert_total (fillState state (minus byte 1) patbyte bordcur' statebase arr t)
200 |     go :  (state : Nat)
201 |        -> (arr : MArray s (mult (plus (length bs) 1) 256) Nat)
202 |        -> (bord : MArray s (S (length bs)) Nat)
203 |        -> F1 s (Maybe (MArray s (mult (plus (length bs) 1) 256) Nat))
204 |     go state arr bord t =
205 |       let False        := state > length bs
206 |             | True =>
207 |                 Just arr # t
208 |           Just state'  := tryNatToFin state
209 |            | Nothing => Nothing # t
210 |           bordcur # t  := get bord state' t
211 |           patbyte      :=
212 |             case index state bs of
213 |               Nothing =>
214 |                 Nothing
215 |               Just b  =>
216 |                 Just (cast {to=Nat} b)
217 |           statebase    := mult state 256
218 |           arr'     # t := fillState state 255 patbyte bordcur statebase arr t
219 |           Just arr''   := arr'
220 |            | Nothing => Nothing # t
221 |         in assert_total (go (S state) arr'' bord t)
222 |
223 | --------------------------------------------------------------------------------
224 | --          Boyer-Moore Preprocessing
225 | --------------------------------------------------------------------------------
226 |
227 | ||| Constructs a lookup table recording the last occurrence of each byte
228 | ||| in the given pattern.
229 | |||
230 | ||| For every byte value, the table stores the index of its last
231 | ||| occurrence within the pattern, excluding the final position.  
232 | |||
233 | ||| This information allows for efficient computation of how far the search
234 | ||| window can safely shift after a mismatch.
235 | |||
236 | ||| When a mismatch occurs at pattern position (position in pattern) on byte (b),
237 | ||| the pattern can be shifted right by at least:
238 | |||
239 | ||| (position in pattern) - (last occurrence of b in initial pattern)
240 | |||
241 | ||| If the byte b does not appear anywhere in the pattern, the search
242 | ||| window can shift so that the pattern starts immediately after the
243 | ||| mismatched byte, resulting in a default shift of 1.
244 | |||
245 | ||| This table is typically used in Boyer–Moore–style pattern matching
246 | ||| algorithms to determine optimal skip distances after mismatches.
247 | |||
248 | ||| O((length of pattern) + (alphabet size))
249 | |||
250 | ||| Example: "ANPANMAN"
251 | |||
252 | ||| | Flat index / ASCII | char | value |
253 | ||| | ------------------ | ---- | ----- |
254 | ||| |        65          | 'A'  |    -6 |
255 | ||| |        77          | 'M'  |    -5 |
256 | ||| |        78          | 'N'  |    -4 |
257 | ||| |        80          | 'P'  |    -2 |
258 | |||
259 | export
260 | occurrences :  (bs : ByteString)
261 |             -> {0 prf : So (not $ null bs)}
262 |             -> F1 s (Maybe (MArray s 256 Int))
263 | occurrences bs t =
264 |   let arr  # t := marray1 256 (the Int 1) t
265 |       arr' # t := go Z (length bs) bs arr t
266 |       Just arr'' := arr'
267 |         | Nothing =>
268 |             Nothing # t
269 |     in Just arr'' # t
270 |   where
271 |     go :  (i : Nat)
272 |        -> (patend : Nat)
273 |        -> (bs : ByteString)
274 |        -> (arr : MArray s 256 Int)
275 |        -> F1 s (Maybe (MArray s 256 Int))
276 |     go i patend bs arr t =
277 |       let False     := (S i) >= patend
278 |             | True =>
279 |                 Just arr # t
280 |           i'        := index i bs
281 |           Just i''  := i'
282 |             | Nothing =>
283 |                 Nothing # t
284 |           Just i''' := tryNatToFin (cast {to=Nat} i'')
285 |             | Nothing =>
286 |                 Nothing # t
287 |           ()    # t := set arr i''' (negate $ cast {to=Int} i) t
288 |         in assert_total (go (S i) patend bs arr t)
289 |           
290 | ||| Builds the table of suffix lengths for the given pattern.
291 | |||
292 | ||| The value at index `i` is the length of the longest common suffix
293 | ||| between the entire pattern and the prefix of the pattern ending at `i`.
294 | |||
295 | ||| Typically, most entries are 0. Only when the byte at position `i`
296 | ||| matches the final byte of the pattern can the value be positive.
297 | |||
298 | ||| The final entry (at `patEnd`) equals the pattern length, since the
299 | ||| pattern is identical to itself. In general, `0 <= ar[i] <= i + 1`.
300 | |||
301 | ||| To ensure linear preprocessing, the algorithm avoids the naive
302 | ||| quadratic approach by reusing information from previously identified
303 | ||| suffixes.
304 | |||
305 | ||| When the current index lies within an already known suffix, we align
306 | ||| that suffix with the end of the pattern and check whether it extends
307 | ||| beyond the current position. If so, we reuse the stored suffix length;
308 | ||| otherwise, we extend the suffix explicitly.
309 | |||
310 | ||| If the current index lies outside any known suffix, we compare against
311 | ||| the final byte of the pattern. If this yields a suffix of length > 1,
312 | ||| we enter the “known suffix” case for subsequent indices; otherwise,
313 | ||| we continue scanning normally.
314 | |||
315 | ||| Example : "ANPANMAN"
316 | |||
317 | ||| Raw suffix-lengths array used to compute the good suffix shift table
318 | |||
319 | ||| | i | pat[i] | matches pattern end? | diff = patEnd - i | nextI = i-1 | prevI (dec diff nextI) | ar[i] |
320 | ||| | - | ------ | -------------------- | ----------------- | ----------- | ---------------------- | ----- |
321 | ||| | 0 |    A   |          No          |         -         |      -      |            -           |   0   |
322 | ||| | 1 |    N   |          Yes         |         6         |      0      |           -1           |   2   |
323 | ||| | 2 |    P   |          No          |         -         |      -      |            -           |   0   |
324 | ||| | 3 |    A   |          No          |         -         |      -      |            -           |   0   |
325 | ||| | 4 |    N   |          Yes         |         3         |      3      |            2           |   2   |
326 | ||| | 5 |    M   |          No          |         -         |      -      |            -           |   0   |
327 | ||| | 6 |    A   |          No          |         -         |      -      |            -           |   0   |
328 | ||| | 7 |    N   |          -           |         -         |      -      |            -           |   8   |
329 | |||
330 | export
331 | suffixLengths :  (bs : ByteString)
332 |               -> {0 prf : So (not $ null bs)}
333 |               -> F1 s (Maybe (MArray s (length bs) Int))
334 | suffixLengths bs t =
335 |   let arr    # t := marray1 (length bs) (the Int 0) t
336 |       Just idx   := tryNatToFin (minus (length bs) 1)
337 |         | Nothing =>
338 |             Nothing # t
339 |       ()     # t := set arr idx (cast {to=Int} (length bs)) t
340 |       arr'   # t := noSuffix (cast {to=Int} (minus (length bs) 2)) bs arr t
341 |       Just arr'' := arr'
342 |         | Nothing =>
343 |             Nothing # t
344 |     in Just arr'' # t
345 |   where
346 |     dec :  (diff : Int)
347 |         -> (j : Int)
348 |         -> F1 s (Maybe Int)
349 |     dec diff j t =
350 |       let False      := j < 0
351 |             | True =>
352 |                 Just j # t
353 |           j'         := index (cast {to=Nat} j) bs
354 |           Just j''   := j'
355 |             | Nothing =>
356 |                 Nothing # t
357 |           j'''       := index (cast {to=Nat} (j + diff)) bs
358 |           Just j'''' := j'''
359 |             | Nothing =>
360 |                 Nothing # t
361 |           False      := j'' /= j''''
362 |             | True =>
363 |                 Just j # t
364 |         in assert_total (dec diff (j - 1) t)
365 |     mutual
366 |       suffixLoop :  (pre : Int)
367 |                  -> (end : Int)
368 |                  -> (idx : Int)
369 |                  -> (bs : ByteString)
370 |                  -> (arr : MArray s (length bs) Int)
371 |                  -> F1 s (Maybe (MArray s (length bs) Int))
372 |       suffixLoop _   _   0   _  arr t =
373 |         Just arr # t
374 |       suffixLoop pre end idx bs arr t =
375 |         let True         := pre < idx
376 |               | False =>
377 |                   noSuffix idx bs arr t
378 |             idx'         := index (cast {to=Nat} idx) bs
379 |             Just idx''   := idx'
380 |               | Nothing =>
381 |                   Nothing # t
382 |             idx'''       := index (minus (length bs) 1) bs
383 |             Just idx'''' := idx'''
384 |               | Nothing =>
385 |                   Nothing # t
386 |             False        := idx'' /= idx''''
387 |               | True =>
388 |                   let Just idxs := tryNatToFin (cast {to=Nat} idx)
389 |                         | Nothing =>
390 |                             Nothing # t
391 |                       ()    # t := set arr idxs 0 t
392 |                     in assert_total (suffixLoop pre (end - 1) (idx - 1) bs arr t)
393 |             Just end'    := tryNatToFin (cast {to=Nat} end)
394 |               | Nothing =>
395 |                   Nothing # t
396 |             prevs    # t := get arr end' t
397 |             Just idxs    := tryNatToFin (cast {to=Nat} idx)
398 |               | Nothing =>
399 |                   Nothing # t
400 |             False        := (pre + prevs) < idx
401 |               | True =>
402 |                   let () # t := set arr idxs prevs t
403 |                     in assert_total (suffixLoop pre (end - 1) (idx - 1) bs arr t)
404 |             pri      # t := dec (cast {to=Int} (minus (length bs) (cast {to=Nat} idx))) pre t
405 |             Just pri'    := pri
406 |               | Nothing =>
407 |                   Nothing # t
408 |             ()       # t := set arr idxs (idx - pri') t
409 |           in assert_total (suffixLoop pri' (cast {to=Int} (minus (length bs) 2)) (idx - 1) bs arr t)
410 |       noSuffix :  (i : Int)
411 |                -> (bs : ByteString)
412 |                -> (arr : MArray s (length bs) Int)
413 |                -> F1 s (Maybe (MArray s (length bs) Int))
414 |       noSuffix 0 _  arr t =
415 |         Just arr # t
416 |       noSuffix i bs arr t =
417 |         let patati         := index (cast {to=Nat} i) bs
418 |             Just patati'   := patati
419 |               | Nothing =>
420 |                   Nothing # t
421 |             patatend       := index (minus (length bs) 1) bs
422 |             Just patatend' := patatend
423 |               | Nothing =>
424 |                   Nothing # t
425 |             True           := patati' == patatend'
426 |               | False =>
427 |                   let Just i' := tryNatToFin (cast {to=Nat} i)
428 |                         | Nothing =>
429 |                             Nothing # t
430 |                       ()  # t := set arr i' 0 t
431 |                     in assert_total (noSuffix (i - 1) bs arr t)
432 |             diff           := (cast {to=Int} (minus (length bs) 1)) - i
433 |             nexti          := i - 1
434 |             previ      # t := dec diff nexti t
435 |             Just previ'    := previ
436 |               | Nothing =>
437 |                   Nothing # t
438 |             Just i'        := tryNatToFin (cast {to=Nat} i)
439 |               | Nothing =>
440 |                   Nothing # t
441 |             False          := previ' == nexti
442 |               | True =>
443 |                   let () # t := set arr i' 1 t
444 |                     in assert_total (noSuffix nexti bs arr t)
445 |             ()         # t := set arr i' (i - previ') t
446 |           in assert_total (suffixLoop previ' (cast {to=Int} (minus (length bs) 2)) nexti bs arr t)
447 |
448 | ||| Table of suffix-shifts
449 | |||
450 | ||| When a mismatch occurs at pattern position patpos, assumed to be not the
451 | ||| last position in the pattern, the suffix u of length (patend - patpos)
452 | ||| has been successfully matched.
453 | ||| Let c be the byte in the pattern at position patpos.
454 | |||
455 | ||| If the sub-pattern u also occurs in the pattern somewhere *not* preceded
456 | ||| by c, let upos be the position of the last byte in u for the last of
457 | ||| all such occurrences. Then there can be no match if the window is shifted
458 | ||| less than (patend - upos) places, because either the part of the string
459 | ||| which matched the suffix u is not aligned with an occurrence of u in the
460 | ||| pattern, or it is aligned with an occurrence of u which is preceded by
461 | ||| the same byte c as the originally matched suffix.
462 | |||
463 | ||| If the complete sub-pattern u does not occur again in the pattern, or all
464 | ||| of its occurrences are preceded by the byte c, then we can align the
465 | ||| pattern with the string so that a suffix v of u matches a prefix of the
466 | ||| pattern. If v is chosen maximal, no smaller shift can give a match, so
467 | ||| we can shift by at least (patlen - length v).
468 | |||
469 | ||| If a complete match is encountered, we can shift by at least the same
470 | ||| amount as if the first byte of the pattern was a mismatch, no complete
471 | ||| match is possible between these positions.
472 | |||
473 | ||| For non-periodic patterns, only very short suffixes will usually occur
474 | ||| again in the pattern, so if a longer suffix has been matched before a
475 | ||| mismatch, the window can then be shifted entirely past the partial
476 | ||| match, so that part of the string will not be re-compared.
477 | ||| For periodic patterns, the suffix shifts will be shorter in general,
478 | ||| leading to an O(strlen * patlen) worst-case performance.
479 | |||
480 | ||| To compute the suffix-shifts, we use an array containing the lengths of
481 | ||| the longest common suffixes of the entire pattern and its prefix ending
482 | ||| with position pos.
483 | |||
484 | ||| Example: "ANPANMAN"
485 | |||
486 | ||| | idx | suff[idx] | target = patEnd - suff[idx] | value = patEnd - idx |    ar after write |
487 | ||| | --- | --------- | --------------------------- | -------------------- | ----------------- |
488 | ||| |   0 |         0 |                   7 - 0 = 7 |            7 - 0 = 7 | [6,6,6,6,6,6,8,7] |
489 | ||| |   1 |         2 |                   7 - 2 = 5 |            7 - 1 = 6 | [6,6,6,6,6,6,8,7] |
490 | ||| |   2 |         0 |                           7 |            7 - 2 = 5 | [6,6,6,6,6,6,8,5] |
491 | ||| |   3 |         0 |                           7 |            7 - 3 = 4 | [6,6,6,6,6,6,8,4] |
492 | ||| |   4 |         2 |                   7 - 2 = 5 |            7 - 4 = 3 | [6,6,6,6,6,3,8,4] |
493 | ||| |   5 |         0 |                           7 |            7 - 5 = 2 | [6,6,6,6,6,3,8,2] |
494 | ||| |   6 |         0 |                           7 |            7 - 6 = 1 | [6,6,6,6,6,3,8,1] |
495 | |||
496 | export
497 | suffixShifts :  (bs : ByteString)
498 |              -> {0 prf : So (not $ null bs)}
499 |              -> F1 s (Maybe (MArray s (length bs) Int))
500 | suffixShifts bs {prf} t =
501 |   let arr      # t := marray1 (length bs) (cast {to=Int} (length bs)) t
502 |       suff     # t := suffixLengths bs {prf=prf} t
503 |       Just suff'   := suff
504 |         | Nothing =>
505 |             Nothing # t
506 |       arr'     # t := prefixShift (cast {to=Int} (minus (length bs) 2)) 0 bs suff' arr t
507 |       Just arr''   := arr'
508 |         | Nothing =>
509 |             Nothing # t
510 |       arr'''   # t := suffixShift 0 bs suff' arr'' t
511 |       Just arr'''' := arr'''
512 |         | Nothing =>
513 |             Nothing # t
514 |     in Just arr'''' # t
515 |   where
516 |     fillToShift :  (i : Int)
517 |                 -> (shift : Int)
518 |                 -> (bs : ByteString)
519 |                 -> (arr : MArray s (length bs) Int)
520 |                 -> F1 s (Maybe (MArray s (length bs) Int))
521 |     fillToShift i shift bs arr t =
522 |       let False   := i == shift
523 |             | True =>
524 |                 Just arr # t
525 |           Just i' := tryNatToFin (cast {to=Nat} i)
526 |             | Nothing =>
527 |                 Nothing # t
528 |           ()  # t := set arr i' shift t
529 |         in assert_total (fillToShift (i + 1) shift bs arr t)
530 |     prefixShift :  (idx : Int)
531 |                 -> (j : Int)
532 |                 -> (bs : ByteString)
533 |                 -> (suff : MArray s (length bs) Int)
534 |                 -> (arr : MArray s (length bs) Int)
535 |                 -> F1 s (Maybe (MArray s (length bs) Int))
536 |     prefixShift idx j bs suff arr t =
537 |       let False      := idx < 0
538 |             | True =>
539 |                 Just arr # t
540 |           Just idx'  := tryNatToFin (cast {to=Nat} idx)
541 |             | Nothing =>
542 |                 Nothing # t
543 |           idx''  # t := get suff idx' t
544 |           True       := idx'' ==  (idx + 1)
545 |             | False =>
546 |                 assert_total (prefixShift (idx - 1) j bs suff arr t)
547 |           shift      := (cast {to=Int} (minus (length bs) 1)) - idx
548 |           arr'   # t := fillToShift j shift bs arr t
549 |           Just arr'' := arr'
550 |             | Nothing =>
551 |                 Nothing # t
552 |         in assert_total (prefixShift (idx - 1) shift bs suff arr'' t)                                      
553 |     suffixShift :  (idx : Int)
554 |                 -> (bs : ByteString)
555 |                 -> (suff : MArray s (length bs) Int)
556 |                 -> (arr : MArray s (length bs) Int)
557 |                 -> F1 s (Maybe (MArray s (length bs) Int))
558 |     suffixShift idx bs suff arr t =
559 |       let patend       := cast {to=Int} (minus (length bs) 1)
560 |           False        := idx >= patend
561 |             | True =>
562 |                 Just arr # t
563 |           Just idx'    := tryNatToFin (cast {to=Nat} idx)
564 |             | Nothing =>
565 |                 Nothing # t
566 |           idx''    # t := get suff idx' t
567 |           target       := patend - idx''
568 |           Just target' := tryNatToFin (cast {to=Nat} target)
569 |             | Nothing =>
570 |                 Nothing # t
571 |           value        := patend - idx
572 |           ()       # t := set arr target' value t
573 |         in assert_total (suffixShift (idx + 1) bs suff arr t)
574 |