New parser based on new version of the Coq backend of Menhir (#276)

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
   types).

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.

1 files changed, 15 insertions, 12 deletions

diff --git a/LICENSE b/LICENSE
index 5c7d7294..5a7ae79f 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 All files in this distribution are part of the CompCert verified compiler.
 
-The CompCert verified compiler is Copyright by Institut National de 
+The CompCert verified compiler is Copyright by Institut National de
 Recherche en Informatique et en Automatique (INRIA) and
 AbsInt Angewandte Informatik GmbH.
 
@@ -9,12 +9,12 @@ INRIA Non-Commercial License Agreement given below or under the terms
 of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH.
 The latter is a separate contract document.
 
-The INRIA Non-Commercial License Agreement is a non-free license that 
-grants you the right to use the CompCert verified compiler for 
-educational, research or evaluation purposes only, but prohibits 
+The INRIA Non-Commercial License Agreement is a non-free license that
+grants you the right to use the CompCert verified compiler for
+educational, research or evaluation purposes only, but prohibits
 any commercial use.
 
-For commercial use you need a Software Usage Agreement from 
+For commercial use you need a Software Usage Agreement from
 AbsInt Angewandte Informatik GmbH.
 
 The following files in this distribution are dual-licensed both under
@@ -38,7 +38,7 @@ option) any later version:
   cfrontend/Ctyping.v
   cfrontend/PrintClight.ml
   cfrontend/PrintCsyntax.ml
-  
+
   backend/Cminor.v
   backend/PrintCminor.ml
 
@@ -46,7 +46,7 @@ option) any later version:
 
   all files in the exportclight/ directory
 
-  the Archi.v, CBuiltins.ml, and extractionMachdep.v files 
+  the Archi.v, CBuiltins.ml, and extractionMachdep.v files
   in directories arm, powerpc, riscV, x86, x86_32, x86_64
 
   extraction/extraction.v
@@ -64,11 +64,14 @@ non-commercial contexts, subject to the terms of the GNU General
 Public License.
 
 The files contained in the flocq/ directory and its subdirectories are
-taken from the Flocq project, http://flocq.gforge.inria.fr/
-These files are Copyright 2010-2017 INRIA and distributed under the
-terms of the GNU Lesser General Public Licence, either version 3 of
-the licence, or (at your option) any later version.  A copy of the GNU
-Lesser General Public Licence version 3 is included below.
+taken from the Flocq project, http://flocq.gforge.inria.fr/. The files
+contained in the MenhirLib directory are taken from the Menhir
+project, http://gallium.inria.fr/~fpottier/menhir/. The files from the
+Flocq project and the files in the MenhirLib directory are Copyright
+2010-2019 INRIA and distributed under the terms of the GNU Lesser
+General Public Licence, either version 3 of the licence, or (at your
+option) any later version. A copy of the GNU Lesser General Public
+Licence version 3 is included below.
 
 The files contained in the runtime/ directory and its subdirectories
 are Copyright 2013-2017 INRIA and distributed under the terms of the BSD