Synchronize vendored MenhirLib with upstream (#416)

It remains compatible with earlier Menhir versions.

7 files changed, 47 insertions, 36 deletions

diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v
index cd849761..8381c014 100644
--- a/MenhirLib/Alphabet.v
+++ b/MenhirLib/Alphabet.v
@@ -37,7 +37,7 @@ Qed.
 Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
   fun x y => compare x y = Lt.
 
-Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+Global Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
   StrictOrder (comparableLt C).
 Proof.
 apply Build_StrictOrder.
@@ -53,7 +53,7 @@ apply compare_trans.
 Qed.
 
 (** nat is comparable. **)
-Program Instance natComparable : Comparable nat :=
+Global Program Instance natComparable : Comparable nat :=
   { compare := Nat.compare }.
 Next Obligation.
 symmetry.
@@ -79,7 +79,7 @@ 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) :
+Global 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
@@ -134,10 +134,10 @@ destruct H.
 rewrite compare_refl; intuition.
 Qed.
 
-Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
+Global Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq.
 
 (** A pair of ComparableLeibnizEq is ComparableLeibnizEq **)
-Instance PairComparableLeibnizEq
+Global Instance PairComparableLeibnizEq
   {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA)
   {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) :
     ComparableLeibnizEq (PairComparable CA CB).
@@ -174,7 +174,7 @@ Class Numbered (A:Type) := {
   inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
 }.
 
-Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+Global 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
@@ -224,7 +224,7 @@ Import OrderedType.
 
 Module Type ComparableM.
   Parameter t : Type.
-  Declare Instance tComparable : Comparable t.
+  Global Declare Instance tComparable : Comparable t.
 End ComparableM.
 
 Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.
diff --git a/MenhirLib/Automaton.v b/MenhirLib/Automaton.v
index d5a19f35..1975be4f 100644
--- a/MenhirLib/Automaton.v
+++ b/MenhirLib/Automaton.v
@@ -23,10 +23,10 @@ Module Type AutInit.
 
   (** The set of non initial state is considered as an alphabet. **)
   Parameter noninitstate : Type.
-  Declare Instance NonInitStateAlph : Alphabet noninitstate.
+  Global Declare Instance NonInitStateAlph : Alphabet noninitstate.
 
   Parameter initstate : Type.
-  Declare Instance InitStateAlph : Alphabet initstate.
+  Global Declare Instance InitStateAlph : Alphabet initstate.
 
   (** When we are at this state, we know that this symbol is the top of the
      stack. **)
@@ -41,7 +41,7 @@ Module Types(Import Init:AutInit).
     | Init: initstate -> state
     | Ninit: noninitstate -> state.
 
