Commit 149d1ec6 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename the wp_focus tactic into wp_bind.

This better reflects the name of the bind rule.

I renamed an internal tactic that was previously called wp_bind into
wp_bind_core.
parent 8ff1fd84
......@@ -138,7 +138,7 @@ Lemma wait_spec l P (Φ : val → iProp Σ) :
Proof.
rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iLöb as "IH". wp_rec. wp_bind (! _)%E.
iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
wp_load. destruct p.
......
......@@ -46,11 +46,11 @@ Lemma inc_spec l j (Φ : val → iProp Σ) :
Proof.
iIntros "[Hl HΦ]". iLöb as "IH". wp_rec.
iDestruct "Hl" as (γ) "(% & #? & #Hγ & Hγf)".
wp_focus (! _)%E.
wp_bind (! _)%E.
iVs (auth_open (counter_inv l) with "[Hγf]") as (j') "(% & Hl & Hclose)"; auto.
rewrite {2}/counter_inv.
wp_load. iVs ("Hclose" $! j with "[Hl]") as "Hγf"; eauto.
iVsIntro. wp_let; wp_op. wp_focus (CAS _ _ _).
iVsIntro. wp_let; wp_op. wp_bind (CAS _ _ _).
iVs (auth_open (counter_inv l) with "[Hγf]") as (j'') "(% & Hl & Hclose)"; auto.
rewrite {2}/counter_inv.
destruct (decide (j `max` j'' = j `max` j')) as [Hj|Hj].
......
......@@ -61,7 +61,7 @@ Lemma acquire_spec l R (Φ : val → iProp Σ) :
is_lock l R (locked l R - R - Φ #()) WP acquire #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ) "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
iInv N as ([]) "[Hl HR]" "Hclose".
- wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
iVsIntro. wp_if. by iApply "IH".
......
......@@ -25,7 +25,7 @@ Proof.
iIntros (?) "(#Hh&Hf1&Hf2&HΦ)".
rewrite /par. wp_value. iVsIntro. wp_let. wp_proj.
wp_apply (spawn_spec parN); try wp_done; try solve_ndisj; iFrame "Hf1 Hh".
iIntros (l) "Hl". wp_let. wp_proj. wp_focus (f2 _).
iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _).
iApply wp_wand_l; iFrame "Hf2"; iIntros (v) "H2". wp_let.
wp_apply join_spec; iFrame "Hl". iIntros (w) "H1".
iSpecialize ("HΦ" with "* [-]"); first by iSplitL "H1". by wp_let.
......
......@@ -60,7 +60,7 @@ Proof.
{ iNext. iExists NONEV. iFrame; eauto. }
wp_apply wp_fork. iSplitR "Hf".
- iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto.
- wp_focus (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
- wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
iInv N as (v') "[Hl _]" "Hclose".
wp_store. iApply "Hclose". iNext. iExists (SOMEV v). iFrame. eauto.
Qed.
......@@ -69,7 +69,7 @@ Lemma join_spec (Ψ : val → iProp Σ) l (Φ : val → iProp Σ) :
join_handle l Ψ ( v, Ψ v - Φ v) WP join #l {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]". iDestruct "H" as (γ) "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
iLöb as "IH". wp_rec. wp_bind (! _)%E. iInv N as (v) "[Hl Hinv]" "Hclose".
wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
- iVs ("Hclose" with "[Hl]"); [iNext; iExists _; iFrame; eauto|].
iVsIntro. wp_match. iApply ("IH" with "Hγ Hv").
......
......@@ -101,7 +101,7 @@ Lemma wait_loop_spec l x R (Φ : val → iProp Σ) :
issued l x R ( l, locked l R - R - Φ #()) WP wait_loop #x #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Ht)".
iLöb as "IH". wp_rec. wp_let. wp_focus (! _)%E.
iLöb as "IH". wp_rec. wp_let. wp_bind (! _)%E.
iInv N as (o n) "[Hl Ha]" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
......@@ -123,12 +123,12 @@ Lemma acquire_spec l R (Φ : val → iProp Σ) :
is_lock l R ( l, locked l R - R - Φ #()) WP acquire #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iLöb as "IH". wp_rec. wp_bind (! _)%E.
iInv N as (o n) "[Hl Ha]" "Hclose".
wp_load. iVs ("Hclose" with "[Hl Ha]").
{ iNext. iExists o, n. by iFrame. }
iVsIntro. wp_let. wp_proj. wp_proj. wp_op.
wp_focus (CAS _ _ _).
wp_bind (CAS _ _ _).
iInv N as (o' n') "[Hl [Hainv Haown]]" "Hclose".
destruct (decide ((#o', #n') = (#o, #n)))%V
as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
......@@ -158,11 +158,11 @@ Lemma release_spec R l (Φ : val → iProp Σ):
locked l R R Φ #() WP release #l {{ Φ }}.
Proof.
iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Hγ)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iLöb as "IH". wp_rec. wp_bind (! _)%E.
iInv N as (o n) "[Hl Hr]" "Hclose".
wp_load. iVs ("Hclose" with "[Hl Hr]").
{ iNext. iExists o, n. by iFrame. }
iVsIntro. wp_let. wp_focus (CAS _ _ _ ).
iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
wp_proj. wp_op. wp_proj.
iInv N as (o' n') "[Hl Hr]" "Hclose".
destruct (decide ((#o', #n') = (#o, #n)))%V
......
......@@ -17,7 +17,7 @@ Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_bindi {E e} Ki Φ :
Lemma wp_bind_ctxi {E e} Ki Φ :
WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }}
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
......
......@@ -89,7 +89,7 @@ End heap.
Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind K; iApply lem; try iNext)
wp_bind_core K; iApply lem; try iNext)
| _ => fail "wp_apply: not a 'wp'"
end.
......@@ -98,7 +98,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
| |- _ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Alloc _ => wp_bind K end)
match eval hnf in e' with Alloc _ => wp_bind_core K end)
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
eapply tac_wp_alloc with _ H _;
[let e' := match goal with |- to_val ?e' = _ => e' end in
......@@ -121,7 +121,7 @@ Tactic Notation "wp_load" :=
| |- _ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Load _ => wp_bind K end)
match eval hnf in e' with Load _ => wp_bind_core K end)
|fail 1 "wp_load: cannot find 'Load' in" e];
eapply tac_wp_load;
[iAssumption || fail "wp_load: cannot find heap_ctx"
......@@ -138,7 +138,7 @@ Tactic Notation "wp_store" :=
| |- _ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Store _ _ => wp_bind K end)
match eval hnf in e' with Store _ _ => wp_bind_core K end)
|fail 1 "wp_store: cannot find 'Store' in" e];
eapply tac_wp_store;
[let e' := match goal with |- to_val ?e' = _ => e' end in
......@@ -158,7 +158,7 @@ Tactic Notation "wp_cas_fail" :=
| |- _ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with CAS _ _ _ => wp_bind K end)
match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
|fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
eapply tac_wp_cas_fail;
[let e' := match goal with |- to_val ?e' = _ => e' end in
......@@ -180,7 +180,7 @@ Tactic Notation "wp_cas_suc" :=
| |- _ wp ?E ?e ?Q =>
first
[reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with CAS _ _ _ => wp_bind K end)
match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
eapply tac_wp_cas_suc;
[let e' := match goal with |- to_val ?e' = _ => e' end in
......
......@@ -3,7 +3,7 @@ From iris.heap_lang Require Export tactics derived.
Import uPred.
(** wp-specific helper tactics *)
Ltac wp_bind K :=
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
| _ => etrans; [|fast_by apply (wp_bind K)]; simpl
......@@ -55,7 +55,7 @@ Ltac wp_finish := intros_revert ltac:(
Tactic Notation "wp_value" :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e
wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
| _ => fail "wp_value: not a wp"
end.
......@@ -65,7 +65,7 @@ Tactic Notation "wp_rec" :=
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
wp_bind K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
wp_bind_core K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e
| _ => fail "wp_rec: not a 'wp'"
end.
......@@ -75,7 +75,7 @@ Tactic Notation "wp_lam" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
wp_bind_core K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e
| _ => fail "wp_lam: not a 'wp'"
end.
......@@ -87,13 +87,13 @@ Tactic Notation "wp_op" :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
lazymatch eval hnf in e' with
| BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
| BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
| BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
| BinOp EqOp _ _ => wp_bind_core K; apply wp_eq; wp_finish
| BinOp _ _ _ =>
wp_bind K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
wp_bind_core K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish
| UnOp _ _ =>
wp_bind K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish
wp_bind_core K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish
end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e
| _ => fail "wp_op: not a 'wp'"
end.
......@@ -102,8 +102,8 @@ Tactic Notation "wp_proj" :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
| Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
| Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
| Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e
| _ => fail "wp_proj: not a 'wp'"
end.
......@@ -113,7 +113,7 @@ Tactic Notation "wp_if" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| If _ _ _ =>
wp_bind K;
wp_bind_core K;
etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
end) || fail "wp_if: cannot find 'If' in" e
| _ => fail "wp_if: not a 'wp'"
......@@ -124,18 +124,18 @@ Tactic Notation "wp_match" :=
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Case _ _ _ =>
wp_bind K;
wp_bind_core K;
etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
simpl_subst; wp_finish
end) || fail "wp_match: cannot find 'Match' in" e
| _ => fail "wp_match: not a 'wp'"
end.
Tactic Notation "wp_focus" open_constr(efoc) :=
Tactic Notation "wp_bind" open_constr(efoc) :=
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with
| efoc => unify e' efoc; wp_bind K
end) || fail "wp_focus: cannot find" efoc "in" e
| _ => fail "wp_focus: not a 'wp'"
| efoc => unify e' efoc; wp_bind_core K
end) || fail "wp_bind: cannot find" efoc "in" e
| _ => fail "wp_bind: not a 'wp'"
end.
......@@ -81,7 +81,7 @@ Proof.
set (workers_post (v : val) := (barrier_res γ Ψ1 barrier_res γ Ψ2)%I).
wp_let. wp_apply (wp_par (λ _, True)%I workers_post); iFrame "Hh".
iSplitL "HP Hs Hγ"; [|iSplitL "Hr"].
- wp_focus eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
- wp_bind eM. iApply wp_wand_l; iSplitR "HP"; [|by iApply "He"].
iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
iVs (own_update with "Hγ") as "Hx".
{ by apply (cmra_update_exclusive (Shot x)). }
......
......@@ -55,7 +55,7 @@ Proof.
iNext; iRight; iExists n; by iFrame.
+ wp_cas_fail. iVs ("Hclose" with "[-]"); last eauto.
rewrite /one_shot_inv; eauto 10.
- iIntros "!#". wp_seq. wp_focus (! _)%E.
- iIntros "!#". wp_seq. wp_bind (! _)%E.
iInv N as ">Hγ" "Hclose".
iAssert ( v, l v ((v = NONEV own γ Pending)
n : Z, v = SOMEV #n own γ (Shot n)))%I with "[Hγ]" as "Hv".
......@@ -72,7 +72,7 @@ Proof.
wp_let. iVsIntro. iIntros "!#". wp_seq.
iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
{ by wp_match. }
wp_match. wp_focus (! _)%E.
wp_match. wp_bind (! _)%E.
iInv N as ">[[Hl Hγ]|H]" "Hclose"; last iDestruct "H" as (m') "[Hl Hγ]".
{ iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as %?. }
wp_load.
......
Markdown is supported
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