Use new function call lemma in spawn, take_mut

theories/typing/function.v

@@ -294,19 +294,19 @@ Section typing.
   Qed.
 
   Lemma type_call_iris E (κs : list lft) {A} x qκs tid
-        p (ps : list path) (k : expr) (fp : A → fn_params (length ps)) :
+        f (ps : list path) (k : expr) (fp : A → fn_params (length ps)) :
     (∀ ϝ, elctx_sat (((λ κ, ϝ ⊑ₑ κ) <$> κs) ++ E) [] ((fp x).(fp_E) ϝ)) →
     is_Some (to_val k) →
     lft_ctx -∗ elctx_interp E -∗ na_own tid ⊤ -∗
     qκs.[lft_intersect_list κs] -∗
-    tctx_elt_interp tid (p ◁ fn fp) -∗
+    (fn fp).(ty_own) tid [f] -∗
     ([∗ list] y ∈ zip_with TCtx_hasty ps (box <$> vec_to_list (fp x).(fp_tys)), tctx_elt_interp tid y) -∗
     (∀ ret, na_own tid top -∗ qκs.[lft_intersect_list κs] -∗
              (box (fp x).(fp_ty)).(ty_own) tid [ret] -∗ 
              WP k [of_val ret] {{ _, cont_postcondition }}) -∗
-    WP (call: p ps → k) {{ _, cont_postcondition }}.
+    WP (call: f ps → k) {{ _, cont_postcondition }}.
   Proof.
