.gitlab-ci.yml

-image: alpine
+image: busybox
 
 pages:
-  stage: deploy
   script:
-  - echo 'Nothing to do...'
+  - mv www public
   artifacts:
     paths:
     - public

CHANGES.md

 # Changes
 
-## 2018/11/12
+## 2019/06/20
+
+* When compiled with OCaml 4.02.3, Menhir could produce OCaml code
+  containing invalid string literals. This was due to a problem in
+  `String.escaped`. Fixed. (Reported by ELLIOTCABLE.)
+
+## 2019/06/13
+
+* Relax the syntax of point-free actions to allow `< >` (with arbitrary
+  whitespace inside the angle brackets) instead of just `<>`.
+  (Suggested by Lélio Brun.)
+
+* When a cycle of `%inline` nonterminal symbols is encountered,
+  the error message now shows the entire cycle,
+  as opposed to just one symbol that participates in the cycle.
+
+* Fix the treatment of the `error` token when printing the grammar for
+  `ocamlyacc`. Its semantic value must not be referred to; a unit value
+  must be used instead. The switch `--only-preprocess-for-ocamlyacc`
+  remains undocumented. (Reported by kris.)
+
+* Coq back-end: multiple changes to stay up-to-date with respect to
+  coq-menhirlib. See [coq-menhirlib/CHANGES.md](coq-menhirlib/CHANGES.md).
+
+* Coq back-end: the generated parser now contains a dedicated inductive
+  type for tokens. This removes the need for `Obj.magic` in client code
+  when the parser is used via extraction.
+
+* Coq back-end: the generated parser checks that the version of
+  MenhirLib matches. This check can be disabled with
+  `--coq-no-version-check`.
+
+* Coq back-end: the fuel parameter is now given as the *logarithm* of
+  the maximum number of steps to perform. Therefore, using e.g., 50
+  makes sure we will not run out of fuel in any reasonable
+  computation time.
+
+## 2018/11/13
 
 * In `.mly` files, a new syntax for rules has been introduced, which is
   slightly more pleasant than the old syntax. (A rule is the definition of a
   nonterminal symbol.) The old syntax remains available; the user chooses
   between the two syntaxes on a per-rule basis. The new syntax is fully
   documented in the manual;
-  [a brief summary of the differences](doc/new-rule-syntax.md)
+  [a brief summary of the differences](doc/new-rule-syntax-summary.md)
   with respect to the old syntax is also available.
   **The new syntax is considered experimental**
   and is subject to change in the near future.
@@ -35,8 +72,6 @@
   the grammar. This makes it slightly easier to read grammars.
   (Contributed by Perry E. Metzger.)
 
-## 2018/10/25
-
 * Until today, the semicolon character `;` was insignificant: it was
   considered as whitespace by Menhir. It is now accepted only in a
   few specific places, namely: after a declaration; after a rule;
@@ -327,7 +362,7 @@
 
 ## 2016/05/04
 
-* In the Coq backend, split the largest definitions into smaller
+* In the Coq back-end, split the largest definitions into smaller
   ones. This circumvents a limitation of vm_compute on 32 bit
   machines. This also enables us to perform sharing between
   definitions, so that the generated files are much smaller.
@@ -579,7 +614,7 @@
 
 ## 2014/02/18
 
-* In the Coq backend, use `'` instead of `_` as separator in identifiers.
+* In the Coq back-end, use `'` instead of `_` as separator in identifiers.
   Also, correct a serious bug that was inadvertently introduced on
   2013/03/01 (r319).
 

LICENSE

@@ -5,8 +5,13 @@ In the following, "THE LIBRARY" refers to the following files:
   2- the OCaml source files whose basename appears in the file
      src/menhirLib.mlpack and whose extension is ".ml" or ".mli".
 
-"THE GENERATOR" refers to all other files in this archive or repository,
-except those in the subdirectory test/, which are not covered by this license.
+"THE COQ LIBRARY" refers to the files in the subdirectory
+coq-menhirlib/.
+
+"THE GENERATOR" refers to the files of this archive which are neither
+part of THE LIBRARY, nor part of THE COQ LIBRARY, nor in the
+subdirectory test/.  Files in the subdirectory test/ are not covered
+by this license.
 
 THE GENERATOR is distributed under the terms of the GNU General Public
 License version 2 (included below).
@@ -14,6 +19,12 @@ License version 2 (included below).
 THE LIBRARY is distributed under the terms of the GNU Library General
 Public License version 2 (included below).
 
+THE COQ LIBRARY 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. Version 3 of the GNU Lesser General Public License is
+included in the file coq-menhirlib/LICENSE.
+
 As a special exception to the GNU Library General Public License, you
 may link, statically or dynamically, a "work that uses the Library"
 with a publicly distributed version of the Library to produce an

README.md

@@ -15,6 +15,13 @@ For manual installation, see [INSTALLATION.md](INSTALLATION.md).
 
 Some instructions for developers can be found in [HOWTO.md](HOWTO.md).
 
+## The Coq backend support library coq-menhirlib
+
+The support library for the Coq backend of Menhir can be found in the
+coq-menhirlib directory. It can be installed using
+`opam install coq-menhirlib`, when the opam Coq "released" repository
+is set up.
+
 ## Authors
 
 * [François Pottier](Francois.Pottier@inria.fr)

check-tarball.sh

@@ -12,16 +12,25 @@ TARBALL=$PACKAGE.tar.gz
 # is what we do. For this reason, we must first check that ocamlfind does not
 # already have some version of menhirLib and menhirSdk.
 
-# We could also create a fresh opam switch, but that would be time-consuming.
+# We use a dedicated opam switch where it is permitted to uninstall/reinstall
+# Menhir.
+
+CURRENT=`opam switch show`
+echo "The current opam switch is $CURRENT. Now switching to test-menhir..."
+opam switch test-menhir 2>/dev/null || opam switch create test-menhir 4.07.1
+eval $(opam env)
+OPAMYES=true opam install ocamlfind ocamlbuild coq
+
+# Uninstall Menhir if it is installed.
 
 if ocamlfind query menhirLib >/dev/null 2>/dev/null ; then
   if opam list -i menhir 2>/dev/null | grep -v -e "^#" | grep menhir ; then
-    echo "Warning: menhir is already installed." ;
-    read -p "Can I remove it [Enter/^C]?" -n 1 -r ;
+    echo "Warning: menhir is already installed. Removing it..." ;
+#   read -p "Can I remove it [Enter/^C]?" -n 1 -r ;
     opam remove menhir ;
   else
-    echo "Warning: menhirLib is already installed." ;
-    read -p "Can I remove it [Enter/^C]?" -n 1 -r ;
+    echo "Warning: menhirLib is already installed. Removing it..." ;
+#   read -p "Can I remove it [Enter/^C]?" -n 1 -r ;
     ocamlfind remove menhirLib ;
     ocamlfind remove menhirSdk || true ;
   fi ;
@@ -32,6 +41,7 @@ fi
 
 TEMPDIR=`mktemp -d /tmp/menhir-test.XXXXXX`
 INSTALL=$TEMPDIR/install
+COQCONTRIB=$INSTALL/coq-contrib
 
 cp $TARBALL $TEMPDIR
 
@@ -42,7 +52,9 @@ echo "   * Compiling and installing."
 mkdir $INSTALL
 (cd $TEMPDIR/$PACKAGE &&
   make PREFIX=$INSTALL USE_OCAMLFIND=true &&
-  make PREFIX=$INSTALL USE_OCAMLFIND=true install
+  make PREFIX=$INSTALL USE_OCAMLFIND=true install &&
+  make -C coq-menhirlib all &&
+  make -C coq-menhirlib CONTRIB=$COQCONTRIB install
 ) > $TEMPDIR/install.log 2>&1 || (cat $TEMPDIR/install.log; exit 1)
 
 echo "   * Building the demos."
@@ -53,6 +65,12 @@ echo "   * Building the demos."
 echo "   * Uninstalling."
 (cd $TEMPDIR/$PACKAGE &&
   make PREFIX=$INSTALL USE_OCAMLFIND=true uninstall
+  make -C coq-menhirlib CONTRIB=$COQCONTRIB uninstall
 ) > $TEMPDIR/uninstall.log 2>&1 || (cat $TEMPDIR/uninstall.log; exit 1)
 
 rm -rf $TEMPDIR
+
+# Move back to the original switch.
+
+echo "Switching back to $CURRENT..."
+opam switch $CURRENT

coq-menhirlib/CHANGES.md

+# Changes
+
+## 2019/06/26
+
+* Fix compatibility with Coq 8.7 and Coq 8.9:
+    - In Coq 8.7, in the syntax { x : T & T' } for the sigT types,
+      it was not possible to omit the type T.
+    - An anomaly in Coq 8.7 has been worked around.
+    - In Coq 8.9, the numeral notation for positives moved from
+      Coq.Numbers.BinNums to Coq.PArith.BinPos.
+
+## 2019/06/13
+
+* The Coq development is now free of any axiom (it used to use axiom
+  `K`), and the parsers can now be executed directly within Coq, without
+  using extraction.
+
+* The parser interpreter is now written using dependent types, so that
+  no dynamic checks are needed anymore at parsing time. When running
+  the extracted code, this should give a performance boost. Moreover,
+  efficient extraction of `int31` is no longer needed. This required
+  some refactoring of the type of parse trees.
+
+* Instead of a dependent pair of a terminal and a semantic
+  value, tokens are now a user-defined (inductive) type.
+
+## 2018/08/27
+
+* Avoid an undocumented mode of use of the `fix` tactic,
+  which would cause an incompatibility with Coq > 8.8.1.
+  (Reported and corrected by Michael Soegtrop.)
+
+## 2018/05/30
+
+* Initial release.

coq-menhirlib/Makefile

+# Delegate the following commands:
+
+.PHONY: all clean install uninstall
+
+all clean install uninstall:
+	@ $(MAKE) -C src --no-print-directory $@

coq-menhirlib/README.md

+# A support library for verified Coq parsers produced by Menhir
+
+The [Menhir](http://gallium.inria.fr/~fpottier/menhir/) parser generator,
+in `--coq` mode, can produce [Coq](https://coq.inria.fr/) parsers.
+
+These parsers must be linked against this library, which provides
+both an interpreter (which allows running the generated parser) and
+a validator (which allows verifying, at parser construction time,
+that the generated parser is correct and complete with respect to
+the grammar).
+
+## Installation
+
+To install the latest released version, use `opam install coq-menhirlib`.
+
+To install from the sources, use `make` followed with `make install`.
+
+## Authors
+
+* [Jacques-Henri Jourdan](jacques-henri.jourdan@lri.fr)

coq-menhirlib/src/.gitignore

+*.vo
+*.glob
+*.v.d
+.*.aux
+_CoqProject

coq-menhirlib/src/Alphabet.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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 Omega List Syntax Relations RelationClasses.
+
+Local Obligation Tactic := intros.
+
+(** A comparable type is equiped with a [compare] function, that define an order
+   relation. **)
+Class Comparable (A:Type) := {
+  compare : A -> A -> comparison;
+  compare_antisym : forall x y, CompOpp (compare x y) = compare y x;
+  compare_trans :  forall x y z c,
+    (compare x y) = c -> (compare y z) = c -> (compare x z) = c
+}.
+
+Theorem compare_refl {A:Type} (C: Comparable A) :
+  forall x, compare x x = Eq.
+Proof.
+intros.
+pose proof (compare_antisym x x).
+destruct (compare x x); intuition; try discriminate.
+Qed.
+
+(** The corresponding order is a strict order. **)
+Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
+  fun x y => compare x y = Lt.
+
+Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+  StrictOrder (comparableLt C).
+Proof.
+apply Build_StrictOrder.
+unfold Irreflexive, Reflexive, complement, comparableLt.
+intros.
+pose proof H.
+rewrite <- compare_antisym in H.
+rewrite H0 in H.
+discriminate H.
+unfold Transitive, comparableLt.
+intros x y z.
+apply compare_trans.
+Qed.
+
+(** nat is comparable. **)
+Program Instance natComparable : Comparable nat :=
+  { compare := Nat.compare }.
+Next Obligation.
+symmetry.
+destruct (Nat.compare x y)  as [] eqn:?.
+rewrite Nat.compare_eq_iff in Heqc.
+destruct Heqc.
+rewrite Nat.compare_eq_iff.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+Qed.
+Next Obligation.
+destruct c.
+rewrite Nat.compare_eq_iff in *; destruct H; assumption.
+rewrite <- nat_compare_lt in *.
+apply (Nat.lt_trans _ _ _ H H0).
+rewrite <- nat_compare_gt in *.
+apply (gt_trans _ _ _ H H0).
+Qed.
+
+(** A pair of comparable is comparable. **)
+Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
+  Comparable (A*B) :=
+  { compare := fun x y =>
+      let (xa, xb) := x in let (ya, yb) := y in
+      match compare xa ya return comparison with
+        | Eq => compare xb yb
+        | x => x
+      end }.
+Next Obligation.
+destruct x, y.
+rewrite <- (compare_antisym a a0).
+rewrite <- (compare_antisym b b0).
+destruct (compare a a0); intuition.
+Qed.
+Next Obligation.
+destruct x, y, z.
+destruct (compare a a0) as [] eqn:?, (compare a0 a1) as [] eqn:?;
+try (rewrite <- H0 in H; discriminate);
+try (destruct (compare a a1) as [] eqn:?;
+  try (rewrite <- compare_antisym in Heqc0;
+         rewrite CompOpp_iff in Heqc0;
+         rewrite (compare_trans _ _ _  _ Heqc0 Heqc2) in Heqc1;
+         discriminate);
+  try (rewrite <- compare_antisym in Heqc1;
+         rewrite CompOpp_iff in Heqc1;
+         rewrite (compare_trans _ _ _ _ Heqc2 Heqc1) in Heqc0;
+         discriminate);
+  assumption);
+rewrite (compare_trans _ _ _ _ Heqc0 Heqc1);
+try assumption.
+apply (compare_trans _ _ _ _ H H0).
+Qed.
+
+(** Special case of comparable, where equality is Leibniz equality. **)
+Class ComparableLeibnizEq {A:Type} (C: Comparable A) :=
+  compare_eq : forall x y, compare x y = Eq -> x = y.
+
+(** Boolean equality for a [Comparable]. **)
+Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) :=
+  match compare x y with
+    | Eq => true
+    | _ => false
+  end.
+
+Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableLeibnizEq C} :
+  forall x y, compare_eqb x y = true <-> x = y.
+Proof.
+unfold compare_eqb.
+intuition.
+apply compare_eq.
+destruct (compare x y); intuition; discriminate.
+destruct H.
+rewrite compare_refl; intuition.
+Qed.
+
+Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
+
+(** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
+Instance PairComparableLeibnizEq
+  {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
+  {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
+    ComparableLeibnizEq (PairComparable CA CB).
+Proof.
+intros x y; destruct x, y; simpl.
+pose proof (compare_eq a a0); pose proof (compare_eq b b0).
+destruct (compare a a0); try discriminate.
+intuition.
+destruct H2, H0.
+reflexivity.
+Qed.
+
+(** An [Finite] type is a type with the list of all elements. **)
+Class Finite (A:Type) := {
+  all_list : list A;
+  all_list_forall : forall x:A, In x all_list
+}.
+
+(** An alphabet is both [ComparableLeibnizEq] and [Finite]. **)
+Class Alphabet (A:Type) := {
+  AlphabetComparable :> Comparable A;
+  AlphabetComparableLeibnizEq :> ComparableLeibnizEq AlphabetComparable;
+  AlphabetFinite :> Finite A
+}.
+
+(** The [Numbered] class provides a conveniant way to build [Alphabet] instances,
+   with a good computationnal complexity. It is mainly a injection from it to
+   [positive] **)
+Class Numbered (A:Type) := {
+  inj : A -> positive;
+  surj : positive -> A;
+  surj_inj_compat : forall x, surj (inj x) = x;
+  inj_bound : positive;
+  inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
+}.
+
+Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+  { AlphabetComparable := {| compare := fun x y => Pos.compare (inj x) (inj y) |};
+    AlphabetFinite :=
+      {| all_list := fst (Pos.iter
+                           (fun '(l, p) => (surj p::l, Pos.succ p))
+                           ([], 1%positive) inj_bound) |} }.
+Next Obligation. simpl. now rewrite <- Pos.compare_antisym. Qed.
+Next Obligation.
+  match goal with c : comparison |- _ => destruct c end.
+  - rewrite Pos.compare_eq_iff in *. congruence.
+  - rewrite Pos.compare_lt_iff in *. eauto using Pos.lt_trans.
+  - rewrite Pos.compare_gt_iff in *. eauto using Pos.lt_trans.
+Qed.
+Next Obligation.
+  intros x y. unfold compare. intros Hxy.
+  assert (Hxy' : inj x = inj y).
+  (* We do not use [Pos.compare_eq_iff] directly to make sure the
+     proof is executable. *)
+  { destruct (Pos.eq_dec (inj x) (inj y)) as [|[]]; [now auto|].
+    now apply Pos.compare_eq_iff. }
+  (* Using rewrite here leads to non-executable proofs. *)
+  transitivity (surj (inj x)).
+  { apply eq_sym, surj_inj_compat. }
+  transitivity (surj (inj y)); cycle 1.
+  { apply surj_inj_compat. }
+  apply f_equal, Hxy'.
+Defined.
+Next Obligation.
+  rewrite <-(surj_inj_compat x).
+  generalize (inj_bound_spec x). generalize (inj x). clear x. intros x.
+  match goal with |- ?Hx -> In ?s (fst ?p) =>
+    assert ((Hx -> In s (fst p)) /\ snd p = Pos.succ inj_bound); [|now intuition] end.
+  rewrite Pos.lt_succ_r.
+  induction inj_bound as [|y [IH1 IH2]] using Pos.peano_ind;
+    (split; [intros Hx|]); simpl.
+  - rewrite (Pos.le_antisym _ _ Hx); auto using Pos.le_1_l.
+  - auto.
+  - rewrite Pos.iter_succ. destruct Pos.iter; simpl in *. subst.
+    rewrite Pos.le_lteq in Hx. destruct Hx as [?%Pos.lt_succ_r| ->]; now auto.
+  - rewrite Pos.iter_succ. destruct Pos.iter. simpl in IH2. subst. reflexivity.
+Qed.
+
+(** Definitions of [FSet]/[FMap] from [Comparable] **)
+Require Import OrderedTypeAlt.
+Require FSetAVL.
+Require FMapAVL.
+Import OrderedType.
+
+Module Type ComparableM.
+  Parameter t : Type.
+  Declare Instance tComparable : Comparable t.
+End ComparableM.
+
+Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.
+  Definition t := C.t.
+  Definition compare : t -> t -> comparison := compare.
+
+  Infix "?=" := compare (at level 70, no associativity).
+
+  Lemma compare_sym x y : (y?=x) = CompOpp (x?=y).
+  Proof. exact (Logic.eq_sym (compare_antisym x y)). Qed.
+  Lemma compare_trans c x y z :
+    (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+  Proof.
+  apply compare_trans.
+  Qed.
+End OrderedTypeAlt_from_ComparableM.
+
+Module OrderedType_from_ComparableM (C:ComparableM) <: OrderedType.
+  Module Alt := OrderedTypeAlt_from_ComparableM C.
+  Include (OrderedType_from_Alt Alt).
+End OrderedType_from_ComparableM.

coq-menhirlib/src/Automaton.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+Require Grammar.
+Require Export Alphabet.
+From Coq Require Import Orders.
+From Coq Require Export List Syntax.
+
+Module Type AutInit.
+  (** The grammar of the automaton. **)
+  Declare Module Gram:Grammar.T.
+  Export Gram.
+
+  (** The set of non initial state is considered as an alphabet. **)
+  Parameter noninitstate : Type.
+  Declare Instance NonInitStateAlph : Alphabet noninitstate.
+
+  Parameter initstate : Type.
+  Declare Instance InitStateAlph : Alphabet initstate.
+
+  (** When we are at this state, we know that this symbol is the top of the
+     stack. **)
+  Parameter last_symb_of_non_init_state: noninitstate -> symbol.
+End AutInit.
+
+Module Types(Import Init:AutInit).
+  (** In many ways, the behaviour of the initial state is different from the
+     behaviour of the other states. So we have chosen to explicitaly separate
+     them: the user has to provide the type of non initial states. **)
+  Inductive state :=
+    | Init: initstate -> state
+    | Ninit: noninitstate -> state.
+
+  Program Instance StateAlph : Alphabet state :=
+    { AlphabetComparable := {| compare := fun x y =>
+        match x, y return comparison with
+          | Init _, Ninit _ => Lt
+          | Init x, Init y => compare x y
+          | Ninit _, Init _ => Gt
+          | Ninit x, Ninit y => compare x y
+        end |};
+      AlphabetFinite := {| all_list := map Init all_list ++ map Ninit all_list |} }.
+  Local Obligation Tactic := intros.
+  Next Obligation.
+  destruct x, y; intuition; apply compare_antisym.
+  Qed.
+  Next Obligation.
+  destruct x, y, z; intuition.
+  apply (compare_trans _ i0); intuition.
+  congruence.
+  congruence.
+  apply (compare_trans _ n0); intuition.
+  Qed.
+  Next Obligation.
+  intros x y.
+  destruct x, y; intuition; try discriminate.
+  rewrite (compare_eq i i0); intuition.
+  rewrite (compare_eq n n0); intuition.
+  Qed.
+  Next Obligation.
+  apply in_or_app; destruct x; intuition;
+    [left|right]; apply in_map; apply  all_list_forall.
+  Qed.
+
+  Coercion Ninit : noninitstate >-> state.
+  Coercion Init : initstate >-> state.
+
+  (** For an LR automaton, there are four kind of actions that can be done at a
+     given state:
+       - Shifting, that is reading a token and putting it into the stack,
+       - Reducing a production, that is popping the right hand side of the
+          production from the stack, and pushing the left hand side,
+       - Failing
+       - Accepting the word (special case of reduction)
+
+     As in the menhir parser generator, we do not want our parser to read after
+     the end of stream. That means that once the parser has read a word in the
+     grammar language, it should stop without peeking the input stream. So, for
+     the automaton to be complete, the grammar must be particular: if a word is
+     in its language, then it is not a prefix of an other word of the language
+     (otherwise, menhir reports an end of stream conflict).
+
+     As a consequence of that, there is two notions of action: the first one is
+     an action performed before having read the stream, the second one is after
+  **)
+
+  Inductive lookahead_action (term:terminal) :=
+  | Shift_act: forall s:noninitstate,
+                 T term = last_symb_of_non_init_state s -> lookahead_action term
+  | Reduce_act: production -> lookahead_action term
+  | Fail_act: lookahead_action term.
+  Arguments Shift_act [term].
+  Arguments Reduce_act [term].
+  Arguments Fail_act [term].
+
+  Inductive action :=
+  | Default_reduce_act: production -> action
+  | Lookahead_act : (forall term:terminal, lookahead_action term) -> action.
+
+  (** Types used for the annotations of the automaton. **)
+
+  (** An item is a part of the annotations given to the validator.
+     It is acually a set of LR(1) items sharing the same core. It is needed
+     to validate completeness. **)
+  Record item := {
+  (** The pseudo-production of the item. **)
+    prod_item: production;
+
+  (** The position of the dot. **)
+    dot_pos_item: nat;
+
+  (** The lookahead symbol of the item. We are using a list, so we can store
+     together multiple LR(1) items sharing the same core. **)
+    lookaheads_item: list terminal
+  }.
+End Types.
+
+Module Type T.
+  Include AutInit <+ Types.
+  Module Export GramDefs := Grammar.Defs Gram.
+
+  (** For each initial state, the non terminal it recognizes. **)
+  Parameter start_nt: initstate -> nonterminal.
+
+  (** The action table maps a state to either a map terminal -> action. **)
+  Parameter action_table:
+    state -> action.
+  (** The goto table of an LR(1) automaton. **)
+  Parameter goto_table: state -> forall nt:nonterminal,
+    option { s:noninitstate | NT nt = last_symb_of_non_init_state s }.
+
+  (** Some annotations on the automaton to help the validation. **)
+
+  (** When we are at this state, we know that these symbols are just below
+     the top of the stack. The list is ordered such that the head correspond
+     to the (almost) top of the stack. **)
+  Parameter past_symb_of_non_init_state: noninitstate -> list symbol.
+
+  (** When we are at this state, the (strictly) previous states verify these
+     predicates. **)
+  Parameter past_state_of_non_init_state: noninitstate -> list (state -> bool).
+
+  (** The items of the state. **)
+  Parameter items_of_state: state -> list item.
+
+  (** The nullable predicate for non terminals :
+     true if and only if the symbol produces the empty string **)
+  Parameter nullable_nterm: nonterminal -> bool.
+
+  (** The first predicates for non terminals, symbols or words of symbols. A
+     terminal is in the returned list if, and only if the parameter produces a
+     word that begins with the given terminal **)
+  Parameter first_nterm: nonterminal -> list terminal.
+End T.

coq-menhirlib/src/Grammar.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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 Orders.
+Require Import Alphabet.
+
+(** The terminal non-terminal alphabets of the grammar. **)
+Module Type Alphs.
+  Parameters terminal nonterminal : Type.
+  Declare Instance TerminalAlph: Alphabet terminal.
+  Declare Instance NonTerminalAlph: Alphabet nonterminal.
+End Alphs.
+
+(** Definition of the alphabet of symbols, given the alphabet of terminals
+    and the alphabet of non terminals **)
+Module Symbol(Import A:Alphs).
+
+  Inductive symbol :=
+    | T: terminal -> symbol
+    | NT: nonterminal -> symbol.
+
+  Program Instance SymbolAlph : Alphabet symbol :=
+    { AlphabetComparable := {| compare := fun x y =>
+        match x, y return comparison with
+          | T _, NT _ => Gt
+          | NT _, T _ => Lt
+          | T x, T y => compare x y
+          | NT x, NT y => compare x y
+        end |};
+      AlphabetFinite := {| all_list :=
+        map T all_list++map NT all_list |} }.
+  Next Obligation.
+    destruct x; destruct y; intuition; apply compare_antisym.
+  Qed.
+  Next Obligation.
+    destruct x; destruct y; destruct z; intuition; try discriminate.
+    apply (compare_trans _ t0); intuition.
+    apply (compare_trans _ n0); intuition.
+  Qed.
+  Next Obligation.
+    intros x y.
+    destruct x; destruct y; try discriminate; intros.
+    rewrite (compare_eq t t0); now intuition.
+    rewrite (compare_eq n n0); now intuition.
+  Defined.
+  Next Obligation.
+    rewrite in_app_iff.
+    destruct x; [left | right]; apply in_map; apply all_list_forall.
+  Qed.
+
+End Symbol.
+
+(** A curryfied function with multiple parameters **)
+Definition arrows_right: Type -> list Type -> Type :=
+  fold_right (fun A B => A -> B).
+
+Module Type T.
+  Include Alphs <+ Symbol.
+
+  (** [symbol_semantic_type] maps a symbols to the type of its semantic
+     values. **)
+  Parameter symbol_semantic_type: symbol -> Type.
+
+  (** The type of productions identifiers **)
+  Parameter production : Type.
+  Declare Instance ProductionAlph : Alphabet production.
+
+  (** Accessors for productions: left hand side, right hand side,
+     and semantic action. The semantic actions are given in the form
+     of curryfied functions, that take arguments in the reverse order. **)
+  Parameter prod_lhs: production -> nonterminal.
+  (* The RHS of a production is given in reversed order, so that symbols  *)
+  Parameter prod_rhs_rev: production -> list symbol.
+  Parameter prod_action:
+    forall p:production,
+      arrows_right
+        (symbol_semantic_type (NT (prod_lhs p)))
+        (map symbol_semantic_type (prod_rhs_rev p)).
+
+  (** Tokens are the atomic elements of the input stream: they contain
+     a terminal and a semantic value of the type corresponding to this
+     terminal. *)
+  Parameter token : Type.
+  Parameter token_term : token -> terminal.
+  Parameter token_sem :
+    forall tok : token, symbol_semantic_type (T (token_term tok)).
+End T.
+
+Module Defs(Import G:T).
+
+  (** The semantics of a grammar is defined in two stages. First, we
+    define the notion of parse tree, which represents one way of
+    recognizing a word with a head symbol. Semantic values are stored
+    at the leaves.
+
+      This notion is defined in two mutually recursive flavours:
+    either for a single head symbol, or for a list of head symbols. *)
+  Inductive parse_tree:
+    forall (head_symbol:symbol) (word:list token), Type :=
+
+  (** Parse tree for a terminal symbol. *)
+  | Terminal_pt:
+    forall (tok:token), parse_tree (T (token_term tok)) [tok]
+
+  (** Parse tree for a non-terminal symbol.  *)
+  | Non_terminal_pt:
+    forall (prod:production) {word:list token},
+      parse_tree_list (prod_rhs_rev prod) word ->
+      parse_tree (NT (prod_lhs prod)) word
+
+  (* Note : the list head_symbols_rev is reversed. *)
+  with parse_tree_list:
+    forall (head_symbols_rev:list symbol) (word:list token), Type :=
+
+  | Nil_ptl: parse_tree_list [] []
+
+  | Cons_ptl:
+    forall {head_symbolsq:list symbol} {wordq:list token},
+      parse_tree_list head_symbolsq wordq ->
+
+    forall {head_symbolt:symbol} {wordt:list token},
+      parse_tree head_symbolt wordt ->
+
+      parse_tree_list (head_symbolt::head_symbolsq) (wordq++wordt).
+
+  (** We can now finish the definition of the semantics of a grammar,
+    by giving the semantic value assotiated with a parse tree. *)
+  Fixpoint pt_sem {head_symbol word} (tree:parse_tree head_symbol word) :
+    symbol_semantic_type head_symbol :=
+    match tree with
+    | Terminal_pt tok => token_sem tok
+    | Non_terminal_pt prod ptl => ptl_sem ptl (prod_action prod)
+    end
+  with ptl_sem {A head_symbols word} (tree:parse_tree_list head_symbols word) :
+    arrows_right A (map symbol_semantic_type head_symbols) -> A :=
+    match tree with
+    | Nil_ptl => fun act => act
+    | Cons_ptl q t => fun act => ptl_sem q (act (pt_sem t))
+    end.
+
+  Fixpoint pt_size {head_symbol word} (tree:parse_tree head_symbol word) :=
+    match tree with
+      | Terminal_pt _ => 1
+      | Non_terminal_pt _ l => S (ptl_size l)
+    end
+  with ptl_size {head_symbols word} (tree:parse_tree_list head_symbols word) :=
+    match tree with
+      | Nil_ptl => 0
+      | Cons_ptl q t =>
+         pt_size t + ptl_size q
+    end.
+End Defs.

coq-menhirlib/src/Interpreter.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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.
+From Coq.ssr Require Import ssreflect.
+Require Automaton.
+Require Import Alphabet Grammar Validator_safe.
+
+Module Make(Import A:Automaton.T).
+Module Import ValidSafe := Validator_safe.Make A.
+
+(** A few helpers for dependent types. *)
+
+(** Decidable propositions. *)
+Class Decidable (P : Prop) := decide : {P} + {~P}.
+Arguments decide _ {_}.
+
+(** A [Comparable] type has decidable equality. *)
+Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) :
+  Decidable (x = y).
+Proof.
+  unfold Decidable.
+  destruct (compare x y) eqn:EQ; [left; apply compare_eq; intuition | ..];
+    right; intros ->; by rewrite compare_refl in EQ.
+Defined.
+
+Instance list_decidable_eq T :
+  (forall x y : T, Decidable (x = y)) ->
+  (forall l1 l2 : list T, Decidable (l1 = l2)).
+Proof. unfold Decidable. decide equality. Defined.
+
+Ltac subst_existT :=
+  repeat
+    match goal with
+    | _ => progress subst
+    | H : @existT ?A ?P ?x ?y1 = @existT ?A ?P ?x ?y2 |- _ =>
+      let DEC := fresh in
+      assert (DEC : forall u1 u2 : A, Decidable (u1 = u2)) by apply _;
+      apply Eqdep_dec.inj_pair2_eq_dec in H; [|by apply DEC];
+      clear DEC
+    end.
+
+(** The interpreter is written using dependent types. In order to
+  avoid reducing proof terms while executing the parser, we thunk all
+  the propositions behind an arrow.
+  Note that thunkP is still in Prop so that it is erased by
+  extraction.
+ *)
+Definition thunkP (P : Prop) : Prop := True -> P.
+
+(** Sometimes, we actually need a reduced proof in a program (for
+  example when using an equality to cast a value). In that case,
+  instead of reducing the proof we already have, we reprove the
+  assertion by using decidability. *)
+Definition reprove {P} `{Decidable P} (p : thunkP P) : P :=
+  match decide P with
+  | left p => p
+  | right np => False_ind _ (np (p I))
+  end.
+
+(** Combination of reprove with eq_rect. *)
+Definition cast {T : Type} (F : T -> Type) {x y : T} (eq : thunkP (x = y))
+                {DEC : unit -> Decidable (x = y)}:
+                F x -> F y :=
+  fun a => eq_rect x F a y (@reprove _ (DEC ()) eq).
+
+Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)} a :
+  cast F eq a = a.
+Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
+
+(** Input buffers and operations on them. **)
+CoInductive buffer : Type :=
+  Buf_cons { buf_head : token; buf_tail : buffer }.
+
+Delimit Scope buffer_scope with buf.
+Bind Scope buffer_scope with buffer.
+
+Infix "::" := Buf_cons (at level 60, right associativity) : buffer_scope.
+
+(** Concatenation of a list and an input buffer **)
+Fixpoint app_buf (l:list token) (buf:buffer) :=
+  match l with
+    | nil => buf
+    | cons t q => (t :: app_buf q buf)%buf
+  end.
+Infix "++" := app_buf (at level 60, right associativity) : buffer_scope.
+
+Lemma app_buf_assoc (l1 l2:list token) (buf:buffer) :
+  (l1 ++ (l2 ++ buf) = (l1 ++ l2) ++ buf)%buf.
+Proof. induction l1 as [|?? IH]=>//=. rewrite IH //. Qed.
+
+(** The type of a non initial state: the type of semantic values associated
+   with the last symbol of this state. *)
+Definition noninitstate_type state :=
+  symbol_semantic_type (last_symb_of_non_init_state state).
+
+(** The stack of the automaton : it can be either nil or contains a non
+    initial state, a semantic value for the symbol associted with this state,
+    and a nested stack. **)
+Definition stack := list (sigT noninitstate_type). (* eg. list {state & state_type state} *)
+
+Section Interpreter.
+
+Hypothesis safe: safe.
+
+(* Properties of the automaton deduced from safety validation. *)
+Proposition shift_head_symbs: shift_head_symbs.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition goto_head_symbs: goto_head_symbs.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition shift_past_state: shift_past_state.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition goto_past_state: goto_past_state.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+Proposition reduce_ok: reduce_ok.
+Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed.
+
+Variable init : initstate.
+
+(** The top state of a stack **)
+Definition state_of_stack (stack:stack): state :=
+  match stack with
+    | [] => init
+    | existT _ s _::_ => s
+  end.
+
+(** The stack of states of an automaton stack **)
+Definition state_stack_of_stack (stack:stack) :=
+  (List.map
+    (fun cell:sigT noninitstate_type => singleton_state_pred (projT1 cell))
+    stack ++ [singleton_state_pred init])%list.
+
+(** The stack of symbols of an automaton stack **)
+Definition symb_stack_of_stack (stack:stack) :=
+  List.map
+    (fun cell:sigT noninitstate_type => last_symb_of_non_init_state (projT1 cell))
+    stack.
+
+(** The stack invariant : it basically states that the assumptions on the
+    states are true. **)
+Inductive stack_invariant: stack -> Prop :=
+  | stack_invariant_constr:
+    forall stack,
+      prefix      (head_symbs_of_state (state_of_stack stack))
+                  (symb_stack_of_stack stack) ->
+      prefix_pred (head_states_of_state (state_of_stack stack))
+                  (state_stack_of_stack stack) ->
+      stack_invariant_next stack ->
+      stack_invariant stack
+with stack_invariant_next: stack -> Prop :=
+  | stack_invariant_next_nil:
+      stack_invariant_next []
+  | stack_invariant_next_cons:
+    forall state_cur st stack_rec,
+      stack_invariant stack_rec ->
+      stack_invariant_next (existT _ state_cur st::stack_rec).
+
+(** [pop] pops some symbols from the stack. It returns the popped semantic
+    values using [sem_popped] as an accumulator and discards the popped
+    states.**)
+Fixpoint pop (symbols_to_pop:list symbol) {A:Type} (stk:stack) :
+  thunkP (prefix symbols_to_pop (symb_stack_of_stack stk)) ->
+  forall (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
+    stack * A.
+unshelve refine
+  (match symbols_to_pop
+      return
+         (thunkP (prefix symbols_to_pop (symb_stack_of_stack stk))) ->
+         forall (action:arrows_right A (map _ symbols_to_pop)), stack * A
+   with
+     | [] => fun _ action => (stk, action)
+     | t::q => fun Hp action =>
+       match stk
+          return thunkP (prefix (t::q) (symb_stack_of_stack stk)) -> stack * A
+       with
+         | existT _ state_cur sem::stack_rec => fun Hp =>
+           let sem_conv := cast symbol_semantic_type _ sem in
+           pop q _ stack_rec _ (action sem_conv)
+         | [] => fun Hp => False_rect _ _
+       end Hp
+   end).
+Proof.
+  - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
+  - clear -Hp. abstract (specialize (Hp I); now inversion Hp).
+  - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp).
+Defined.
+
+(* Equivalent declarative specification for pop, so that we avoid
+   (part of) the dependent types nightmare. *)
+Inductive pop_spec {A:Type} :
+    forall (symbols_to_pop:list symbol) (stk : stack)
+           (action : arrows_right A (map symbol_semantic_type symbols_to_pop))
+           (stk' : stack) (sem : A),
+      Prop :=
+  | Nil_pop_spec stk sem : pop_spec [] stk sem stk sem
+  | Cons_pop_spec symbols_to_pop st stk action sem stk' res :
+      pop_spec symbols_to_pop stk (action sem) stk' res ->
+      pop_spec (last_symb_of_non_init_state st::symbols_to_pop)
+               (existT _ st sem :: stk) action stk' res.
+
+Lemma pop_spec_ok {A:Type} symbols_to_pop stk Hp action stk' res:
+  pop symbols_to_pop stk Hp action = (stk', res) <->
+  pop_spec (A:=A) symbols_to_pop stk action stk' res.
+Proof.
+  revert stk Hp action.
+  induction symbols_to_pop as [|t symbols_to_pop IH]=>stk Hp action /=.
+  - split.
+    + intros [= <- <-]. constructor.
+    + intros H. inversion H. by subst_existT.
+  - destruct stk as [|[st sem]]=>/=; [by destruct pop_subproof0|].
+    remember (pop_subproof t symbols_to_pop stk st Hp) as EQ eqn:eq. clear eq.
+    generalize EQ. revert Hp action. rewrite <-(EQ I)=>Hp action ?.
+    rewrite cast_eq. rewrite IH. split.
+    + intros. by constructor.
+    + intros H. inversion H. by subst_existT.
+Qed.
+
+
+Lemma pop_preserves_invariant symbols_to_pop stk Hp A action :
+  stack_invariant stk ->
+  stack_invariant (fst (pop symbols_to_pop stk Hp (A:=A) action)).
+Proof.
+  revert stk Hp A action. induction symbols_to_pop as [|t q IH]=>//=.
+  intros stk Hp A action Hi.
+  destruct Hi as [stack Hp' Hpp [|state st stk']].
+  - destruct pop_subproof0.
+  - now apply IH.
+Qed.
+
+Lemma pop_state_valid symbols_to_pop stk Hp A action lpred :
+  prefix_pred lpred (state_stack_of_stack stk) ->
+  let stk' := fst (pop symbols_to_pop stk Hp (A:=A) action) in
+  state_valid_after_pop (state_of_stack stk') symbols_to_pop lpred.
+Proof.
+  revert stk Hp A action lpred. induction symbols_to_pop as [|t q IH]=>/=.
+  - intros stk Hp A a lpred Hpp. destruct lpred as [|pred lpred]; constructor.
+    inversion Hpp as [|? lpred' ? pred' Himpl Hpp' eq1 eq2]; subst.
+    specialize (Himpl (state_of_stack stk)).
+    destruct (pred' (state_of_stack stk)) as [] eqn:Heqpred'=>//.
+    destruct stk as [|[]]; simpl in *.
+    + inversion eq2; subst; clear eq2.
+      unfold singleton_state_pred in Heqpred'.
+      now rewrite compare_refl in Heqpred'; discriminate.
+    + inversion eq2; subst; clear eq2.
+      unfold singleton_state_pred in Heqpred'.
+      now rewrite compare_refl in Heqpred'; discriminate.
+  - intros stk Hp A a lpred Hpp. destruct stk as [|[] stk]=>//=.
+    + destruct pop_subproof0.
+    + destruct lpred as [|pred lpred]; [by constructor|].
+      constructor. apply IH. by inversion Hpp.
+Qed.
+
+(** [step_result] represents the result of one step of the automaton : it can
+    fail, accept or progress. [Fail_sr] means that the input is incorrect.
+    [Accept_sr] means that this is the last step of the automaton, and it
+    returns the semantic value of the input word. [Progress_sr] means that
+    some progress has been made, but new steps are needed in order to accept
+    a word.
+
+    For [Accept_sr] and [Progress_sr], the result contains the new input buffer.
+
+    [Fail_sr] means that the input word is rejected by the automaton. It is
+    different to [Err] (from the error monad), which mean that the automaton is
+    bogus and has perfomed a forbidden action. **)
+Inductive step_result :=
+  | Fail_sr: step_result
+  | Accept_sr: symbol_semantic_type (NT (start_nt init)) -> buffer -> step_result
+  | Progress_sr: stack -> buffer -> step_result.
+
+(** [reduce_step] does a reduce action :
+   - pops some elements from the stack
+   - execute the action of the production
+   - follows the goto for the produced non terminal symbol **)
+Definition reduce_step stk prod (buffer : buffer)
+        (Hval : thunkP (valid_for_reduce (state_of_stack stk) prod))
+        (Hi : thunkP (stack_invariant stk))
+  : step_result.
+refine
+  ((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod)
+      return thunkP (state_valid_after_pop (state_of_stack (fst ss)) _
+                               (head_states_of_state (state_of_stack stk))) -> _
+    in fun Hval' =>
+    match goto_table (state_of_stack stk') (prod_lhs prod) as goto
+      return (thunkP (goto = None ->
+                      match state_of_stack stk' with
+                      | Init i => prod_lhs prod = start_nt i
+                      | Ninit _ => False
+                      end)) -> _
+    with
+    | Some (exist _ state_new e) => fun _ =>
+      let sem := eq_rect _ _ sem _ e in
+      Progress_sr (existT noninitstate_type state_new sem::stk') buffer
+    | None => fun Hval =>
+      let sem := cast symbol_semantic_type _ sem in
+      Accept_sr sem buffer
+    end (fun _ => _))
+   (fun _ => pop_state_valid _ _ _ _ _ _ _)).
+Proof.
+  - clear -Hi Hval.
+    abstract (intros _; destruct Hi=>//; eapply prefix_trans; [by apply Hval|eassumption]).
+  - clear -Hval.
+    abstract (intros _; f_equal; specialize (Hval I eq_refl); destruct stk' as [|[]]=>//).
+  - simpl in Hval'. clear -Hval Hval'.
+    abstract (move : Hval => /(_ I) [_ /(_ _ (Hval' I))] Hval2 Hgoto; by rewrite Hgoto in Hval2).
+  - clear -Hi. abstract by destruct Hi.
+Defined.
+
+Lemma reduce_step_stack_invariant_preserved stk prod buffer Hv Hi stk' buffer':
+  reduce_step stk prod buffer Hv Hi = Progress_sr stk' buffer' ->
+  stack_invariant stk'.
+Proof.
+  unfold reduce_step.
+  match goal with
+  | |- context [pop ?symbols_to_pop stk ?Hp ?action] =>
+    assert (Hi':=pop_preserves_invariant symbols_to_pop stk Hp _ action (Hi I));
+    generalize (pop_state_valid symbols_to_pop stk Hp _ action)
+  end.
+  destruct pop as [stk0 sem]=>/=. simpl in Hi'. intros Hv'.
+  assert (Hgoto1:=goto_head_symbs (state_of_stack stk0) (prod_lhs prod)).
+  assert (Hgoto2:=goto_past_state (state_of_stack stk0) (prod_lhs prod)).
+  match goal with | |- context [fun _ : True => ?X] => generalize X end.
+  destruct goto_table as [[state_new e]|] eqn:EQgoto=>//.
+  intros _ [= <- <-]. constructor=>/=.
+  - constructor. eapply prefix_trans. apply Hgoto1. by destruct Hi'.
+  - unfold state_stack_of_stack; simpl; constructor.
+    + intros ?. by destruct singleton_state_pred.
+    + eapply prefix_pred_trans. apply Hgoto2. by destruct Hi'.
+  - by constructor.
+Qed.
+
+(** One step of parsing. **)
+Definition step stk buffer (Hi : thunkP (stack_invariant stk)): step_result :=
+  match action_table (state_of_stack stk) as a return
+    thunkP
+      match a return Prop with
+      | Default_reduce_act prod => _
+      | Lookahead_act awt => forall t : terminal,
+        match awt t with
+        | Reduce_act p => _
+        | _ => True
+        end
+      end -> _
+  with
+  | Default_reduce_act prod => fun Hv =>
+    reduce_step stk prod buffer Hv Hi
+  | Lookahead_act awt => fun Hv =>
+    match buf_head buffer with
+    | tok =>
+      match awt (token_term tok) as a return
+        thunkP match a return Prop with Reduce_act p => _ | _ => _ end -> _
+      with
+      | Shift_act state_new e => fun _ =>
+        let sem_conv := eq_rect _ symbol_semantic_type (token_sem tok) _ e in
+        Progress_sr (existT noninitstate_type state_new sem_conv::stk)
+                    (buf_tail buffer)
+      | Reduce_act prod => fun Hv =>
+        reduce_step stk prod buffer Hv Hi
+      | Fail_act => fun _ =>
+        Fail_sr
+      end (fun _ => Hv I (token_term tok))
+    end
+  end (fun _ => reduce_ok _).
+
+Lemma step_stack_invariant_preserved stk buffer Hi stk' buffer':
+  step stk buffer Hi = Progress_sr stk' buffer' ->
+  stack_invariant stk'.
+Proof.
+  unfold step.
+  generalize (reduce_ok (state_of_stack stk))=>Hred.
+  assert (Hshift1 := shift_head_symbs (state_of_stack stk)).
+  assert (Hshift2 := shift_past_state (state_of_stack stk)).
+  destruct action_table as [prod|awt]=>/=.
+  - eauto using reduce_step_stack_invariant_preserved.
+  - set (term := token_term (buf_head buffer)).
+    generalize (Hred term). clear Hred. intros Hred.
+    specialize (Hshift1 term). specialize (Hshift2 term).
+    destruct (awt term) as [state_new e|prod|]=>//.
+    + intros [= <- <-]. constructor=>/=.
+      * constructor. eapply prefix_trans. apply Hshift1. by destruct Hi.
+      * unfold state_stack_of_stack; simpl; constructor.
+        -- intros ?. by destruct singleton_state_pred.
+        -- eapply prefix_pred_trans. apply Hshift2. by destruct Hi.
+      * constructor; by apply Hi.
+    + eauto using reduce_step_stack_invariant_preserved.
+Qed.
+
+(** The parsing use a [nat] fuel parameter [log_n_steps], so that we
+    do not have to prove terminaison, which is difficult.
+
+    Note that [log_n_steps] is *not* the fuel in the conventionnal
+    sense: this parameter contains the logarithm (in base 2) of the
+    number of steps to perform. Hence, a value of, e.g., 50 will
+    usually be enough to ensure termination. *)
+Fixpoint parse_fix stk buffer (log_n_steps : nat) (Hi : thunkP (stack_invariant stk)):
+  { sr : step_result |
+    forall stk' buffer', sr = Progress_sr stk' buffer' -> stack_invariant stk' } :=
+  match log_n_steps with
+  | O => exist _ (step stk buffer Hi)
+                 (step_stack_invariant_preserved _ _ Hi)
+  | S log_n_steps =>
+    match parse_fix stk buffer log_n_steps Hi with
+    | exist _ (Progress_sr stk buffer) Hi' =>
+      parse_fix stk buffer log_n_steps (fun _ => Hi' _ buffer eq_refl)
+    | sr => sr
+    end
+  end.
+
+(** The final result of a parsing is either a failure (the automaton
+    has rejected the input word), either a timeout (the automaton has
+    spent all the given [2^log_n_steps]), either a parsed semantic value
+    with a rest of the input buffer.
+
+    Note that we do not make parse_result depend on start_nt for the
+    result type, so that this inductive is extracted without the use
+    of Obj.t in OCaml.  **)
+Inductive parse_result {A : Type} :=
+  | Fail_pr: parse_result
+  | Timeout_pr: parse_result
+  | Parsed_pr: A -> buffer -> parse_result.
+Global Arguments parse_result _ : clear implicits.
+
+Definition parse (buffer : buffer) (log_n_steps : nat):
+  parse_result (symbol_semantic_type (NT (start_nt init))).
+refine (match proj1_sig (parse_fix [] buffer log_n_steps _) with
+        | Fail_sr => Fail_pr
+        | Accept_sr sem buffer' => Parsed_pr sem buffer'
+        | Progress_sr _ _ => Timeout_pr
+        end).
+Proof.
+  abstract (repeat constructor; intros; by destruct singleton_state_pred).
+Defined.
+
+End Interpreter.
+
+Arguments Fail_sr {init}.
+Arguments Accept_sr {init} _ _.
+Arguments Progress_sr {init} _ _.
+
+End Make.
+
+Module Type T(A:Automaton.T).
+  Include (Make A).
+End T.

coq-menhirlib/src/Interpreter_correct.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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.
+Require Import Alphabet.
+Require Grammar Automaton Interpreter.
+From Coq.ssr Require Import ssreflect.
+
+Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
+
+(** * Correctness of the interpreter **)
+
+(** We prove that, in any case, if the interpreter accepts returning a
+    semantic value, then this is a semantic value of the input **)
+
+Section Init.
+
+Variable init:initstate.
+
+(** [word_has_stack_semantics] relates a word with a stack, stating that the
+    word is a concatenation of words that have the semantic values stored in
+    the stack. **)
+Inductive word_has_stack_semantics:
+  forall (word:list token) (stack:stack), Prop :=
+  | Nil_stack_whss: word_has_stack_semantics [] []
+  | Cons_stack_whss:
+    forall (wordq:list token) (stackq:stack),
+      word_has_stack_semantics wordq stackq ->
+
+    forall (wordt:list token) (s:noninitstate)
+           (pt:parse_tree (last_symb_of_non_init_state s) wordt),
+
+    word_has_stack_semantics
+       (wordq++wordt) (existT noninitstate_type s (pt_sem pt)::stackq).
+
+(** [pop] preserves the invariant **)
+Lemma pop_spec_ptl A symbols_to_pop action word_stk stk (res : A) stk' :
+  pop_spec symbols_to_pop stk action stk' res ->
+  word_has_stack_semantics word_stk stk ->
+  exists word_stk' word_res (ptl:parse_tree_list symbols_to_pop word_res),
+    (word_stk' ++ word_res = word_stk)%list /\
+    word_has_stack_semantics word_stk' stk' /\
+    ptl_sem ptl action = res.
+Proof.
+  intros Hspec. revert word_stk.
+  induction Hspec as [stk sem|symbols_to_pop st stk action sem stk' res Hspec IH];
+    intros word_stk Hword_stk.
+  - exists word_stk, [], Nil_ptl. rewrite -app_nil_end. eauto.
+  - inversion Hword_stk. subst_existT.
+    edestruct IH as (word_stk' & word_res & ptl & ? & Hword_stk'' & ?); [eassumption|].
+    subst. eexists word_stk', (word_res ++ _)%list, (Cons_ptl ptl _).
+    split; [|split]=>//. rewrite app_assoc //.
+Qed.
+
+(** [reduce_step] preserves the invariant **)
+Lemma reduce_step_invariant (stk:stack) (prod:production) Hv Hi word buffer :
+  word_has_stack_semantics word stk ->
+  match reduce_step init stk prod buffer Hv Hi with
+  | Accept_sr sem buffer_new =>
+    exists pt : parse_tree (NT (start_nt init)) word,
+    buffer = buffer_new /\ pt_sem pt = sem
+  | Progress_sr stk' buffer_new =>
+    buffer = buffer_new /\ word_has_stack_semantics word stk'
+  | Fail_sr => True
+  end.
+Proof.
+  intros Hword_stk. unfold reduce_step.
+  match goal with
+  | |- context [pop_state_valid init ?stp stk ?x1 ?x2 ?x3 ?x4 ?x5] =>
+    generalize (pop_state_valid init stp stk x1 x2 x3 x4 x5)
+  end.
+  destruct pop as [stk' sem] eqn:Hpop=>/= Hv'.
+  apply pop_spec_ok in Hpop. apply pop_spec_ptl with (word_stk := word) in Hpop=>//.
+  destruct Hpop as (word1 & word2 & ptl & <- & Hword1 & <-).
+  generalize (reduce_step_subproof1 init stk prod Hv stk' (fun _ : True => Hv')).
+  destruct goto_table as [[st' EQ]|].
+  - intros _. split=>//.
+    change (ptl_sem ptl (prod_action prod)) with (pt_sem (Non_terminal_pt prod ptl)).
+    generalize (Non_terminal_pt prod ptl). rewrite ->EQ. intros pt. by constructor.
+  - intros Hstk'. destruct Hword1; [|by destruct Hstk'].
+    generalize (reduce_step_subproof0 init prod [] (fun _ : True => Hstk')).
+    simpl in Hstk'. rewrite -Hstk' // => EQ. rewrite cast_eq.
+    exists (Non_terminal_pt prod ptl). by split.
+Qed.
+
+(** [step] preserves the invariant **)
+Lemma step_invariant stk word buffer safe Hi :
+  word_has_stack_semantics word stk ->
+  match step safe init stk buffer Hi with
+  | Accept_sr sem buffer_new =>
+    exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      pt_sem pt = sem
+  | Progress_sr stk_new buffer_new =>
+    exists word_new,
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      word_has_stack_semantics word_new stk_new
+  | Fail_sr => True
+  end.
+Proof.
+  intros Hword_stk. unfold step.
+  generalize (reduce_ok safe (state_of_stack init stk)).
+  destruct action_table as [prod|awt].
+  - intros Hv.
+    apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word buffer) in Hword_stk.
+    destruct reduce_step=>//.
+    + destruct Hword_stk as (pt & <- & <-); eauto.
+    + destruct Hword_stk as [<- ?]; eauto.
+  - destruct buffer as [tok buffer]=>/=.
+    move=> /(_ (token_term tok)) Hv. destruct (awt (token_term tok)) as [st EQ|prod|]=>//.
+    + eexists _. split; [by apply app_buf_assoc with (l2 := [_])|].
+      change (token_sem tok) with (pt_sem (Terminal_pt tok)).
+      generalize (Terminal_pt tok). generalize [tok].
+      rewrite -> EQ=>word' pt /=. by constructor.
+    + apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word (tok::buffer))
+        in Hword_stk.
+      destruct reduce_step=>//.
+      * destruct Hword_stk as (pt & <- & <-); eauto.
+      * destruct Hword_stk as [<- ?]; eauto.
+Qed.
+
+(** [step] preserves the invariant **)
+Lemma parse_fix_invariant stk word buffer safe log_n_steps Hi :
+  word_has_stack_semantics word stk ->
+  match proj1_sig (parse_fix safe init stk buffer log_n_steps Hi) with
+  | Accept_sr sem buffer_new =>
+    exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      pt_sem pt = sem
+  | Progress_sr stk_new buffer_new =>
+    exists word_new,
+      (word ++ buffer = word_new ++ buffer_new)%buf /\
+      word_has_stack_semantics word_new stk_new
+  | Fail_sr => True
+  end.
+Proof.
+  revert stk word buffer Hi.
+  induction log_n_steps as [|log_n_steps IH]=>/= stk word buffer Hi Hstk;
+    [by apply step_invariant|].
+  assert (IH1 := IH stk word buffer Hi Hstk).
+  destruct parse_fix as [[] Hi']=>/=; try by apply IH1.
+  destruct IH1 as (word' & -> & Hstk')=>//. by apply IH.
+Qed.
+
+(** The interpreter is correct : if it returns a semantic value, then the input
+    word has this semantic value.
+**)
+Theorem parse_correct safe buffer log_n_steps:
+  match parse safe init buffer log_n_steps with
+  | Parsed_pr sem buffer_new =>
+    exists word_new (pt:parse_tree (NT (start_nt init)) word_new),
+      buffer = (word_new ++ buffer_new)%buf /\
+      pt_sem pt = sem
+  | _ => True
+  end.
+Proof.
+  unfold parse.
+  assert (Hparse := parse_fix_invariant [] [] buffer safe log_n_steps
+                                        (parse_subproof init)).
+  destruct proj1_sig=>//. apply Hparse. constructor.
+Qed.
+
+End Init.
+
+End Make.

coq-menhirlib/src/Main.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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.            *)
+(*                                                                          *)
+(****************************************************************************)
+
+Require Grammar Automaton Interpreter_correct Interpreter_complete.
+From Coq Require Import Syntax Arith.
+
+Module Make(Export Aut:Automaton.T).
+Export Aut.Gram.
+Export Aut.GramDefs.
+
+Module Import Inter := Interpreter.Make Aut.
+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 := ValidSafe.is_safe.
+Definition parse (safe:safe_validator ()=true) init log_n_steps buffer :
+  parse_result (symbol_semantic_type (NT (start_nt init))):=
+  parse (ValidSafe.safe_is_validator safe) init buffer log_n_steps.
+
+(** Correction theorem. **)
+Theorem parse_correct
+  (safe:safe_validator ()= true) init log_n_steps buffer:
+  match parse safe init log_n_steps buffer with
+    | Parsed_pr sem buffer_new =>
+      exists word (pt : parse_tree (NT (start_nt init)) word),
+        buffer = (word ++ buffer_new)%buf /\
+        pt_sem pt = sem
+    | _ => True
+  end.
+Proof. apply Correct.parse_correct. Qed.
+
+(** Completeness theorem. **)
+Theorem parse_complete
+  (safe:safe_validator () = true) init log_n_steps word buffer_end:
+  complete_validator () = true ->
+  forall tree:parse_tree (NT (start_nt init)) word,
+  match parse safe init log_n_steps (word ++ buffer_end) with
+  | Fail_pr => False
+  | Parsed_pr sem_res buffer_end_res =>
+    sem_res = pt_sem tree /\ buffer_end_res = buffer_end /\
+    pt_size tree <= 2^log_n_steps
+  | Timeout_pr => 2^log_n_steps < pt_size tree
+  end.
+Proof.
+  intros. now apply Complete.parse_complete, Complete.Valid.complete_is_validator.
+Qed.
+
+(** Unambiguity theorem. **)
+Theorem unambiguity:
+  safe_validator () = true -> complete_validator () = true -> inhabited token ->
+  forall init word,
+  forall (tree1 tree2:parse_tree (NT (start_nt init)) word),
+    pt_sem tree1 = pt_sem tree2.
+Proof.
+  intros Hsafe Hcomp [tok] init word tree1 tree2.
+  pose (buf_end := cofix buf_end := (tok :: buf_end)%buf).
+  assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word buf_end
+                                   Hcomp tree1).
+  assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word buf_end
+                                   Hcomp tree2).
+  destruct parse.
+  - destruct Hcomp1.
+  - exfalso. eapply PeanoNat.Nat.lt_irrefl. etransitivity; [|apply Hcomp1].
+    eapply Nat.pow_gt_lin_r. constructor.
+  - destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
+Qed.
+
+End Make.

coq-menhirlib/src/Makefile

+PWD := $(shell pwd)
+
+COQINCLUDE := -R $(PWD) MenhirLib \
+
+export
+
+.PHONY: all clean install uninstall
+
+all:
+
+_CoqProject:
+	@ $(MAKE) -f Makefile.coq --no-print-directory _CoqProject
+
+all: _CoqProject
+	@ $(MAKE) -f Makefile.coq --no-print-directory all
+
+clean:
+	@ $(MAKE) -f Makefile.coq --no-print-directory clean
+	@ rm -f _CoqProject
+
+# The role of DESTDIR is explained here:
+# https://www.gnu.org/prep/standards/html_node/DESTDIR.html
+# Basically, it is empty in a normal installation.
+# A nonempty value can be used to perform a dummy installation
+# in a different location.
+
+CONTRIB := $(shell $(COQBIN)coqc -where)/user-contrib
+TARGET  := $(DESTDIR)$(CONTRIB)/MenhirLib
+
+install: all
+	rm -rf $(TARGET)
+	mkdir -p $(TARGET)
+	install -m 644 *.v *.vo *.glob $(TARGET)
+
+uninstall:
+	rm -rf $(TARGET)

coq-menhirlib/src/Makefile.coq

+############################################################################
+# Requirements.
+
+# We need bash. We use the pipefail option to control the exit code of a
+# pipeline.
+
+SHELL := /usr/bin/env bash
+
+############################################################################
+# Configuration
+#
+#
+# This Makefile relies on the following variables:
+# ROOTDIR    (default: `pwd`)
+# COQBIN     (default: empty)
+# COQINCLUDE (default: empty)
+# V          (default: *.v)
+# V_AUX      (default: undefined/empty)
+# SERIOUS    (default: 1)
+#            (if 0, we produce .vio files)
+#            (if 1, we produce .vo files in the old way)
+# VERBOSE    (default: undefined)
+#            (if defined, commands are displayed)
+
+# We usually refer to the .v files using relative paths (such as Foo.v)
+# but [coqdep -R] produces dependencies that refer to absolute paths
+# (such as /bar/Foo.v). This confuses [make], which does not recognize
+# that these files are the same. As a result, [make] does not respect
+# the dependencies.
+
+# We fix this by using ABSOLUTE PATHS EVERYWHERE. The paths used in targets,
+# in -R options, etc., must be absolute paths.
+
+ifndef ROOTDIR
+	ROOTDIR := $(shell pwd)
+endif
+
+ifndef V
+	V := $(wildcard $(ROOTDIR)/*.v)
+endif
+
+# Typically, $(V) should list only the .v files that we are ultimately
+# interested in checking. $(V_AUX) should list every other .v file in the
+# project. $(VD) is obtained from $(V) and $(V_AUX), so [make] sees all
+# dependencies and can rebuild files anywhere in the project, if needed, and
+# only if needed.
+
+ifndef VD
+	VD  := $(patsubst %.v,%.v.d,$(V) $(V_AUX))
+endif
+
+VIO := $(patsubst %.v,%.vio,$(V))
+VQ  := $(patsubst %.v,%.vq,$(V))
+VO  := $(patsubst %.v,%.vo,$(V))
+
+SERIOUS := 1
+
+############################################################################
+# Binaries
+
+COQC   := $(COQBIN)coqc $(COQFLAGS)
+COQDEP := $(COQBIN)coqdep
+COQIDE := $(COQBIN)coqide $(COQFLAGS)
+COQCHK := $(COQBIN)coqchk
+
+############################################################################
+# Targets
+
+.PHONY: all proof depend quick proof_vo proof_vq
+
+all: proof
+ifeq ($(SERIOUS),0)
+proof: proof_vq
+else
+proof: proof_vo
+endif
+proof_vq: $(VQ)
+depend: $(VD)
+quick: $(VIO)
+proof_vo: $(VO)
+
+############################################################################
+# Verbosity control.
+
+# Our commands are pretty long (due, among other things, to the use of
+# absolute paths everywhere). So, we hide them by default, and echo a short
+# message instead. However, sometimes one wants to see the command.
+
+# By default, VERBOSE is undefined, so the .SILENT directive is read, so no
+# commands are echoed. If VERBOSE is defined by the user, then the .SILENT
+# directive is ignored, so commands are echoed, unless they begin with an
+# explicit @.
+
+ifndef VERBOSE
+.SILENT:
+endif
+
+############################################################################
+# Verbosity filter.
+
+# Coq is way too verbose when using one of the -schedule-* commands.
+# So, we grep its output and remove any line that contains 'Checking task'.
+
+# We need a pipe that keeps the exit code of the *first* process. In
+# bash, when the pipefail option is set, the exit code is the logical
+# conjunction of the exit codes of the two processes. If we make sure
+# that the second process always succeeds, then we get the exit code
+# of the first process, as desired.
+
+############################################################################
+# Rules
+
+# If B uses A, then the dependencies produced by coqdep are:
+# B.vo:  B.v A.vo
+# B.vio: B.v A.vio
+
+%.v.d: %.v
+	$(COQDEP) $(COQINCLUDE) $< > $@
+
+ifeq ($(SERIOUS),0)
+
+%.vo: %.vio
+	@echo "Compiling `basename $*`..."
+	set -o pipefail; ( \
+	  $(COQC) $(COQINCLUDE) -schedule-vio2vo 1 $* \
+	  2>&1 | (grep -v 'Checking task' || true))
+
+# The recipe for producing %.vio destroys %.vo. In other words, we do not
+# allow a young .vio file to co-exist with an old (possibly out-of-date) .vo
+# file, because this seems to lead Coq into various kinds of problems
+# ("inconsistent assumption" errors, "undefined universe" errors, warnings
+# about the existence of both files, and so on). Destroying %.vo should be OK
+# as long as the user does not try to build a mixture of .vo and .vio files in
+# one invocation of make.
+%.vio: %.v
+	@echo "Digesting `basename $*`..."
+	rm -f $*.vo
+	$(COQC) $(COQINCLUDE) -quick $<
+
+%.vq: %.vio
+	@echo "Checking `basename $*`..."
+	set -o pipefail; ( \
+	  $(COQC) $(COQINCLUDE) -schedule-vio-checking 1 $< \
+	  2>&1 | (grep -v 'Checking task' || true))
+	touch $@
+
+endif
+
+ifeq ($(SERIOUS),1)
+
+%.vo: %.v
+	@echo "Compiling `basename $*`..."
+	$(COQC) $(COQINCLUDE) $<
+
+# 	@echo "$(COQC) $(COQINCLUDE) $<"
+
+endif
+
+_CoqProject: .FORCE
+	@echo $(COQINCLUDE) > $@
+
+.FORCE:
+
+############################################################################
+# Dependencies
+
+ifeq ($(findstring $(MAKECMDGOALS),depend clean),)
+-include $(VD)
+endif
+
+############################################################################
+# IDE
+
+.PHONY: ide
+
+.coqide:
+	@echo '$(COQIDE) $(COQINCLUDE) $$*' > .coqide
+	@chmod +x .coqide
+
+ide: _CoqProject
+	$(COQIDE) $(COQINCLUDE)
+
+############################################################################
+# Clean
+
+.PHONY: clean
+
+# In a multi-directory setting, it is not entirely clear how to find the
+# files that we wish to remove.
+
+# One approach would be to view $(V) as the authoritative list of source files
+# and remove just the derived files $(VO), etc.
+
+# Another approach is to scan all subdirectories of $(ROOTDIR) and remove all
+# object files in them. We follow this approach.
+
+# Be careful to use regular expressions that work both with GNU find
+# and with BSD find (MacOS).
+
+clean::
+	for d in `find $(ROOTDIR) -type d -not -regex ".*\\.git.*"` ; do \
+	  (cd $$d && \
+	     rm -f *~ && \
+	     rm -f .*.aux && \
+	     rm -f *.{vo,vio,vq,v.d,aux,glob,cache,crashcoqide} && \
+	     rm -rf *.coq-native *.coqide && \
+	     true) ; \
+	done

coq-menhirlib/src/Validator_classes.v

+(****************************************************************************)
+(*                                                                          *)
+(*                                   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.
+From Coq.ssr Require Import ssreflect.
+Require Import Alphabet.
+
+Class IsValidator (P : Prop) (b : bool) :=
+  is_validator : b = true -> P.
+Hint Mode IsValidator + -.
+
+Instance is_validator_true : IsValidator True true.
+Proof. done. Qed.
+
+Instance is_validator_false : IsValidator False false.
+Proof. done. Qed.
+
+Instance is_validator_eq_true b :
+  IsValidator (b = true) b.
+Proof. done. Qed.
+
+Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
+  IsValidator (P1 /\ P2) (if b1 then b2 else false).
+Proof. split; destruct b1, b2; auto using is_validator. Qed.
+
+Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
+  ComparableLeibnizEq C ->
+  IsValidator (x = y) (compare_eqb x y).
+Proof. intros ??. by apply compare_eqb_iff. Qed.
+
+Instance is_validator_comparable_eq_impl A `(Comparable A) (x y : A) P b :
+  IsValidator P b ->
+  IsValidator (x = y -> P) (if compare_eqb x y then b else true).
+Proof.
+  intros Hval Val ->. rewrite /compare_eqb compare_refl in Val. auto.
+Qed.
+
+Lemma is_validator_forall_finite A P b `(Finite A) :
+  (forall (x : A), IsValidator (P x) (b x)) ->
+  IsValidator (forall (x : A), P x) (forallb b all_list).
+Proof.
+  move=> ? /forallb_forall.
+  auto using all_list_forall, is_validator, forallb_forall.
+Qed.
+(* We do not use an instance directly here, because we need somehow to
+   force Coq to instantiate b with a lambda. *)
+Hint Extern 2 (IsValidator (forall x : ?A, _) _) =>
+    eapply (is_validator_forall_finite _ _ (fun (x:A) => _))
+  : typeclass_instances.
+
+(* Hint for synthetizing pattern-matching. *)
+Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) =>
+    let b := fresh "b" in
+    unshelve notypeclasses refine (let b : bool := _ in _);
+      [destruct u; intros; shelve|];    (* Synthetize `match .. with` in the validator. *)
+    unify b b0;
+    unfold b; destruct u; clear b
+  : typeclass_instances.
+
+(* Hint for unfolding definitions. This is necessary because many
+  hints for IsValidator use [Hint Extern], which do not automatically
+  unfold identifiers. *)
+Hint Extern 100 (IsValidator ?X _) => unfold X
+  : typeclass_instances.