new parser for lp files

[fblanqui]

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:

• fix parser.ml to parse strings and other entries with the new parser
• extend the parser to the search command and patterns
• fix problem with tests/OK/Tactic.lp
• 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?
• fix comments below
• accept "id+ : term" for parameters ?

[fblanqui]

looks wrong

[fblanqui]

this is a temporary fix for the old parser to compile

[sacerdot]

Since you are working on the parser, the old parser did not accept binders of the form "id+ : term", it only accepted "id+" or "(id+ : term)" (and many more variations). This was a limitation of the Menhir technology (a shift/reduce conflict). In the Rocq parser me and Abdelghani have just written in Bologna, we managed to accept that combination (that is valid in Rocq) by having Menhir parse a larger grammar and then check if the input made sense in the OCaml code. I think that it would make sense to also accept the missing case in your new parser.