make some more heap_lang libs lc-generic; tweak atomic_heap handling

iris_heap_lang/lib/atomic_heap.v

@@ -5,8 +5,18 @@ From iris.heap_lang Require Export derived_laws.
 From iris.heap_lang Require Import notation proofmode.
 From iris.prelude Require Import options.
 
-(** A general logically atomic interface for a heap. *)
-Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
+(** A general logically atomic interface for a heap.
+All parameters are implicit, since it is expected that there is only one
+[heapGS_gen] in scope that could possibly apply. For example:
+  
+  Context `{!heapGS_gen hlc Σ, !atomic_heap}.
+
+Or, for libraries that require later credits:
+
+  Context `{!heapGS Σ, !atomic_heap}.
+
+*)
+Class atomic_heap `{!heapGS_gen hlc Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   free : val;
@@ -45,7 +55,7 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
       <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
-Global Arguments atomic_heap _ {_}.
+Global Hint Mode atomic_heap + + + : typeclass_instances.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
@@ -69,7 +79,7 @@ Module notation.
 End notation.
 
 Section derived.
-  Context `{!heapGS Σ, !atomic_heap Σ}.
+  Context `{!heapGS_gen hlc Σ, !atomic_heap}.
 
   Import notation.
 
@@ -99,7 +109,7 @@ Definition primitive_cmpxchg : val :=
   λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2".
 
 Section proof.
-  Context `{!heapGS Σ}.
+  Context `{!heapGS_gen hlc Σ}.
 
   Lemma primitive_alloc_spec (v : val) :
     {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
@@ -148,7 +158,7 @@ End proof.
 
 (* NOT an instance because users should choose explicitly to use it
      (using [Explicit Instance]). *)
-Definition primitive_atomic_heap `{!heapGS Σ} : atomic_heap Σ :=
+Definition primitive_atomic_heap `{!heapGS_gen hlc Σ} : atomic_heap :=
   {| alloc_spec := primitive_alloc_spec;
      free_spec := primitive_free_spec;
      load_spec := primitive_load_spec;

iris_heap_lang/lib/increment.v

@@ -38,7 +38,7 @@ End increment_physical.
 (** Next: logically atomic increment on top of an arbitrary logically atomic heap *)
 
 Section increment.
-  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ, !atomic_heap}.
 
   Import atomic_heap.notation.
 

iris_heap_lang/lib/lock.v

@@ -2,7 +2,10 @@ From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import primitive_laws notation.
 From iris.prelude Require Import options.
 
-Structure lock Σ `{!heapGS Σ} := Lock {
+(** A general interface for a lock.
+All parameters are implicit, since it is expected that there is only one
+[heapGS_gen] in scope that could possibly apply. *)
+Structure lock `{!heapGS_gen hlc Σ} := Lock {
   (** * Operations *)
   newlock : val;
   acquire : val;
@@ -29,14 +32,9 @@ Structure lock Σ `{!heapGS Σ} := Lock {
   release_spec γ lk R :
     {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
 }.
-
-Global Arguments newlock {_ _} _.
-Global Arguments acquire {_ _} _.
-Global Arguments release {_ _} _.
-Global Arguments is_lock {_ _} _ _ _ _.
-Global Arguments locked {_ _} _ _.
+Global Hint Mode lock + + + : typeclass_instances.
 
 Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
 
-Global Instance is_lock_proper Σ `{!heapGS Σ} (L: lock Σ) γ lk:
-  Proper ((≡) ==> (≡)) (is_lock L γ lk) := ne_proper _.
+Global Instance is_lock_proper hlc Σ `{!heapGS_gen hlc Σ} (L : lock) γ lk :
+  Proper ((≡) ==> (≡)) (L.(is_lock) γ lk) := ne_proper _.

iris_heap_lang/lib/par.v

@@ -15,7 +15,7 @@ Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
-Context `{!heapGS Σ, !spawnG Σ}.
+Context `{!heapGS_gen hlc Σ, !spawnG Σ}.
 
 (* Notice that this allows us to strip a later *after* the two Ψ have been
    brought together.  That is strictly stronger than first stripping a later

iris_heap_lang/lib/spawn.v

@@ -29,7 +29,7 @@ Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
 Section proof.
-Context `{!heapGS Σ, !spawnG Σ} (N : namespace).
+Context `{!heapGS_gen hlc Σ, !spawnG Σ} (N : namespace).
 
 Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
   ∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨

iris_heap_lang/lib/spin_lock.v

@@ -23,7 +23,7 @@ Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS Σ, !lockG Σ}.
+  Context `{!heapGS_gen hlc Σ, !lockG Σ}.
   Let N := nroot .@ "spin_lock".
 
   Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
@@ -104,7 +104,7 @@ End proof.
 
 Typeclasses Opaque is_lock locked.
 
-Canonical Structure spin_lock `{!heapGS Σ, !lockG Σ} : lock Σ :=
+Canonical Structure spin_lock `{!heapGS_gen hlc Σ, !lockG Σ} : lock :=
   {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
      lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.

iris_heap_lang/lib/ticket_lock.v

@@ -38,7 +38,7 @@ Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-  Context `{!heapGS Σ, !tlockG Σ}.
+  Context `{!heapGS_gen hlc Σ, !tlockG Σ}.
   Let N := nroot .@ "ticket_lock".
 
   Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
@@ -174,7 +174,7 @@ End proof.
 
 Typeclasses Opaque is_lock issued locked.
 
-Canonical Structure ticket_lock `{!heapGS Σ, !tlockG Σ} : lock Σ :=
+Canonical Structure ticket_lock `{!heapGS_gen hlc Σ, !tlockG Σ} : lock :=
   {| lock.locked_exclusive := locked_exclusive; lock.is_lock_iff := is_lock_iff;
      lock.newlock_spec := newlock_spec;
      lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.

tests/atomic.ref

@@ -4,7 +4,7 @@ Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap Σ
+  aheap : atomic_heap
   Q : iProp Σ
   l : loc
   v : val
@@ -20,7 +20,7 @@ Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap Σ
+  aheap : atomic_heap
   P : iProp Σ
   l : loc
   ============================
@@ -33,7 +33,7 @@ Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
-  aheap : atomic_heap Σ
+  aheap : atomic_heap
   P : iProp Σ
   l : loc
   ============================

tests/atomic.v

@@ -27,7 +27,7 @@ Section general_bi_tests.
 End general_bi_tests.
 
 Section tests.
-  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap}.
   Import atomic_heap.notation.
 
   (* FIXME: removing the `val` type annotation breaks printing. *)
@@ -41,7 +41,7 @@ End tests.
 
 (* Test if we get reasonable error messages with non-laterable assertions in the context. *)
 Section error.
-  Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
+  Context `{!heapGS Σ} {aheap: atomic_heap}.
   Import atomic_heap.notation.
 
   Check "non_laterable".