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, 0 insertions, 92 deletions

diff --git a/cparser/MenhirLib/Main.v b/cparser/MenhirLib/Main.v
deleted file mode 100644
index 1a17e988..00000000
--- a/cparser/MenhirLib/Main.v
+++ /dev/null
@@ -1,92 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-Require Grammar.
-Require Automaton.
-Require Interpreter_safe.
-Require Interpreter_correct.
-Require Interpreter_complete.
-Require Import Syntax.
-
-Module Make(Export Aut:Automaton.T).
-Export Aut.Gram.
-Export Aut.GramDefs.
-
-Module Import Inter := Interpreter.Make Aut.
-Module Safe := Interpreter_safe.Make Aut Inter.
-Module Correct := Interpreter_correct.Make Aut Inter.
-Module Complete := Interpreter_complete.Make Aut Inter.
-
-Definition complete_validator:unit->bool := Complete.Valid.is_complete.
-Definition safe_validator:unit->bool := Safe.Valid.is_safe.
-Definition parse (safe:safe_validator ()=true) init n_steps buffer : parse_result init:=
-  Safe.parse_with_safe (Safe.Valid.is_safe_correct safe) init buffer n_steps.
-
-(** Correction theorem. **)
-Theorem parse_correct
-  (safe:safe_validator ()= true) init n_steps buffer:
-  match parse safe init n_steps buffer with
-    | Parsed_pr sem buffer_new =>
-      exists word,
-        buffer = word ++ buffer_new /\ inhabited (parse_tree (NT (start_nt init)) word sem)
-    | _ => True
-  end.
-Proof.
-unfold parse, Safe.parse_with_safe.
-pose proof (Correct.parse_correct init buffer n_steps).
-generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init buffer n_steps).
-destruct (Inter.parse init buffer n_steps); intros.
-now destruct (n (eq_refl _)).
-now destruct p; trivial.
-Qed.
-
-(** Completeness theorem. **)
-Theorem parse_complete
-  (safe:safe_validator () = true) init n_steps word buffer_end sem:
-  complete_validator () = true ->
-  forall tree:parse_tree (NT (start_nt init)) word sem,
-  match parse safe init n_steps (word ++ buffer_end) with
-    | Fail_pr => False
-    | Parsed_pr sem_res buffer_end_res =>
-      sem_res = sem /\ buffer_end_res = buffer_end /\ pt_size tree <= n_steps
-    | Timeout_pr => n_steps < pt_size tree
-  end.
-Proof.
-intros.
-unfold parse, Safe.parse_with_safe.
-pose proof (Complete.parse_complete (Complete.Valid.is_complete_correct H) init _ buffer_end _ tree n_steps).
-generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init (word ++ buffer_end) n_steps).
-destruct (Inter.parse init (word ++ buffer_end) n_steps); intros.
-now destruct (n eq_refl).
-now exact H0.
-Qed.
-
-(** Unambiguity theorem. **)
-Theorem unambiguity:
-  safe_validator () = true -> complete_validator () = true -> inhabited token ->
-  forall init word,
-  forall sem1 (tree1:parse_tree (NT (start_nt init)) word sem1),
-  forall sem2 (tree2:parse_tree (NT (start_nt init)) word sem2),
-  sem1 = sem2.
-Proof.
-intros.
-destruct H1.
-pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem1) H0 tree1.
-pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem2) H0 tree2.
-destruct (parse H init (pt_size tree1) (word ++ Streams.const X)); intuition.
-rewrite <- H3, H1; reflexivity.
-Qed.
-
-End Make.