ql.mm grammar is broken

[digama0]

Minimized example:

$c term wff |- ' = $.
$( $j syntax 'term' 'wff'; syntax '|-' as 'wff'; $)
$v a b ph $.
va $f term a $.
vb $f term b $.
wph $f wff ph $.
weq $a wff a = b $.
tc $a term a ' $.
ax $a |- a = a ' $.

There are no type conversions here, and I don't see what garden path I would need to supply here. The automaton looks like this:

which doesn't seem correct, it is missing a ' edge from node 6 to node 7.

cc: @tirix

[tirix]

I had a look at this problem two weeks ago and my conclusion at that time was that in the current state, grammar.rs does not handle postfixes well:

It's been lazily built for set.mm and the set.mm database syntax has the nice property (through many parentheses) that prefixes are disjoint and you always know how deep you are in a construct.

• For example, in `' `' `' F you encounter 3 `' symbols so you know you are 3 "converse" constructs down once you parse the F symbol.
• Another good example is the U_ x e. A B construct which has been made distinct from U. B. Once you read the first symbol, you know exactly in which branch you are, and when the construct will end.

The way the parsing works is that to parse the necessary term after node 5, the automaton goes back to node 0. The syntax could be something recursively complex, but in the end it would resolve to a single term, return and then pop the stack and move to node 6. In this case it does so after having shifted only the a. This resolves to a term, so it's happy and does not care about what's after, and that the term might not be complete, and it completely misses the final ' which appears to be too much.

So the parser has been built using a nice property of set.mm, which ql.mm does not have.

Additional changes are needed in grammar.rs to handle this case correctly.