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