package lrgrep

  1. Overview
  2. Docs
package lrgrep
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Kernel.RedposSource

Compact representation of reduction positions

This module provides an efficient compact representation for positions in reductions of the form (n, A) where:

  • n is the number of stack elements to pop
  • A is the nonterminal symbol for the goto transition

The position is interpreted as: "pop n elements from the stack before following the goto transition labeled A".

Design and implementation:

  • The table structure uses a contiguous memory layout where positions for each nonterminal are allocated consecutively. This enables O(1) access and efficient cache usage.
  • 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:

  • The zero position for each nonterminal is stored separately to enable efficient lookups when we need to start a reduction.
  • Index arithmetic is used for compactness: positions are offsets from the zero position of the associated nonterminal.
  • The previous' function handles None (for Optional type) in addition to the regular case, enabling use with optional positions.
type 'a t
module Const (M : sig ... end) : sig ... end
module Eq (M : sig ... end) : sig ... end

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.

Sourcetype 'g table = {
  1. desc : ('g t, 'g desc) Fix.Indexing.vector;
  2. 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.

Sourceval make : 'g Info.grammar -> 'g table

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.

Sourceval inj : 'g table -> int -> int -> int

Inject a (nonterminal, offset) pair into a compact table index. Raises Assert_failure if the offset is out of range.

Sourceval prj : 'g table -> int -> 'g desc

Project a compact table index back to its (nonterminal, offset) pair.

Sourceval previous : 'g table -> int -> ('g Info.nonterminal Fix.Indexing.index, int) Stdlib.Either.t

Navigate 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).

Sourceval previous' : 'g table -> int -> ('g Info.nonterminal Fix.Indexing.index, int) Stdlib.Either.t

Like previous but accepts an optional index. Returns Right Opt.none when the input is None. Used in reduction graphs where positions may be absent.

Sourceval is_zero : 'g table -> int -> bool

Check whether the position is at offset 0 (start of a reduction).