Commit 0671e00d authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'local-instances' into 'master'

Make inG instances local

See merge request !780
parents 15ff8094 1411b0a9
Pipeline #63619 passed with stage
in 10 minutes and 10 seconds
......@@ -99,9 +99,10 @@ for further details on `libG` classes). For example, the STS library is
parameterized by an STS and assumes that the STS state space is inhabited:
```coq
Class stsG Σ (sts : stsT) := {
sts_inG :> inG Σ (stsR sts);
sts_inG : inG Σ (stsR sts);
sts_inhabited :> Inhabited (sts.state sts);
}.
Local Existing Instance sts_inG.
```
In this case, the `Instance` for this `libG` class has more than just a `subG`
assumption:
......
......@@ -14,12 +14,20 @@ Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
not have to expose to clients what exactly their resource algebras are. For
example, in the [one-shot example](../tests/one_shot.v), we have:
```coq
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
Local Existing Instances one_shot_inG.
```
The `:>` means that the projection `one_shot_inG` is automatically registered as
an instance for type-class resolution. If you need several resource algebras,
just add more `inG` fields. If you are using another module as part of yours,
add a field like `one_shot_other :> otherG Σ`.
Here, the projection `one_shot_inG` is registered as an instance for type-class
resolution. If you need several resource algebras, just add more `inG` fields.
If you are using another module as part of yours, add a field like
`one_shot_other : otherG Σ`. All of these fields should be added to the
`Local Existing Instances` command.
The code above enables these typeclass instances only in the surrounding file
where they are used to define the new abstractions by the library. The
interface of these abstractions will only depend on the `one_shotG` class.
Since `one_shot_inG` will be hidden from clients, they will not accidentally
rely on it in their code.
Having defined the type class, we need to provide a way to instantiate it. This
is an important step, as not every resource algebra can actually be used: if
......@@ -118,12 +126,14 @@ class for the generalized heap module, bundles the usual `inG` assumptions
together with the `gname`:
```coq
Class gen_heapGpreS (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heapGpreS_heap :> ghost_mapG Σ L V;
gen_heapGpreS_heap : ghost_mapG Σ L V;
}.
Local Existing Instances gen_heapGpreS_heap.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
gen_heap_inG :> gen_heapGpreS L V Σ;
gen_heap_inG : gen_heapGpreS L V Σ;
gen_heap_name : gname;
}.
Local Existing Instances gen_heap_inG.
```
The trailing `S` here is for "singleton", because the idea is that only one
instance of `gen_heapGS` ever exists. This is important, since two instances
......@@ -273,7 +283,9 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
your example would look as follows:
```coq
Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
Local Existing Instance lib_inG.
Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * )))].
Instance subG_libΣ {Σ} : subG libΣ Σ libG Σ.
Proof. solve_inG. Qed.
......
......@@ -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,7 +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 }.
Local Existing Instance cinv_inG.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ cinvG Σ.
......
......@@ -66,16 +66,18 @@ these can be matched up with the invariant namespaces. *)
(** The CMRAs we need, and the global ghost names we are using. *)
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_heap : ghost_mapG Σ L V;
gen_heapGpreS_meta : ghost_mapG Σ L gname;
gen_heapGpreS_meta_data : inG Σ (reservation_mapR (agreeR positiveO));
}.
Local Existing Instances gen_heapGpreS_meta_data gen_heapGpreS_heap gen_heapGpreS_meta.
Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
gen_heap_inG :> gen_heapGpreS L V Σ;
gen_heap_inG : gen_heapGpreS L V Σ;
gen_heap_name : gname;
gen_meta_name : gname
}.
Local Existing Instance gen_heap_inG.
Global Arguments GenHeapGS L V Σ {_ _ _} _ _.
Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
......
......@@ -31,13 +31,15 @@ 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 Σ;
inv_heap_inG : inv_heapGpreS L V Σ;
inv_heap_name : gname
}.
Local Existing Instance inv_heap_inG.
Global Arguments Inv_HeapG _ _ {_ _ _ _}.
Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
......
......@@ -12,8 +12,10 @@ 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,7 +28,8 @@ 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); }.
Local Existing Instance gset_bijG_inG.
Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
......
......@@ -14,7 +14,9 @@ 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,9 @@ 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,14 +9,16 @@ Definition proph_val_list (P V : Type) := list (P * V).
(** The CMRA we need. *)
Class proph_mapGpreS (P V : Type) (Σ : gFunctors) `{Countable P} := {
proph_map_GpreS_inG :> ghost_mapG Σ P (list V)
proph_map_GpreS_inG : ghost_mapG Σ P (list V)
}.
Local Existing Instances proph_map_GpreS_inG.
Class proph_mapGS (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapGS {
proph_map_inG :> proph_mapGpreS P V Σ;
proph_map_inG : proph_mapGpreS P V Σ;
proph_map_name : gname
}.
Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
Local Existing Instances proph_map_inG.
Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
#[ghost_mapΣ P (list V)].
......
......@@ -9,9 +9,11 @@ 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,13 +9,13 @@ 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 {
inv_inG :> invGpreS Σ;
inv_inG : invGpreS Σ;
invariant_name : gname;
enabled_name : gname;
disabled_name : gname;
......@@ -30,6 +30,7 @@ Module invGS.
Proof. solve_inG. Qed.
End invGS.
Import invGS.
Local Existing Instances inv_inG invGpreS_inv invGpreS_enabled invGpreS_disabled.
Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
Next P.
......
......@@ -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,11 @@ 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,9 @@ 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 +88,9 @@ 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,9 @@ 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,9 @@ 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 Σ.
......
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