From d82763889a5fc12e83a28c788f7eb48b72ae45de Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Sun, 6 Dec 2020 08:40:17 +0100
Subject: [PATCH] Test that the dfrac notation prints correctly

---
 tests/heap_lang.ref | 28 ++++++++++++++++++++++++++++
 tests/heap_lang.v   | 16 +++++++++++++---
 2 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index d06576189..0118b3b39 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -151,6 +151,34 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   |={⊤}=> True
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  v : val
+  Φ : val → iPropI Σ
+  ============================
+  "Hl" : l ↦□ v
+  --------------------------------------â–¡
+  "HΦ" : ▷ (True -∗ Φ v)
+  --------------------------------------∗
+  WP ! #l {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  dq : dfrac
+  l : loc
+  v : val
+  Φ : val → iPropI Σ
+  ============================
+  "Hl" : l ↦{dq} v
+  "HΦ" : True -∗ Φ v
+  --------------------------------------∗
+  WP ! #l [{ v, Φ v }]
+  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 2d43b14bf..88c103024 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -265,13 +265,16 @@ Section tests.
   Abort.
 End tests.
 
-Section persistent_mapsto_tests.
+Section mapsto_tests.
   Context `{!heapG Σ}.
 
+  (* Test that the different versions of mapsto work with the tactics, parses,
+     and prints correctly. *)
+
   (* Loading from a persistent points-to predicate in the _persistent_ context. *)
   Lemma persistent_mapsto_load_persistent l v :
     {{{ l ↦□ v }}} ! #l {{{ RET v; True }}}.
-  Proof. iIntros (Φ) "#Hl HΦ". wp_load. by iApply "HΦ". Qed.
+  Proof. iIntros (Φ) "#Hl HΦ". Show. wp_load. by iApply "HΦ". Qed.
 
   (* Loading from a persistent points-to predicate in the _spatial_ context. *)
   Lemma persistent_mapsto_load_spatial l v :
@@ -295,7 +298,14 @@ Section persistent_mapsto_tests.
     wp_load. by iApply "HΦ".
   Qed.
 
-End persistent_mapsto_tests.
+  (* Loading from the general mapsto for any [dfrac]. *)
+  Lemma general_mapsto dq l v :
+    [[{ l ↦{dq} v }]] ! #l [[{ RET v; True }]].
+  Proof. 
+    iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
+  Qed.
+
+End mapsto_tests.
 
 Section inv_mapsto_tests.
   Context `{!heapG Σ}.
-- 
GitLab