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

Use menhir #2910

Merged
merged 19 commits into from
May 9, 2023
Merged

Use menhir #2910

merged 19 commits into from
May 9, 2023

Conversation

mtzguido
Copy link
Member

@mtzguido mtzguido commented May 3, 2023

This PR removes ocamlyacc and fully uses menhir to generate our parser. The positions in the parser actions are changed to use menhir syntax, instead of the rhs/rhs2 module which depended on the Parsing module. This actually improves some ranges (e.g. it fixes #1955).

There also some build system changes. Would be good if @tahina-pro can take a look to check I didn't mess it up.

Note: dune drives the generation of the parser, so no snapshot is checked in. I still need to measure, but it seems like even while generating the parser is fast, the build slows down a bit.

I still need to update some READMEs, posting to not lose track of this.

@mtzguido
Copy link
Member Author

mtzguido commented May 3, 2023

Everything mostly works, except incremental parsing for some reason. The test in FStar.Tests.Pars fails to parse a single decl, and throws an error positioned at the let after the module Demo. This happens even if there's nothing (EOF) after the module Demo. The same happens for other decls, but not others, assume X : False worked.

So, this reeks of something related to lookahead, but it's not the problem we had before with the parser consuming an extra token that needs to be put back. Here the parser never successfully returns, it fails to parse (incrementally) any prefix of the module.

It's weird that also it seems to accept this, see this run of menhir --interpret

Warning: 5 states have shift/reduce conflicts.
Warning: 6 shift/reduce conflicts were arbitrarily resolved.
Warning: 291 end-of-stream conflicts were arbitrarily resolved.
Ready!

Then write: oneDeclOrEOF: MODULE IDENT, and get

ACCEPT
[oneDeclOrEOF:
  [decl:
    [list(decoration):]
    [rawDecl: MODULE [qlident: [path(lident): [lident: IDENT]]]]
  ]
]

So I'm rather confused. I will look at this later. I disabled interactive tests in this branch for now. We'll probably get a failure on expected output but hopefully no serious problem.

@nikswamy
Copy link
Collaborator

nikswamy commented May 9, 2023

I've updated the README and fixed incremental parsing. Thanks Guido!

@nikswamy nikswamy marked this pull request as ready for review May 9, 2023 01:57
@nikswamy nikswamy merged commit 62ffc2a into master May 9, 2023
@nikswamy nikswamy deleted the guido_menhir branch May 9, 2023 02:21
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

Successfully merging this pull request may close these issues.

Bad range on bogus operator
2 participants