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, 27 insertions, 27 deletions

diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 5865ab69..5f12e8a1 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -20,7 +20,7 @@ Parameter string : Type.
 (* OCaml's int64 type, used to represent individual characters in literals. *)
 Parameter char_code : Type.
 (* Context information. *)
-Parameter cabsloc : Type.
+Parameter loc : Type.
 
 Record floatInfo := {
   isHex_FI:bool;
@@ -51,7 +51,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *)
    * They also have a list of __attribute__s that appeared between the
    * keyword and the type name (definitions only) *)
   | Tstruct_union : structOrUnion -> option string -> option (list field_group) -> list attribute -> typeSpecifier
-  | Tenum : option string -> option (list (string * option expression * cabsloc)) -> list attribute -> typeSpecifier
+  | Tenum : option string -> option (list (string * option expression * loc)) -> list attribute -> typeSpecifier
 
 with storage :=
   AUTO | STATIC | EXTERN | REGISTER | TYPEDEF
@@ -87,18 +87,18 @@ with decl_type :=
  | PROTO_OLD : decl_type -> list string -> decl_type
 
 with parameter :=
-  | PARAM : list spec_elem -> option string -> decl_type -> list attribute -> cabsloc -> parameter
+  | PARAM : list spec_elem -> option string -> decl_type -> list attribute -> loc -> parameter
 
 (* The optional expression is the bitfield *)
 with field_group :=
-  | Field_group : list spec_elem -> list (option name * option expression) -> cabsloc -> field_group
+  | Field_group : list spec_elem -> list (option name * option expression) -> loc -> field_group
 
 (* The decl_type is in the order in which they are printed. Only the name of
  * the declared identifier is pulled out. *)
 (* e.g: in "int *x", "*x" is the declarator; "x" will be pulled out as *)
 (* the string, and decl_type will be PTR([], JUSTBASE) *)
 with name :=
-  | Name : string -> decl_type -> list attribute -> cabsloc -> name
+  | Name : string -> decl_type -> list attribute -> loc -> name
 
 (* A variable declarator ("name") with an initializer *)
 with init_name :=
@@ -161,9 +161,9 @@ with initwhat :=
   | ATINDEX_INIT : expression -> initwhat
 
 with attribute :=
-  | GCC_ATTR : list gcc_attribute -> cabsloc -> attribute
-  | PACKED_ATTR : list expression -> cabsloc -> attribute
-  | ALIGNAS_ATTR : list expression -> cabsloc -> attribute
+  | GCC_ATTR : list gcc_attribute -> loc -> attribute
+  | PACKED_ATTR : list expression -> loc -> attribute
+  | ALIGNAS_ATTR : list expression -> loc -> attribute
 
 with gcc_attribute :=
   | GCC_ATTR_EMPTY
@@ -194,31 +194,31 @@ Definition asm_flag := (bool * list char_code)%type.
 ** Declaration definition (at toplevel)
 *)
 Inductive definition :=
- | FUNDEF : list spec_elem -> name -> list definition -> statement -> cabsloc -> definition
- | DECDEF : init_name_group -> cabsloc -> definition  (* global variable(s), or function prototype *)
- | PRAGMA : string -> cabsloc -> definition
+ | FUNDEF : list spec_elem -> name -> list definition -> statement -> loc -> definition
+ | DECDEF : init_name_group -> loc -> definition  (* global variable(s), or function prototype *)
+ | PRAGMA : string -> loc -> definition
 
 (*
 ** statements
 *)
 
 with statement :=
- | NOP : cabsloc -> statement
- | COMPUTATION : expression -> cabsloc -> statement
- | BLOCK : list statement -> cabsloc -> statement
- | If : expression -> statement -> option statement -> cabsloc -> statement
- | WHILE : expression -> statement -> cabsloc -> statement
- | DOWHILE : expression -> statement -> cabsloc -> statement
- | FOR : option for_clause -> option expression -> option expression -> statement -> cabsloc -> statement
- | BREAK : cabsloc -> statement
- | CONTINUE : cabsloc -> statement
- | RETURN : option expression -> cabsloc -> statement
- | SWITCH : expression -> statement -> cabsloc -> statement
- | CASE : expression -> statement -> cabsloc -> statement
- | DEFAULT : statement -> cabsloc -> statement
- | LABEL : string -> statement -> cabsloc -> statement
- | GOTO : string -> cabsloc -> statement
- | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> cabsloc -> statement
+ | NOP : loc -> statement
+ | COMPUTATION : expression -> loc -> statement
+ | BLOCK : list statement -> loc -> statement
+ | If : expression -> statement -> option statement -> loc -> statement
+ | WHILE : expression -> statement -> loc -> statement
+ | DOWHILE : expression -> statement -> loc -> statement
+ | FOR : option for_clause -> option expression -> option expression -> statement -> loc -> statement
+ | BREAK : loc -> statement
+ | CONTINUE : loc -> statement
+ | RETURN : option expression -> loc -> statement
+ | SWITCH : expression -> statement -> loc -> statement
+ | CASE : expression -> statement -> loc -> statement
+ | DEFAULT : statement -> loc -> statement
+ | LABEL : string -> statement -> loc -> statement
+ | GOTO : string -> loc -> statement
+ | ASM : list cvspec -> bool -> list char_code -> list asm_operand -> list asm_operand -> list asm_flag -> loc -> statement
  | DEFINITION : definition -> statement (*definition or declaration of a variable or type*)
 
 with for_clause :=