From 07823f5a6065fc8a8ae95d53cc9da92ea2724688 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Oct 2020 12:52:08 +0100
Subject: [PATCH] more printing tests for prop-level notations

---
 tests/heap_lang2.ref | 18 ++++++++++++++++++
 tests/heap_lang2.v   | 13 +++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
index 73cfb45d3..b21642a0e 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,5 +1,12 @@
 1 subgoal
   
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P, Q : iProp Σ
+  ============================
+  P ={⊤}=∗ Q
+1 subgoal
+  
   Σ : gFunctors
   heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
@@ -10,3 +17,14 @@
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    let: "val2" := fun2 "val1" in
+    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 4ec6061cc..334732089 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -8,6 +8,10 @@ Set Default Proof Using "Type".
 Section printing_tests.
   Context `{!heapG Σ}.
 
+  Lemma vs_print (P Q : iProp Σ) :
+    P ={⊤}=∗ Q.
+  Proof. Show. Abort.
+
   Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
     True -∗ WP let: "val1" := fun1 #() in
        let: "val2" := fun2 "val1" in
@@ -17,4 +21,13 @@ Section printing_tests.
     iIntros "_". Show.
   Abort.
 
+  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
+    {{{ True }}}
+       let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"
+    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
+  Proof. Show. Abort.
+
 End printing_tests.
-- 
GitLab