Moving to menhir

Menhir is ocaml-based LR(1) parser generator with a lot of interesting features such as parametrized production rules, nice syntactic additions over the mainstream yacc syntax and really good error reporting of parser conflicts. Being based on ocamlyacc the syntax is pretty close to fsyacc.

The main motivation for this major change are :

• having a simpler parser (a code easier to dive in and modify), closer to the expected bnf of FStar
• having better maintenance tools (i.e for analysing shift/reduce, reduce/reduce and end-of-stream conflicts)
• having better error reporting of syntactic errors (not done yet...)

Modification of FStar organisation

Until now, the main parser was written in fsyacc and sed-compiled into a ocamlyacc-compatible file which was used for the ocaml based FStar. The introduction of menhir swap the situation : the official parser is written in a menhir compatible file format and then preprocessed to ocamlyacc and fsyacc.

Inpact on FStar users

If you are not modifying the parser, there is currently no change to your workflow. You only need menhir if you start modifying the parser. In that case do not forget to regenerate the ocamlyacc and fsyacc parsers by calling make -C src/ocaml-output parser before pushing your changes.

Modification in the parser

A lot of small syntax fixes have been incorporated in this new parser.

• Multi-binders :
• val can take parameters :
• infix definition of operators :

Regressions/Syntactic fixes :

• (| t |) is no longer accepted as a variant of ( t ) in particular the correct syntax for defining a dependent pair type is (x:a & b(x)) (if the parens are necessary)
• The focusing let has been slightly modified : let ~> rec bidule = ... has been replaced by let rec ~> bidule = ...