-  Program Instance StateAlph : Alphabet state :=
+  Global Program Instance StateAlph : Alphabet state :=
     { AlphabetComparable := {| compare := fun x y =>
         match x, y return comparison with
           | Init _, Ninit _ => Lt
diff --git a/MenhirLib/Grammar.v b/MenhirLib/Grammar.v
index 9be374e8..35ccbd8b 100644
--- a/MenhirLib/Grammar.v
+++ b/MenhirLib/Grammar.v
@@ -18,8 +18,8 @@ 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.
+  Global Declare Instance TerminalAlph: Alphabet terminal.
+  Global Declare Instance NonTerminalAlph: Alphabet nonterminal.
 End Alphs.
 
 (** Definition of the alphabet of symbols, given the alphabet of terminals
@@ -30,7 +30,7 @@ Module Symbol(Import A:Alphs).
     | T: terminal -> symbol
     | NT: nonterminal -> symbol.
 
-  Program Instance SymbolAlph : Alphabet symbol :=
+  Global Program Instance SymbolAlph : Alphabet symbol :=
     { AlphabetComparable := {| compare := fun x y =>
         match x, y return comparison with
           | T _, NT _ => Gt
@@ -74,7 +74,7 @@ Module Type T.
 
   (** The type of productions identifiers **)
   Parameter production : Type.
-  Declare Instance ProductionAlph : Alphabet production.
+  Global 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
diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v
index 07aeae5a..158bba9f 100644
--- a/MenhirLib/Interpreter.v
+++ b/MenhirLib/Interpreter.v
@@ -27,7 +27,7 @@ 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) :
+Global Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) :
   Decidable (x = y).
 Proof.
   unfold Decidable.
@@ -35,7 +35,7 @@ Proof.
     right; intros ->; by rewrite compare_refl in EQ.
 Defined.
 
-Instance list_decidable_eq T :
+Global 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.
@@ -83,6 +83,9 @@ Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed.
 CoInductive buffer : Type :=
   Buf_cons { buf_head : token; buf_tail : buffer }.
 
+(* Note: Coq 8.12.0 wants a Declare Scope command,
+   but this breaks compatibility with Coq < 8.10.
+   Declare Scope buffer_scope. *)
 Delimit Scope buffer_scope with buf.
 Bind Scope buffer_scope with buffer.
 
@@ -274,10 +277,11 @@ Qed.
     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
+  | Fail_sr_full: state -> token -> 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
@@ -367,7 +371,7 @@ Definition step stk buffer (Hi : thunkP (stack_invariant stk)): step_result :=
       | Reduce_act prod => fun Hv =>
         reduce_step stk prod buffer Hv Hi
       | Fail_act => fun _ =>
-        Fail_sr
+        Fail_sr_full (state_of_stack stk) tok
       end (fun _ => Hv I (token_term tok))
     end
   end (fun _ => reduce_ok _).
@@ -425,7 +429,7 @@ Fixpoint parse_fix stk buffer (log_n_steps : nat) (Hi : thunkP (stack_invariant
     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
+  | Fail_pr_full: state -> token -> parse_result
   | Timeout_pr: parse_result
   | Parsed_pr: A -> buffer -> parse_result.
 Global Arguments parse_result _ : clear implicits.
@@ -433,7 +437,7 @@ 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
+        | Fail_sr_full st tok => Fail_pr_full st tok
         | Accept_sr sem buffer' => Parsed_pr sem buffer'
         | Progress_sr _ _ => Timeout_pr
         end).
@@ -443,10 +447,17 @@ Defined.
 
 End Interpreter.
 
-Arguments Fail_sr {init}.
+Arguments Fail_sr_full {init} _ _.
 Arguments Accept_sr {init} _ _.
 Arguments Progress_sr {init} _ _.
 
+(* These notations are provided for backwards compatibility with Coq code
+ * from before the addition of the return information. They are used in the 
+ * theorem statements. 
+ *)
+Notation Fail_sr := (Fail_sr_full _ _) (only parsing).
+Notation Fail_pr := (Fail_pr_full _ _) (only parsing).
+
 End Make.
 
 Module Type T(A:Automaton.T).
diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v
index 781a6aa6..cced28ac 100644
--- a/MenhirLib/Validator_classes.v
+++ b/MenhirLib/Validator_classes.v
@@ -19,26 +19,26 @@ Class IsValidator (P : Prop) (b : bool) :=
   is_validator : b = true -> P.
 Global Hint Mode IsValidator + - : typeclass_instances.
 
-Instance is_validator_true : IsValidator True true.
+Global Instance is_validator_true : IsValidator True true.
 Proof. done. Qed.
 
-Instance is_validator_false : IsValidator False false.
+Global Instance is_validator_false : IsValidator False false.
 Proof. done. Qed.
 
-Instance is_validator_eq_true b :
+Global 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}:
+Global Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}:
   IsValidator (P1 /\ P2) (if b1 then b2 else false).
 Proof. by split; destruct b1, b2; apply is_validator. Qed.
 
-Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) :
+Global 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 :
+Global 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.
diff --git a/MenhirLib/Validator_complete.v b/MenhirLib/Validator_complete.v
index ac4dd0c4..4b4d127a 100644
--- a/MenhirLib/Validator_complete.v
+++ b/MenhirLib/Validator_complete.v
@@ -22,12 +22,12 @@ Module Make(Import A:Automaton.T).
 (** We instantiate some sets/map. **)
 Module TerminalComparableM <: ComparableM.
   Definition t := terminal.
-  Instance tComparable : Comparable t := _.
+  Global Instance tComparable : Comparable t := _.
 End TerminalComparableM.
 Module TerminalOrderedType := OrderedType_from_ComparableM TerminalComparableM.
 Module StateProdPosComparableM <: ComparableM.
   Definition t := (state*production*nat)%type.
-  Instance tComparable : Comparable t := _.
+  Global Instance tComparable : Comparable t := _.
 End StateProdPosComparableM.
 Module StateProdPosOrderedType :=
   OrderedType_from_ComparableM StateProdPosComparableM.
@@ -117,7 +117,7 @@ Definition forallb_items items_map (P:state -> production -> nat -> TerminalSet.
 
 (** Typeclass instances for synthetizing the validator. *)
 
-Instance is_validator_subset S1 S2 :
+Global Instance is_validator_subset S1 S2 :
   IsValidator (TerminalSet.Subset S1 S2) (TerminalSet.subset S1 S2).
 Proof. intros ?. by apply TerminalSet.subset_2. Qed.
 
@@ -150,7 +150,7 @@ Global Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) =>
   validator.
 
   This instance is used for [non_terminal_closed]. *)
-Instance is_validator_forall_lookahead_set lset P b:
+Global Instance is_validator_forall_lookahead_set lset P b:
   (forall lookahead, TerminalSet.In lookahead lset -> IsValidator (P lookahead) b) ->
   IsValidator (forall lookahead, TerminalSet.In lookahead lset -> P lookahead) b.
 Proof. unfold IsValidator. firstorder. Qed.
@@ -237,7 +237,7 @@ Proof.
     eapply Hval2 with (pos := pos); eauto; [].
     revert EQ. unfold future_of_prod=>-> //.
 Qed.
-(* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *)
+(* We need a hint to explicitly instantiate b1 and b2 with lambdas. *)
 Global Hint Extern 0 (IsValidator
                  (forall st prod fut lookahead,
                      state_has_future st prod fut lookahead -> _)
@@ -247,7 +247,7 @@ Global Hint Extern 0 (IsValidator
   : typeclass_instances.
 
 (* Used in [start_future] only. *)
-Instance is_validator_forall_state_has_future im st prod :
+Global Instance is_validator_forall_state_has_future im st prod :
   IsItemsMap im ->
   IsValidator
     (forall look, state_has_future st prod (rev' (prod_rhs_rev prod)) look)
diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v
index e7a54b47..0f32ea50 100644
--- a/MenhirLib/Validator_safe.v
+++ b/MenhirLib/Validator_safe.v
@@ -62,7 +62,7 @@ Fixpoint is_prefix (l1 l2:list symbol) :=
   | _::_, [] => false
   end.
 
-Instance prefix_is_validator l1 l2 : IsValidator (prefix l1 l2) (is_prefix l1 l2).
+Global 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.
@@ -127,7 +127,7 @@ Fixpoint is_prefix_pred (l1 l2:list (state->bool)) :=
   | _::_, [] => false
   end.
 
-Instance prefix_pred_is_validator l1 l2 :
+Global 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.
@@ -180,7 +180,7 @@ Fixpoint is_state_valid_after_pop (state:state) (to_pop:list symbol) annot :=
   | 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 :
+Global 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).