From 8f23e9370c6f0c456d045e1d1c75df7b0a9eff78 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 May 2017 15:35:34 +0200
Subject: [PATCH] make the static dispatch for closures look more like it looks
 in Rust

---
 theories/typing/lib/rc/rc.v               |  2 +-
 theories/typing/lib/refcell/ref_code.v    | 18 +++++++++---------
 theories/typing/lib/refcell/refmut_code.v | 18 +++++++++---------
 theories/typing/lib/spawn.v               | 20 ++++++++++----------
 theories/typing/lib/take_mut.v            | 16 ++++++++--------
 5 files changed, 37 insertions(+), 37 deletions(-)

diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 7e63812f..e6591e2b 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -984,7 +984,7 @@ Section code.
       delete [ #1; "rc"];; return: ["r"].
 
   Lemma rc_make_mut_type ty `{!TyWf ty} clone :
-    typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) →
+    typed_val clone (fn(∀ α, ∅; &shr{α} ty) → ty) → (* ty : Clone, as witnessed by the impl clone *)
     typed_val (rc_make_mut ty clone) (fn(∀ α, ∅; &uniq{α} rc ty) → &uniq{α} ty).
   Proof.
     intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index c493cfc9..6e07357b 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -204,21 +204,21 @@ Section ref_functions.
   Qed.
 
   (* Apply a function within the ref, typically for accessing a component. *)
-  Definition ref_map (f : val) : val :=
-    funrec: <> ["ref"; "env"] :=
-      let: "f" := f in
+  Definition ref_map (call_once : val) : val :=
+    funrec: <> ["ref"; "f"] :=
+      let: "call_once" := call_once in
       Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
-      letcall: "r" := "f" ["env"; "x"]%E in
+      letcall: "r" := "call_once" ["f"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
       Endlft;;
       "ref" <- "r'";;
       return: ["ref"].
 
-  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).
+  Lemma ref_map_type ty1 ty2 call_once fty `{!TyWf ty1, !TyWf ty2, !TyWf fty} :
+    typed_val call_once (fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2) → (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    typed_val (ref_map call_once) (fn(∀ α, ∅; ref α ty1, fty) → ref α ty2).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
@@ -244,8 +244,8 @@ Section ref_functions.
       iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
     iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _) _
         [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&shr{α ⊓ ν}ty2)])]
