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 lo...
    998f3c5f
This project is licensed under the GNU General Public License v2.0 or later. Learn more