Add faster implementation of LRijkstraCore
This MR tracks the progress integrating the new implementation of LRijkstra into Menhir. The implementation is ready, but the code is still lacking some comments and cleanups.
In this branch, menhir --list-errors
defaults to the new algorithm, though the behavior is configurable with the added --list-errors-algorithm
flag. It can be set to:
-
fast
: use the new algorithm -
classic
: use the previous algorithm -
validate
: run both, check that shortest lengths match, then usefast
for producing actual erroneous sentences
The Fix library has a few additions:
-
DataFlow.RunCustomMaps
which exposes a lower-level interface than the existingDataFlow
solver, crucial for efficiently solving the large problems generated byLRijkstraFast
-
CompactQueue
, an alternative to the standardQueue
which is a more compact and improved the time and space consumption ofDataFlow.RunCustomMaps
on large problems -
Numbering.Typed
which implements various type-level tricks to manipulate finite set and vectors indexed by elements from finite sets Once we are done with this MR, I will open a new one to update the Fix library upstream.
Inside Menhir, besides the addition of new algorithms, the main change is that LRijsktra
is now parameterized by the reachability algorithm. The logic to chose which algorithm to instantiate LRijkstra
with is added to Back