-        [ f' ◁ fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2;
-          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box envty ]
+        [ f' ◁ fn(∀ α, ∅; fty, &shr{α}ty1) → &shr{α}ty2;
+          #lx ◁ box (&shr{α ⊓ ν}ty1); env ◁ box fty ]
        with "[] LFT [] Hna HL [-H† Hlx Henv]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 666181c7..2dc9b2e5 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -151,21 +151,21 @@ Section refmut_functions.
   Qed.
 
   (* Apply a function within the refmut, typically for accessing a component. *)
-  Definition refmut_map (f : val) : val :=
-    funrec: <> ["ref"; "env"] :=
-      let: "f" := f in
+  Definition refmut_map (call_once : val) : val :=
+    funrec: <> ["ref"; "f"] :=
+      let: "call_once" := call_once in
       Newlft;;
       let: "x'" := !"ref" in
       letalloc: "x" <- "x'" in
-      letcall: "r" := "f" ["env"; "x"]%E in
+      letcall: "r" := "call_once" ["f"; "x"]%E in
       let: "r'" := !"r" in delete [ #1; "r"];;
       Endlft;;
       "ref" <- "r'";;
       return: ["ref"].
 
-  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).
+  Lemma refmut_map_type ty1 ty2 call_once fty `{!TyWf ty1, !TyWf ty2, !TyWf fty} :
+    typed_val call_once (fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2) → (* fty : for<'a>, FnOnce(&'a ty1) -> &'a ty2, as witnessed by the impl call_once *)
+    typed_val (refmut_map call_once) (fn(∀ α, ∅; refmut α ty1, fty) → refmut α ty2).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
        inv_vec arg=>ref env. simpl_subst.
@@ -191,8 +191,8 @@ Section refmut_functions.
       iApply (bor_fracture with "LFT [> -]"); first done. rewrite /= Qp_mult_1_r //. }
     iApply (type_type ((κ ⊑ₑ α ⊓ ν) :: (α ⊓ ν ⊑ₑ α) :: _) _
         [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box (&uniq{α ⊓ ν}ty2)])]
-        [ f' ◁ fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2;
-          #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box envty ]
+        [ f' ◁ fn(∀ α, ∅; fty, &uniq{α}ty1) → &uniq{α}ty2;
+          #lx ◁ box (&uniq{α ⊓ ν}ty1); env ◁ box fty ]
        with "[] LFT [] Hna HL [-H† Hlx Henv Hbor]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index a90d8eab..a7f02d57 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -78,20 +78,20 @@ End join_handle.
 Section spawn.
   Context `{!typeG Σ, !spawnG Σ}.
 
-  Definition spawn (f : val) : val :=
-    funrec: <> ["env"] :=
-      let: "f" := f in
+  Definition spawn (call_once : val) : val :=
+    funrec: <> ["f"] :=
+      let: "call_once" := call_once in
       let: "join" := spawn [λ: ["c"],
-                            letcall: "r" := "f" ["env":expr] in
+                            letcall: "r" := "call_once" ["f":expr] in
                             finish ["c"; "r"]] in
       letalloc: "r" <- "join" in
       return: ["r"].
 
-  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 f) (fn(E; envty) → join_handle retty).
+  Lemma spawn_type fty retty call_once `{!TyWf fty, !TyWf retty}
+        `(!Send fty, !Send retty) :
+    typed_val call_once (fn(∅; fty) → retty) → (* fty : FnOnce() -> retty, as witnessed by the impl call_once *)
+    let E ϝ := fty.(ty_outlives_E) static ++ retty.(ty_outlives_E) static in
+    typed_val (spawn call_once) (fn(E; fty) → join_handle retty).
   Proof.
     intros Hf ? E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ϝ ret arg). inv_vec arg=>env. simpl_subst.
@@ -107,7 +107,7 @@ Section spawn.
       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 ∅ [# envty] retty) in _).
+                (λ _:(), 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]").
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index aae1d7b7..ec89f1c0 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -9,20 +9,20 @@ Set Default Proof Using "Type".
 Section code.
   Context `{typeG Σ}.
 
-  Definition take ty (f : val) : val :=
-    funrec: <> ["x"; "env"] :=
+  Definition take ty (call_once : val) : val :=
+    funrec: <> ["x"; "f"] :=
       let: "x'" := !"x" in
-      let: "f" := f in
+      let: "call_once" := call_once in
       letalloc: "t" <-{ty.(ty_size)} !"x'" in
-      letcall: "r" := "f" ["env"; "t"]%E 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"].
 
-  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).
+  Lemma take_type ty fty call_once `{!TyWf ty, !TyWf fty} :
+    typed_val call_once (fn(∅; fty, ty) → ty) → (* fty : FnOnce(ty) -> ty, as witnessed by the impl call_once *)
+    typed_val (take ty call_once) (fn(∀ α, ∅; &uniq{α} ty, fty) → unit).
   Proof.
     intros Hf E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret arg).
       inv_vec arg=>x env. simpl_subst.
@@ -53,7 +53,7 @@ Section code.
     iApply (wp_let' _ _ _ _ k _ EQk). simpl_subst. iNext.
     iApply (type_type ((β ⊑ₑ ϝ) :: _) [β ⊑ₗ []]
         [k ◁cont(_, λ x:vec val 1, [ x!!!0 ◁ box ty])]
-        [ f' ◁ fn(∅; envty, ty) → ty; #tl ◁ box ty; env ◁ box envty ]
+        [ 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 "∗#". }
-- 
GitLab