Commit 8f25b2f2 authored by Ralf Jung's avatar Ralf Jung
Browse files

add a version of bind for ectx items

parent b7401c68
...@@ -313,3 +313,10 @@ Proof. ...@@ -313,3 +313,10 @@ Proof.
exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto. exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
econstructor; eauto. econstructor; eauto.
Qed. 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.
...@@ -13,7 +13,11 @@ Implicit Types K : ectx. ...@@ -13,7 +13,11 @@ Implicit Types K : ectx.
(** Bind. *) (** Bind. *)
Lemma wp_bind {E e} K Q : 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. 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. *) (** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Q : Lemma wp_alloc_pst E σ e v Q :
......
...@@ -34,9 +34,9 @@ Module LiftingTests. ...@@ -34,9 +34,9 @@ Module LiftingTests.
rewrite -later_intro. apply forall_intro=>l. rewrite -later_intro. apply forall_intro=>l.
apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_. apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
rewrite -later_intro. asimpl. rewrite -later_intro. asimpl.
rewrite -(wp_bind [SeqCtx (Load (Loc _))]). rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
rewrite -(wp_bind [StoreRCtx (LocV _)]). rewrite -(wp_bindi (StoreRCtx (LocV _))).
rewrite -(wp_bind [PlusLCtx _]). rewrite -(wp_bindi (PlusLCtx _)).
rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first. 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. *) { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
rewrite -later_intro. apply wand_intro_l. rewrite right_id. rewrite -later_intro. apply wand_intro_l. rewrite right_id.
...@@ -75,7 +75,7 @@ Module LiftingTests. ...@@ -75,7 +75,7 @@ Module LiftingTests.
(* Go on. *) (* Go on. *)
rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))). rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
rewrite -wp_plus. asimpl. rewrite -wp_plus. asimpl.
rewrite -(wp_bind [CaseCtx _ _]). rewrite -(wp_bindi (CaseCtx _ _)).
rewrite -!later_intro /=. rewrite -!later_intro /=.
apply wp_lt; intros Hn12. apply wp_lt; intros Hn12.
* (* TODO RJ: It would be better if we could use wp_if_true here * (* TODO RJ: It would be better if we could use wp_if_true here
...@@ -97,7 +97,7 @@ Module LiftingTests. ...@@ -97,7 +97,7 @@ Module LiftingTests.
Q (LitNatV $ pred n) wp E (App Pred (LitNat n)) Q. Q (LitNatV $ pred n) wp E (App Pred (LitNat n)) Q.
Proof. Proof.
rewrite -wp_lam //. asimpl. rewrite -wp_lam //. asimpl.
rewrite -(wp_bind [CaseCtx _ _]). rewrite -(wp_bindi (CaseCtx _ _)).
apply later_mono, wp_le=> Hn. apply later_mono, wp_le=> Hn.
- rewrite -wp_case_inl //. - rewrite -wp_case_inl //.
rewrite -!later_intro -wp_value' //. rewrite -!later_intro -wp_value' //.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment