WIP.

theories/typing/examples/get_x.v

@@ -12,12 +12,12 @@ Section get_x.
        delete [ #1; "p"] ;; "return" ["r"].
 
   Lemma get_x_type :
-    typed_val get_x (fn(∀ α, [α]; &uniq{α} Π[int; int]) → &shr{α} int).
+    typed_val get_x (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α} Π[int; int]) → &shr{α} int).
   (* FIXME: The above is pretty-printed with some explicit scope annotations,
      and without using 'typed_instruction_ty'.  I think that's related to
      the list notation that we added to %TC. *)
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ϝ ret p).
     inv_vec p=>p. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (p'); simpl_subst.
     iApply (type_letalloc_1 (&shr{α}int)); [solve_typing..|]. iIntros (r). simpl_subst.

theories/typing/examples/init_prod.v

@@ -13,10 +13,10 @@ Section init_prod.
        delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
 
   Lemma init_prod_type :
-    typed_val init_prod (fn([]; int, int) → Π[int;int]).
+    typed_val init_prod (fn(λ ϝ, []; int, int) → Π[int;int]).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
-      inv_vec p=>x y. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>x y. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (y'). simpl_subst.
     iApply (type_new_subtype (Π[uninit 1; uninit 1])); [solve_typing..|].

theories/typing/examples/lazy_lft.v

@@ -18,10 +18,10 @@ Section lazy_lft.
       Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
 
   Lemma lazy_lft_type :
-    typed_val lazy_lft (fn([]) → unit).
+    typed_val lazy_lft (fn(λ ϝ, []) → unit).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
-      inv_vec p. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p. simpl_subst.
     iApply (type_newlft []). iIntros (α).
     iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
       iIntros (t). simpl_subst.

theories/typing/examples/rebor.v

@@ -17,10 +17,10 @@ Section rebor.
                  delete [ #1; "x"] ;; "return" ["r"].
 
   Lemma rebor_type :
-    typed_val rebor (fn([]; Π[int; int], Π[int; int]) → int).
+    typed_val rebor (fn(λ ϝ, []; Π[int; int], Π[int; int]) → int).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros ([] ret p).
-       inv_vec p=>t1 t2. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros ([] ϝ ret p). inv_vec p=>t1 t2. simpl_subst.
     iApply (type_newlft []). iIntros (α).
     iApply (type_letalloc_1 (&uniq{α}Π[int; int])); [solve_typing..|]. iIntros (x). simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.

theories/typing/examples/unbox.v

@@ -12,10 +12,10 @@ Section unbox.
        delete [ #1; "b"] ;; "return" ["r"].
 
   Lemma ubox_type :
-    typed_val unbox (fn(∀ α, [α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
+    typed_val unbox (fn(∀ α, λ ϝ, [ϝ ⊑ α]; &uniq{α}box (Π[int; int])) → &uniq{α} int).
   Proof.
-    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret b).
-      inv_vec b=>b. simpl_subst.
+    intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
+      iIntros (α ϝ ret b). inv_vec b=>b. simpl_subst.
     iApply type_deref; [solve_typing..|]. iIntros (b'); simpl_subst.
     iApply type_deref_uniq_own; [solve_typing..|]. iIntros (bx); simpl_subst.
     iApply type_letalloc_1; [solve_typing..|]. iIntros (r). simpl_subst.

theories/typing/lib/fake_shared_box.v

@@ -11,15 +11,15 @@ Section fake_shared_box.
 
   Lemma cell_replace_type ty :
     typed_val fake_shared_box
-      (fn (fun '(α, β) => FP [α; β; α ⊑ β]%EL
+      (fn (fun '(α, β) => FP (λ ϝ, [ϝ ⊑ α; α ⊑ β]%EL)
                               [# &shr{α}(&shr{β} ty)] (&shr{α}box ty))).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
-      iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
-    iIntros (tid qE) "#LFT Hna HE HL Hk HT".
+      iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    rewrite {1}/elctx_interp 2!big_sepL_cons big_sepL_singleton.
-    iDestruct "HE" as "(Hα & Hβ & #Hαβ)".
+    rewrite {1}/elctx_interp big_sepL_cons big_sepL_singleton.
+    iDestruct "HE" as "(Hβ & #Hαβ)".
     iAssert (▷ ty_own (own_ptr 1 (&shr{α} box ty)) tid [x])%I with "[HT]" as "HT".
     { destruct x as [[|l|]|]=>//=. iDestruct "HT" as "[H $]".
       iNext. iDestruct "H" as ([|[[]|][]]) "[H↦ H]"; try done.
@@ -30,10 +30,10 @@ Section fake_shared_box.
       iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
       by iApply ty_shr_mono. }
     wp_seq.
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α}box ty) ]%TC
-            with "[] LFT Hna [Hα Hβ Hαβ] HL Hk [HT]"); last first.
+    iApply (type_type [] _ _ [ x ◁ box (&shr{α}box ty) ]%TC
+            with "[] LFT [] Hna HL Hk [HT]"); last first.
     { by rewrite tctx_interp_singleton tctx_hasty_val. }
-    { rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
+    { by rewrite /elctx_interp. }
     iApply type_jump; simpl; solve_typing.
   Qed.
 End fake_shared_box.

theories/typing/lib/refcell/refcell.v

@@ -62,17 +62,18 @@ Section refcell_inv.
     eapply refcell_inv_type_ne, type_dist_dist2. done.
   Qed.
 
-  Lemma refcell_inv_proper E L tid l γ α ty1 ty2 :
+  Lemma refcell_inv_proper E L ty1 ty2 q :
     eqtype E L ty1 ty2 →
-    elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
-    refcell_inv tid l γ α ty1 -∗ refcell_inv tid l γ α ty2.
+    llctx_interp L q -∗ ∀ tid l γ α, □ (elctx_interp E -∗
+    refcell_inv tid l γ α ty1 -∗ refcell_inv tid l γ α ty2).
   Proof.
-    (* TODO : this proof is essentially [solve_proper], but within the logic.
-              It would easily gain from some automation. *)
-    iIntros (Hty%eqtype_unfold) "#HE #HL H". unfold refcell_inv.
-    iDestruct (Hty with "HE HL") as "(% & Hown & Hshr)".
+    (* TODO : this proof is essentially [solve_proper], but within the logic. *)
+  (*             It would easily gain from some automation. *)
+    rewrite eqtype_unfold. iIntros (Hty) "HL".
+    iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
+    iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
     iAssert (□ (&{α} shift_loc l 1 ↦∗: ty_own ty1 tid -∗
-                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I with "[]" as "#Hb".
+                &{α} shift_loc l 1 ↦∗: ty_own ty2 tid))%I as "#Hb".
     { iIntros "!# H". iApply bor_iff; last done.
       iSplit; iIntros "!>!#H"; iDestruct "H" as (vl) "[Hf H]"; iExists vl;
       iFrame; by iApply "Hown". }
@@ -171,14 +172,17 @@ Section refcell.
   Proof.
     (* TODO : this proof is essentially [solve_proper], but within the logic.
               It would easily gain from some automation. *)
-    iIntros (ty1 ty2 EQ) "#HE #HL". pose proof EQ as EQ'%eqtype_unfold.
-    iDestruct (EQ' with "HE HL") as "(% & #Hown & #Hshr)".
+    iIntros (ty1 ty2 EQ qL) "HL". generalize EQ. rewrite eqtype_unfold=>EQ'.
+    iDestruct (EQ' with "HL") as "#EQ'".
+    iDestruct (refcell_inv_proper with "HL") as "#Hty1ty2"; first done.
+    iDestruct (refcell_inv_proper with "HL") as "#Hty2ty1"; first by symmetry.
+    iIntros "!# #HE". iDestruct ("EQ'" with "HE") as "(% & #Hown & #Hshr)".
     iSplit; [|iSplit; iIntros "!# * H"].
     - iPureIntro. simpl. congruence.
     - destruct vl as [|[[]|]]; try done. iDestruct "H" as "[$ H]". by iApply "Hown".
     - iDestruct "H" as (a γ) "[Ha H]". iExists a, γ. iFrame.
-      iApply na_bor_iff; last done.
-      iSplit; iIntros "!>!# H"; by iApply refcell_inv_proper.
+      iApply na_bor_iff; last done. iSplit; iIntros "!>!# H".
+      by iApply "Hty1ty2". by iApply "Hty2ty1".
   Qed.
   Lemma refcell_mono' E L ty1 ty2 :
     eqtype E L ty1 ty2 → subtype E L (refcell ty1) (refcell ty2).

theories/typing/soundness.v

@@ -23,7 +23,7 @@ Proof. solve_inG. Qed.
 Section type_soundness.
   Definition exit_cont : val := λ: [<>], #().
 
-  Definition main_type `{typeG Σ} := (fn([]) → unit)%T.
+  Definition main_type `{typeG Σ} := (fn(λ ϝ, []) → unit)%T.
 
   Theorem type_soundness `{typePreG Σ} (main : val) σ t :
     (∀ `{typeG Σ}, typed_val main main_type) →
@@ -39,20 +39,23 @@ Section type_soundness.
     iMod lft_init as (?) "#LFT". done.
     iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
     wp_bind (of_val main). iApply (wp_wand with "[Htl]").
-    iApply (Hmain _ [] [] $! tid 1%Qp with "LFT Htl [] [] []").
+    iApply (Hmain _ [] [] $! tid with "LFT [] Htl [] []").
     { by rewrite /elctx_interp big_sepL_nil. }
     { by rewrite /llctx_interp big_sepL_nil. }
     { by rewrite tctx_interp_nil. }
-    clear Hrtc Hmain main. iIntros (main) "(Htl & HE & HL & Hmain)".
-    rewrite tctx_interp_singleton. iDestruct "Hmain" as (?) "[EQ Hmain]".
+    clear Hrtc Hmain main. iIntros (main) "(Htl & _ & Hmain & _)".
+    iDestruct "Hmain" as (?) "[EQ Hmain]".
     rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
     iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].
     destruct x; try done.
     iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
     { repeat econstructor. apply to_of_val. }
-    iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "LFT Htl HE HL []");
+    iMod (lft_create with "LFT") as (ϝ) "Hϝ". done.
+    iApply ("Hmain" $! () ϝ exit_cont [#] tid with "LFT [] Htl [Hϝ] []");
       last by rewrite tctx_interp_nil.
-    iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
+    { by rewrite /elctx_interp /=. }
+    { rewrite /llctx_interp big_sepL_singleton. iExists ϝ. iFrame. by rewrite /= left_id. }
+    rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_ /=". by wp_lam.
   Qed.
 End type_soundness.