From 278515b88af583879f026518e41d6fe966e58244 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Jun 2018 10:32:24 +0200
Subject: [PATCH] tests/ipm_paper: show goals where they were shown in the
 paper

---
 tests/ipm_paper.ref | 94 +++++++++++++++++++++++++++++++++++++++++++++
 tests/ipm_paper.v   | 10 ++---
 2 files changed, 99 insertions(+), 5 deletions(-)

diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index e69de29bb..315580437 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -0,0 +1,94 @@
+1 subgoal
+  
+  M : ucmraT
+  A : Type
+  P, R : iProp
+  Ψ : A → iProp
+  x : A
+  ============================
+  "HP" : P
+  "HΨ" : Ψ x
+  "HR" : R
+  --------------------------------------∗
+  Ψ x ∗ P
+  
+2 subgoals
+  
+  M : ucmraT
+  A : Type
+  P, R : iProp
+  Ψ : A → iProp
+  x : A
+  ============================
+  "HΨ" : Ψ x
+  --------------------------------------∗
+  Ψ x
+  
+
+subgoal 2 is:
+ "HP" : P
+"HR" : R
+--------------------------------------∗
+P
+
+1 subgoal
+  
+  M : ucmraT
+  A : Type
+  P, R : iProp
+  Ψ : A → iProp
+  x : A
+  ============================
+  "HP" : P
+  "HR" : R
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  M : ucmraT
+  A : Type
+  P, R : iProp
+  Ψ : A → iProp
+  ============================
+  "HP" : P
+  "HΨ" : ∃ a : A, Ψ a
+  "HR" : R
+  --------------------------------------∗
+  ∃ a : A, Ψ a ∗ P
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  counterG0 : counterG Σ
+  l : loc
+  n : nat
+  N : namespace
+  γ : gname
+  ============================
+  "Hinv" : inv N (I γ l)
+  --------------------------------------â–¡
+  "Hγf" : own γ (Frag n)
+  --------------------------------------∗
+  WP ! #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  counterG0 : counterG Σ
+  l : loc
+  n : nat
+  N : namespace
+  γ : gname
+  c : nat
+  ============================
+  "Hinv" : inv N (I γ l)
+  --------------------------------------â–¡
+  "Hγf" : own γ (Frag n)
+  "Hl" : l ↦ #c
+  "Hγ" : own γ (Auth c)
+  --------------------------------------∗
+  ▷ I γ l ∗ (∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m)
+  
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 930c7dec4..f423ed213 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -30,14 +30,14 @@ Section demo.
   Proof.
     iIntros "[HP [HΨ HR]]".
     iDestruct "HΨ" as (x) "HΨ".
-    iExists x.
-    iSplitL "HΨ". iAssumption. iAssumption.
+    iExists x. Show.
+    iSplitL "HΨ". Show. iAssumption. Show. iAssumption.
   Qed.
 
   (* The short version in IPM, as in the paper *)
   Lemma sep_exist_short A (P R: iProp) (Ψ: A → iProp) :
     P ∗ (∃ a, Ψ a) ∗ R ⊢ ∃ a, Ψ a ∗ P.
-  Proof. iIntros "[HP [HΨ HR]]". iFrame "HP". iAssumption. Qed.
+  Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
 
   (* An even shorter version in IPM, using the frame introduction pattern `$` *)
   Lemma sep_exist_shorter A (P R: iProp) (Ψ: A → iProp) :
@@ -239,8 +239,8 @@ Section counter_proof.
     {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}.
   Proof.
     iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
-    rewrite /read /=. wp_let. iApply wp_inv_open; last iFrame "Hinv"; auto.
-    iDestruct 1 as (c) "[Hl Hγ]". wp_load.
+    rewrite /read /=. wp_let. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
+    iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
     iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
     { iApply own_op. by iFrame. }
     rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
-- 
GitLab