Unverified Commit 9c0037c6 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Make `inG` instances local

parent 96883dbd
......@@ -6,9 +6,10 @@ Import uPred.
(** The CMRAs we need. *)
Class boxG Σ :=
boxG_inG :> inG Σ (prodR
boxG_inG : inG Σ (prodR
(excl_authR boolO)
(optionR (agreeR (laterO (iPropO Σ))))).
Local Existing Instance boxG_inG.
Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
optionRF (agreeRF ( )) ) ].
......
......@@ -5,8 +5,9 @@ From iris.base_logic.lib Require Export invariants.
From iris.prelude Require Import options.
Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR.
Class cinvG Σ := cinv_inG : inG Σ fracR.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
Local Existing Instance cinv_inG.
Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ cinvG Σ.
Proof. solve_inG. Qed.
......
......@@ -68,8 +68,9 @@ these can be matched up with the invariant namespaces. *)
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heapGpreS_heap :> ghost_mapG Σ L V;
gen_heapGpreS_meta :> ghost_mapG Σ L gname;
gen_heapGpreS_meta_data :> inG Σ (reservation_mapR (agreeR positiveO));
gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
}.
Local Existing Instance gen_heapGpreS_meta_data.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
gen_heap_inG :> gen_heapGpreS L V Σ;
......
......@@ -31,8 +31,9 @@ Definition to_inv_heap {L V : Type} `{Countable L}
prod_map (λ x, Excl' x) to_agree <$> h.
Class inv_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
inv_heapGpreS_inG :> inG Σ (authR (inv_heap_mapUR L V))
inv_heapGpreS_inG : inG Σ (authR (inv_heap_mapUR L V))
}.
Local Existing Instance inv_heapGpreS_inG.
Class inv_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
inv_heap_inG :> inv_heapGpreS L V Σ;
......
......@@ -12,8 +12,9 @@ From iris.prelude Require Import options.
FIXME: This is intentionally discrete-only, but
should we support setoids via [Equiv]? *)
Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
ghost_map_inG :> inG Σ (gmap_viewR K (leibnizO V));
ghost_map_inG : inG Σ (gmap_viewR K (leibnizO V));
}.
Local Existing Instance ghost_map_inG.
Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
#[ GFunctor (gmap_viewR K (leibnizO V)) ].
......
......@@ -8,8 +8,9 @@ From iris.prelude Require Import options.
(** The CMRA we need. *)
Class ghost_varG Σ (A : Type) := GhostVarG {
ghost_var_inG :> inG Σ (dfrac_agreeR $ leibnizO A);
ghost_var_inG : inG Σ (dfrac_agreeR $ leibnizO A);
}.
Local Existing Instance ghost_var_inG.
Global Hint Mode ghost_varG - ! : typeclass_instances.
Definition ghost_varΣ (A : Type) : gFunctors :=
......
......@@ -28,8 +28,9 @@ From iris.prelude Require Import options.
(* The uCMRA we need. *)
Class gset_bijG Σ A B `{Countable A, Countable B} :=
GsetBijG { gset_bijG_inG :> inG Σ (gset_bijR A B); }.
GsetBijG { gset_bijG_inG : inG Σ (gset_bijR A B); }.
Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
Local Existing Instance gset_bijG_inG.
Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
#[ GFunctor (gset_bijR A B) ].
......
......@@ -14,7 +14,8 @@ From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options.
Class mono_natG Σ :=
MonoNatG { mono_natG_inG :> inG Σ mono_natR; }.
MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
Local Existing Instance mono_natG_inG.
Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ mono_natG Σ.
Proof. solve_inG. Qed.
......
......@@ -9,7 +9,8 @@ Import uPred.
Definition na_inv_pool_name := gname.
Class na_invG Σ :=
na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
na_inv_inG : inG Σ (prodR coPset_disjR (gset_disjR positive)).
Local Existing Instance na_inv_inG.
Definition na_invΣ : gFunctors :=
#[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
Global Instance subG_na_invG {Σ} : subG na_invΣ Σ na_invG Σ.
......
......@@ -9,9 +9,10 @@ Import uPred.
saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
saved_anything_inG : inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}.
Local Existing Instance saved_anything_inG.
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
#[ GFunctor (agreeRF F) ].
......
......@@ -9,9 +9,9 @@ exception of what's in the [invGS] module. The module [invGS] is thus exported i
[fancy_updates], where [wsat] is only imported. *)
Module invGS.
Class invGpreS (Σ : gFunctors) : Set := InvGpreS {
invGpreS_inv :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
invGpreS_enabled :> inG Σ coPset_disjR;
invGpreS_disabled :> inG Σ (gset_disjR positive);
invGpreS_inv : inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
invGpreS_enabled : inG Σ coPset_disjR;
invGpreS_disabled : inG Σ (gset_disjR positive);
}.
Class invGS (Σ : gFunctors) : Set := InvG {
......
......@@ -16,9 +16,10 @@ union.
Class ownPGS (Λ : language) (Σ : gFunctors) := OwnPGS {
ownP_invG : invGS Σ;
ownP_inG :> inG Σ (excl_authR (stateO Λ));
ownP_inG : inG Σ (excl_authR (stateO Λ));
ownP_name : gname;
}.
Local Existing Instance ownP_inG.
Global Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ := {
iris_invGS := ownP_invG;
......@@ -35,8 +36,9 @@ Definition ownPΣ (Λ : language) : gFunctors :=
Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set := {
ownPPre_invG :> invGpreS Σ;
ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
ownPPre_state_inG : inG Σ (excl_authR (stateO Λ))
}.
Local Existing Instance ownPPre_state_inG.
Global Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ ownPGpreS Λ Σ.
Proof. solve_inG. Qed.
......
......@@ -11,9 +11,10 @@ Import uPred.
(* The CMRA we need. *)
Class authG Σ (A : ucmra) := AuthG {
auth_inG :> inG Σ (authR A);
auth_inG : inG Σ (authR A);
auth_cmra_discrete :> CmraDiscrete A;
}.
Local Existing Instance auth_inG.
Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
Global Instance subG_authΣ Σ A : subG (authΣ A) Σ CmraDiscrete A authG Σ A.
......
......@@ -10,9 +10,10 @@ Import uPred.
(** The CMRA we need. *)
Class stsG Σ (sts : stsT) := StsG {
sts_inG :> inG Σ (sts_resR sts);
sts_inG : inG Σ (sts_resR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
Local Existing Instance sts_inG.
Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (sts_resR sts) ].
Global Instance subG_stsΣ Σ sts :
......
......@@ -13,7 +13,8 @@ Definition incr : val := rec: "incr" "l" :=
Definition read : val := λ: "l", !"l".
(** Monotone counter *)
Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR max_natUR) }.
Class mcounterG Σ := MCounterG { mcounter_inG : inG Σ (authR max_natUR) }.
Local Existing Instance mcounter_inG.
Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ mcounterG Σ.
......@@ -86,7 +87,8 @@ End mono_proof.
(** Counter with contributions *)
Class ccounterG Σ :=
CCounterG { ccounter_inG :> inG Σ (frac_authR natR) }.
CCounterG { ccounter_inG : inG Σ (frac_authR natR) }.
Local Existing Instance ccounter_inG.
Definition ccounterΣ : gFunctors :=
#[GFunctor (frac_authR natR)].
......
......@@ -19,7 +19,8 @@ Definition join : val :=
(** The CMRA & functor we need. *)
(* Not bundling heapGS, as it may be shared with other users. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (exclR unitO) }.
Local Existing Instance spawn_tokG.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
......
......@@ -14,7 +14,8 @@ Definition release : val := λ: "l", "l" <- #false.
(** The CMRA we need. *)
(* Not bundling heapGS, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
Class lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
Local Existing Instance lock_tokG.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
......
......@@ -28,7 +28,8 @@ Definition release : val :=
(** The CMRAs we need. *)
Class tlockG Σ :=
tlock_G :> inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
tlock_G : inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
Local Existing Instance tlock_G.
Definition tlockΣ : gFunctors :=
#[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
......
......@@ -22,7 +22,8 @@ From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options.
Class mono_listG (A : Type) Σ :=
MonoListG { mono_list_inG :> inG Σ (mono_listR (leibnizO A)) }.
MonoListG { mono_list_inG : inG Σ (mono_listR (leibnizO A)) }.
Local Existing Instance mono_list_inG.
Definition mono_listΣ (A : Type) : gFunctors :=
#[GFunctor (mono_listR (leibnizO A))].
......
......@@ -188,7 +188,8 @@ Section M.
Qed.
End M.
Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
Class counterG Σ := CounterG { counter_tokG : inG Σ M_UR }.
Local Existing Instance counter_tokG.
Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
Global Instance subG_counterΣ {Σ} : subG counterΣ Σ counterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
......
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