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, 414 deletions

diff --git a/cparser/MenhirLib/Validator_safe.v b/cparser/MenhirLib/Validator_safe.v
deleted file mode 100644
index 183d661b..00000000
--- a/cparser/MenhirLib/Validator_safe.v
+++ /dev/null
@@ -1,414 +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 Automaton.
-Require Import Alphabet.
-Require Import List.
-Require Import Syntax.
-
-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).
-
-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.
-
-Property is_prefix_correct (l1 l2:list symbol):
-  is_prefix l1 l2 = true -> prefix l1 l2.
-Proof.
-revert l2.
-induction l1; intros.
-apply prefix_nil.
-unfold is_prefix in H.
-destruct l2; intuition; try discriminate.
-rewrite Bool.andb_true_iff in H.
-destruct H.
-rewrite compare_eqb_iff in H.
-destruct H.
-apply prefix_cons.
-apply IHl1; intuition.
-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.
-
-Definition is_shift_head_symbs (_:unit) :=
-  forallb (fun s:state =>
-    match action_table s with
-      | Lookahead_act awp =>
-        forallb (fun t =>
-          match awp t with
-            | Shift_act s2 _ =>
-              is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
-            | _ => true
-          end)
-          all_list
-      | _ => true
-    end)
-    all_list.
-
-Property is_shift_head_symbs_correct:
-  is_shift_head_symbs () = true -> shift_head_symbs.
-Proof.
-unfold is_shift_head_symbs, shift_head_symbs.
-intros.
-rewrite forallb_forall in H.
-specialize (H s (all_list_forall s)).
-destruct (action_table s); intuition.
-rewrite forallb_forall in H.
-specialize (H t (all_list_forall t)).
-destruct (l t); intuition.
-apply is_prefix_correct; intuition.
-Qed.
-
-(** 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.
-
-Definition is_goto_head_symbs (_:unit) :=
-  forallb (fun s:state =>
-    forallb (fun nt =>
-      match goto_table s nt with
-        | Some (exist _ s2 _) =>
-          is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
-        | None => true
-      end)
-      all_list)
-    all_list.
-
-Property is_goto_head_symbs_correct:
-  is_goto_head_symbs () = true -> goto_head_symbs.
-Proof.
-unfold is_goto_head_symbs, goto_head_symbs.
-intros.
-rewrite forallb_forall in H.
-specialize (H s (all_list_forall s)).
-rewrite forallb_forall in H.
-specialize (H nt (all_list_forall nt)).
-destruct (goto_table s nt); intuition.
-destruct s0.
-apply is_prefix_correct; intuition.
-Qed.
-
-(** 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).
-
-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.
-
-Property is_prefix_pred_correct (l1 l2:list (state->bool)) :
-  is_prefix_pred l1 l2 = true -> prefix_pred l1 l2.
-Proof.
-revert l2.
-induction l1.
-intros.
-apply prefix_pred_nil.
-intros.
-destruct l2; intuition; try discriminate.
-unfold is_prefix_pred in H.
-rewrite Bool.andb_true_iff in H.
-rewrite forallb_forall in H.
-apply prefix_pred_cons; intuition.
-apply H0.
-apply 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.
-
-Definition is_shift_past_state (_:unit) :=
-  forallb (fun s:state =>
-    match action_table s with
-      | Lookahead_act awp =>
-        forallb (fun t =>
-          match awp t with
-            | Shift_act s2 _ =>
-              is_prefix_pred
-                (past_state_of_non_init_state s2) (head_states_of_state s)
-            | _ => true
-          end)
-          all_list
-      | _ => true
-    end)
-    all_list.
-
-Property is_shift_past_state_correct:
- is_shift_past_state () = true -> shift_past_state.
-Proof.
-unfold is_shift_past_state, shift_past_state.
-intros.
-rewrite forallb_forall in H.
-specialize (H s (all_list_forall s)).
-destruct (action_table s); intuition.
-rewrite forallb_forall in H.
-specialize (H t (all_list_forall t)).
-destruct (l t); intuition.
-apply is_prefix_pred_correct; intuition.
-Qed.
-
-(** 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.
-
-Definition is_goto_past_state (_:unit) :=
-  forallb (fun s:state =>
-    forallb (fun nt =>
-      match goto_table s nt with
-        | Some (exist _ s2 _) =>
-          is_prefix_pred
-            (past_state_of_non_init_state s2) (head_states_of_state s)
-        | None => true
-      end)
-      all_list)
-    all_list.
-
-Property is_goto_past_state_correct :
-  is_goto_past_state () = true -> goto_past_state.
-Proof.
-unfold is_goto_past_state, goto_past_state.
-intros.
-rewrite forallb_forall in H.
-specialize (H s (all_list_forall s)).
-rewrite forallb_forall in H.
-specialize (H nt (all_list_forall nt)).
-destruct (goto_table s nt); intuition.
-destruct s0.
-apply is_prefix_pred_correct; intuition.
-Qed.
-
-(** 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.
-
-Property is_state_valid_after_pop_complete state sl pl :
-  state_valid_after_pop state sl pl -> is_state_valid_after_pop state sl pl = true.
-Proof.
-intro.
-induction H; intuition.
-destruct sl; intuition.
-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) ->
-    goto_table state_new (prod_lhs prod) = None ->
-    match state_new with
-      | Init i => prod_lhs prod = start_nt i
-      | Ninit _ => False
-    end.
-
-Definition is_valid_for_reduce (state:state) prod:=
-  (is_prefix (prod_rhs_rev prod) (head_symbs_of_state state) &&
-   forallb (fun state_new =>
-     if is_state_valid_after_pop state_new (prod_rhs_rev prod)
-                                           (head_states_of_state state) then
-       match goto_table state_new (prod_lhs prod) with
-         | Some _ => true
-         | None =>
-           match state_new with
-             | Init i => compare_eqb (prod_lhs prod) (start_nt i)
-             | Ninit _ => false
-           end
-       end
-     else
-       true)
-     all_list)%bool.
-
-Property is_valid_for_reduce_correct (state:state) prod:
-  is_valid_for_reduce state prod = true -> valid_for_reduce state prod.
-Proof.
-unfold is_valid_for_reduce, valid_for_reduce.
-intros.
-rewrite Bool.andb_true_iff in H.
-split.
-apply is_prefix_correct.
-intuition.
-intros.
-rewrite forallb_forall in H.
-destruct H.
-specialize (H2 state_new (all_list_forall state_new)).
-rewrite is_state_valid_after_pop_complete, H1 in H2.
-destruct state_new; intuition.
-rewrite compare_eqb_iff in H2; intuition.
-intuition.
-Qed.
-
-(** 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.
-
-Definition is_reduce_ok (_:unit) :=
-  forallb (fun s =>
-    match action_table s with
-      | Lookahead_act awp =>
-        forallb (fun t =>
-          match awp t with
-            | Reduce_act p => is_valid_for_reduce s p
-            | _ => true
-          end)
-          all_list
-      | Default_reduce_act p => is_valid_for_reduce s p
-    end)
-    all_list.
-
-Property is_reduce_ok_correct :
-  is_reduce_ok () = true -> reduce_ok.
-Proof.
-unfold is_reduce_ok, reduce_ok.
-intros.
-rewrite forallb_forall in H.
-specialize (H s (all_list_forall s)).
-destruct (action_table s).
-apply is_valid_for_reduce_correct; intuition.
-intro.
-rewrite forallb_forall in H.
-specialize (H t (all_list_forall t)).
-destruct (l t); intuition.
-apply is_valid_for_reduce_correct; intuition.
-Qed.
-
-(** The automaton is safe **)
-Definition safe :=
-  shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\
-  goto_past_state /\ reduce_ok.
-
-Definition is_safe (_:unit) :=
-  (is_shift_head_symbs () && is_goto_head_symbs () && is_shift_past_state () &&
-    is_goto_past_state () && is_reduce_ok ())%bool.
-
-Property is_safe_correct:
-  is_safe () = true -> safe.
-Proof.
-unfold safe, is_safe.
-repeat rewrite Bool.andb_true_iff.
-intuition.
-apply is_shift_head_symbs_correct; assumption.
-apply is_goto_head_symbs_correct; assumption.
-apply is_shift_past_state_correct; assumption.
-apply is_goto_past_state_correct; assumption.
-apply is_reduce_ok_correct; assumption.
-Qed.
-
-End Make.