Kernel.RedposSourceCompact representation of reduction positions
This module provides an efficient compact representation for positions in reductions of the form (n, A) where:
The position is interpreted as: "pop n elements from the stack before following the goto transition labeled A".
Design and implementation:
inj converts a (nonterminal, position) pair to an index into the table.prj converts an index back to (nonterminal, position).previous returns whether the position is at the start of a reduction (Left nt means we're at the start and need to follow goto nt) or in the middle of a reduction (Right pos gives the previous position).is_zero checks if we're at the start of a reduction (position 0).Tricky implementation details:
previous' function handles None (for Optional type) in addition to the regular case, enabling use with optional positions.A position as a (nonterminal, offset) pair. The offset is the number of stack elements to pop before following the goto transition labeled by the nonterminal.
type 'g table = {desc : ('g t, 'g desc) Fix.Indexing.vector;zero : ('g Info.nonterminal, 'g t Fix.Indexing.index) Fix.Indexing.vector;}Table mapping compact indices to (nonterminal, offset) positions. desc stores positions contiguously per nonterminal for O(1) access. zero maps each nonterminal to the index of its position-0 entry, enabling fast injection of (nt, 0) pairs.
Build a position table from a grammar. For each nonterminal, allocates contiguous slots equal to the maximum RHS length of its productions, plus a sentinel at index 0. Total cardinality = 1 + sum of max production lengths per nonterminal.
Inject a (nonterminal, offset) pair into a compact table index. Raises Assert_failure if the offset is out of range.
Project a compact table index back to its (nonterminal, offset) pair.
val previous :
'g table ->
int ->
('g Info.nonterminal Fix.Indexing.index, int) Stdlib.Either.tNavigate to the predecessor position in a reduction. Returns Left nt if at position 0 for nonterminal nt (start of a reduction — follow the goto transition labeled nt). Returns Right pos' if at position > 0 (middle of a reduction — pos' is the previous position, obtained via O(1) Index.pred).
val previous' :
'g table ->
int ->
('g Info.nonterminal Fix.Indexing.index, int) Stdlib.Either.tLike previous but accepts an optional index. Returns Right Opt.none when the input is None. Used in reduction graphs where positions may be absent.