From 8f25b2f21e5b651724ad3a1802c43b700c056e51 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Feb 2016 18:39:53 +0100
Subject: [PATCH] add a version of bind for ectx items

---
 heap_lang/heap_lang.v |  7 +++++++
 heap_lang/lifting.v   |  6 +++++-
 heap_lang/tests.v     | 10 +++++-----
 3 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index 93f206bd9..5482c8e01 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -313,3 +313,10 @@ Proof.
     exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
     econstructor; eauto.
 Qed.
+
+Global Instance heap_lang_ctx_item Ki :
+  LanguageCtx heap_lang (heap_lang.fill_item Ki).
+Proof.
+  change (LanguageCtx heap_lang (heap_lang.fill [Ki])).
+  by apply _.
+Qed.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 71116edec..e89728dac 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -13,7 +13,11 @@ Implicit Types K : ectx.
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
   wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
-Proof. apply wp_bind. Qed.
+Proof. apply weakestpre.wp_bind. Qed.
+
+Lemma wp_bindi {E e} Ki Q :
+  wp E e (λ v, wp E (fill_item Ki (of_val v)) Q) ⊑ wp E (fill_item Ki e) Q.
+Proof. apply weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
 Lemma wp_alloc_pst E σ e v Q :
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index c79b53174..d5297a534 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -34,9 +34,9 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
-    rewrite -(wp_bind [SeqCtx (Load (Loc _))]).
-    rewrite -(wp_bind [StoreRCtx (LocV _)]).
-    rewrite -(wp_bind [PlusLCtx _]).
+    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
+    rewrite -(wp_bindi (StoreRCtx (LocV _))).
+    rewrite -(wp_bindi (PlusLCtx _)).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
     { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
@@ -75,7 +75,7 @@ Module LiftingTests.
     (* Go on. *)
     rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
     rewrite -wp_plus. asimpl.
-    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -(wp_bindi (CaseCtx _ _)).
     rewrite -!later_intro /=.
     apply wp_lt; intros Hn12.
     * (* TODO RJ: It would be better if we could use wp_if_true here
@@ -97,7 +97,7 @@ Module LiftingTests.
     ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
-    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -(wp_bindi (CaseCtx _ _)).
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_case_inl //.
       rewrite -!later_intro -wp_value' //.
-- 
GitLab