Data.ByteString.Search.DFA.Types

(source)

Types for the DFA string searching algorithm.

Definitions

dfaStateLimit : Bits32

  One greater than the maximum number of DFA states whose flattened
  256-way transition table can be represented without overflow in
  `Bits32`.
  
  A DFA must have fewer than 2^24 states because every state owns 256
  transition entries:
  
      states * 256 < 2^32

Totality: total
Visibility: public export

DFAStateCount : Type

  Evidence that a DFA state count can safely be used to construct a
  flattened 256-way transition table using `Bits32` indexing.
  
  The proof stored by `Index` is erased at runtime.

Totality: total
Visibility: public export

DFAState : Bits32 -> Type

  A valid state in a DFA containing `states` states.
  
  The underlying state number is represented by `Index`, so its proof that
  the state lies in `[0, states)` is erased at runtime.

Totality: total
Visibility: public export

record DFAIndex : Bits32 -> Type

  A valid DFA transition coordinate.
  
  `state` is already known to be within the DFA's state range, while `byte`
  is intrinsically limited to the 256 possible byte values.

Totality: total
Visibility: public export
Constructor:

MkDFAIndex : Index states -> Bits8 -> DFAIndex states

Projections:

.byte : DFAIndex states -> Bits8
.state : DFAIndex states -> Index states

.state : DFAIndex states -> Index states

Totality: total
Visibility: public export

state : DFAIndex states -> Index states

Totality: total
Visibility: public export

.byte : DFAIndex states -> Bits8

Totality: total
Visibility: public export

byte : DFAIndex states -> Bits8

Totality: total
Visibility: public export

dfaIndex : {auto 0 _ : states < dfaStateLimit} -> DFAIndex states -> Index (states * 256)

  Flatten a DFA state and input byte into a transition-table index.
  
  The resulting `Index` is constructed directly from statically carried
  bounds evidence. No dynamic range check is performed.
  
  The DFA state-count proof guarantees that multiplication by 256 cannot
  overflow `Bits32`.

Totality: total
Visibility: export

dfaStateValue : DFAState states -> Bits32

  Return the runtime state number represented by a valid DFA state.
  
  The bound proof carried by `Index` is erased, so this operation is
  simply extraction of the underlying `Bits32` value.

Totality: total
Visibility: export

dfaTransitionIndex : {auto 0 _ : states < dfaStateLimit} -> DFAState states -> Bits8 -> Index (states * 256)

  Construct the valid flattened transition-table index for a DFA state and
  input byte.
  
  No dynamic bounds check is performed. The state-count bound and state
  bound are carried exclusively as erased evidence.

Totality: total
Visibility: export

record DFATable : Type -> Bits32 -> Type

  Mutable DFA transition storage.
  
  The underlying pointer is an Idris primitive array containing
  `states * 256` transitions.

Totality: total
Visibility: public export
Constructor:

MkDFATable : AnyPtr -> DFATable s states

Projection:

.arr : DFATable s states -> AnyPtr

.arr : DFATable s states -> AnyPtr

Totality: total
Visibility: public export

arr : DFATable s states -> AnyPtr

Totality: total
Visibility: public export

newDFATable : {auto 0 _ : states < dfaStateLimit} -> F1 s (DFATable s states)

  Allocate an uninitialized DFA transition table.

Totality: total
Visibility: export

dfaTransition : {auto 0 _ : states < dfaStateLimit} -> DFATable s states -> DFAState states -> Bits8 -> F1 s (DFAState states)

  Read the next DFA state for a current state and input byte.
  
  The flattened transition index is already bounded, so no explicit
  `tryIndex` or `tryNatToFin` conversion occurs in the search loop.
  
  The primitive array is accessed directly using the prevalidated
  flattened `Index`.

Totality: total
Visibility: export

setDFATransition : {auto 0 _ : states < dfaStateLimit} -> DFATable s states -> DFAState states -> Bits8 -> DFAState states -> F1' s

  Write a DFA transition.
  
  The flattened index is derived from an already-bounded DFA state and
  byte, avoiding any explicit dynamic bounds conversion.
  
  The primitive array is written directly using the prevalidated
  flattened `Index`.

Totality: total
Visibility: export

record DFAStateSpace : Type

  Runtime description of a valid DFA state space.
  
  `states` is the number of states in the DFA. The erased proofs establish
  that the state count is positive and small enough for the flattened
  256-way transition table to fit within the `Bits32` index space.

Totality: total
Visibility: public export
Constructor:

MkDFAStateSpace : (states : Bits32) -> (0 _ : 0 < states) -> (0 _ : states < dfaStateLimit) -> DFAStateSpace

Projections:

.states : DFAStateSpace -> Bits32
0 .statesBounded : ({rec:0} : DFAStateSpace) -> states {rec:0} < dfaStateLimit
0 .statesPositive : ({rec:0} : DFAStateSpace) -> 0 < states {rec:0}

.states : DFAStateSpace -> Bits32

Totality: total
Visibility: public export

states : DFAStateSpace -> Bits32

Totality: total
Visibility: public export

0 .statesPositive : ({rec:0} : DFAStateSpace) -> 0 < states {rec:0}

Totality: total
Visibility: public export

0 statesPositive : ({rec:0} : DFAStateSpace) -> 0 < states {rec:0}

Totality: total
Visibility: public export

0 .statesBounded : ({rec:0} : DFAStateSpace) -> states {rec:0} < dfaStateLimit

Totality: total
Visibility: public export

0 statesBounded : ({rec:0} : DFAStateSpace) -> states {rec:0} < dfaStateLimit

Totality: total
Visibility: public export

dfaStateSpace : ByteString -> Maybe DFAStateSpace

  Construct the state space for a DFA matching `bs`.
  
  A pattern of length `n` requires `n + 1` states, including state zero.
  The upper-bound check is performed once during DFA construction. All
  subsequent state and transition indexing carries erased `Index` proofs
  and requires no repeated bounds validation.

Totality: total
Visibility: export

record DFAutomaton : Type -> Type

  A constructed DFA transition automaton.
  
  The runtime state-space description is packaged together with a
  transition table indexed by that state count.
  
  Every transition stored in the table is itself a valid `DFAState`,
  allowing a lookup result to feed directly into the next lookup.

Totality: total
Visibility: public export
Constructor:

MkDFAutomaton : (space : DFAStateSpace) -> DFATable s (space .states) -> DFAutomaton s

Projections:

.space : DFAutomaton s -> DFAStateSpace
.table : ({rec:0} : DFAutomaton s) -> DFATable s ((space {rec:0}) .states)

.space : DFAutomaton s -> DFAStateSpace

Totality: total
Visibility: public export

space : DFAutomaton s -> DFAStateSpace

Totality: total
Visibility: public export

.table : ({rec:0} : DFAutomaton s) -> DFATable s ((space {rec:0}) .states)

Totality: total
Visibility: public export

table : ({rec:0} : DFAutomaton s) -> DFATable s ((space {rec:0}) .states)

Totality: total
Visibility: public export

toDFAState : (space : DFAStateSpace) -> Nat -> Maybe (DFAState (space .states))

  Convert a `Nat` state number into a valid state of the supplied DFA
  state space.
  
  This helper is used only while constructing the DFA. Search-time
  transitions already produce bounded states directly and therefore do not
  require this check.

Totality: total
Visibility: export

zeroDFAState : (space : DFAStateSpace) -> DFAState (space .states)

  State zero for a valid DFA state space.
  
  No dynamic check is required because every DFA state space is known to
  contain at least one state.

Totality: total
Visibility: export