lambdapi
lambdapi copied to clipboard
new parser for lp files
This PR provides a new parser for lp files not based on Menhir but written by hand. It is more efficient, provides better error messages and is easier to change later if needed.
It also integrates search queries properly.
Performance of parsing on the translation to lp of the HOL-Light base file hol.ml (1.2 Go): 1m22s with the master branch, and 1m8s with the PR: -16%.
TODO:
- [x] fix parser.ml to parse strings and other entries with the new parser
- [x] extend the parser to the search command and patterns
- [ ] fix parser on search queries: first parse a STRINGLIT and then call the search parser on the string (be careful with position in error messages)
- [ ] add tests for parser on search queries
- [ ] check the diff
- [ ] simplify (and optimize) lexer?
- [ ] remove searchQuerySyntax.ml and lpParser.mly
- [ ] rename the new parser file to lpParser.ml
- [ ] try to optimize a little bit more?
- [ ] try to factorize the code?