record KMPBorderTable : Type -> Bits32 -> Type Mutable storage for the KMP border table.
The table contains one entry for every DFA state. Both table indices and
stored border values are represented by `DFAState`, so their bounds are
established once and carried as erased evidence.
The underlying storage is an Idris primitive array.
Totality: total
Visibility: public export
Constructor: MkKMPBorderTable : AnyPtr -> KMPBorderTable s states
Projection: .arr : KMPBorderTable s states -> AnyPtr
.arr : KMPBorderTable s states -> AnyPtr- Totality: total
Visibility: public export arr : KMPBorderTable s states -> AnyPtr- Totality: total
Visibility: public export record KMPBorders : Type -> Type A constructed KMP border table together with the DFA state space to
which its indices and values belong.
Packaging the state space with the table allows `automaton` to reuse the
exact same state-space witness rather than independently reconstructing
and validating the pattern's state count.
Totality: total
Visibility: public export
Constructor: MkKMPBorders : (space : DFAStateSpace) -> KMPBorderTable s (space .states) -> KMPBorders s
Projections:
.space : KMPBorders s -> DFAStateSpace.table : ({rec:0} : KMPBorders s) -> KMPBorderTable s ((space {rec:0}) .states)
.space : KMPBorders s -> DFAStateSpace- Totality: total
Visibility: public export space : KMPBorders s -> DFAStateSpace- Totality: total
Visibility: public export .table : ({rec:0} : KMPBorders s) -> KMPBorderTable s ((space {rec:0}) .states)- Totality: total
Visibility: public export table : ({rec:0} : KMPBorders s) -> KMPBorderTable s ((space {rec:0}) .states)- Totality: total
Visibility: public export newKMPBorderTable : F1 s (KMPBorderTable s states) Allocate an uninitialized KMP border table.
The table contains exactly one entry for each DFA state.
Totality: total
Visibility: exportkmpBorder : KMPBorderTable s states -> DFAState states -> F1 s (DFAState states) Read a border value from the KMP border table.
The supplied index is already a valid `DFAState`, so no dynamic bounds
validation is required. The stored result is itself another valid DFA
state.
Totality: total
Visibility: exportsetKMPBorder : KMPBorderTable s states -> DFAState states -> DFAState states -> F1' s Write a border value to the KMP border table.
Both the destination index and stored border value are already bounded by
the same DFA state space, so no `Fin` conversion or runtime bounds check
is required.
Totality: total
Visibility: exportnextDFAState : (space : DFAStateSpace) -> DFAState (space .states) -> Maybe (DFAState (space .states)) Construct the successor of a DFA state during DFA preprocessing.
This check occurs only while constructing preprocessing tables. It is
never executed by the target-scanning DFA hot path.
Totality: total
Visibility: exportkmpBorders : ByteString -> F1 s (Maybe (KMPBorders s)) Computes the suffix-oriented KMP border table for a given pattern.
Each entry associated with DFA state `i` stores the length of the longest
proper prefix of `pattern[0..i-1]` that is also a suffix.
Unlike the previous implementation, table indices and border values are
represented directly by bounded `DFAState` values rather than `Nat`
values indexed through `Fin`.
Consequently, accesses to the border table require no `tryNatToFin` or
equivalent dynamic table-bounds conversion.
The result packages the table together with its `DFAStateSpace`, allowing
construction of the DFA transition table to reuse exactly the same state
space.
Example: "ANPANMAN"
Indices: 0 1 2 3 4 5 6 7 8
Borders: 0 0 0 0 1 2 0 1 2
Totality: total
Visibility: export