-    iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk".
+    iIntros (HE Hk') "#LFT #HE Htl Hκs Hf Hargs Hk". rewrite -tctx_hasty_val.
     iApply (type_call_iris' with "LFT HE Htl [] Hκs Hf Hargs [Hk]"); [done..| |].
     - instantiate (1 := 1%Qp). by rewrite /llctx_interp.
     - iIntros "* Htl _". iApply "Hk". done.

theories/typing/lib/spawn.v

@@ -105,23 +105,15 @@ Section spawn.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
-      (* FIXME this is horrible. *)
-      refine (let Hcall := type_call' _ [] [] [] f' [env:expr]
-                (λ _:(), FP_wf ∅ [# fty] retty) in _).
-      specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
-      erewrite of_val_unlock in Hcall; last done.
-      iApply (Hcall with "LFT HE Htl [] [Hfin]").
-      - constructor.
+      iApply (type_call_iris _ [] tt 1%Qp with "LFT HE Htl [] [Hf'] [Henv]"). 4: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
       - solve_typing.
-      - by rewrite /llctx_interp /=.
-      - rewrite /cctx_interp. iIntros "* Hin".
-        iDestruct "Hin" as %Hin%elem_of_list_singleton. subst x.
-        rewrite /cctx_elt_interp. iIntros "* ?? Hret". inv_vec args=>arg /=.
+      - solve_to_val.
+      - iApply lft_tok_static.
+      - iSplitL; last done. (* FIXME: iSplit should work, the RHS is persistent. *)
+        rewrite !tctx_hasty_val. iApply @send_change_tid. done.
+      - iIntros (r) "Htl _ Hret".
         wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
-        rewrite tctx_interp_singleton tctx_hasty_val. by iApply @send_change_tid.
-      - rewrite tctx_interp_cons tctx_interp_singleton. iSplitL "Hf'".
-        + rewrite !tctx_hasty_val. by iApply @send_change_tid.
-        + rewrite !tctx_hasty_val. by iApply @send_change_tid. }
+        by iApply @send_change_tid. }
     iIntros (v). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_assign; [solve_typing..|].

theories/typing/lib/take_mut.v

@@ -15,7 +15,6 @@ Section code.
       let: "call_once" := call_once in
       letalloc: "t" <-{ty.(ty_size)} !"x'" in
       letcall: "r" := "call_once" ["f"; "t"]%E in
-      Endlft;;
       "x'" <-{ty.(ty_size)} !"r";;
       delete [ #1; "x"];;  delete [ #ty.(ty_size); "r"];;
       let: "r" := new [ #0] in return: ["r"].
@@ -31,7 +30,7 @@ Section code.
     iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
     (* Switch to Iris. *)
     iIntros (tid) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
-    rewrite !tctx_hasty_val [[x]]lock [[f']]lock [[env]]lock.
+    rewrite !tctx_hasty_val [[x]]lock [[env]]lock [fn _]lock. 
     iDestruct (ownptr_uninit_own with "Ht") as (tl tvl) "(% & >Htl & Htl†)". subst t. simpl.
     destruct x' as [[|lx'|]|]; try done. simpl.
     iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose1)"; [solve_typing..|].
@@ -40,39 +39,22 @@ Section code.
     iDestruct (heap_mapsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
     wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
     iIntros "[Htl Hx'↦]". wp_seq.
-    (* Prepare the lifetime, call the function.
-       In principle, we could try to make the β we create here the ϝ of the called
-       function, but that seems to actually be more work because we could not use
-       the lemmas proven in function.v. *)
-    iMod (lft_create with "LFT") as (β) "[Hβ Hβ†]"; first done.
-    iMod (bor_create with "LFT Hϝ") as "[Hβϝ Hβ†ϝ]"; first done.
-    iDestruct (frac_bor_lft_incl β ϝ with "LFT [>Hβϝ]") as "#Hβϝ".
-    { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
-    match goal with | |- context [(WP (_ [?k']) {{_, _}})%I] =>
-      assert (∃ k, to_val k' = Some k) as [k EQk] by (eexists; solve_to_val) end.
-    iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
-    iApply (type_type ((β ⊑ₑ ϝ) :: _) [β ⊑ₗ []]
-        [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box ty])]
-        [ f' ◁ fn(∅; fty, ty) → ty; #tl ◁ box ty; env ◁ box fty ]
-       with "[] LFT [] Hna [Hβ Hβ†] [-Hf' Htl Htl† Hx'vl Henv]"); swap 1 3; swap 4 5.
-    { rewrite /llctx_interp. iSplitL; last done. (* FIXME: iSplit should work as one side is 'True', thus persistent. *)
-      iExists β. simpl. iSplit; first by rewrite left_id. iFrame "∗#". }
-    { iSplitL; last iApply "HE". iExact "Hβϝ". }
-    { iApply (type_call ()); solve_typing. (* This is showing that the lifetime bounds of f' are satisfied. *) }
-    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists _. iFrame. }
+    (* Call the function. *)
+    wp_let. unlock.
+    iApply (type_call_iris _ [ϝ] tt with "LFT HE Hna [Hϝ] [Hf'] [Henv Htl Htl† Hx'vl]"). 4: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
+    { solve_typing. }
+    { solve_to_val. }
+    { simpl. rewrite (right_id static). done. }
+    { simpl. rewrite !tctx_hasty_val. iFrame. iSplit; last done.
+      rewrite tctx_hasty_val' //. iFrame. iExists _. iFrame. }
     (* Prove the continuation of the function call. *)
-    iIntros (? ->%elem_of_list_singleton arg) "Hna Hβ". inv_vec arg=>r.
-    iIntros "[Hr _]". rewrite tctx_hasty_val /=.
+    iIntros (r) "Hna Hϝ Hr". simpl.
     iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
-    apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
+    iApply wp_rec; try (done || apply _).
     { repeat econstructor. } simpl_subst. iNext.
-    iDestruct "Hβ" as "[Hβ _]". iDestruct "Hβ" as (Λ) "(% & Hβ & #Hβ†)".
-    simpl in *. subst β. rewrite (left_id static). iSpecialize ("Hβ†" with "Hβ").
-    wp_bind Endlft. iApply wp_mask_mono; last iApply (wp_step_fupd with "Hβ†"); auto with ndisj.
-    wp_seq. iIntros "#H↠!>". wp_seq.
+    rewrite (right_id static).
     wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using vec_to_list_length..|].
-    iIntros "[Hlx' Hlr]". wp_seq. iMod ("Hβ†ϝ" with "Hβ†") as ">Hϝ".
+    iIntros "[Hlx' Hlr]". wp_seq.
     iMod ("Hclose3" with "[Hlx' Hrvl]") as "[Hlx' Hα]".
     { iExists _. iFrame. }
     iMod ("Hclose2" with "Hϝ HL") as "HL".