Fix for #135

[tirix]

These are the changes required to make the minimal database from #137 pass. Details below.

[tirix]

The initial DB for #135 is the following:

    $c = class wff setvar -> ( ) |- + [ ] $.
    $( $j syntax 'setvar' 'class' 'wff'; syntax '|-' as 'wff'; $)
    $v x A B ph ps $.
    vx $f setvar x $.
    wph $f wff ph $.
    wps $f wff ps $.
    cA $f class A $.
    cB $f class B $.
    cv $a class x $.
    wn $a wff [ A ] $.
    wceq $a wff A = B $.
    wi $a wff ( ph -> ps ) $.
    cdif $a class ( A + B ) $.
    ax1 $a |- [ x ] $.
    ax2 $a |- ( x = x -> ph ) $.

This database requires "type conversion" (from setvar to class, using cv), but the grammar is not told to perform it. Here is the original generated grammar tree:

If we add this command to the database

    $( $j type_conversions; $)

The grammar tree becomes:

It is the same as the previous one, with every "class" transition replaced by a choice between the same "class" transition, or a "setvar + vc" transition.

This does the trick for ax1. No bug here.

[tirix]

The statement ax2 is more tricky, since it involves the famous "garden paths". If we start with ( x and follow in the previous grammar tree, we land at node 17, were we should have been going toward 13. We have to tell the grammar parser that this needs special care. The command garden_path ( x => ( ph ; says exactly that : a formula starting with ( x (leading to node 17) could actually be the start of a wff (leading to node 13). Once we provide this additional information to the grammar parser, the grammar tree becomes:

Where the path from 17 to 13 is opened, through a new node 21.

However, there was still a bug here. Between nodes 21 and 13, only a wceq is performed, the vc to transform the second setvar into a class before wceq is missing. There was indeed a bug in this case, that part was simply forgotten.

This is the change done in grammar.rs.

With this, the grammar tree becomes:

It is almost identical with the previous one, except that when a setvar is found in node 21, first the cv is performed, and then the wceq.

[digama0]

This does the trick for ax1. No bug here.

Can you explain why a $j comment with no contents is even necessary here? type_conversions; provides no information that the verifier didn't already have. The grammar is the same as it was before the command, and exactly the same strings are accepted and rejected. So what assertion is it making? And why is it legal to put that at the very beginning of the database, before anything has been read in yet?

If the purpose is to say "this database has type conversions in it", there is no need for that, you already know there are type conversions because they are collected in a list in the Grammar. So why not trigger the action of type_conversions after the first type conversion, or after every new axiom after the first type conversion? Then we can remove the $j command.

As for the garden path, I will pay more attention to garden path markings in my minimization and see if that works for set.mm as well (it won't be the same garden path in the real thing, this is a minimized example). It would be good if you could provide some tools to diagnose a garden path. In particular, the grammar construction should fail if it is not able to produce a correct automaton for the grammar, and when it does so it should give information regarding the conflict, or possibly even suggest a garden path command. (Note: one way you could conceptualize the KLR parser is as doing exactly this analysis, and instead of suggesting the garden path it just pretends it was given that command and continues. So it ends up being able to parse everything without any help from the user.)

[digama0]

Okay, I have confirmed that both the ISSUE_135 minimization and also set.mm are fixed by correcting the garden_path and type_conversions directives. As a result I no longer have a test case for the change done in this PR (the same fix also works on master). Do you have an example that performs differently under the PR?

[tirix]

There is a test case for the change done to grammar.rs in this PR, it's the additional test "test_issue_135" listed in this PR. Without the change, the test fails with:

thread 'grammar_tests::test_issue_135' panicked at 'assertion failed: `(left == right)`
  left: `"(wi (wceq (cv vx) vx) wph)"`,
 right: `"(wi (wceq (cv vx) (cv vx)) wph)"`', src/grammar_tests.rs:362:5

That is, the second x, after the equal sign, does not get its cv conversion, even though the database includes the type conversion command.

[tirix]

Can you explain why a $j comment with no contents is even necessary here? type_conversions; provides no information that the verifier didn't already have.

I found out that in set.mm some garden paths expansions had to be run first, then the type conversion, and then more garden paths. This is the sequence for set.mm:

  $( $j garden_path ( x   =>   ( ph ;
        garden_path ( A   =>   ( ph ;
        type_conversions;
        garden_path ( x e. A   =>   ( ph ;
        garden_path { <.   =>   { A ;
        garden_path { <. <.   =>   { A ;
  $)

in this order.

Since I have to tell the grammar pass when to run the type conversion, they are only run when the command is found. Granted, this is clumsy!

In particular, the grammar construction should fail if it is not able to produce a correct automaton for the grammar, and when it does so it should give information regarding the conflict, or possibly even suggest a garden path command.

Yes that would be nice to have! However the first priority should be to find the issue with the current set.mm and fix it if possible.

[digama0]

The set.mm issue is fixed in metamath/set.mm#3536.

I did not realize the garden_path commands are order-dependent. That makes it so much more difficult to determine what they should be! I will put the build_grammar pass higher on my todo list.

[tirix]

The set.mm issue is fixed in metamath/set.mm#3536

Yes! I misse one episode, I was not done yet checking all updates. Thanks for finding and fixing that issue!