Use a "static dispatch" way of presenting higher order functions.

theories/typing/lib/refcell/ref_code.v

@@ -204,27 +204,26 @@ Section ref_functions.
   Qed.
 
   (* Apply a function within the ref, typically for accessing a component. *)
-  Definition ref_map : val :=
-    funrec: <> ["ref"; "f"; "env"] :=
-      let: "f'" := !"f" in
+  Definition ref_map (f : val) : val :=
+    funrec: <> ["ref"; "env"] :=
+      let: "f" := f in
       Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
-      letcall: "r" := "f'" ["env"; "x"]%E in
+      letcall: "r" := "f" ["env"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
       Endlft;;
       "ref" <- "r'";;
-      delete [ #1; "f"];; return: ["ref"].
+      return: ["ref"].
 
-  Lemma ref_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
-    typed_val ref_map
-      (fn(∀ β, ∅; ref β ty1, fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2, envty)
-       → ref β ty2).
+  Lemma ref_map_type ty1 ty2 f envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
+    typed_val f (fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2) →
+    typed_val (ref_map f) (fn(∀ α, ∅; ref α ty1, envty) → ref α ty2).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
-       inv_vec arg=>ref f env. simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
-    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+       inv_vec arg=>ref env. simpl_subst.
+    iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
+    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
     rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
@@ -267,15 +266,12 @@ Section ref_functions.
     iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
     wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
       first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
-    iApply (type_type _ [_] _
-        [ f ◁ box (fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2);
-          #lref ◁ box (ref α ty2) ]
+    iApply (type_type _ [_] _ [ #lref ◁ box (ref α ty2) ]
        with "[] LFT HE Hna [HL] Hk"); first last.
-    { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
+    { rewrite tctx_interp_singleton. iExists _. iSplit. done.
       iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     { rewrite /llctx_interp /=; auto. }
-    iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
 End ref_functions.

theories/typing/lib/refcell/refmut_code.v

@@ -151,28 +151,26 @@ Section refmut_functions.
   Qed.
 
   (* Apply a function within the refmut, typically for accessing a component. *)
-  Definition refmut_map : val :=
-    funrec: <> ["ref"; "f"; "env"] :=
-      let: "f'" := !"f" in
+  Definition refmut_map (f : val) : val :=
+    funrec: <> ["ref"; "env"] :=
+      let: "f" := f in
       Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
-      letcall: "r" := "f'" ["env"; "x"]%E in
+      letcall: "r" := "f" ["env"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
       Endlft;;
       "ref" <- "r'";;
-      delete [ #1; "f"];; return: ["ref"].
+      return: ["ref"].
 
-  Lemma refmut_map_type ty1 ty2 envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
-    typed_val refmut_map
-      (fn(∀ β, ∅; refmut β ty1,
-            fn(∀ α, ∅; envty, &uniq{α} ty1) → &uniq{α} ty2, envty)
-       → refmut β ty2).
+  Lemma refmut_map_type ty1 ty2 f envty `{!TyWf ty1, !TyWf ty2, !TyWf envty} :
+    typed_val f (fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2) →
+    typed_val (refmut_map f) (fn(∀ α, ∅; refmut α ty1, envty) → refmut α ty2).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
-       inv_vec arg=>ref f env. simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
-    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (Hf & #Hf' & Href & Henv)".
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+       inv_vec arg=>ref env. simpl_subst.
+    iApply type_let; [apply Hf | solve_typing |]. iIntros (f'). simpl_subst.
+    iApply (type_newlft [ϝ]). iIntros (κ tid) "#LFT #HE Hna HL Hk (#Hf' & Href & Henv & _)".
     rewrite (tctx_hasty_val _ ref). destruct ref as [[|lref|]|]; try done.
     iDestruct "Href" as "[Href Href†]".
     iDestruct "Href" as ([|[[|lv|]|][|[[|lrc|]|][]]]) "Href";
@@ -215,15 +213,12 @@ Section refmut_functions.
     iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
     wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
       first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
-    iApply (type_type _ [_] _
-        [ f ◁ box (fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2);
-          #lref ◁ box (refmut α ty2) ]
+    iApply (type_type _ [_] _ [ #lref ◁ box (refmut α ty2) ]
        with "[] LFT HE Hna [HL] Hk"); first last.
-    { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
+    { rewrite tctx_interp_singleton tctx_hasty_val. iExists _. iSplit. done.
       iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
     { rewrite /llctx_interp /=; auto. }
-    iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
 End refmut_functions.

theories/typing/lib/spawn.v

@@ -78,23 +78,24 @@ End join_handle.
 Section spawn.
   Context `{!typeG Σ, !spawnG Σ}.
 
-  Definition spawn : val :=
-    funrec: <> ["f"; "env"] :=
-      let: "f'" := !"f" in
+  Definition spawn (f : val) : val :=
+    funrec: <> ["env"] :=
+      let: "f" := f in
       let: "join" := spawn [λ: ["c"],
-                            letcall: "r" := "f'" ["env":expr] in
+                            letcall: "r" := "f" ["env":expr] in
                             finish ["c"; "r"]] in
       letalloc: "r" <- "join" in
-      delete [ #1; "f"];; return: ["r"].
+      return: ["r"].
 
-  Lemma spawn_type envty retty `{!TyWf envty, !TyWf retty}
+  Lemma spawn_type envty retty f `{!TyWf envty, !TyWf retty}
         `(!Send envty, !Send retty) :
+    typed_val f (fn(∅; envty) → retty) →
     let E ϝ := envty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
-    typed_val spawn (fn(E; (fn(∅; envty) → retty), envty) → join_handle retty).
+    typed_val (spawn f) (fn(E; envty) → join_handle retty).
   Proof.
-    intros ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros (_ ϝ ret arg). inv_vec arg=>f env. simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (f'). simpl_subst.
+    intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (_ ϝ ret arg). inv_vec arg=>env. simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]. iIntros (f'). simpl_subst.
     iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _])
                      (λ j, [j ◁ join_handle retty])); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
@@ -124,7 +125,6 @@ Section spawn.
     iIntros (v). simpl_subst.
     iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_assign; [solve_typing..|].
-    iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
 

theories/typing/lib/take_mut.v

@@ -9,29 +9,29 @@ Set Default Proof Using "Type".
 Section code.
   Context `{typeG Σ}.
 
-  Definition take ty : val :=
-    funrec: <> ["x"; "f"; "env"] :=
+  Definition take ty (f : val) : val :=
+    funrec: <> ["x"; "env"] :=
       let: "x'" := !"x" in
-      let: "f'" := !"f" in
+      let: "f" := f in
       letalloc: "t" <-{ty.(ty_size)} !"x'" in
-      letcall: "r" := "f'" ["env"; "t"]%E in
+      letcall: "r" := "f" ["env"; "t"]%E in
       Endlft;;
       "x'" <-{ty.(ty_size)} !"r";;
-      delete [ #1; "x"];; delete [ #1; "f"];;  delete [ #ty.(ty_size); "r"];;
+      delete [ #1; "x"];;  delete [ #ty.(ty_size); "r"];;
       let: "r" := new [ #0] in return: ["r"].
 
-  Lemma take_type ty envty `{!TyWf ty, !TyWf envty} :
-    typed_val (take ty)
-      (fn(∀ α, ∅; &uniq{α} ty, fn(∅; envty, ty) → ty, envty) → unit).
+  Lemma take_type ty envty f `{!TyWf ty, !TyWf envty} :
+    typed_val f (fn(∅; envty, ty) → ty) →
+    typed_val (take ty f) (fn(∀ α, ∅; &uniq{α} ty, envty) → unit).
   Proof.
-    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
-      inv_vec arg=>x f env. simpl_subst.
+    intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
+      inv_vec arg=>x env. simpl_subst.
     iApply type_deref; [solve_typing..|]; iIntros (x'); simpl_subst.
-    iApply type_deref; [solve_typing..|]; iIntros (f'); simpl_subst.
+    iApply type_let; [apply Hf|solve_typing|]; iIntros (f'); simpl_subst.
     iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (t); simpl_subst.
     (* Switch to Iris. *)
-    iIntros (tid) "#LFT #HE Hna HL Hk [Ht [Hf [Hf' [Hx [Hx' [Henv _]]]]]]".
-    rewrite !tctx_hasty_val [[x]]lock [[f]]lock [[f']]lock [[env]]lock.
+    iIntros (tid) "#LFT #HE Hna HL Hk (Ht & Hf' & Hx & Hx' & Henv & _)".
+    rewrite !tctx_hasty_val [[x]]lock [[f']]lock [[env]]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..|].
@@ -78,15 +78,13 @@ Section code.
     iMod ("Hclose2" with "Hϝ HL") as "HL".
     iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
-    iApply (type_type _ _ _ [ x ◁ _; f ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
+    iApply (type_type _ _ _ [ x ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
-    { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
+    { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
       unlock. iFrame. iExists _. rewrite uninit_own. iFrame. auto using vec_to_list_length. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
-    iApply type_delete; [solve_typing..|].
     iApply (type_new _); [solve_typing..|]; iIntros (r); simpl_subst.
     iApply type_jump; solve_typing.
   Qed.
-
 End code.