From e241324ac66ef145486c97bea1f8cf99c575ec2d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 21 Jan 2016 22:33:23 +0100 Subject: [PATCH] consistent naming for the CMRAs making up Iris resources: iGst, iPst, iWld --- iris/model.v | 8 +++++++- iris/ownership.v | 4 ++-- iris/pviewshifts.v | 4 ++-- iris/viewshifts.v | 4 ++-- iris/wsat.v | 2 +- 5 files changed, 14 insertions(+), 8 deletions(-) diff --git a/iris/model.v b/iris/model.v index 77dbb5612..61b2f1566 100644 --- a/iris/model.v +++ b/iris/model.v @@ -24,7 +24,9 @@ End iProp. Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ. Notation iRes Σ := (res Σ (laterC (iPreProp Σ))). Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))). -Notation iCMRA Σ := (icmra Σ (laterC (iPreProp Σ))). +Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))). +Notation iPst Σ := (exclRA (istateC Σ)). +Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))). Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ). Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _. Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _. @@ -38,3 +40,7 @@ Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ). Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed. Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ). Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed. + +Module Test. (* Make sure we got the notations right. *) + Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g. +End Test. diff --git a/iris/ownership.v b/iris/ownership.v index 48103aebc..68f99ad9e 100644 --- a/iris/ownership.v +++ b/iris/ownership.v @@ -4,7 +4,7 @@ Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ := uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅). Arguments inv {_} _ _%I. Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅). -Definition ownG {Σ} (m : iCMRA Σ) : iProp Σ := uPred_own (Res ∅ ∅ m). +Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res ∅ ∅ m). Instance: Params (@inv) 2. Instance: Params (@ownP) 1. Instance: Params (@ownG) 1. @@ -16,7 +16,7 @@ Context {Σ : iParam}. Implicit Types r : iRes Σ. Implicit Types σ : istate Σ. Implicit Types P : iProp Σ. -Implicit Types m : iCMRA Σ. +Implicit Types m : iGst Σ. (* Invariants *) Global Instance inv_contractive i : Contractive (@inv Σ i). diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v index 3ce4f29fe..81ee2f4ee 100644 --- a/iris/pviewshifts.v +++ b/iris/pviewshifts.v @@ -29,7 +29,7 @@ Instance: Params (@pvs) 3. Section pvs. Context {Σ : iParam}. Implicit Types P Q : iProp Σ. -Implicit Types m : iCMRA Σ. +Implicit Types m : iGst Σ. Transparent uPred_holds. Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2). @@ -96,7 +96,7 @@ Proof. * by rewrite -(left_id_L ∅ (∪) Ef). * apply uPred_weaken with r n; auto. Qed. -Lemma pvs_updateP E m (P : iCMRA Σ → Prop) : +Lemma pvs_updateP E m (P : iGst Σ → Prop) : m ⇝: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m'). Proof. intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia. diff --git a/iris/viewshifts.v b/iris/viewshifts.v index 4c3da218a..a090f5f85 100644 --- a/iris/viewshifts.v +++ b/iris/viewshifts.v @@ -16,7 +16,7 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I) Section vs. Context {Σ : iParam}. Implicit Types P Q : iProp Σ. -Implicit Types m : iCMRA Σ. +Implicit Types m : iGst Σ. Import uPred. Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q. @@ -85,7 +85,7 @@ Proof. intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of. apply vs_close. Qed. -Lemma vs_updateP E m (P : iCMRA Σ → Prop) : +Lemma vs_updateP E m (P : iGst Σ → Prop) : m ⇝: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m'). Proof. by intros; apply vs_alt, pvs_updateP. Qed. Lemma vs_update E m m' : m ⇝ m' → ownG m >{E}> ownG m'. diff --git a/iris/wsat.v b/iris/wsat.v index 3f197c2d7..a9afb6fac 100644 --- a/iris/wsat.v +++ b/iris/wsat.v @@ -120,7 +120,7 @@ Proof. split; [done|exists rs]. by constructor; split_ands'; try (rewrite /= -(associative _) Hpst'). Qed. -Lemma wsat_update_gst n E σ r rf m1 (P : iCMRA Σ → Prop) : +Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) : m1 ≼{S n} gst r → m1 ⇝: P → wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2. Proof. -- GitLab