Data.ByteString.Search.BoyerMoore.Internal

Utilities for the Boyer-Moore string searching algorithm.

Definitions

bmPatternLimit : Bits32

  One greater than the maximum supported Boyer–Moore pattern size.
  
  Pattern-table indices are represented by `Bits32`, so the pattern length
  must fit within that index space.

Totality: total
Visibility: public export

record BMPatternSpace : Type

  Runtime description of a Boyer–Moore pattern index space.
  
  `size` is the number of bytes in the pattern. Boyer–Moore preprocessing
  requires a nonempty pattern, so every valid pattern space contains at
  least one index.
  

Totality: total
Visibility: public export
Constructor: 

MkBMPatternSpace : (size : Bits32) -> (0 _ : 0 < size) -> (0 _ : size < bmPatternLimit) -> BMPatternSpace

Projections:

.size : BMPatternSpace -> Bits32

0 .sizeBounded : ({rec:0} : BMPatternSpace) -> size {rec:0} < bmPatternLimit

0 .sizePositive : ({rec:0} : BMPatternSpace) -> 0 < size {rec:0}

.size : BMPatternSpace -> Bits32

Totality: total
Visibility: public export

size : BMPatternSpace -> Bits32

Totality: total
Visibility: public export

0 .sizePositive : ({rec:0} : BMPatternSpace) -> 0 < size {rec:0}

Totality: total
Visibility: public export

0 sizePositive : ({rec:0} : BMPatternSpace) -> 0 < size {rec:0}

Totality: total
Visibility: public export

0 .sizeBounded : ({rec:0} : BMPatternSpace) -> size {rec:0} < bmPatternLimit

Totality: total
Visibility: public export

0 sizeBounded : ({rec:0} : BMPatternSpace) -> size {rec:0} < bmPatternLimit

Totality: total
Visibility: public export

PatternIndex : Bits32 -> Type

  A valid position within a Boyer–Moore pattern.
  
  The bound proof carried by `Index` is erased at runtime.
  

Totality: total
Visibility: public export

bmPatternSpace : (bs : ByteString) -> Maybe BMPatternSpace

  Construct the Boyer–Moore index space for a nonempty pattern.
  
  The pattern size is validated once during preprocessing. Subsequent table
  accesses use bounded `PatternIndex` values.
  

Totality: total
Visibility: export

patternIndexValue : PatternIndex size -> Bits32

  Return the runtime value represented by a bounded pattern index.
  

Totality: total
Visibility: export

toPatternIndex : (space : BMPatternSpace) -> Nat -> Maybe (PatternIndex (space .size))

  Convert a construction-time `Nat` position into a bounded pattern index.
  
  This validation is used during preprocessing and is not part of the
  Boyer–Moore target-scanning hot path.
  

Totality: total
Visibility: export

record BMIntTable : Type -> Bits32 -> Type

  Runtime-sized mutable integer table used by Boyer–Moore preprocessing.
  
  The underlying primitive array contains exactly `size` entries.
  

Totality: total
Visibility: public export
Constructor: 

MkBMIntTable : AnyPtr -> BMIntTable s size

Projection: 

.arr : BMIntTable s size -> AnyPtr

.arr : BMIntTable s size -> AnyPtr

Totality: total
Visibility: public export

arr : BMIntTable s size -> AnyPtr

Totality: total
Visibility: public export

record BMPatternTable : Type -> Type

  A runtime-sized Boyer–Moore integer table packaged with its pattern
  index space.
  

Totality: total
Visibility: public export
Constructor: 

MkBMPatternTable : (space : BMPatternSpace) -> BMIntTable s (space .size) -> BMPatternTable s

Projections:

.space : BMPatternTable s -> BMPatternSpace

.table : ({rec:0} : BMPatternTable s) -> BMIntTable s ((space {rec:0}) .size)

.space : BMPatternTable s -> BMPatternSpace

Totality: total
Visibility: public export

space : BMPatternTable s -> BMPatternSpace

