
   0 | ||| Utilities for the Boyer-Moore string searching algorithm.
   1 | module Data.ByteString.Search.BoyerMoore.Internal
   2 | 
   3 | import Data.Array.Core
   4 | import Data.Bits
   5 | import Data.ByteString
   6 | import Data.Enum
   7 | import Data.Linear.Ref1
   8 | 
   9 | %hide Data.Buffer.Core.get
  10 | %hide Data.Buffer.Core.set
  11 | %hide Data.List.Elem.get
  12 | 
  13 | %default total
  14 | 
  15 | ||| One greater than the maximum supported Boyer–Moore pattern size.
  16 | |||
  17 | ||| Pattern-table indices are represented by `Bits32`, so the pattern length
  18 | ||| must fit within that index space.
  19 | public export
  20 | bmPatternLimit : Bits32
  21 | bmPatternLimit = 0xffffffff
  22 | 
  23 | ||| Runtime description of a Boyer–Moore pattern index space.
  24 | |||
  25 | ||| `size` is the number of bytes in the pattern. Boyer–Moore preprocessing
  26 | ||| requires a nonempty pattern, so every valid pattern space contains at
  27 | ||| least one index.
  28 | |||
  29 | public export
  30 | record BMPatternSpace where
  31 |   constructor MkBMPatternSpace
  32 |   size : Bits32
  33 |   0 sizePositive : 0 < size
  34 |   0 sizeBounded : size < Data.ByteString.Search.BoyerMoore.Internal.bmPatternLimit
  35 | 
  36 | ||| A valid position within a Boyer–Moore pattern.
  37 | |||
  38 | ||| The bound proof carried by `Index` is erased at runtime.
  39 | |||
  40 | public export
  41 | PatternIndex : Bits32 -> Type
  42 | PatternIndex = Index
  43 | 
  44 | ||| Construct the Boyer–Moore index space for a nonempty pattern.
  45 | |||
  46 | ||| The pattern size is validated once during preprocessing. Subsequent table
  47 | ||| accesses use bounded `PatternIndex` values.
  48 | |||
  49 | export
  50 | bmPatternSpace :  (bs : ByteString)
  51 |                -> {0 prf : So (not $ null bs)}
  52 |                -> Maybe BMPatternSpace
  53 | bmPatternSpace bs =
  54 |   let size : Bits32
  55 |       size = cast $ length bs
  56 |    in case tryIndex {r = bmPatternLimit} size of
  57 |         Nothing              =>
  58 |           Nothing
  59 |         Just (I size' {prf = sizePrf}) =>
  60 |           Just (MkBMPatternSpace size' (believe_me ()) sizePrf)
  61 | 
  62 | ||| Return the runtime value represented by a bounded pattern index.
  63 | |||
  64 | export %inline
  65 | patternIndexValue :  {size : Bits32}
  66 |                   -> PatternIndex size
  67 |                   -> Bits32
  68 | patternIndexValue (I idx) = idx
  69 | 
  70 | ||| Convert a construction-time `Nat` position into a bounded pattern index.
  71 | |||
  72 | ||| This validation is used during preprocessing and is not part of the
  73 | ||| Boyer–Moore target-scanning hot path.
  74 | |||
  75 | export %inline
  76 | toPatternIndex :  (space : BMPatternSpace)
  77 |                -> Nat
  78 |                -> Maybe (PatternIndex space.size)
  79 | toPatternIndex space idx =
  80 |   tryIndex {r = space.size} (cast idx)
  81 | 
  82 | ||| Runtime-sized mutable integer table used by Boyer–Moore preprocessing.
  83 | |||
  84 | ||| The underlying primitive array contains exactly `size` entries.
  85 | |||
  86 | public export
  87 | record BMIntTable (s : Type) (size : Bits32) where
  88 |   constructor MkBMIntTable
  89 |   arr : AnyPtr
  90 | 
  91 | ||| A runtime-sized Boyer–Moore integer table packaged with its pattern
  92 | ||| index space.
  93 | |||
  94 | public export
  95 | record BMPatternTable (s : Type) where
  96 |   constructor MkBMPatternTable
  97 |   space : BMPatternSpace
  98 |   table : BMIntTable s space.size
  99 | 
 100 | ||| Allocate an uninitialized Boyer–Moore integer table.
 101 | |||
 102 | export
 103 | newBMIntTable :  {size : Bits32}
 104 |               -> F1 s (BMIntTable s size)
 105 | newBMIntTable {size} t =
 106 |   let arr # t := ffi (prim__emptyArray $ cast size) t
 107 |    in MkBMIntTable arr # t
 108 | 
 109 | ||| Read an entry from a Boyer–Moore integer table.
 110 | |||
 111 | ||| The index is already bounded, so no dynamic table-bounds conversion is
 112 | ||| performed.
 113 | |||
 114 | export %inline
 115 | bmGet :  {size : Bits32}
 116 |       -> BMIntTable s size
 117 |       -> PatternIndex size
 118 |       -> F1 s Int
 119 | bmGet table idx t =
 120 |   let I pos := idx
 121 |    in believe_me (prim__arrayGet table.arr (cast pos)) # t
 122 | 
 123 | ||| Write an entry to a Boyer–Moore integer table.
 124 | |||
 125 | ||| The index is already bounded, so no dynamic table-bounds conversion is
 126 | ||| performed.
 127 | |||
 128 | export %inline
 129 | bmSet :  {size : Bits32}
 130 |       -> BMIntTable s size
 131 |       -> PatternIndex size
 132 |       -> Int
 133 |       -> F1' s
 134 | bmSet table idx value t =
 135 |   let I pos := idx
 136 |    in ffi (prim__arraySet table.arr (cast pos) (believe_me value)) t
 137 | 
 138 | ||| Allocate and initialize every entry in a Boyer–Moore integer table.
 139 | |||
 140 | ||| The initialization loop ranges from zero to `size - 1`, so each primitive
 141 | ||| write is known by construction to lie within the newly allocated array.
 142 | |||
 143 | export
 144 | newBMIntTableWith :  {size : Bits32}
 145 |                   -> Int
 146 |                   -> F1 s (BMIntTable s size)
 147 | newBMIntTableWith {size} initial t =
 148 |   let table # t := newBMIntTable {size} t
 149 |     in fill 0 table t
 150 |   where
 151 |     fill :  {size : Bits32}
 152 |          -> Bits32
 153 |          -> BMIntTable s size
 154 |          -> F1 s (BMIntTable s size)
 155 |     fill idx table t =
 156 |       let False  := idx == size
 157 |             | True =>
 158 |                 table # t
 159 |           () # t := ffi (prim__arraySet table.arr (cast idx) (believe_me initial)) t
 160 |         in assert_total (fill (idx + 1) table t)
 161 | 
 162 | ||| Mutable Boyer–Moore bad-character occurrence table.
 163 | |||
 164 | ||| The table contains exactly one entry for each possible byte value and can
 165 | ||| therefore be indexed directly by `Bits8`.
 166 | |||
 167 | public export
 168 | record OccurrenceTable (s : Type) where
 169 |   constructor MkOccurrenceTable
 170 |   arr : AnyPtr
 171 | 
 172 | ||| Allocate an occurrence table with every byte initialized to shift `1`.
 173 | |||
 174 | export
 175 | newOccurrenceTable : F1 s (OccurrenceTable s)
 176 | newOccurrenceTable t =
 177 |   let arr # t := ffi (prim__emptyArray 256) t
 178 |       table   := MkOccurrenceTable arr
 179 |    in fill 0 table t
 180 |   where
 181 |     fill :  Nat
 182 |          -> OccurrenceTable s
 183 |          -> F1 s (OccurrenceTable s)
 184 |     fill idx table t =
 185 |       let False := idx == 256
 186 |             | True =>
 187 |                 table # t
 188 |           () # t := ffi (prim__arraySet table.arr (cast idx) (believe_me $ the Int 1)) t
 189 |        in assert_total (fill (S idx) table t)
 190 | 
 191 | ||| Read the bad-character entry associated with a byte.
 192 | |||
 193 | ||| Since `Bits8` intrinsically ranges from 0 through 255, no bounds
 194 | ||| conversion or validation is required.
 195 | |||
 196 | export %inline
 197 | occurrence :  OccurrenceTable s
 198 |            -> Bits8
 199 |            -> F1 s Int
 200 | occurrence table byte t =
 201 |   believe_me (prim__arrayGet table.arr (cast byte)) # t
 202 | 
 203 | ||| Write the bad-character entry associated with a byte.
 204 | |||
 205 | ||| Since `Bits8` intrinsically ranges from 0 through 255, no bounds
 206 | ||| conversion or validation is required.
 207 | |||
 208 | export %inline
 209 | setOccurrence :  OccurrenceTable s
 210 |               -> Bits8
 211 |               -> Int
 212 |               -> F1' s
 213 | setOccurrence table byte value t =
 214 |   ffi (prim__arraySet table.arr (cast byte) (believe_me value)) t
 215 | 
 216 | ||| Constructs a lookup table recording the last occurrence of each byte
 217 | ||| in the given pattern.
 218 | |||
 219 | ||| For every byte value, the table stores the negated index of its last
 220 | ||| occurrence within the pattern, excluding the final pattern position.
 221 | |||
 222 | ||| The table is indexed directly by `Bits8`, eliminating the previous
 223 | ||| `Bits8 -> Nat -> Fin 256` conversion and its dynamic bounds validation.
 224 | |||
 225 | ||| O((length of pattern) + 256)
 226 | |||
 227 | export
 228 | occurrences :  (bs : ByteString)
 229 |             -> {0 prf : So (not $ null bs)}
 230 |             -> F1 s (Maybe (OccurrenceTable s))
 231 | occurrences bs t =
 232 |   let arr # t := newOccurrenceTable t
 233 |     in go Z (length bs) arr t
 234 |   where
 235 |     go :  (i : Nat)
 236 |       -> (patend : Nat)
 237 |       -> OccurrenceTable s
 238 |       -> F1 s (Maybe (OccurrenceTable s))
 239 |     go i patend arr t =
 240 |       let False     := S i >= patend
 241 |             | True =>
 242 |                 Just arr # t
 243 |           Just byte := index i bs
 244 |             | Nothing =>
 245 |                 Nothing # t
 246 |           ()    # t := setOccurrence arr byte (negate $ cast {to=Int} i) t
 247 |        in assert_total (go (S i) patend arr t)
 248 | 
 249 | ||| Builds the table of suffix lengths for the given pattern.
 250 | |||
 251 | ||| The table is backed by a runtime-sized primitive array containing exactly
 252 | ||| `length bs` entries.
 253 | |||
 254 | ||| Table positions are represented by bounded `PatternIndex` values rather
 255 | ||| than `Fin (length bs)`, eliminating `tryNatToFin` from primitive table
 256 | ||| reads and writes.
 257 | |||
 258 | export
 259 | suffixLengths :  (bs : ByteString)
 260 |               -> {0 prf : So (not $ null bs)}
 261 |               -> F1 s (Maybe (BMPatternTable s))
 262 | suffixLengths bs {prf} t =
 263 |   let Just stspace := bmPatternSpace bs {prf = prf}
 264 |         | Nothing =>
 265 |             Nothing # t
 266 |       arr      # t := newBMIntTableWith {size = stspace.size} 0 t
 267 |       lastidxnat   := minus (length bs) 1
 268 |       Just lastidx := toPatternIndex stspace lastidxnat
 269 |         | Nothing =>
 270 |             Nothing # t
 271 |       ()       # t := bmSet arr lastidx (cast {to=Int} $ length bs) t
 272 |       arr'     # t := noSuffix stspace (cast {to=Int} $ minus (length bs) 2) arr t
 273 |       Just arr''   := arr'
 274 |         | Nothing =>
 275 |             Nothing # t
 276 |     in Just (MkBMPatternTable stspace arr'') # t
 277 |   where
 278 |     dec :  (diff : Int)
 279 |         -> (j : Int)
 280 |         -> F1 s (Maybe Int)
 281 |     dec diff j t =
 282 |       let False        := j < 0
 283 |             | True =>
 284 |                 Just j # t
 285 |           Just jbyte   := index (cast {to=Nat} j) bs
 286 |             | Nothing =>
 287 |                 Nothing # t
 288 |           Just shifted := index (cast {to=Nat} (j + diff)) bs
 289 |             | Nothing =>
 290 |                 Nothing # t
 291 |           False        := jbyte /= shifted
 292 |             | True =>
 293 |                 Just j # t
 294 |         in assert_total (dec diff (j - 1) t)
 295 |     mutual
 296 |       suffixLoop :  (stspace : BMPatternSpace)
 297 |                  -> (pre : Int)
 298 |                  -> (end : Int)
 299 |                  -> (idx : Int)
 300 |                  -> (arr : BMIntTable s stspace.size)
 301 |                  -> F1 s (Maybe (BMIntTable s stspace.size))
 302 |       suffixLoop _       _   _   0   arr t =
 303 |         Just arr # t
 304 |       suffixLoop stspace pre end idx arr t =
 305 |         let True         := pre < idx
 306 |               | False =>
 307 |                   noSuffix stspace idx arr t
 308 |             Just idxbyte := index (cast {to=Nat} idx) bs
 309 |               | Nothing =>
 310 |                   Nothing # t
 311 |             Just endbyte := index (minus (length bs) 1) bs
 312 |               | Nothing =>
 313 |                   Nothing # t
 314 |             Just idxpos := toPatternIndex stspace (cast {to=Nat} idx)
 315 |               | Nothing =>
 316 |                   Nothing # t
 317 |             False       := idxbyte /= endbyte
 318 |               | True =>
 319 |                   let () # t := bmSet arr idxpos 0 t
 320 |                     in assert_total (suffixLoop stspace pre (end - 1) (idx - 1) arr t)
 321 |             Just endpos := toPatternIndex stspace (cast {to=Nat} end)
 322 |               | Nothing =>
 323 |                   Nothing # t
 324 |             prevs   # t := bmGet arr endpos t
 325 |             False       := (pre + prevs) < idx
 326 |               | True =>
 327 |                   let () # t := bmSet arr idxpos prevs t
 328 |                     in assert_total (suffixLoop stspace pre (end - 1) (idx - 1) arr t)
 329 |             pri     # t := dec (cast {to=Int} (minus (length bs) (cast {to=Nat} idx))) pre t
 330 |             Just pri'   := pri
 331 |               | Nothing =>
 332 |                   Nothing # t
 333 |             ()      # t := bmSet arr idxpos (idx - pri') t
 334 |           in assert_total (suffixLoop stspace pri' (cast {to=Int} $ minus (length bs) 2) (idx - 1) arr t)
 335 |       noSuffix :  (stspace : BMPatternSpace)
 336 |                -> (i : Int)
 337 |                -> (arr : BMIntTable s stspace.size)
 338 |                -> F1 s (Maybe (BMIntTable s stspace.size))
 339 |       noSuffix _       0 arr t =
 340 |         Just arr # t
 341 |       noSuffix stspace i arr t =
 342 |         let Just patati   := index (cast {to=Nat} i) bs
 343 |               | Nothing =>
 344 |                   Nothing # t
 345 |             Just patatend := index (minus (length bs) 1) bs
 346 |               | Nothing =>
 347 |                   Nothing # t
 348 |             Just ipos     := toPatternIndex stspace (cast {to=Nat} i)
 349 |               | Nothing =>
 350 |                   Nothing # t
 351 |             True          := patati == patatend
 352 |               | False =>
 353 |                   let () # t := bmSet arr ipos 0 t
 354 |                     in assert_total (noSuffix stspace (i - 1) arr t)
 355 |             diff             := cast {to=Int} (minus (length bs) 1) - i
 356 |             nexti            := i - 1
 357 |             previ        # t := dec diff nexti t
 358 |             Just previ'      := previ
 359 |               | Nothing =>
 360 |                   Nothing # t
 361 |             False            := previ' == nexti
 362 |               | True =>
 363 |                   let () # t := bmSet arr ipos 1 t
 364 |                     in assert_total (noSuffix stspace nexti arr t)
 365 |             ()           # t := bmSet arr ipos (i - previ') t
 366 |           in assert_total (suffixLoop stspace previ' (cast {to=Int} $ minus (length bs) 2) nexti arr t)
 367 | 
 368 | ||| Build the Boyer–Moore good-suffix shift table.
 369 | |||
 370 | ||| The suffix-length table and resulting shift table share the same bounded
 371 | ||| pattern index space.
 372 | |||
 373 | ||| Primitive table accesses therefore use `PatternIndex` rather than
 374 | ||| dynamically constructed `Fin` values.
 375 | |||
 376 | export
 377 | suffixShifts :  (bs : ByteString)
 378 |              -> {0 prf : So (not $ null bs)}
 379 |              -> F1 s (Maybe (BMPatternTable s))
 380 | suffixShifts bs {prf} t =
 381 |   let suff                              # t := suffixLengths bs {prf = prf} t
 382 |       Just (MkBMPatternTable stspace suff') := suff
 383 |         | Nothing =>
 384 |             Nothing # t
 385 |       arr                               # t := newBMIntTableWith {size = stspace.size} (cast {to=Int} $ length bs) t
 386 |       arr'                              # t := prefixShift stspace (cast {to=Int} $ minus (length bs) 2) 0 suff' arr t
 387 |       Just arr''                            := arr'
 388 |         | Nothing =>
 389 |             Nothing # t
 390 |       arr'''                            # t := suffixShift stspace 0 suff' arr'' t
 391 |       Just arr''''                          := arr'''
 392 |         | Nothing =>
 393 |             Nothing # t
 394 |     in Just (MkBMPatternTable stspace arr'''') # t
 395 |   where
 396 |     fillToShift :  (stspace : BMPatternSpace)
 397 |                 -> (i : Int)
 398 |                 -> (shift : Int)
 399 |                 -> (arr : BMIntTable s stspace.size)
 400 |                 -> F1 s (Maybe (BMIntTable s stspace.size))
 401 |     fillToShift stspace i shift arr t =
 402 |       let False     := i == shift
 403 |             | True =>
 404 |                 Just arr # t
 405 |           Just ipos := toPatternIndex stspace (cast {to=Nat} i)
 406 |             | Nothing =>
 407 |                 Nothing # t
 408 |           ()    # t := bmSet arr ipos shift t
 409 |         in assert_total (fillToShift stspace (i + 1) shift arr t)
 410 |     prefixShift :  (stspace : BMPatternSpace)
 411 |                 -> (idx : Int)
 412 |                 -> (j : Int)
 413 |                 -> (suff : BMIntTable s stspace.size)
 414 |                 -> (arr : BMIntTable s stspace.size)
 415 |                 -> F1 s (Maybe (BMIntTable s stspace.size))
 416 |     prefixShift stspace idx j suff arr t =
 417 |       let False       := idx < 0
 418 |             | True =>
 419 |                 Just arr # t
 420 |           Just idxpos := toPatternIndex stspace (cast {to=Nat} idx)
 421 |             | Nothing =>
 422 |                 Nothing # t
 423 |           idxval  # t := bmGet suff idxpos t
 424 |           True        := idxval == idx + 1
 425 |             | False =>
 426 |                 assert_total (prefixShift stspace (idx - 1) j suff arr t)
 427 |           shift       := cast {to=Int} (minus (length bs) 1) - idx
 428 |           arr'    # t := fillToShift stspace j shift arr t
 429 |           Just arr''  := arr'
 430 |             | Nothing =>
 431 |                 Nothing # t
 432 |         in assert_total (prefixShift stspace (idx - 1) shift suff arr'' t)
 433 |     suffixShift :  (stspace : BMPatternSpace)
 434 |                 -> (idx : Int)
 435 |                 -> (suff : BMIntTable s stspace.size)
 436 |                 -> (arr : BMIntTable s stspace.size)
 437 |                 -> F1 s (Maybe (BMIntTable s stspace.size))
 438 |     suffixShift stspace idx suff arr t =
 439 |       let patend         := cast {to=Int} (minus (length bs) 1)
 440 |           False          := idx >= patend
 441 |             | True =>
 442 |                 Just arr # t
 443 |           Just idxpos    := toPatternIndex stspace (cast {to=Nat} idx)
 444 |             | Nothing =>
 445 |                 Nothing # t
 446 |           sufflen    # t := bmGet suff idxpos t
 447 |           target         := patend - sufflen
 448 |           Just targetpos := toPatternIndex stspace (cast {to=Nat} target)
 449 |             | Nothing =>
 450 |                 Nothing # t
 451 |           value          := patend - idx
 452 |           ()         # t := bmSet arr targetpos value t
 453 |         in assert_total (suffixShift stspace (idx + 1) suff arr t)
 454 |