From a85a8e2f9815e50b807b6aca52b8e123c08dffd8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 11:29:26 +0200
Subject: [PATCH] fix yet another case of broken heap_lang notation

---
 tests/heap_lang2.ref          | 12 ++++++++++++
 tests/heap_lang2.v            | 20 ++++++++++++++++++++
 theories/heap_lang/lang.v     | 14 ++++++++++++++
 theories/heap_lang/notation.v | 12 ++----------
 4 files changed, 48 insertions(+), 10 deletions(-)
 create mode 100644 tests/heap_lang2.ref
 create mode 100644 tests/heap_lang2.v

diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
new file mode 100644
index 000000000..eb393dc01
--- /dev/null
+++ b/tests/heap_lang2.ref
@@ -0,0 +1,12 @@
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{ _, True }}
+  
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
new file mode 100644
index 000000000..cada4949b
--- /dev/null
+++ b/tests/heap_lang2.v
@@ -0,0 +1,20 @@
+(* Test yet another way of importing heap_lang modules that used to break
+printing *)
+From iris.heap_lang Require Export lifting notation.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+Section printing_tests.
+  Context `{heapG Σ}.
+
+  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
+    True -∗ WP let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
+  Proof.
+    iIntros "_". Show.
+  Abort.
+
+End printing_tests.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index f8d167e59..538eafe00 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -4,6 +4,9 @@ From stdpp Require Export strings.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+
 Module heap_lang.
 Open Scope Z_scope.
 
@@ -529,3 +532,14 @@ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
 
 (* Prefer heap_lang names over ectx_language names. *)
 Export heap_lang.
+
+(** Define some derived forms. *)
+Notation Lam x e := (Rec BAnon x e) (only parsing).
+Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing).
+Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
+Notation LamV x e := (RecV BAnon x e) (only parsing).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
+Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
+Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
+
+Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 340f78407..b3f40e897 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -2,16 +2,8 @@ From iris.program_logic Require Import language.
 From iris.heap_lang Require Export lang tactics.
 Set Default Proof Using "Type".
 
-(** Define some derived forms. Happens in the same file because the order of
-    this and the following notations being defined is very relevant. *)
-Notation Lam x e := (Rec BAnon x e).
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let BAnon e1 e2).
-Notation LamV x e := (RecV BAnon x e).
-Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
-Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
-- 
GitLab