Kernel.Sentence_generationSourceGenerating parse sentences from transitions
This module provides functionality to generate concrete parse examples (sentences) from sequences of LR states or LR transitions. It's used for generating counterexamples and debug information.
Core algorithm:
to_transitions converts a sequence of LR states to a sequence of transitions that connect those states.to_cells maps transitions to reduction graph cells, using dynamic programming to find the minimum-cost path through the reduction graph.expand_cells recursively expands cells back to the original terminal symbols that would trigger the reductions.Key data structures:
Implementation details:
to_cells uses a sophisticated dynamic programming approach where at each transition, it considers:expand_cells handles two cases:L tr: A transition node - either shift (return the terminal) or goto (recursively solve the subproblem with minimum cost)R (l, r): An inner node - decompose into left and right subproblems, finding solutions that minimize total costBreak exception is used to short-circuit when a minimal-cost solution is found during the exploration of all possible decompositions.val find_transition :
'g Info.grammar ->
'g Kernel__Info.lr1 Fix.Indexing.index ->
'g Info.Lr1.n Fix.Indexing.index ->
('g Kernel__Info.goto_transition, 'g Kernel__Info.shift_transition)
Fix.Indexing.Sum.n
Fix.Indexing.indexFind the transition from LR state x to LR state y. Returns a goto transition if y is reached via a non-production, or a shift transition if y is reached via a terminal. Raises Invalid_argument if y is an entrypoint. Raises Not_found if there is no transition from x to y.
val to_transitions :
'a Info.grammar ->
'a Info.Lr1.n Fix.Indexing.index list ->
'a Info.Lr1.n Fix.Indexing.index
* ('a Kernel__Info.goto_transition, 'a Kernel__Info.shift_transition)
Fix.Indexing.Sum.n
Fix.Indexing.index
listConvert a sequence of LR states to the initial state and the list of transitions connecting consecutive states. Raises Invalid_argument if the input list is empty.
val to_cells :
'g Info.grammar ->
('g, 'cell) Reachability.t_cell ->
'g Info.transition Fix.Indexing.index list ->
'cell Fix.Indexing.index listMap a list of transitions to reduction graph cells, finding the minimum-cost path through the cost DAG using dynamic programming.
Processes transitions right-to-left. For each transition, iterates all post_classes and pre_classes, selecting the (pre, post) pair that minimizes the total cost: cost(cell) + cost(suffix).
Returns the list of cells along the minimum-cost path.
val expand_cells :
'g Info.grammar ->
('g, 'cell) Reachability.t_cell ->
'cell Fix.Indexing.index list ->
'g Info.terminal Fix.Indexing.index listRecursively expand reduction graph cells back to terminal symbols.
Handles two node types from the cost tree:
L tr: A leaf transition — shifts return the terminal symbol; gotos check for nullable reductions first, then recurse into the minimum-cost non-nullable reduction equation.R (l, r): An inner node — decomposes into left and right sub-problems via the coercion matrix, recursing into both children whose combined cost equals the current cost.Uses a Break exception to short-circuit once a minimal-cost decomposition is found.
val sentence_of_transitions :
'g Info.grammar ->
'g Reachability.t ->
'g Info.transition Fix.Indexing.index list ->
'g Info.terminal Fix.Indexing.index listGenerate a terminal sentence from a list of transitions. Combines to_cells and expand_cells in a single pipeline.
val sentence_of_stack :
'g Info.grammar ->
'g Reachability.t ->
'g Info.Lr1.n Fix.Indexing.index list ->
'g Info.terminal Fix.Indexing.index listGenerate a terminal sentence from a list of LR states (a parse stack). Combines to_transitions, to_cells, and expand_cells in a single pipeline. The input list must be non-empty (see to_transitions).