Commit 626a2258 authored by Robbert Krebbers's avatar Robbert Krebbers

Hint Mode for Persistent, Timeless, Exclusive, ...

parent 7c61518e
Pipeline #3751 passed with stage
in 4 minutes and 25 seconds
...@@ -130,10 +130,12 @@ Infix "⋅?" := opM (at level 50, left associativity) : C_scope. ...@@ -130,10 +130,12 @@ Infix "⋅?" := opM (at level 50, left associativity) : C_scope.
(** * Persistent elements *) (** * Persistent elements *)
Class Persistent {A : cmraT} (x : A) := persistent : pcore x Some x. Class Persistent {A : cmraT} (x : A) := persistent : pcore x Some x.
Arguments persistent {_} _ {_}. Arguments persistent {_} _ {_}.
Hint Mode Persistent + ! : typeclass_instances.
(** * Exclusive elements (i.e., elements that cannot have a frame). *) (** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False. Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : {0} (x y) False.
Arguments exclusive0_l {_} _ {_} _ _. Arguments exclusive0_l {_} _ {_} _ _.
Hint Mode Exclusive + ! : typeclass_instances.
(** * CMRAs whose core is total *) (** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total (** The function [core] may return a dummy when used on CMRAs without total
...@@ -545,7 +547,7 @@ Section ucmra. ...@@ -545,7 +547,7 @@ Section ucmra.
Global Instance cmra_unit_total : CMRATotal A. Global Instance cmra_unit_total : CMRATotal A.
Proof. Proof.
intros x. destruct (cmra_pcore_mono' x ) as (cx&->&?); intros x. destruct (cmra_pcore_mono' x ) as (cx&->&?);
eauto using ucmra_unit_least, (persistent ). eauto using ucmra_unit_least, (persistent (:A)).
Qed. Qed.
End ucmra. End ucmra.
Hint Immediate cmra_unit_total. Hint Immediate cmra_unit_total.
......
...@@ -72,8 +72,10 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption. ...@@ -72,8 +72,10 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
(** Discrete OFEs and Timeless elements *) (** Discrete OFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes (* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *) more sense. *)
Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x {0} y x y. Class Timeless {A : ofeT} (x : A) := timeless y : x {0} y x y.
Arguments timeless {_ _ _} _ {_} _ _. Arguments timeless {_} _ {_} _ _.
Hint Mode Timeless + ! : typeclass_instances.
Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x. Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
(** OFEs with a completion *) (** OFEs with a completion *)
...@@ -1029,12 +1031,13 @@ Section sigma. ...@@ -1029,12 +1031,13 @@ Section sigma.
Global Instance sig_timeless (x : sig P) : Global Instance sig_timeless (x : sig P) :
Timeless (proj1_sig x) Timeless x. Timeless (proj1_sig x) Timeless x.
Proof. intros ? y. destruct x, y. unfold dist, sig_dist, equiv, sig_equiv. apply (timeless _). Qed.
Global Instance sig_discrete_cofe : Discrete A Discrete sigC.
Proof. Proof.
intros ? [??] [??]. rewrite /dist /equiv /ofe_dist /ofe_equiv /=. intros ? [b ?]; destruct x as [a ?].
rewrite /sig_dist /sig_equiv /=. apply discrete_timeless. rewrite /dist /ofe_dist /= /sig_dist /equiv /ofe_equiv /= /sig_equiv /=.
Qed. apply (timeless _).
Qed.
Global Instance sig_discrete_cofe : Discrete A Discrete sigC.
Proof. intros ??. apply _. Qed.
End sigma. End sigma.
Arguments sigC {_} _. Arguments sigC {_} _.
...@@ -115,10 +115,12 @@ Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P)) ...@@ -115,10 +115,12 @@ Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
Class PersistentL {M} (Ps : list (uPred M)) := Class PersistentL {M} (Ps : list (uPred M)) :=
persistentL : Forall PersistentP Ps. persistentL : Forall PersistentP Ps.
Arguments persistentL {_} _ {_}. Arguments persistentL {_} _ {_}.
Hint Mode PersistentL + ! : typeclass_instances.
Class TimelessL {M} (Ps : list (uPred M)) := Class TimelessL {M} (Ps : list (uPred M)) :=
timelessL : Forall TimelessP Ps. timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}. Arguments timelessL {_} _ {_}.
Hint Mode TimelessP + ! : typeclass_instances.
(** * Properties *) (** * Properties *)
Section big_op. Section big_op.
......
...@@ -31,10 +31,12 @@ Typeclasses Opaque uPred_except_0. ...@@ -31,10 +31,12 @@ Typeclasses Opaque uPred_except_0.
Class TimelessP {M} (P : uPred M) := timelessP : P P. Class TimelessP {M} (P : uPred M) := timelessP : P P.
Arguments timelessP {_} _ {_}. Arguments timelessP {_} _ {_}.
Hint Mode TimelessP + ! : typeclass_instances.
Class PersistentP {M} (P : uPred M) := persistentP : P P. Class PersistentP {M} (P : uPred M) := persistentP : P P.
Hint Mode PersistentP - ! : typeclass_instances. Hint Mode PersistentP - ! : typeclass_instances.
Arguments persistentP {_} _ {_}. Arguments persistentP {_} _ {_}.
Hint Mode PersistentP + ! : typeclass_instances.
Module uPred. Module uPred.
Section derived. Section derived.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment