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