Commit e241324a authored by Ralf Jung's avatar Ralf Jung

consistent naming for the CMRAs making up Iris resources: iGst, iPst, iWld

parent d543c264
......@@ -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.
......@@ -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).
......
......@@ -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.
......
......@@ -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'.
......
......@@ -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.
......
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