Change the notation for borrows : now, it is just a notation for the predicate...

Change the notation for borrows : now, it is just a notation for the predicate transformer (it does not include the payload of the borrow).
---
--- The new behavior is somewhat more intuitive, and better behaved wrt view predicates.

theories/lifetime/at_borrow.v

@@ -9,8 +9,8 @@ Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ⊥ lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
-Notation "&at{ κ , N } P" := (at_bor κ N P)
-  (format "&at{ κ , N }  P", at level 20, right associativity) : uPred_scope.
+Notation "&at{ κ , N }" := (at_bor κ N)
+  (format "&at{ κ , N }", at level 20, right associativity) : uPred_scope.
 
 Section atomic_bors.
   Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
@@ -31,9 +31,9 @@ Section atomic_bors.
   Global Instance at_bor_persistent : PersistentP (&at{κ, N} P) := _.
 
   Lemma bor_share E κ :
-    ↑lftN ⊆ E → N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
+    N ⊥ lftN → &{κ}P ={E}=∗ &at{κ, N}P.
   Proof.
-    iIntros (? HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
+    iIntros (HN) "HP". rewrite bor_unfold_idx. iDestruct "HP" as (i) "(#?&Hown)".
     iExists i. iFrame "#".
     iLeft. iSplitR. done. by iMod (inv_alloc with "[Hown]") as "$"; auto.
   Qed.

theories/lifetime/frac_borrow.v

@@ -8,10 +8,10 @@ Set Default Proof Using "Type".
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
 Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
-  (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} ∃ q, φ q ∗ own γ q ∗
-                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
-Notation "&frac{ κ } P" := (frac_bor κ P)
-  (format "&frac{ κ }  P", at level 20, right associativity) : uPred_scope.
+  (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗
+                       (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ'])))%I.
+Notation "&frac{ κ }" := (frac_bor κ)
+  (format "&frac{ κ }", at level 20, right associativity) : uPred_scope.
 
 Section frac_bor.
   Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).

theories/lifetime/lifetime.v

@@ -75,7 +75,7 @@ Qed.
 
 Lemma bor_exists {A} (Φ : A → iProp Σ) `{!Inhabited A} E κ :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}Φ x.
+  lft_ctx -∗ &{κ}(∃ x, Φ x) ={E}=∗ ∃ x, &{κ}(Φ x).
 Proof.
   iIntros (?) "#LFT Hb".
   iMod (bor_acc_atomic_cons with "LFT Hb") as "[H|[H† >_]]"; first done.
@@ -168,7 +168,7 @@ Qed.
 
 Lemma bor_unnest E κ κ' P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ'} &{κ} P ={E}▷=∗ &{κ ⊓ κ'} P.
+  lft_ctx -∗ &{κ'} (&{κ} P) ={E}▷=∗ &{κ ⊓ κ'} P.
 Proof.
   iIntros (?) "#LFT Hbor".
   rewrite ->(bor_unfold_idx _ P).

theories/lifetime/lifetime_sig.v

@@ -39,10 +39,10 @@ Module Type lifetime_sig.
       (format "q .[ κ ]", at level 0) : uPred_scope.
   Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
 
-  Notation "&{ κ } P" := (bor κ P)
-    (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
-  Notation "&{ κ , i } P" := (idx_bor κ i P)
-    (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ }" := (bor κ)
+    (format "&{ κ }", at level 20, right associativity) : uPred_scope.
+  Notation "&{ κ , i }" := (idx_bor κ i)
+    (format "&{ κ , i }", at level 20, right associativity) : uPred_scope.
 
   Infix "⊑" := lft_incl (at level 70) : uPred_scope.
   Infix "⊓" := lft_intersect (at level 40) : C_scope.
@@ -115,7 +115,7 @@ Module Type lifetime_sig.
   Parameter idx_bor_iff : ∀ κ i P P', ▷ □ (P ↔ P') -∗ &{κ,i}P -∗ &{κ,i}P'.
 
   Parameter idx_bor_unnest : ∀ E κ κ' i P,
-    ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+    ↑lftN ⊆ E → lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
 
   Parameter idx_bor_acc : ∀ E q κ i P, ↑lftN ⊆ E →
     lft_ctx -∗ &{κ,i}P -∗ idx_bor_own 1 i -∗ q.[κ] ={E}=∗

theories/lifetime/model/definitions.v

@@ -212,10 +212,10 @@ Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 0) : uPred_scope.
 Notation "[† κ ]" := (lft_dead κ) (format "[† κ ]"): uPred_scope.
 
-Notation "&{ κ } P" := (bor κ P)
-  (format "&{ κ }  P", at level 20, right associativity) : uPred_scope.
-Notation "&{ κ , i } P" := (idx_bor κ i P)
-  (format "&{ κ , i }  P", at level 20, right associativity) : uPred_scope.
+Notation "&{ κ }" := (bor κ)
+  (format "&{ κ }", at level 20, right associativity) : uPred_scope.
+Notation "&{ κ , i }" := (idx_bor κ i)
+  (format "&{ κ , i }", at level 20, right associativity) : uPred_scope.
 
 Infix "⊑" := lft_incl (at level 70) : uPred_scope.
 

theories/lifetime/model/reborrow.v

@@ -160,7 +160,7 @@ Qed.
 
 Lemma idx_bor_unnest E κ κ' i P :
   ↑lftN ⊆ E →
-  lft_ctx -∗ &{κ,i} P -∗ &{κ'} idx_bor_own 1 i ={E}=∗ &{κ ⊓ κ'} P.
+  lft_ctx -∗ &{κ,i} P -∗ &{κ'}(idx_bor_own 1 i) ={E}=∗ &{κ ⊓ κ'} P.
 Proof.
   iIntros (?) "#LFT #HP Hbor".
   rewrite [(&{κ'}_)%I]/bor. iDestruct "Hbor" as (κ'0) "[#Hκ'κ'0 Hbor]".

theories/lifetime/na_borrow.v

@@ -7,8 +7,8 @@ Definition na_bor `{invG Σ, lftG Σ, na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
-Notation "&na{ κ , tid , N } P" := (na_bor κ tid N P)
-  (format "&na{ κ , tid , N }  P", at level 20, right associativity) : uPred_scope.
+Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
+  (format "&na{ κ , tid , N }", at level 20, right associativity) : uPred_scope.
 
 Section na_bor.
   Context `{invG Σ, lftG Σ, na_invG Σ}

theories/typing/lib/cell.v

@@ -12,7 +12,7 @@ Section cell.
   Program Definition cell (ty : type) :=
     {| ty_size := ty.(ty_size);
        ty_own := ty.(ty_own);
-       ty_shr κ tid l := (&na{κ, tid, shrN.@l}l ↦∗: ty.(ty_own) tid)%I |}.
+       ty_shr κ tid l := (&na{κ, tid, shrN.@l}(l ↦∗: ty.(ty_own) tid))%I |}.
   Next Obligation. apply ty_size_eq. Qed.
   Next Obligation.
     iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply (bor_na with "Hown").
@@ -146,7 +146,7 @@ Section typing.
       delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
 
   Lemma cell_replace_type ty `{!TyWf ty} :
-    typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α} cell ty, ty) → ty).
+    typed_val (cell_replace ty) (fn(∀ α, ∅; &shr{α}(cell ty), ty) → ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
@@ -178,7 +178,7 @@ Section typing.
     iMod ("Hclose1" with "Htok HL") as "HL".
     (* Now go back to typing level. *)
     iApply (type_type _ _ _
-           [c ◁ box (&shr{α} cell ty); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
+           [c ◁ box (&shr{α}(cell ty)); #x ◁ box (uninit ty.(ty_size)); #r ◁ box ty]
     with "[] LFT HE Htl HL HC"); last first.
     { rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
       iFrame "Hc". rewrite !tctx_hasty_val' //. iSplitL "Hx↦ Hx†".
@@ -198,17 +198,17 @@ Section typing.
       delete [ #1; "x"];; return: ["r"].
 
   Lemma fake_shared_cell_type ty `{!TyWf ty} :
-    typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α} cell ty).
+    typed_val fake_shared_cell (fn(∀ α, ∅; &uniq{α} ty) → &shr{α}(cell ty)).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
     iIntros (tid) "#LFT #HE Hna HL Hk HT".
     rewrite tctx_interp_singleton tctx_hasty_val.
-    iApply (type_type _ _ _ [ x ◁ box (&uniq{α}cell ty) ]
+    iApply (type_type _ _ _ [ x ◁ box (&uniq{α}(cell ty)) ]
             with "[] LFT HE Hna HL Hk [HT]"); last first.
     { by rewrite tctx_interp_singleton tctx_hasty_val. }
     iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
-    iApply (type_letalloc_1 (&shr{α}cell ty)); [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_letalloc_1 (&shr{α}(cell ty))); [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.

theories/typing/lib/mutex/mutex.v

@@ -34,7 +34,7 @@ Section mutex.
            ⌜∃ b, z = Z_of_bool b⌝ ∗ ty.(ty_own) tid vl'
          | _ => False end;
        ty_shr κ tid l := ∃ κ', κ ⊑ κ' ∗
-           &at{κ, mutexN} (lock_proto l (&{κ'} (l +ₗ 1) ↦∗: ty.(ty_own) tid))
+           &at{κ, mutexN} (lock_proto l (&{κ'}((l +ₗ 1) ↦∗: ty.(ty_own) tid)))
     |}%I.
   Next Obligation.
     iIntros (??[|[[]|]]); try iIntros "[]". rewrite ty_size_eq.
@@ -125,7 +125,6 @@ Section mutex.
     iApply heap_mapsto_pred_iff_proper.
     iAlways; iIntros; iSplit; iIntros; by iApply send_change_tid.
   Qed.
-
 End mutex.
 
 Section code.
@@ -217,7 +216,7 @@ Section code.
       return: ["m"].
 
   Lemma mutex_get_mut_type ty `{!TyWf ty} :
-    typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α} mutex ty) → &uniq{α} ty).
+    typed_val mutex_get_mut (fn(∀ α, ∅; &uniq{α}(mutex ty)) → &uniq{α} ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg); inv_vec arg=>m; simpl_subst.

theories/typing/lib/mutex/mutexguard.v

@@ -35,7 +35,7 @@ Section mguard.
          match vl return _ with
          | [ #(LitLoc l) ] =>
            ∃ β, α ⊑ β ∗
-             &at{α, mutexN} (lock_proto l (&{β} (l +ₗ 1) ↦∗: ty.(ty_own) tid)) ∗
+             &at{α, mutexN} (lock_proto l (&{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid))) ∗
              &{β} ((l +ₗ 1) ↦∗: ty.(ty_own) tid)
          | _ => False end;
        ty_shr κ tid l :=
@@ -136,8 +136,8 @@ Section code.
 
   Lemma mutex_acc E l ty tid q α κ :
     ↑lftN ⊆ E → ↑mutexN ⊆ E →
-    let R := (&{κ} (l +ₗ 1) ↦∗: ty_own ty tid)%I in
-    lft_ctx -∗ &at{α,mutexN} lock_proto l R -∗ α ⊑ κ -∗
+    let R := (&{κ}((l +ₗ 1) ↦∗: ty_own ty tid))%I in
+    lft_ctx -∗ &at{α,mutexN}(lock_proto l R) -∗ α ⊑ κ -∗
     □ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
   Proof.
     (* FIXME: This should work: iIntros (?? R). *) intros ?? R.
@@ -157,7 +157,7 @@ Section code.
       delete [ #1; "mutex" ];; return: ["guard"].
 
   Lemma mutex_lock_type ty `{!TyWf ty} :
-    typed_val mutex_lock (fn(∀ α, ∅; &shr{α} mutex ty) → mutexguard α ty).
+    typed_val mutex_lock (fn(∀ α, ∅; &shr{α}(mutex ty)) → mutexguard α ty).
   Proof.
     intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.

theories/typing/lib/refcell/ref_code.v

@@ -16,7 +16,7 @@ Section ref_functions.
     ∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌝ ∗
             own γ (● Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
             ty.(ty_shr) (α ⊓ ν) tid (l +ₗ 1) ∗
-            ((1).[ν] ={↑lftN,∅}▷=∗ &{α} (l +ₗ 1) ↦∗: ty_own ty tid) ∗
+            ((1).[ν] ={↑lftN,∅}▷=∗ &{α}((l +ₗ 1) ↦∗: ty_own ty tid)) ∗
             ∃ q'', ⌜(q' + q'' = 1)%Qp⌝ ∗ q''.[ν].
   Proof.
     iIntros "INV H◯".
@@ -134,7 +134,7 @@ Section ref_functions.
     iMod ("Hcloseα" with "[$H↦1 $H↦2]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
     iApply (type_type _ _ _
-        [ x ◁ box (&shr{α} ref β ty); #lv ◁ &shr{α}ty]
+        [ x ◁ box (&shr{α}(ref β ty)); #lv ◁ &shr{α}ty]
         with "[] LFT HE Hna HL Hk"); first last.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr"). by iApply lft_incl_glb. }

theories/typing/lib/refcell/refcell.v

@@ -72,8 +72,8 @@ Section refcell_inv.
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α} (l +ₗ 1) ↦∗: ty_own ty1 tid -∗
-                &{α} (l +ₗ 1) ↦∗: ty_own ty2 tid))%I as "#Hb".
+    iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
+                &{α}((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". }

theories/typing/lib/refcell/refmut_code.v

@@ -43,7 +43,7 @@ Section refmut_functions.
     iMod ("Hcloseα1" with "[$H↦1 $H↦2]") as "Hα1".
     iMod ("Hclose''" with "Hβ HL") as "HL". iMod ("Hclose'" with "[$] HL") as "HL".
     iDestruct (lctx_lft_incl_incl α β with "HL HE") as "#Hαβ"; [solve_typing..|].
-    iApply (type_type _ _ _ [ x ◁ box (&shr{α} refmut β ty); #lv ◁ &shr{α}ty]
+    iApply (type_type _ _ _ [ x ◁ box (&shr{α}(refmut β ty)); #lv ◁ &shr{α}ty]
             with "[] LFT HE Hna HL Hk"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
       iFrame. iApply (ty_shr_mono with "[] Hshr'").

theories/typing/lib/rwlock/rwlock.v

@@ -68,8 +68,8 @@ Section rwlock_inv.
     rewrite eqtype_unfold. iIntros (Hty) "HL".
     iDestruct (Hty with "HL") as "#Hty". iIntros "* !# #HE H".
     iDestruct ("Hty" with "HE") as "(% & #Hown & #Hshr)".
-    iAssert (□ (&{α} (l +ₗ 1) ↦∗: ty_own ty1 tid -∗
-                &{α} (l +ₗ 1) ↦∗: ty_own ty2 tid))%I as "#Hb".
+    iAssert (□ (&{α}((l +ₗ 1) ↦∗: ty_own ty1 tid) -∗
+                &{α}((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". }

theories/typing/sum.v

@@ -60,8 +60,8 @@ Section sum.
                                 (nth i tyl emp0).(ty_own) tid vl')%I;
        ty_shr κ tid l :=
          (∃ (i : nat),
-             (&frac{κ} λ q, l ↦{q} #i ∗
-                       (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
+           &frac{κ} (λ q, l ↦{q} #i ∗
+                     (l +ₗ (S $ (nth i tyl emp0).(ty_size))) ↦∗{q}: is_pad i tyl) ∗
                (nth i tyl emp0).(ty_shr) κ tid (l +ₗ 1))%I
     |}.
   Next Obligation.

theories/typing/type.v

@@ -126,8 +126,7 @@ Program Definition ty_of_st `{typeG Σ} (st : simple_type) : type :=
          borrow, otherwise I do not know how to prove the shr part of
          [subtype_shr_mono]. *)
      ty_shr := λ κ tid l,
-               (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗
-                                                 ▷ st.(st_own) tid vl)%I
+               (∃ vl, &frac{κ} (λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
   |}.
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.

theories/typing/uniq_bor.v

@@ -12,7 +12,7 @@ Section uniq_bor.
     {| ty_size := 1;
        ty_own tid vl :=
          match vl return _ with
-         | [ #(LitLoc l) ] => &{κ} l ↦∗: ty.(ty_own) tid
+         | [ #(LitLoc l) ] => &{κ} (l ↦∗: ty.(ty_own) tid)
          | _ => False
          end;
        ty_shr κ' tid l :=

theories/typing/util.v

@@ -27,7 +27,7 @@ Section util.
 
   Lemma delay_sharing_later N κ l ty tid :
     lftE ⊆ N →
-    lft_ctx -∗ &{κ} ▷ l ↦∗: ty_own ty tid ={N}=∗
+    lft_ctx -∗ &{κ}(▷ l ↦∗: ty_own ty tid) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
        ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ tid l ∗ (q).[κ].
   Proof.
@@ -49,7 +49,7 @@ Section util.
 
   Lemma delay_sharing_nested N κ κ' κ'' l ty tid :
     lftE ⊆ N →
-    lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'} &{κ} l ↦∗: ty_own ty tid ={N}=∗
+    lft_ctx -∗ ▷ (κ'' ⊑ κ ⊓ κ') -∗ &{κ'}(&{κ}(l ↦∗: ty_own ty tid)) ={N}=∗
        □ ∀ (F : coPset) (q : Qp),
        ⌜↑shrN ∪ lftE ⊆ F⌝ -∗ (q).[κ''] ={F,F ∖ ↑shrN}▷=∗ ty.(ty_shr) κ'' tid l ∗ (q).[κ''].
   Proof.