Commit b0ed7748 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add notation iPrePropG.

parent f69e44a9
...@@ -20,6 +20,7 @@ Definition gname := positive. ...@@ -20,6 +20,7 @@ Definition gname := positive.
Definition globalF (Σ : gFunctors) : iFunctor := Definition globalF (Σ : gFunctors) : iFunctor :=
IFunctor (iprodURF (λ i, gmapURF gname (projT2 Σ i))). IFunctor (iprodURF (λ i, gmapURF gname (projT2 Σ i))).
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)). Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation iPrePropG Λ Σ := (iPreProp Λ (globalF Σ)).
Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG { Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
inG_id : gid Σ; inG_id : gid Σ;
...@@ -114,7 +115,7 @@ their first argument to avoid loops. For example, the instances [authGF_inGF] ...@@ -114,7 +115,7 @@ their first argument to avoid loops. For example, the instances [authGF_inGF]
and [auth_identity] otherwise create a cycle that pops up arbitrarily. *) and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode inGF + + - : typeclass_instances. Hint Mode inGF + + - : typeclass_instances.
Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (iPreProp Λ (globalF Σ))). Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (iPrePropG Λ Σ)).
Proof. exists inGF_id. by rewrite -inGF_prf. Qed. Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
Instance inGF_here {Λ Σ} (F: gFunctor) : inGF Λ (gFunctors.cons F Σ) F. Instance inGF_here {Λ Σ} (F: gFunctor) : inGF Λ (gFunctors.cons F Σ) F.
Proof. by exists 0%fin. Qed. Proof. by exists 0%fin. Qed.
......
...@@ -3,7 +3,7 @@ From iris.program_logic Require Export ghost_ownership. ...@@ -3,7 +3,7 @@ From iris.program_logic Require Export ghost_ownership.
Import uPred. Import uPred.
Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) := Class oneShotG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
one_shot_inG :> inG Λ Σ (one_shotR $ agreeR $ laterC $ F (iPreProp Λ (globalF Σ))). one_shot_inG :> inG Λ Σ (one_shotR $ agreeR $ laterC $ F (iPrePropG Λ Σ)).
Definition oneShotGF (F : cFunctor) : gFunctor := Definition oneShotGF (F : cFunctor) : gFunctor :=
GFunctor (one_shotRF (agreeRF ( F))). GFunctor (one_shotRF (agreeRF ( F))).
Instance inGF_oneShotG `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F. Instance inGF_oneShotG `{inGF Λ Σ (oneShotGF F)} : oneShotG Λ Σ F.
......
...@@ -3,7 +3,7 @@ From iris.program_logic Require Export ghost_ownership. ...@@ -3,7 +3,7 @@ From iris.program_logic Require Export ghost_ownership.
Import uPred. Import uPred.
Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) := Class savedPropG (Λ : language) (Σ : gFunctors) (F : cFunctor) :=
saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPreProp Λ (globalF Σ))))). saved_prop_inG :> inG Λ Σ (agreeR (laterC (F (iPrePropG Λ Σ)))).
Definition savedPropGF (F : cFunctor) : gFunctor := Definition savedPropGF (F : cFunctor) : gFunctor :=
GFunctor (agreeRF ( F)). GFunctor (agreeRF ( F)).
Instance inGF_savedPropG `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F. Instance inGF_savedPropG `{inGF Λ Σ (savedPropGF F)} : savedPropG Λ Σ F.
......
Supports Markdown
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