avoid using wp_bind; use wp_apply instead

theories/lang/spawn.v

@@ -74,10 +74,9 @@ Proof.
   iDestruct "Hl" as "[Hc Hd]". wp_write. clear v0.
   iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".
   { iNext. iRight. iExists false. auto. }
-  (* TODO: Cannot use wp_apply due to curried lemma. *)
-  wp_bind (Fork _). iApply (wp_fork with "[Hγf Hf Hd]").
-  - iNext. iApply "Hf". iExists _, _, _. iFrame. auto.
-  - iIntros "!> _". wp_seq. iApply "HΦ". iExists _, _.
+  wp_apply (wp_fork with "[Hγf Hf Hd]").
+  - iApply "Hf". iExists _, _, _. iFrame. auto.
+  - iIntros "_". wp_seq. iApply "HΦ". iExists _, _.
     iFrame. auto.
 Qed.
 

theories/typing/borrow.v

@@ -50,7 +50,7 @@ Section borrow.
     iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
       (try iDestruct "Hown" as "[]").
     iMod (bor_acc_cons with "LFT Hown Htok") as "[H↦ Hclose']". done.
     iDestruct "H↦" as ([|[[|l'|]|][]]) "[>H↦ Hown]"; try iDestruct "Hown" as ">[]".
@@ -83,7 +83,7 @@ Section borrow.
     iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
     rewrite tctx_interp_singleton.
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
       (try iDestruct "Hown" as "[]"). iDestruct "Hown" as (l') "#[H↦b #Hown]".
     iMod (frac_bor_acc with "LFT H↦b Htok1") as (q''') "[>H↦ Hclose']". done.
     iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
@@ -113,7 +113,7 @@ Section borrow.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
       try iDestruct "Hown" as "[]".
     iMod (bor_exists with "LFT Hown") as (vl) "Hbor". done.
     iMod (bor_sep with "LFT Hbor") as "[H↦ Hbor]". done.
@@ -149,7 +149,7 @@ Section borrow.
     iPoseProof (Hincl with "[#] [#]") as "Hincl".
     { by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
     iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
-    wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr";
+    wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr";
       try iDestruct "Hshr" as "[]". iDestruct "Hshr" as (l') "[H↦ Hown]".
     iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
     iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".

theories/typing/function.v

@@ -193,7 +193,7 @@ Section typing.
   Proof.
     iIntros (HE) "!# * #LFT Htl HE HL HC".
     rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
-    wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
+    wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = k⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (tys x))%I
             with "[Hargs]"); first wp_done.

theories/typing/int.v

@@ -42,9 +42,9 @@ Section typing.
   Proof.
     iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1").
+    wp_apply (wp_hasty with "Hp1").
     iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
-    wp_bind p2. iApply (wp_hasty with "Hp2").
+    wp_apply (wp_hasty with "Hp2").
     iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
@@ -63,9 +63,9 @@ Section typing.
   Proof.
     iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1").
+    wp_apply (wp_hasty with "Hp1").
     iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
-    wp_bind p2. iApply (wp_hasty with "Hp2").
+    wp_apply (wp_hasty with "Hp2").
     iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
     wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.
@@ -84,9 +84,9 @@ Section typing.
   Proof.
     iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
     iIntros "[Hp1 Hp2]".
-    wp_bind p1. iApply (wp_hasty with "Hp1").
+    wp_apply (wp_hasty with "Hp1").
     iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
-    wp_bind p2. iApply (wp_hasty with "Hp2").
+    wp_apply (wp_hasty with "Hp2").
     iIntros ([[]|]) "_ H2"; try iDestruct "H2" as "[]".
     wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
   Qed.

theories/typing/unsafe/cell.v

@@ -163,19 +163,17 @@ Section typing.
     iDestruct (ty_size_eq with "Hc'own") as "#>%".
     iDestruct "Hr" as "[Hr↦ Hr†]". iDestruct "Hr↦" as (vr) "[>Hr↦ Hrown]".
     iDestruct (ty_size_eq with "Hrown") as ">Heq". iDestruct "Heq" as %Heq.
-    (* TODO: We need `wp_apply ... with ...`. *)
-    wp_bind (_ <-{_} !_)%E.
     (* FIXME: Changing the order of $Hr↦ $Hc'↦ breaks applying...?? *)
-    iApply (wp_memcpy with "[$Hr↦ $Hc'↦]").
+    wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]").
     { by rewrite Heq Nat2Z.id. }
     { f_equal. done. }
-    iNext. iIntros "[Hr↦ Hc'↦]". wp_seq.
+    iIntros "[Hr↦ Hc'↦]". wp_seq.
     iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
     rewrite Nat2Z.id. iDestruct (ty_size_eq with "Hxown") as "#%".
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hc'↦ $Hx↦]").
+    wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]").
     { f_equal. done. }
     { f_equal. done. }
-    iNext. iIntros "[Hc'↦ Hx↦]". wp_seq.
+    iIntros "[Hc'↦ Hx↦]". wp_seq.
     iMod ("Hclose" with "[Hc'↦ Hxown] Htl") as "[HE Htl]".
     { iExists _. iFrame. }
     (* Now go back to typing level. *)

theories/typing/unsafe/refcell/ref_code.v

@@ -85,12 +85,11 @@ Section ref_functions.
       - change ((q''/2+q')%Qp ≤ 1%Qp)%Qc. rewrite -Hq'q'' comm -{2}(Qp_div_2 q'').
         apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q''/2)%Qp).
         apply Qcplus_le_mono_r, Qp_ge_0. }
-    wp_bind (new [ #2])%E. iApply wp_new; [done..|]. iNext. iIntros (lr ?) "(%&?&Hlr)".
+    wp_apply wp_new; [done..|]. iIntros (lr ?) "(%&?&Hlr)".
     iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I  with "[H↦1 H↦2]" as "H↦".
     { rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
-    wp_let. wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
-    iIntros "!>[Hlr H↦]". wp_seq.
-    iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
+    wp_let. wp_apply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
+    iIntros "[Hlr H↦]". wp_seq. iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
     iMod ("Hcloseδ" with "[H↦lrc H● Hν1 Hshr' H†] Hna") as "[Hδ Hna]".
     { iExists _. rewrite Z.add_comm. iFrame. iExists _. iFrame. iSplitR.
       - rewrite /= agree_idemp. auto.

theories/typing/unsafe/refcell/refcell_code.v

@@ -36,8 +36,8 @@ Section refcell_functions.
     iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
     rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
-    iIntros "!> [Hr↦1 Hx↦]". wp_seq.
+    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
+    iIntros "[Hr↦1 Hx↦]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]%TC
         with "LFT Hna HE HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
@@ -52,7 +52,9 @@ Section refcell_functions.
   Definition refcell_into_inner ty : val :=
     funrec: <> ["x"] :=
       let: "r" := new [ #ty.(ty_size)] in
-      "r" <-{ty.(ty_size)} !"x" +ₗ #1;;
+      "r" <-{ty.(ty_size)} !("x" +ₗ #1);;
+          (* TODO RJ: Can we make it so that the parenthesis above are mandatory?
+             Leaving them away is inconsistent with `let ... := !"x" +ₗ #1`. *)
        delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
 
   Lemma refcell_into_inner_type ty :
@@ -71,8 +73,8 @@ Section refcell_functions.
     iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
     iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
     iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
-    iIntros "!> [Hr↦ Hx↦1]". wp_seq.
+    wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
+    iIntros "[Hr↦ Hx↦1]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]%TC
         with "LFT Hna HE HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
@@ -126,7 +128,7 @@ Section refcell_functions.
       let: "n" := !"x'" in
       if: "n" ≤ #-1 then
         "r" <-{Σ 1} ();;
-        "k" ["r"]
+        "k" ["r"] (* FIXME RJ: this is very confusing, "k" does not even look like it is bound here... *)
       else
         "x'" <- "n" + #1;;
         let: "ref" := new [ #2 ] in
@@ -170,7 +172,7 @@ Section refcell_functions.
       eapply (type_sum_assign_unit [ref α ty; unit]);
         [solve_typing..|by eapply write_own|]; first last.
       simpl. eapply (type_jump [_]); solve_typing.
-    - wp_op. wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
+    - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
       destruct vl as [|?[|?[]]]; try done. wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
@@ -266,7 +268,7 @@ Section refcell_functions.
     iMod (lft_incl_acc with "Hαβ HE") as (qβ) "[Hβtok Hclose]". done.
     iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose')"; try done.
     iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
-    - wp_write. wp_bind (new _). iApply wp_new; [done..|]. iNext.
+    - wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
       destruct vl as [|?[|?[]]]; try done. wp_let.
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.