Unverified Commit 3f934cbe authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Extend style to other files: more empty lines

parent 9932a4b7
Pipeline #62760 passed with stage
in 8 minutes and 22 seconds
......@@ -15,6 +15,7 @@ Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
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)) ].
......
......@@ -16,6 +16,7 @@ From iris.prelude Require Import options.
Class mono_natG Σ :=
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.
......
......@@ -11,6 +11,7 @@ Definition na_inv_pool_name := gname.
Class na_invG Σ :=
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 Σ.
......
......@@ -13,6 +13,7 @@ Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
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) ].
......
......@@ -15,6 +15,7 @@ Class authG Σ (A : ucmra) := AuthG {
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.
......
......@@ -15,6 +15,7 @@ Definition read : val := λ: "l", !"l".
(** Monotone counter *)
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 Σ.
......@@ -89,6 +90,7 @@ End mono_proof.
Class ccounterG Σ :=
CCounterG { ccounter_inG : inG Σ (frac_authR natR) }.
Local Existing Instance ccounter_inG.
Definition ccounterΣ : gFunctors :=
#[GFunctor (frac_authR natR)].
......
......@@ -21,6 +21,7 @@ Definition join : val :=
(* Not bundling heapGS, as it may be shared with other users. *)
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 Σ.
......
......@@ -16,6 +16,7 @@ Definition release : val := λ: "l", "l" <- #false.
(* Not bundling heapGS, as it may be shared with other users. *)
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 Σ.
......
......@@ -30,6 +30,7 @@ Definition release : val :=
Class tlockG Σ :=
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))) ].
......
......@@ -24,6 +24,7 @@ From iris.prelude Require Import options.
Class mono_listG (A : Type) Σ :=
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))].
......
......@@ -190,6 +190,7 @@ End M.
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.
......
......@@ -33,6 +33,7 @@ Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
Local Existing Instance one_shot_inG.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ one_shotG Σ.
Proof. solve_inG. Qed.
......
......@@ -30,6 +30,7 @@ Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
Local Existing Instance one_shot_inG.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ one_shotG Σ.
Proof. solve_inG. 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