Commit 59a8f5bf authored by Ralf Jung's avatar Ralf Jung
Browse files

better spacing for functor declarations

parent 7b6a32fe
...@@ -7,15 +7,14 @@ From iris.program_logic Require Import saved_prop sts. ...@@ -7,15 +7,14 @@ From iris.program_logic Require Import saved_prop sts.
From iris.heap_lang Require Import proofmode. From iris.heap_lang Require Import proofmode.
From iris.heap_lang.lib.barrier Require Import protocol. From iris.heap_lang.lib.barrier Require Import protocol.
(** The CMRAs we need. *) (** The CMRAs/functors we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class barrierG Σ := BarrierG { Class barrierG Σ := BarrierG {
barrier_stsG :> stsG Σ sts; barrier_stsG :> stsG Σ sts;
barrier_savedPropG :> savedPropG Σ idCF; barrier_savedPropG :> savedPropG Σ idCF;
}. }.
(** The Functors we need. *)
Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF]. Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
(* Show and register that they match. *)
Instance subG_barrierΣ {Σ} : subG barrierΣ Σ barrierG Σ. Instance subG_barrierΣ {Σ} : subG barrierΣ Σ barrierG Σ.
Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed. Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
......
...@@ -14,8 +14,8 @@ Global Opaque newcounter inc get. ...@@ -14,8 +14,8 @@ Global Opaque newcounter inc get.
(** The CMRA we need. *) (** The CMRA we need. *)
Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }. Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
Definition counterΣ : gFunctors := #[authΣ mnatUR]. Definition counterΣ : gFunctors := #[authΣ mnatUR].
Instance subG_counterΣ {Σ} : subG counterΣ Σ counterG Σ. Instance subG_counterΣ {Σ} : subG counterΣ Σ counterG Σ.
Proof. intros [? _]%subG_inv. split; apply _. Qed. Proof. intros [? _]%subG_inv. split; apply _. Qed.
......
...@@ -14,8 +14,8 @@ Global Opaque newlock acquire release. ...@@ -14,8 +14,8 @@ Global Opaque newlock acquire release.
(** The CMRA we need. *) (** The CMRA we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }. Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))]. Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ. Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
......
...@@ -16,12 +16,11 @@ Definition join : val := ...@@ -16,12 +16,11 @@ Definition join : val :=
end. end.
Global Opaque spawn join. Global Opaque spawn join.
(** The CMRA we need. *) (** The CMRA & functor we need. *)
(* Not bundling heapG, as it may be shared with other users. *) (* Not bundling heapG, as it may be shared with other users. *)
Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }. Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
(** The functor we need and register that they match. *)
Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))]. Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ. Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
......
...@@ -35,9 +35,9 @@ Class tlockG Σ := TlockG { ...@@ -35,9 +35,9 @@ Class tlockG Σ := TlockG {
tlock_G :> authG Σ (gset_disjUR nat); tlock_G :> authG Σ (gset_disjUR nat);
tlock_exclG :> inG Σ (exclR unitC) tlock_exclG :> inG Σ (exclR unitC)
}. }.
Definition tlockΣ : gFunctors := Definition tlockΣ : gFunctors :=
#[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))]. #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ tlockG Σ. Instance subG_tlockΣ {Σ} : subG tlockΣ Σ tlockG Σ.
Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed. Proof. intros [? [?%subG_inG _]%subG_inv]%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