The lane table algorithm is technically incorrect, is this an issue ?

[arnaudgolfouse]

The following grammar is rejected by lalrpop (because it is rejected by the lane table algorithm), but it is in fact LR(1):

grammar;

pub A: () = {
    T "a",
    U "a",
}
T: () = {
    "t" X1,
    "t" X2 "b",
}
U: () = {
    "u" X2,
    "u" X1 "b",
}
X1: () = { "x" }
X2: () = { "x" }

Details:

The LALR tables look like this (only representing the states that interest us):

state 0:
    A  →∙T "a"      [EOF]
    A  →∙U "a"      [EOF]
    T  →∙"t" X1     ["a"]
    T  →∙"t" X2 "b" ["a"]
    U  →∙"u" X2     ["a"]
    U  →∙"u" X1 "b" ["a"]

state 1:
    T  → "t"∙X1     ["a"]
    T  → "t"∙X2 "b" ["a"]
    X1 →∙"x"        ["a"]
    X2 →∙"x"        ["b"]

state 2:
    U  → "u"∙X2     ["a"]
    U  → "u"∙X1 "b" ["a"]
    X1 →∙"x"        ["b"]
    X2 →∙"x"        ["a"]

state 3:
    X1 → "x"∙       ["a", "b"]
    X2 → "x"∙       ["a", "b"]

Then the lane table algorithm refuses to split state 3, resulting in a reduce/reduce conflict.

Note that this particular pattern seems exceedingly rare, so it may not be an issue: I cannot really imagine a real life grammar that would exhibit this error. But you never know...

[Pat-Lafon]

Is this related to #391? Note the comment with the minimized grammar #391 (comment)

[modulovalue]

Then the lane table algorithm refuses to split state 3, resulting in a reduce/reduce conflict.

I've looked at this grammar on grammophone and I don't quite understand what's so special about it that the lane table algorithm rejects it?

[arnaudgolfouse]

Is this related to #391? Note the comment with the minimized grammar #391 (comment)

They look similar, but there is in fact a key difference. In summary, I believe the lane table algorithm should be able to handle the grammar you linked, but I think it has a fundamental limitation which prevents it from accepting the grammar I proposed.

Precisions

(To be clear: this is based on my understanding of the algorithm, which is very close (if not the same) to nikomatsakis (based on this comment))

Roughly speaking, the lane table algorithm works by identifying reduce/reduce conflicts, and then:

• Finding the source of those conflicts, aka the state + configuration which holds the conflicted lookahead.
• Associate those lookaheads to their state.
• Walk the LR0 machine and propagate these lookaheads along the traced lanes. If a state ends up with the same lookahead from 2 different sources, try to split it. If it cannot be split, error out.

Right ?

BUT: this is not correct! Indeed, the two sides of a conflict can come from the same state, but different configurations. This is what my example shows: we have a conflict in state 3 on the "a" lookahead, and that conflict can be traced back to the state 0 (first two configurations).

State	C1	C2	Successor
state 0	{a}	{a}	1, 2
state 1		{b}	3
state 2	{b}		3
state 3

In this case, the algorithm will consider state 0 to be conflicting, and unsplittable, but this isn't quite true: the real conflict only manifest itself in state 3, and this one we could split.

Now, we could imagine that this could be fixed, by saying that we associate lookaheads to a pair of state + configuration (instead of just a state). I don't really remember the exact details, but I tried to do this and failed miserably: the resulting algorithm explodes in complexity.

Hopefully this is understandable 😅

[Pat-Lafon]

Ah, thanks for the detailed explanation! Happy to keep this issue open then.