From c1449e94c9c1f8aceafe9a704efb84e1b73f90d4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 22:05:02 +0100
Subject: [PATCH] make wp_par usable

---
 theories/heap_lang/lib/increment.v | 2 +-
 theories/heap_lang/lib/par.v       | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 79f600e20..5b4c6129f 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -155,7 +155,7 @@ Section increment_client.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
       done.
     }
-    wp_apply par_spec; wp_pures.
+    wp_apply wp_par.
     - iAssumption.
     - iAssumption.
     - iIntros (??) "_ !>". done.
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 5fd18ec3f..0d55d3a4b 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,6 +12,8 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
+(* Not a value itself, but with *unlocked* value lambdas. *)
+Local Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
@@ -37,7 +39,7 @@ Qed.
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
   WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP e1 ||| e2 {{ Φ }}.
+  WP (e1 ||| e2)%V {{ Φ }}.
 Proof.
   iIntros "H1 H2 H".
   wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
-- 
GitLab