From 990c96e18ca31781484f558d46c94537b5ec59cf Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sun, 3 Oct 2021 18:42:50 +0200 Subject: Synchronize vendored MenhirLib with upstream (#416) It remains compatible with earlier Menhir versions. --- MenhirLib/Alphabet.v | 14 +++++++------- MenhirLib/Automaton.v | 6 +++--- MenhirLib/Grammar.v | 8 ++++---- MenhirLib/Interpreter.v | 25 ++++++++++++++++++------- MenhirLib/Validator_classes.v | 12 ++++++------ MenhirLib/Validator_complete.v | 12 ++++++------ MenhirLib/Validator_safe.v | 6 +++--- 7 files changed, 47 insertions(+), 36 deletions(-) (limited to 'MenhirLib') 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). -- cgit