Module Kernel.AutomataSource

DFA construction and analysis for LR error pattern matching

This module implements a deterministic finite automaton (DFA) construction for analyzing failures of an LR automaton by consuming its stack.

Architecture:

• NFA module: Constructs NFA (nondeterministic finite automaton) from regular expressions specifying error patterns. Transitions are lazy — NFA states are only materialized when explored during determinization. Uses K.derive to compute transitions, then partitions them by label equivalence (via IndexRefine.annotated_partition) to merge transitions with the same filter, captures, and usage.

• DFA module: Converts the NFA to a DFA using a modified power set construction (ordered to respect clause priorities). This is a "power sequence" construction, not a power set — the order of NFA states in each kernel matters for priority resolution. Three key differences from standard subset construction:
• NFA states in each kernel are ordered by priority
• Only paths corresponding to reachable LR stacks are determinized, omitting transitions to unreachable configurations (automata implication)
• Branches that can never fire due to lower priority are implicitly pruned, avoiding combinatorial state explosion

Hash-consing ensures canonical representation of equivalent DFA states.

The DFA states contain:

• A kernel of NFA states (ordered by priority)
• Transitions with mappings to relate the kernels of the source and target state (to answer questions like which NFA state of the source an NFA state of the target comes from?)

• Dataflow module: Performs multi-pass fixpoint analysis on the DFA:
• Reachability of branches from accepting states
• Marking of reachable transitions (usage tracking)
• Dead-code analysis and unreachable clause warnings
• Priority splits for distinguishing clause precedence
• Priority chain construction via Order_chain for dynamically ordering continuations from the same branch
• Liveness of captured variables
• Defined variables at each state
• Variable class computation for register allocation
• Register allocation for captured values

Register allocation is done lazily based on live ranges. The naive greedy allocation assigns registers according to variable classes, leading to less efficient but more minimizable ("factorizable") code.

• Machine module: Abstract machine representation for code generation. Contains:
• Sparse transition table with states and transitions labelled by LR(1)
• A register transfer language for implementing captures (moves, captures, clear operations)
• Dynamic priority chain: each accepting state stores a list of (clause, priority, registers) tuples; at runtime the first matching clause wins. This avoids statically duplicating states for each priority ordering, which would cause combinatorial state explosion.
• Minimization using a refinement of Valmari's algorithm with custom decomposition by accepted actions and register transfer operations.

The stacks type parameterizes the DFA construction with the actual stack topology, allowing the same construction to work over plain LR(1) states or refined LRC states.