Totality: total
Visibility: public export

.table : ({rec:0} : BMPatternTable s) -> BMIntTable s ((space {rec:0}) .size)

Totality: total
Visibility: public export

table : ({rec:0} : BMPatternTable s) -> BMIntTable s ((space {rec:0}) .size)

Totality: total
Visibility: public export

newBMIntTable : F1 s (BMIntTable s size)

  Allocate an uninitialized Boyer–Moore integer table.
  

Totality: total
Visibility: export

bmGet : BMIntTable s size -> PatternIndex size -> F1 s Int

  Read an entry from a Boyer–Moore integer table.
  
  The index is already bounded, so no dynamic table-bounds conversion is
  performed.
  

Totality: total
Visibility: export

bmSet : BMIntTable s size -> PatternIndex size -> Int -> F1' s

  Write an entry to a Boyer–Moore integer table.
  
  The index is already bounded, so no dynamic table-bounds conversion is
  performed.
  

Totality: total
Visibility: export

newBMIntTableWith : Int -> F1 s (BMIntTable s size)

  Allocate and initialize every entry in a Boyer–Moore integer table.
  
  The initialization loop ranges from zero to `size - 1`, so each primitive
  write is known by construction to lie within the newly allocated array.
  

Totality: total
Visibility: export

record OccurrenceTable : Type -> Type

  Mutable Boyer–Moore bad-character occurrence table.
  
  The table contains exactly one entry for each possible byte value and can
  therefore be indexed directly by `Bits8`.
  

Totality: total
Visibility: public export
Constructor: 

MkOccurrenceTable : AnyPtr -> OccurrenceTable s

Projection: 

.arr : OccurrenceTable s -> AnyPtr

.arr : OccurrenceTable s -> AnyPtr

Totality: total
Visibility: public export

arr : OccurrenceTable s -> AnyPtr

Totality: total
Visibility: public export

newOccurrenceTable : F1 s (OccurrenceTable s)

  Allocate an occurrence table with every byte initialized to shift `1`.
  

Totality: total
Visibility: export

occurrence : OccurrenceTable s -> Bits8 -> F1 s Int

  Read the bad-character entry associated with a byte.
  
  Since `Bits8` intrinsically ranges from 0 through 255, no bounds
  conversion or validation is required.
  

Totality: total
Visibility: export

setOccurrence : OccurrenceTable s -> Bits8 -> Int -> F1' s

  Write the bad-character entry associated with a byte.
  
  Since `Bits8` intrinsically ranges from 0 through 255, no bounds
  conversion or validation is required.
  

Totality: total
Visibility: export

occurrences : (bs : ByteString) -> F1 s (Maybe (OccurrenceTable s))

  Constructs a lookup table recording the last occurrence of each byte
  in the given pattern.
  
  For every byte value, the table stores the negated index of its last
  occurrence within the pattern, excluding the final pattern position.
  
  The table is indexed directly by `Bits8`, eliminating the previous
  `Bits8 -> Nat -> Fin 256` conversion and its dynamic bounds validation.
  
  O((length of pattern) + 256)
  

Totality: total
Visibility: export

suffixLengths : (bs : ByteString) -> F1 s (Maybe (BMPatternTable s))

  Builds the table of suffix lengths for the given pattern.
  
  The table is backed by a runtime-sized primitive array containing exactly
  `length bs` entries.
  
  Table positions are represented by bounded `PatternIndex` values rather
  than `Fin (length bs)`, eliminating `tryNatToFin` from primitive table
  reads and writes.
  

Totality: total
Visibility: export

suffixShifts : (bs : ByteString) -> F1 s (Maybe (BMPatternTable s))

  Build the Boyer–Moore good-suffix shift table.
  
  The suffix-length table and resulting shift table share the same bounded
  pattern index space.
  
  Primitive table accesses therefore use `PatternIndex` rather than
  dynamically constructed `Fin` values.
  

Totality: total
Visibility: export