From bf2b810d32424ffcbc28a54bc6213aa0d3e25c98 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 12 Jan 2021 11:39:52 +0100
Subject: [PATCH] reuse PreG class in G class where possible

---
 iris/base_logic/lib/gen_inv_heap.v | 10 +++++-----
 iris/base_logic/lib/proph_map.v    |  8 ++++----
 iris/base_logic/lib/wsat.v         | 18 ++++++++----------
 3 files changed, 17 insertions(+), 19 deletions(-)

diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 62ca46136..9ebda575a 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -30,17 +30,17 @@ Definition to_inv_heap {L V : Type} `{Countable L}
     (h: gmap L (V * (V -d> PropO))) : inv_heap_mapUR L V :=
   prod_map (λ x, Excl' x) to_agree <$> h.
 
+Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
+}.
+
 Class inv_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := Inv_HeapG {
-  inv_heap_inG :> inG Σ (authR (inv_heap_mapUR L V));
+  inv_heap_inG :> inv_heapPreG L V Σ;
   inv_heap_name : gname
 }.
 Global Arguments Inv_HeapG _ _ {_ _ _ _}.
 Global Arguments inv_heap_name {_ _ _ _ _} _ : assert.
 
-Class inv_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
-  inv_heap_preG_inG :> inG Σ (authR (inv_heap_mapUR L V))
-}.
-
 Definition inv_heapΣ (L V : Type) `{Countable L} : gFunctors :=
   #[ GFunctor (authR (inv_heap_mapUR L V)) ].
 
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index f28cce425..ba401e7db 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -8,15 +8,15 @@ Local Notation proph_map P V := (gmap P (list V)).
 Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
+Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
+  { proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V)) }.
+
 Class proph_mapG (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
-  proph_map_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V));
+  proph_map_inG :> proph_mapPreG P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _} _ : assert.
 
-Class proph_mapPreG (P V : Type) (Σ : gFunctors) `{Countable P} :=
-  { proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V)) }.
-
 Definition proph_mapΣ (P V : Type) `{Countable P} : gFunctors :=
   #[GFunctor (gmap_viewR P (listO $ leibnizO V))].
 
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 5092971c7..77e391a49 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -8,10 +8,14 @@ From iris.prelude Require Import options.
 exception of what's in the [invG] module. The module [invG] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
 Module invG.
+  Class invPreG (Σ : gFunctors) : Set := WsatPreG {
+    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
+    enabled_inPreG :> inG Σ coPset_disjR;
+    disabled_inPreG :> inG Σ (gset_disjR positive);
+  }.
+
   Class invG (Σ : gFunctors) : Set := WsatG {
-    inv_inG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inG :> inG Σ coPset_disjR;
-    disabled_inG :> inG Σ (gset_disjR positive);
+    inv_inG :> invPreG Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
@@ -22,12 +26,6 @@ Module invG.
       GFunctor coPset_disjR;
       GFunctor (gset_disjR positive)].
 
-  Class invPreG (Σ : gFunctors) : Set := WsatPreG {
-    inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inPreG :> inG Σ coPset_disjR;
-    disabled_inPreG :> inG Σ (gset_disjR positive);
-  }.
-
   Global Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
   Proof. solve_inG. Qed.
 End invG.
@@ -192,7 +190,7 @@ Proof.
     first by apply gmap_view_auth_valid.
   iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
   iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
+  iModIntro; iExists (WsatG _ _ γI γE γD).
   rewrite /wsat /ownE -lock; iFrame.
   iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
 Qed.
-- 
GitLab