make the global functor stuff in the various constructions more uniform;...

make the global functor stuff in the various constructions more uniform; change it such that barrier/proof does not have to repeat the functors it needs

barrier/proof.v

@@ -6,17 +6,17 @@ From barrier Require Export barrier.
 From barrier Require Import protocol.
 Import uPred.
 
-(** The monoids we need. *)
+(** The CMRAs we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG heap_lang Σ sts;
   barrier_savedPropG :> savedPropG heap_lang Σ idCF;
 }.
+(** The Functors we need. *)
 Definition barrierGF : rFunctors := [stsGF sts; agreeRF idCF].
-
-Instance inGF_barrierG
-  `{inGF heap_lang Σ (stsGF sts), inGF heap_lang Σ (agreeRF idCF)} : barrierG Σ.
-Proof. split; apply _. Qed.
+(* Show and register that they match. *)
+Instance inGF_barrierG `{H : inGFs heap_lang Σ barrierGF} : barrierG Σ.
+Proof. destruct H as (?&?&?). split; apply _. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.

heap_lang/heap.v

@@ -8,14 +8,14 @@ Import uPred.
    predicates over finmaps instead of just ownP. *)
 
 Definition heapR : cmraT := mapR loc (fracR (dec_agreeR val)).
-Definition heapGF : rFunctor := authGF heapR.
 
+(** The CMRA we need. *)
 Class heapG Σ := HeapG {
-  heap_inG : inG heap_lang Σ (authR heapR);
+  heap_inG :> authG heap_lang Σ heapR;
   heap_name : gname
 }.
-Instance heap_authG `{i : heapG Σ} : authG heap_lang Σ heapR :=
-  {| auth_inG := heap_inG |}.
+(** The Functor we need. *)
+Definition heapGF : rFunctor := authGF heapR.
 
 Definition to_heap : state → heapR := fmap (λ v, Frac 1 (DecAgree v)).
 Definition of_heap : heapR → state :=

heap_lang/spawn.v

@@ -14,13 +14,14 @@ Definition join : val :=
     | InjL <>  => '"join" '"c"
     end.
 
-(** The monoids we need. *)
+(** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG {
   spawn_tokG :> inG heap_lang Σ (exclR unitC);
 }.
+(** The functor we need. *)
 Definition spawnGF : rFunctors := [constRF (exclR unitC)].
-
+(* Show and register that they match. *)
 Instance inGF_spawnG
   `{inGF heap_lang Σ (constRF (exclR unitC))} : spawnG Σ.
 Proof. split. apply: inGF_inG. Qed.

program_logic/auth.v

@@ -2,13 +2,15 @@ From algebra Require Export auth upred_tactics.
 From program_logic Require Export invariants global_functor.
 Import uPred.
 
+(* The CMRA we need. *)
 Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_inG :> inG Λ Σ (authR A);
   auth_identity :> CMRAIdentity A;
   auth_timeless :> CMRADiscrete A;
 }.
-
+(* The Functor we need. *)
 Definition authGF (A : cmraT) : rFunctor := constRF (authR A).
+(* Show and register that they match. *)
 Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
   `{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
 Proof. split; try apply _. apply: inGF_inG. Qed.

program_logic/global_functor.v

@@ -5,6 +5,12 @@ Module rFunctors.
     | nil  : rFunctors
     | cons : rFunctor → rFunctors → rFunctors.
   Coercion singleton (F : rFunctor) : rFunctors := cons F nil.
+
+  Fixpoint fold_right {A} (f : rFunctor → A → A) (a : A) (Fs : rFunctors) : A :=
+    match Fs with
+    | nil => a
+    | cons F Fs => f F (fold_right f a Fs)
+    end.
 End rFunctors.
 Notation rFunctors := rFunctors.rFunctors.
 
@@ -58,3 +64,16 @@ Proof. by exists 0. Qed.
 Instance inGF_further {Λ Σ} (F F': rFunctor) :
   inGF Λ Σ F → inGF Λ (rFunctorG.cons F' Σ) F.
 Proof. intros [i ?]. by exists (S i). Qed.
+
+(** For modules that need more than one functor, we offer a typeclass
+    [inGFs] to demand a list of rFunctor to be available. We do
+    *not* register any instances that go from there to [inGF], to
+    avoid cycles. *)
+Class inGFs (Λ : language) (Σ : rFunctorG) (Fs : rFunctors) :=
+  InGFs : (rFunctors.fold_right (λ F T, inGF Λ Σ F * T) () Fs)%type.
+
+Instance inGFs_nil {Λ Σ} : inGFs Λ Σ [].
+Proof. exact tt. Qed.
+Instance inGFs_cons {Λ Σ} F Fs :
+  inGF Λ Σ F → inGFs Λ Σ Fs → inGFs Λ Σ (rFunctors.cons F Fs).
+Proof. split; done. Qed.

program_logic/sts.v

@@ -2,13 +2,15 @@ From algebra Require Export sts upred_tactics.
 From program_logic Require Export invariants global_functor.
 Import uPred.
 
+(** The CMRA we need. *)
 Class stsG Λ Σ (sts : stsT) := StsG {
   sts_inG :> inG Λ Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
 Coercion sts_inG : stsG >-> inG.
-
+(** The Functor we need. *)
 Definition stsGF (sts : stsT) : rFunctor := constRF (stsR sts).
+(* Show and register that they match. *)
 Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
   `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
 Proof. split; try apply _. apply: inGF_inG. Qed.