Turn CNT into a context in the notation.

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 :
-    ⊢ᵣ clone @: (fn(∀ α : lft, ∅; &shr{α} ty) → ty) →
+    (⊢ᵣ clone @: fn(∀ α : lft, ∅; &shr{α} ty) → ty) →
     ⊢ᵣ rc_make_mut ty clone @: fn(∀ α : lft, ∅; &uniq{α} rc ty) → &uniq{α} ty.
   Proof.
     intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".

theories/typing/programs.v

@@ -78,23 +78,24 @@ Section typing.
   Global Arguments typed_read _ _ _%T _%T _%T.
 End typing.
 
-Notation "'ELFT' E , 'LFT' L , 'TYPE' T ⊢ᵣ e 'CNT' C" :=
+Notation "'ELFT' E , 'LFT' L , 'CNT' C , 'TYPE' T ⊢ᵣ e" :=
   (typed_body E L C T e) (at level 20, e at level 200).
 
 Notation "'ELFT' E , 'LFT' L , 'TYPE' T ⊢ᵣ e ⊣ v , T'" :=
-  (typed_instruction E L T e (λ v, T')) (at level 20, e at level 200).
+  (typed_instruction E L T e (λ v, T'))
+  (at level 20, e at level 200, v at level 0, T' at level 200).
 
 Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : iProp Σ :=
   ELFT E, LFT L, TYPE T ⊢ᵣ e ⊣ v, [v ◁ ty].
 Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 Notation "'ELFT' E , 'LFT' L , 'TYPE' T ⊢ᵣ e @: τ" :=
-  (typed_instruction_ty E L T e τ) (at level 20, e at level 200).
+  (typed_instruction_ty E L T e τ) (at level 20, e, τ at level 200).
 
 Definition typed_val `{typeG Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, typed_instruction_ty E L [] (of_val v) ty.
 Arguments typed_val _ _ _%V _%T.
-Notation "⊢ᵣ v @: τ" := (typed_val v τ) (at level 20, v at level 200).
+Notation "⊢ᵣ v @: τ" := (typed_val v τ) (at level 20, v, τ at level 200).
 
 Section typing_rules.
   Context `{typeG Σ}.
@@ -102,15 +103,15 @@ Section typing_rules.
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
   Lemma type_type E L C T e :
-    ELFT E, LFT L, TYPE T ⊢ᵣ e CNT C -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ e CNT C.
+    (ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ e) -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ e.
   Proof. done. Qed.
 
   (* TODO: Proof a version of this that substitutes into a compatible context...
      if we really want to do that. *)
   Lemma type_equivalize_lft E L C T κ1 κ2 e :
-    ELFT (κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E, LFT L, TYPE T ⊢ᵣ e CNT C -∗
-    ELFT E, LFT (κ1 ⊑ₗ [κ2]) :: L, TYPE T ⊢ᵣ e CNT C.
+    (ELFT (κ1 ⊑ₑ κ2) :: (κ2 ⊑ₑ κ1) :: E, LFT L, CNT C, TYPE T ⊢ᵣ e) -∗
+    ELFT E, LFT (κ1 ⊑ₗ [κ2]) :: L, CNT C, TYPE T ⊢ᵣ e.
   Proof.
     iIntros "He"; iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
     iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
@@ -119,9 +120,9 @@ Section typing_rules.
 
   Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
     Closed (xb :b: []) e' →
-    ELFT E, LFT L, TYPE T1 ⊢ᵣ e ⊣ v, T2 v -∗
-    (∀ v : val, ELFT E, LFT L, TYPE T2 v ++ T ⊢ᵣ subst' xb v e' CNT C) -∗
-    ELFT E, LFT L, TYPE T1 ++ T ⊢ᵣ let: xb := e in e' CNT C.
+    (ELFT E, LFT L, TYPE T1 ⊢ᵣ e ⊣ v, T2 v) -∗
+    (∀ v : val, ELFT E, LFT L, CNT C, TYPE T2 v ++ T ⊢ᵣ subst' xb v e') -∗
+    ELFT E, LFT L, CNT C, TYPE T1 ++ T ⊢ᵣ let: xb := e in e'.
   Proof.
     iIntros (Hc) "He He'". iIntros (tid) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
     iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
@@ -138,10 +139,10 @@ Section typing_rules.
      for the following hypothesis. *)
   Lemma type_let E L T T' T1 T2 C xb e e' :
     Closed (xb :b: []) e' →
-    ELFT E, LFT L, TYPE T1 ⊢ᵣ e ⊣ v, T2 v →
+    (ELFT E, LFT L, TYPE T1 ⊢ᵣ e ⊣ v, T2 v) →
     tctx_extract_ctx E L T1 T T' →
-    (∀ v : val, ELFT E, LFT L, TYPE T2 v ++ T' ⊢ᵣ subst' xb v e' CNT C) -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ let: xb := e in e' CNT C.
+    (∀ v : val, ELFT E, LFT L, CNT C, TYPE T2 v ++ T' ⊢ᵣ subst' xb v e') -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ let: xb := e in e'.
   Proof.
     unfold tctx_extract_ctx. iIntros (? He ->) "?". iApply type_let'; last done.
     iApply He.
@@ -149,16 +150,16 @@ Section typing_rules.
 
   Lemma type_seq E L T T' T1 T2 C e e' :
     Closed [] e' →
-    ELFT E, LFT L, TYPE T1 ⊢ᵣ e ⊣ _, T2 →
+    (ELFT E, LFT L, TYPE T1 ⊢ᵣ e ⊣ _, T2) →
     tctx_extract_ctx E L T1 T T' →
-    ELFT E, LFT L, TYPE T2 ++ T' ⊢ᵣ e' CNT C -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ e ;; e' CNT C.
+    (ELFT E, LFT L, CNT C, TYPE T2 ++ T' ⊢ᵣ e') -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ e ;; e'.
   Proof. iIntros. iApply (type_let E L T T' T1 (λ _, T2)); auto. Qed.
 
   Lemma type_newlft {E L C T} κs e :
     Closed [] e →
-    (∀ κ, ELFT E, LFT (κ ⊑ₗ κs) :: L, TYPE T ⊢ᵣ e CNT C) -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ Newlft ;; e CNT C.
+    (∀ κ, ELFT E, LFT (κ ⊑ₗ κs) :: L, CNT C, TYPE T ⊢ᵣ e) -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ Newlft ;; e.
   Proof.
     iIntros (Hc) "He". iIntros (tid) "#LFT #HE Htl HL HC HT".
     iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
@@ -171,8 +172,8 @@ Section typing_rules.
      Right now, we could take two. *)
   Lemma type_endlft E L C T1 T2 κ κs e :
     Closed [] e → UnblockTctx κ T1 T2 →
-    ELFT E, LFT L, TYPE T2 ⊢ᵣ e CNT C -∗
-    ELFT E, LFT (κ ⊑ₗ κs) :: L, TYPE T1 ⊢ᵣ Endlft ;; e CNT C.
+    (ELFT E, LFT L, CNT C, TYPE T2 ⊢ᵣ e) -∗
+    ELFT E, LFT (κ ⊑ₗ κs) :: L, CNT C, TYPE T1 ⊢ᵣ Endlft ;; e.
   Proof.
     iIntros (Hc Hub) "He". iIntros (tid) "#LFT #HE Htl [Hκ HL] HC HT".
     iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
@@ -194,8 +195,8 @@ Section typing_rules.
   Lemma type_letpath {E L} ty C T T' x p e :
     Closed (x :b: []) e →
     tctx_extract_hasty E L p ty T T' →
-    (∀ v : val, ELFT E, LFT L, TYPE (v ◁ ty) :: T' ⊢ᵣ subst' x v e CNT C) -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ let: x := p in e CNT C.
+    (∀ v : val, ELFT E, LFT L, CNT C, TYPE (v ◁ ty) :: T' ⊢ᵣ subst' x v e) -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ let: x := p in e.
   Proof. iIntros. iApply type_let; [by apply type_path_instr|solve_typing|done]. Qed.
 
   Lemma type_assign_instr {E L} ty ty1 ty1' p1 p2 :
@@ -220,8 +221,8 @@ Section typing_rules.
     Closed [] e →
     tctx_extract_ctx E L [p1 ◁ ty1; p2 ◁ ty] T T' →
     typed_write E L ty1 ty ty1' →
-    ELFT E, LFT L, TYPE (p1 ◁ ty1') :: T' ⊢ᵣ e CNT C -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ p1 <- p2 ;; e CNT C.
+    (ELFT E, LFT L, CNT C, TYPE (p1 ◁ ty1') :: T' ⊢ᵣ e) -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ p1 <- p2 ;; e.
   Proof. iIntros. by iApply type_seq; first apply type_assign_instr. Qed.
 
   Lemma type_deref_instr {E L} ty ty1 ty1' p :
@@ -246,8 +247,8 @@ Section typing_rules.
     tctx_extract_hasty E L p ty1 T T' →
     typed_read E L ty1 ty ty1' →
     ty.(ty_size) = 1%nat →
-    (∀ v : val, ELFT E, LFT L, TYPE (p ◁ ty1') :: (v ◁ ty) :: T' ⊢ᵣ subst' x v e CNT C) -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ let: x := !p in e CNT C.
+    (∀ v : val, ELFT E, LFT L, CNT C, TYPE (p ◁ ty1') :: (v ◁ ty) :: T' ⊢ᵣ subst' x v e) -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ let: x := !p in e.
   Proof. iIntros. by iApply type_let; [apply type_deref_instr|solve_typing|]. Qed.
 
   Lemma type_memcpy_iris E L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
@@ -294,8 +295,8 @@ Section typing_rules.
     typed_write E L ty1 ty ty1' →
     typed_read E L ty2 ty ty2' →
     Z.of_nat (ty.(ty_size)) = n →
-    ELFT E, LFT L, TYPE (p1 ◁ ty1') :: (p2 ◁ ty2') :: T' ⊢ᵣ e CNT C -∗
-    ELFT E, LFT L, TYPE T ⊢ᵣ p1 <-{n} !p2 ;; e CNT C.
+    (ELFT E, LFT L, CNT C, TYPE (p1 ◁ ty1') :: (p2 ◁ ty2') :: T' ⊢ᵣ e) -∗
+    ELFT E, LFT L, CNT C, TYPE T ⊢ᵣ p1 <-{n} !p2 ;; e.
   Proof. iIntros. by iApply type_seq; first eapply (type_memcpy_instr ty ty1 ty1'). Qed.
 End typing_rules.