From 9fee613ca2cfd6f87cec62c1fd1c208701de086d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 21 Feb 2024 17:37:55 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590 --- src/Common.v | 6 +++-- src/Common/Frame.v | 24 ++++++++++++------- src/Common/Gensym.v | 6 +++-- src/Common/Monad.v | 6 +++-- .../ContextFreeGrammar/Fix/Definitions.v | 2 +- src/Parsers/ContextFreeGrammar/Fold.v | 3 ++- src/Parsers/CorrectnessBaseTypes.v | 9 ++++--- src/Parsers/StringLike/Core.v | 17 ++++++++----- 8 files changed, 48 insertions(+), 25 deletions(-) diff --git a/src/Common.v b/src/Common.v index e3ea01bfa..758fac871 100644 --- a/src/Common.v +++ b/src/Common.v @@ -479,8 +479,10 @@ Class ReflexiveT A (R : A -> A -> Type) := Class TransitiveT A (R : A -> A -> Type) := transitivityT : forall x y z, R x y -> R y z -> R x z. Class PreOrderT A (R : A -> A -> Type) := - { PreOrderT_ReflexiveT :> ReflexiveT R; - PreOrderT_TransitiveT :> TransitiveT R }. + { PreOrderT_ReflexiveT : ReflexiveT R; + PreOrderT_TransitiveT : TransitiveT R }. +#[global] Existing Instance PreOrderT_ReflexiveT. +#[global] Existing Instance PreOrderT_TransitiveT. Definition respectful_heteroT A B C D (R : A -> B -> Type) (R' : forall (x : A) (y : B), C x -> D y -> Type) diff --git a/src/Common/Frame.v b/src/Common/Frame.v index 65681af97..565e216c1 100644 --- a/src/Common/Frame.v +++ b/src/Common/Frame.v @@ -283,10 +283,11 @@ Arguments PreO.max {A} {le} _ _ _. such that [eq x y] exactly when both [le x y] and [le y x]. *) Module PO. Class t {A : Type} {le : A -> A -> Prop} {eq : A -> A -> Prop} : Prop := - { PreO :> PreO.t le + { PreO : PreO.t le ; le_proper : Proper (eq ==> eq ==> iff) le ; le_antisym : forall x y, le x y -> le y x -> eq x y }. + #[global] Existing Instance PreO. Arguments t {A} le eq. @@ -494,10 +495,11 @@ Module JoinLat. a join semi-lattice? We need [le] and [eq] to be a partial order, and we need our [max] operation to actually implement a maximum. *) Class t {A : Type} {O : Ops A} : Prop := - { PO :> PO.t le eq + { PO : PO.t le eq ; max_proper : Proper (eq ==> eq ==> eq) max ; max_ok : forall l r, PreO.max (le := le) l r (max l r) }. + #[global] Existing Instance PO. Arguments t : clear implicits. @@ -670,10 +672,11 @@ Module MeetLat. Arguments Ops : clear implicits. Class t {A : Type} {O : Ops A} : Prop := - { PO :> PO.t le eq + { PO : PO.t le eq ; min_proper : Proper (eq ==> eq ==> eq) min ; min_ok : forall l r, PreO.min (le := le) l r (min l r) }. + #[global] Existing Instance PO. Arguments t : clear implicits. @@ -866,12 +869,13 @@ Module Lattice. Arguments Ops : clear implicits. Class t {A : Type} {O : Ops A} : Prop := - { PO :> PO.t le eq + { PO : PO.t le eq ; max_proper : Proper (eq ==> eq ==> eq) max ; max_ok : forall l r, PreO.max (le := le) l r (max l r) ; min_proper : Proper (eq ==> eq ==> eq) min ; min_ok : forall l r, PreO.min (le := le) l r (min l r) }. + #[global] Existing Instance PO. Arguments t : clear implicits. @@ -1257,20 +1261,22 @@ End CompleteLattice. *) Module Frame. Class Ops {A} := - { LOps :> L.Ops A + { LOps : L.Ops A ; sup : forall {Ix : Type}, (Ix -> A) -> A }. + #[global] Existing Instance LOps. Arguments Ops : clear implicits. Class t {A} {OA : Ops A}: Type := - { L :> L.t A LOps + { L : L.t A LOps ; sup_proper : forall {Ix : Type}, Proper (pointwise_relation _ L.eq ==> L.eq) (@sup _ _ Ix) ; sup_ok : forall {Ix : Type} (f : Ix -> A), PreO.sup (le := L.le) f (sup f) ; sup_distr : forall x {Ix : Type} (f : Ix -> A) , L.eq (L.min x (sup f)) (sup (fun i => L.min x (f i))) }. + #[global] Existing Instance L. Arguments t : clear implicits. Section Facts. @@ -1489,12 +1495,14 @@ Module CommIdemSG. (** [dot] is a binary operation which is commutative, idempotent, and associative. It is effectively a max or min. *) Class t {A} {eq : A -> A -> Prop} {dot : A -> A -> A} := - { eq_equiv :> Equivalence eq - ; dot_proper :> Proper (eq ==> eq ==> eq) dot + { eq_equiv : Equivalence eq + ; dot_proper : Proper (eq ==> eq ==> eq) dot ; dot_idempotent : forall a, eq (dot a a) a ; dot_comm : forall a b, eq (dot a b) (dot b a) ; dot_assoc : forall a b c, eq (dot a (dot b c)) (dot (dot a b) c) }. + #[global] Existing Instance eq_equiv. + #[global] Existing Instance dot_proper. Arguments t : clear implicits. diff --git a/src/Common/Gensym.v b/src/Common/Gensym.v index d29755afb..1eaeb18dd 100644 --- a/src/Common/Gensym.v +++ b/src/Common/Gensym.v @@ -11,10 +11,12 @@ Class PreGensym A := { s_gt : A -> A -> Prop; sym_init : A; combine_symbols : A -> A -> A; - s_gt_Asymmetric :> Asymmetric s_gt; - s_gt_Transitive :> Transitive s_gt; + s_gt_Asymmetric : Asymmetric s_gt; + s_gt_Transitive : Transitive s_gt; combine_respectful_l : forall x y, s_gt (combine_symbols x y) x; combine_respectful_r : forall x y, s_gt (combine_symbols x y) y }. + #[global] Existing Instance s_gt_Asymmetric. + #[global] Existing Instance s_gt_Transitive. Delimit Scope gensym_scope with gensym. Infix ">" := s_gt : gensym_scope. diff --git a/src/Common/Monad.v b/src/Common/Monad.v index 0b1c29525..1f0c575b6 100644 --- a/src/Common/Monad.v +++ b/src/Common/Monad.v @@ -26,14 +26,16 @@ Class MonadLaws M `{MonadOps M} Arguments MonadLaws M {_}. Class MonadTransformerOps (T : (Type -> Type) -> (Type -> Type)) - := { Tops :> forall M `{MonadOps M}, MonadOps (T M); + := { Tops : forall M `{MonadOps M}, MonadOps (T M); lift : forall {M} `{MonadOps M} {A}, M A -> T M A }. +#[global] Existing Instance Tops. Class MonadTransformerLaws T `{MonadTransformerOps T} - := { Tlaws :> forall {M} `{MonadLaws M}, MonadLaws (T M); + := { Tlaws : forall {M} `{MonadLaws M}, MonadLaws (T M); lift_ret : forall {M} `{MonadLaws M} {A} (x : A), lift (ret x) = ret x; lift_bind : forall {M} `{MonadLaws M} {A B} (f : A -> M B) x, lift (bind x f) = bind (lift x) (fun u => lift (f u)) }. +#[global] Existing Instance Tlaws. Arguments MonadTransformerLaws T {_}. Create HintDb monad discriminated. diff --git a/src/Parsers/ContextFreeGrammar/Fix/Definitions.v b/src/Parsers/ContextFreeGrammar/Fix/Definitions.v index ee64a2684..eef0c1f71 100644 --- a/src/Parsers/ContextFreeGrammar/Fix/Definitions.v +++ b/src/Parsers/ContextFreeGrammar/Fix/Definitions.v @@ -156,7 +156,7 @@ Proof. Qed. Class grammar_fixedpoint_lattice_data prestate := - { state :> _ := lattice_for prestate; + { state : _ := lattice_for prestate; prestate_lt : prestate -> prestate -> bool; state_lt : state -> state -> bool := lattice_for_lt prestate_lt; diff --git a/src/Parsers/ContextFreeGrammar/Fold.v b/src/Parsers/ContextFreeGrammar/Fold.v index 7c7c6a65c..1d9824dfe 100644 --- a/src/Parsers/ContextFreeGrammar/Fold.v +++ b/src/Parsers/ContextFreeGrammar/Fold.v @@ -168,7 +168,7 @@ Section fold_correctness. Ppat : nonterminals_listT -> production Char -> T -> Type; Ppats : nonterminals_listT -> productions Char -> T -> Type }. Class fold_grammar_correctness_data := - { fgccd :> fold_grammar_correctness_computational_data; + { fgccd : fold_grammar_correctness_computational_data; Pnt_lift : forall valid0 nt value, sub_nonterminals_listT valid0 initial_nonterminals_data -> is_valid_nonterminal valid0 (of_nonterminal nt) @@ -198,6 +198,7 @@ Section fold_correctness. -> Ppat valid0 x p -> Ppats valid0 xs ps -> Ppats valid0 (x::xs) (combine_productions p ps) }. + #[global] Existing Instance fgccd. Context {FGCD : fold_grammar_correctness_data}. Lemma fold_production'_correct diff --git a/src/Parsers/CorrectnessBaseTypes.v b/src/Parsers/CorrectnessBaseTypes.v index ad93a8351..a0054cebb 100644 --- a/src/Parsers/CorrectnessBaseTypes.v +++ b/src/Parsers/CorrectnessBaseTypes.v @@ -46,7 +46,10 @@ Section general. : split_list_completeT split_string_for_production }. Class boolean_parser_correctness_dataT := - { data :> boolean_parser_dataT; - rdata' :> @parser_removal_dataT' _ G _; - cdata' :> boolean_parser_completeness_dataT' }. + { data : boolean_parser_dataT; + rdata' : @parser_removal_dataT' _ G _; + cdata' : boolean_parser_completeness_dataT' }. + #[global] Existing Instance data. + #[global] Existing Instance rdata'. + #[global] Existing Instance cdata'. End general. diff --git a/src/Parsers/StringLike/Core.v b/src/Parsers/StringLike/Core.v index 676b526ed..f3fc319f8 100644 --- a/src/Parsers/StringLike/Core.v +++ b/src/Parsers/StringLike/Core.v @@ -20,7 +20,7 @@ Reserved Notation "[ x ]". Module Export StringLike. Class StringLikeMin {Char : Type} := { - String :> Type; + String : Type; char_at_matches : nat -> String -> (Char -> bool) -> bool; unsafe_get : nat -> String -> Char; length : String -> nat @@ -114,11 +114,11 @@ Module Export StringLike. unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch; length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; - is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; - length_Proper :> Proper (beq ==> eq) length; - take_Proper :> Proper (eq ==> beq ==> beq) take; - drop_Proper :> Proper (eq ==> beq ==> beq) drop; - bool_eq_Equivalence :> Equivalence beq; + is_char_Proper : Proper (beq ==> eq ==> eq) is_char; + length_Proper : Proper (beq ==> eq) length; + take_Proper : Proper (eq ==> beq ==> beq) take; + drop_Proper : Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence : Equivalence beq; bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; take_short_length : forall str n, n <= length str -> length (take n str) = n; take_long : forall str n, length str <= n -> take n str =s str; @@ -131,6 +131,11 @@ Module Export StringLike. bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str'; strings_nontrivial : forall n, exists str, length str = n }. + #[global] Existing Instance is_char_Proper. + #[global] Existing Instance length_Proper. + #[global] Existing Instance take_Proper. + #[global] Existing Instance drop_Proper. + #[global] Existing Instance bool_eq_Equivalence. Class StringIsoProperties {Char} {HSLM} {HSL : @StringLike Char HSLM} {HSI : @StringIso Char HSLM} := {