From bd7a1b9627180f9ecb546cbe0ac380af87723ef6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 09:42:44 +0200
Subject: [PATCH] improve printing of texan triples

---
 tests/heap_lang.ref                 | 11 +++++
 tests/heap_lang.v                   |  9 +++++
 theories/program_logic/weakestpre.v | 62 ++++++++++-------------------
 3 files changed, 42 insertions(+), 40 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 27abe6a52..9bddbbb8b 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -30,3 +30,14 @@
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  H : 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_lang.v b/tests/heap_lang.v
index bcc2e47de..962c4a5ca 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -128,6 +128,15 @@ 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.
 
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index bf585cc9c..6382b8046 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -89,93 +89,75 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  s ;  E  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  ? '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  x  ..  y ,  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  ? '/' {{{  x  ..  y ,   RET  pat ;  Q  } } } ']'") : bi_scope.
+
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  s ;  E  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  @  E  ? '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
     (at level 20,
-     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : bi_scope.
+     format "'[hv' {{{  P  } } }  '/  ' e  ? '/' {{{  RET  pat ;  Q  } } } ']'") : bi_scope.
 
+(* Aliases for stdpp scope -- they inherit the levels and format from above. *)
 Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
-      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
-    (at level 20, x closed binder, y closed binder,
-     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q  } } }") : stdpp_scope.
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }}) : stdpp_scope.
 Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
-  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
-    (at level 20,
-     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q  } } }") : stdpp_scope.
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }}) : stdpp_scope.
 
 Section wp.
 Context `{irisG Λ Σ}.
-- 
GitLab