Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ql.mm grammar is broken #141

Open
digama0 opened this issue Sep 30, 2023 · 1 comment
Open

ql.mm grammar is broken #141

digama0 opened this issue Sep 30, 2023 · 1 comment

Comments

@digama0
Copy link
Member

digama0 commented Sep 30, 2023

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:

grammar

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

cc: @tirix

@digama0 digama0 changed the title nf.mm grammar is broken ql.mm grammar is broken Sep 30, 2023
@tirix
Copy link
Collaborator

tirix commented Oct 18, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants