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

diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v
new file mode 100644
index 00000000..2d2ea4b3
--- /dev/null
+++ b/MenhirLib/Validator_safe.v
@@ -0,0 +1,234 @@
+(****************************************************************************)
+(*                                                                          *)
+(*                                   Menhir                                 *)
+(*                                                                          *)
+(*           Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud         *)
+(*                                                                          *)
+(*  Copyright Inria. All rights reserved. This file is distributed under    *)
+(*  the terms of the GNU Lesser General Public License as published by the  *)
+(*  Free Software Foundation, either version 3 of the License, or (at your  *)
+(*  option) any later version, as described in the file LICENSE.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+From Coq Require Import List Syntax Derive.
+From Coq.ssr Require Import ssreflect.
+Require Automaton.
+Require Import Alphabet Validator_classes.
+
+Module Make(Import A:Automaton.T).
+
+(** The singleton predicate for states **)
+Definition singleton_state_pred (state:state) :=
+  (fun state' => match compare state state' with Eq => true |_ => false end).
+
+(** [past_state_of_non_init_state], extended for all states. **)
+Definition past_state_of_state (state:state) :=
+  match state with
+  | Init _ => []
+  | Ninit nis => past_state_of_non_init_state nis
+  end.
+
+(** Concatenations of last and past **)
+Definition head_symbs_of_state (state:state) :=
+  match state with
+  | Init _ => []
+  | Ninit s =>
+    last_symb_of_non_init_state s::past_symb_of_non_init_state s
+  end.
+Definition head_states_of_state (state:state) :=
+  singleton_state_pred state::past_state_of_state state.
+
+(** * Validation for correctness **)
+
+(** Prefix predicate between two lists of symbols. **)
+Inductive prefix: list symbol -> list symbol -> Prop :=
+| prefix_nil: forall l, prefix [] l
+| prefix_cons: forall l1 l2 x, prefix l1 l2 -> prefix (x::l1) (x::l2).
+
+(** [prefix] is transitive **)
+Lemma prefix_trans:
+  forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3.
+Proof.
+  intros l1 l2 l3 H1 H2. revert l3 H2.
+  induction H1; [now constructor|]. inversion 1. subst. constructor. eauto.
+Qed.
+
+Fixpoint is_prefix (l1 l2:list symbol) :=
+  match l1, l2 with
+  | [], _ => true
+  | t1::q1, t2::q2 => (compare_eqb t1 t2 && is_prefix q1 q2)%bool
+  | _::_, [] => false
+  end.
+
+Instance prefix_is_validator l1 l2 : IsValidator (prefix l1 l2) (is_prefix l1 l2).
+Proof.
+  revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref.
+  - constructor.
+  - destruct l2 as [|x2 l2]=>//.
+    move: Hpref=> /andb_prop [/compare_eqb_iff -> /IH ?]. by constructor.
+Qed.
+
+(** If we shift, then the known top symbols of the destination state is
+    a prefix of the known top symbols of the source state, with the new
+    symbol added. **)
+Definition shift_head_symbs :=
+  forall s,
+    match action_table s with
+    | Lookahead_act awp => forall t,
+        match awp t with
+        | Shift_act s2 _ =>
+          prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+        | _ => True
+        end
+    | _ => True
+    end.
+
+(** When a goto happens, then the known top symbols of the destination state
+    is a prefix of the known top symbols of the source state, with the new
+    symbol added. **)
+Definition goto_head_symbs :=
+  forall s nt,
+    match goto_table s nt with
+    | Some (exist _ s2 _) =>
+      prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+    | None => True
+    end.
+
+(** We have to say the same kind of checks for the assumptions about the
+    states stack. However, theses assumptions are predicates. So we define
+    a notion of "prefix" over predicates lists, that means, basically, that
+    an assumption entails another **)
+Inductive prefix_pred: list (state->bool) -> list (state->bool) -> Prop :=
+  | prefix_pred_nil: forall l, prefix_pred [] l
+  | prefix_pred_cons: forall l1 l2 f1 f2,
+     (forall x, implb (f2 x) (f1 x) = true) ->
+     prefix_pred l1 l2 -> prefix_pred (f1::l1) (f2::l2).
+
+(** [prefix_pred] is transitive **)
+Lemma prefix_pred_trans:
+  forall (l1 l2 l3:list (state->bool)),
+  prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3.
+Proof.
+  intros l1 l2 l3 H1 H2. revert l3 H2.
+  induction H1 as [|l1 l2 f1 f2 Hf2f1]; [now constructor|].
+  intros l3. inversion 1 as [|??? f3 Hf3f2]. subst. constructor; [|now eauto].
+  intros x. specialize (Hf3f2 x). specialize (Hf2f1 x).
+  repeat destruct (_ x); auto.
+Qed.
+
+Fixpoint is_prefix_pred (l1 l2:list (state->bool)) :=
+  match l1, l2 with
+  | [], _ => true
+  | f1::q1, f2::q2 =>
+    (forallb (fun x => implb (f2 x) (f1 x)) all_list
+      && is_prefix_pred q1 q2)%bool
+  | _::_, [] => false
+  end.
+
+Instance prefix_pred_is_validator l1 l2 :
+  IsValidator (prefix_pred l1 l2) (is_prefix_pred l1 l2).
+Proof.
+  revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref.
+  - constructor.
+  - destruct l2 as [|x2 l2]=>//.
+    move: Hpref=> /andb_prop [/forallb_forall ? /IH ?].
+    constructor; auto using all_list_forall.
+Qed.
+
+(** The assumptions about state stack is conserved when we shift **)
+Definition shift_past_state :=
+  forall s,
+    match action_table s with
+    | Lookahead_act awp => forall t,
+        match awp t with
+        | Shift_act s2 _ =>
+          prefix_pred (past_state_of_non_init_state s2)
+                      (head_states_of_state s)
+        | _ => True
+        end
+    | _ => True
+    end.
+
+(** The assumptions about state stack is conserved when we do a goto **)
+Definition goto_past_state :=
+  forall s nt,
+    match goto_table s nt with
+    | Some (exist _ s2 _) =>
+      prefix_pred (past_state_of_non_init_state s2)
+                  (head_states_of_state s)
+    | None => True
+    end.
+
+(** What states are possible after having popped these symbols from the
+    stack, given the annotation of the current state ? **)
+Inductive state_valid_after_pop (s:state):
+  list symbol -> list (state -> bool) -> Prop :=
+  | state_valid_after_pop_nil1:
+    forall p pl, p s = true -> state_valid_after_pop s [] (p::pl)
+  | state_valid_after_pop_nil2:
+    forall sl, state_valid_after_pop s sl []
+  | state_valid_after_pop_cons:
+    forall st sq p pl, state_valid_after_pop s sq pl ->
+      state_valid_after_pop s (st::sq) (p::pl).
+
+Fixpoint is_state_valid_after_pop (state:state) (to_pop:list symbol) annot :=
+  match annot, to_pop with
+  | [], _ => true
+  | p::_, [] => p state
+  | p::pl, s::sl => is_state_valid_after_pop state sl pl
+  end.
+
+Instance impl_is_state_valid_after_pop_is_validator state sl pl P b :
+  IsValidator P b ->
+  IsValidator (state_valid_after_pop state sl pl -> P)
+              (if is_state_valid_after_pop state sl pl then b else true).
+Proof.
+  destruct (is_state_valid_after_pop state0 sl pl) eqn:EQ.
+  - intros ??. auto using is_validator.
+  - intros _ _ Hsvap. exfalso. induction Hsvap=>//; [simpl in EQ; congruence|].
+    by destruct sl.
+Qed.
+
+(** A state is valid for reducing a production when :
+      - The assumptions on the state are such that we will find the right hand
+        side of the production on the stack.
+      - We will be able to do a goto after having popped the right hand side.
+**)
+Definition valid_for_reduce (state:state) prod :=
+    prefix (prod_rhs_rev prod) (head_symbs_of_state state) /\
+    forall state_new,
+    state_valid_after_pop state_new
+      (prod_rhs_rev prod) (head_states_of_state state) ->
+    match goto_table state_new (prod_lhs prod) with
+    | None =>
+      match state_new with
+      | Init i => prod_lhs prod = start_nt i
+      | Ninit _ => False
+      end
+    | _ => True
+    end.
+
+(** All the states that does a reduce are valid for reduction **)
+Definition reduce_ok :=
+  forall s,
+    match action_table s with
+    | Lookahead_act awp =>
+      forall t, match awp t with
+                | Reduce_act p => valid_for_reduce s p
+                | _ => True
+                end
+    | Default_reduce_act p => valid_for_reduce s p
+    end.
+
+(** The automaton is safe **)
+Definition safe :=
+  shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\
+  goto_past_state /\ reduce_ok.
+
+Derive is_safe
+SuchThat (IsValidator safe (is_safe ()))
+As safe_is_validator.
+Proof. subst is_safe. instantiate (1:=fun _ => _). apply _. Qed.
+
+End Make.