Skip to content
  • Jacques-Henri Jourdan's avatar
    New parser based on new version of the Coq backend of Menhir (#276) · 998f3c5f
    Jacques-Henri Jourdan authored
    What's new:
    1. A rewrite of the Coq interpreter of Menhir automaton, with
       dependent types removing the need for runtime checks for the
       well-formedness of the LR stack. This seem to cause some speedup on
       the parsing time (~10% for lexing + parsing).
    2. Thanks to 1., it is now possible to avoid the use of int31 for
       comparing symbols: Since this is only used for validation,
       positives are enough.
    3. Speedup of Validation: on my machine, the time needed for compiling
       Parser.v goes from about 2 minutes to about 1 minute. This seem to
       be related to a performance bug in the completeness validator and
       to the use of positive instead of int31.
    3. Menhir now generates a dedicated inductive type for
       (semantic-value-carrying) tokens (in addition to the already
       existing inductive type for (non-semantic-value-carrying)
       terminals. The end result is that the OCaml support code for the
       parser no longer contain calls to Obj.magic. The bad side of this
       change is that the formal specification of the parser is perhaps
       harder to read.
    4. The parser and its library are now free of axioms (I used to use
       axiom K and proof irrelevance for easing proofs involving dependent
    5. Use of a dedicated custom negative coinductive type for the input
       stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
       positive coinductive type, which are now deprecated by Coq.
    6. The fuel of the parser is now specified using its logarithm instead
       of its actual value. This makes it possible to give large fuel
       values instead of using the `let rec fuel = S fuel` hack.
    7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
    The corresponding changes in Menhir have been released as part of
    version 20190626. The `MenhirLib` directory is identical to the
    content of the `src` directory of the corresponding `coq-menhirlib`
    opam package except that:
       - In order to try to make CompCert compatible with several Menhir
         versions without updates, we do not check the version of menhir
         is compatible with the version of coq-menhirlib. Hence the
         `Version.v` file is not present in CompCert's copy.
       - Build-system related files have been removed.
This project is licensed under the GNU General Public License v2.0 or later. Learn more