Module Kernel.ReachabilitySource

Reachability analysis for LR automata after conflict resolution

This module computes the reachability of states in a parser automaton after conflicts have been resolved (some transitions removed). It's used to reason about the actual behavior of the parser and compute minimal parsing costs.

Architecture:

• The module computes classes of terminals that have identical behavior across all transitions. This is used to compact cost matrices.

• The Tree module builds a DAG of all matrix products that appear in the cost equations.

• The Cell module provides compact encoding of matrix cells as integers.

• The Analysis module solves the resulting dataflow problem to compute minimal costs for reaching each state with each lookahead class.

The module uses:

• Tarjan's SCC algorithm for computing strongly connected components
• Dataflow analysis with fixpoint iteration for computing costs

Implementation details:

• The Classes module uses a refinement-based fixedpoint iteration to compute partitionings of terminals. Each SCC is processed in reverse topological order, using the current approximation for recursive occurrences.

• The Coercion module implements the coerce matrices for changing between different partitionings. The infix function handles the special case where the last class is omitted (it has infinite cost).

• The Tree module hash-conses the matrix DAG to avoid duplicates. The ConsedTree functor produces a tree where inner nodes represent matrix products and leaves represent individual transition costs.

• The Cell module uses a clever bit-packing scheme to encode (node, pre_class, post_class) as a single integer, enabling efficient storage of large cost matrices.

• The Solver module implements two analyses:
• Shortest path analysis computing minimal costs
• Finite language analysis computing which cells are reachable

• The Reverse_dependencies module tracks how changes to one cell affect others, enabling efficient incremental updates during the dataflow analysis.