From c74d8afde2c9877cd952c9ef6bc1a4c98d001e2e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Dec 2020 14:38:00 +0100
Subject: [PATCH] Add some FIXMES.

---
 iris/base_logic/lib/gen_heap.v   |  2 ++
 iris_heap_lang/derived_laws.v    |  3 +++
 iris_heap_lang/lib/atomic_heap.v | 30 ++++++++++++++++--------------
 iris_heap_lang/primitive_laws.v  |  2 ++
 4 files changed, 23 insertions(+), 14 deletions(-)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index b0c417223..41c7652b2 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -123,6 +123,8 @@ Section definitions.
 End definitions.
 Arguments meta {L _ _ V Σ _ A _ _} l N x.
 
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Local Notation "l ↦{ dq } v" := (mapsto l dq v)
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
 Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index b0bfdf89c..72ce1856a 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -16,6 +16,9 @@ with lists of values. *)
 
 Definition array `{!heapG Σ} (l : loc) (dq : dfrac) (vs : list val) : iProp Σ :=
   ([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I.
+
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Notation "l ↦∗{ dq } vs" := (array l dq vs)
   (at level 20, format "l  ↦∗{ dq }  vs") : bi_scope.
 Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 5b3c1c802..85255d127 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -48,21 +48,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
 Arguments atomic_heap _ {_}.
 
 (** Notation for heap primitives, in a module so you can import it separately. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Module notation.
-Notation "l ↦{ dq } v" := (mapsto l dq v)
-  (at level 20, format "l  ↦{ dq }  v") : bi_scope.
-Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
-  (at level 20, format "l  ↦□  v") : bi_scope.
-Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
-  (at level 20, format "l  ↦{# q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
-  (at level 20, format "l  ↦  v") : bi_scope.
-
-Notation "'ref' e" := (alloc e) : expr_scope.
-Notation "! e" := (load e) : expr_scope.
-Notation "e1 <- e2" := (store e1 e2) : expr_scope.
-
-Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
+  Notation "l ↦{ dq } v" := (mapsto l dq v)
+    (at level 20, format "l  ↦{ dq }  v") : bi_scope.
+  Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
+    (at level 20, format "l  ↦□  v") : bi_scope.
+  Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
+    (at level 20, format "l  ↦{# q }  v") : bi_scope.
+  Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
+    (at level 20, format "l  ↦  v") : bi_scope.
+
+  Notation "'ref' e" := (alloc e) : expr_scope.
+  Notation "! e" := (load e) : expr_scope.
+  Notation "e1 <- e2" := (store e1 e2) : expr_scope.
+
+  Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)).
 
 End notation.
 
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index e2ef9e733..0f168abe0 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -28,6 +28,8 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
 
 (** Since we use an [option val] instance of [gen_heap], we need to overwrite
 the notations.  That also helps for scopes and coercions. *)
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
 Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
 Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))
-- 
GitLab