From 8d96f50cda79d995e5a6bed01e34d89bb1ca97ad Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 26 Jul 2023 12:24:37 +0200
Subject: [PATCH] awp_apply: dont leave behind ugly goals

---
 iris_heap_lang/proofmode.v |  6 ++++--
 tests/atomic.ref           | 25 ++++++++++++++++++++++---
 tests/atomic.v             | 10 +++++++++-
 3 files changed, 35 insertions(+), 6 deletions(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 7c048fcf5..4d72ae4fa 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -727,7 +727,8 @@ premise. The second one additionaly does some framing: it gets rid of [Hs] from
 the context, reducing clutter. You get them all back in the continuation of the
 atomic operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
-  wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
+  (* [pm_prettify] is needed to clean up telescopes. *)
+  wp_apply_core lem ltac:(fun H => iApplyHyp H; pm_prettify) ltac:(fun cont => fail);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   (* Convert "list of hypothesis" into specialization pattern. *)
@@ -736,7 +737,8 @@ Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   wp_apply_core lem
     ltac:(fun H =>
       iApply (wp_frame_wand with
-        [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
+        [SGoal $ SpecGoal GSpatial false [] Hs false]);
+         [iAccu|iApplyHyp H; pm_prettify])
     ltac:(fun cont => fail);
   last iAuIntro.
 
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 90a359e12..131326ff0 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,3 +1,22 @@
+"test_awp_apply"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  aheap : atomic_heap
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "HQ" : Q
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC << ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT Q ∗ l ↦ v >>
+       @ ⊤ ∖ ∅, ∅
+       << l ↦{q} v0, COMM Q >>
+"test_awp_apply_without"
+     : string
 1 goal
   
   H : atomic_heap
@@ -10,9 +29,9 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  atomic_acc (⊤ ∖ ∅) ∅ (tele_app (λ (v0 : val) (q : dfrac), l ↦{q} v0))
-    (l ↦ v) (tele_app (λ (v0 : val) (q : dfrac), tele_app (l ↦{q} v0)))
-    (λ.. (_ : [tele (_ : val) (_ : dfrac)]) (_ : [tele]), Q -∗ Q)
+  AACC << ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
+       @ ⊤ ∖ ∅, ∅
+       << l ↦{q} v0, COMM Q -∗ Q >>
 "printing"
      : string
 1 goal
diff --git a/tests/atomic.v b/tests/atomic.v
index 32b5595bc..26688dbf2 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -25,7 +25,15 @@ Section tests.
   Context `{!atomic_heap, !heapGS Σ, !atomic_heapGS Σ}.
   Import atomic_heap.notation.
 
-  (* FIXME: removing the `val` type annotation breaks printing. *)
+  Check "test_awp_apply".
+  Lemma test_awp_apply (Q : iProp Σ) (l : loc) v :
+    Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
+  Proof.
+    iIntros "HQ Hl". awp_apply load_spec. Show.
+    iAaccIntro with "Hl"; eauto with iFrame.
+  Qed.
+
+  Check "test_awp_apply_without".
   Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
     Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
   Proof.
-- 
GitLab