diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index 54bf50d14663078b722ef13f49cd89e65982e2a4..3b6930650355e84fcbad1e358313045623fc0118 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -18,9 +18,8 @@ Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
-Notation "'case:' e0 'of' [ e1 , .. , en ]" :=
- (Case e0%E (cons e1%E .. (cons en%E nil) ..))
- (e0, e1, en at level 200) : expr_scope.
+Notation "'case:' e0 'of' el" := (Case e0%E el%E)
+ (at level 102, e0, el at level 200) : expr_scope.
Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
(at level 200, e1, e2, e3 at level 200) : expr_scope.
Notation "()" := LitUnit : val_scope.
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index ea832478422d397d89291f9ca198bfe338cca331..580cd631a6b38f19e001c328e8d67e2bc47c10dd 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -25,7 +25,7 @@ Section typing.
Lemma type_if E L C T e1 e2 p:
typed_body E L C T e1 → typed_body E L C T e2 →
- typed_body E L C (TCtx_hasty p bool :: T) (if: p then e1 else e2).
+ typed_body E L C ((p â— bool) :: T) (if: p then e1 else e2).
Proof.
iIntros (He1 He2 tid qE) "#HEAP #LFT Htl HE HL HC".
rewrite tctx_interp_cons. iIntros "[Hp HT]".
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index c61c66963ae838c7a83792787934302fefdd3c95..c9062f75e9480df3c6fb9f808d1f2e87b0e0d1cf 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.base_logic Require Import big_op.
From lrust.lifetime Require Import reborrow frac_borrow.
From lrust.lang Require Import heap.
-From lrust.typing Require Export uniq_bor shr_bor own.
+From lrust.typing Require Export uniq_bor shr_bor own sum.
From lrust.typing Require Import lft_contexts type_context programs.
(** The rules for borrowing and derferencing borrowed non-Copy pointers are in
@@ -13,8 +13,7 @@ Section borrow.
Context `{typeG Σ}.
Lemma tctx_borrow E L p n ty κ :
- tctx_incl E L [TCtx_hasty p (own n ty)]
- [TCtx_hasty p (&uniq{κ}ty); TCtx_blocked p κ (own n ty)].
+ tctx_incl E L [p â— own n ty] [p â— &uniq{κ}ty; p â—{κ} own n ty].
Proof.
iIntros (tid ??) "#LFT $ $ H".
rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
@@ -28,8 +27,7 @@ Section borrow.
Lemma type_deref_uniq_own E L κ p n ty :
lctx_lft_alive E L κ →
- typed_instruction_ty E L [TCtx_hasty p (&uniq{κ} own n ty)] (!p)
- (&uniq{κ} ty).
+ typed_instruction_ty E L [p ◠&uniq{κ} own n ty] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
@@ -52,8 +50,7 @@ Section borrow.
Lemma type_deref_shr_own E L κ p n ty :
lctx_lft_alive E L κ →
- typed_instruction_ty E L [TCtx_hasty p (&shr{κ} own n ty)] (!p)
- (&shr{κ} ty).
+ typed_instruction_ty E L [p ◠&shr{κ} own n ty] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
@@ -70,8 +67,7 @@ Section borrow.
Lemma type_deref_uniq_uniq E L κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- typed_instruction_ty E L [TCtx_hasty p (&uniq{κ} &uniq{κ'} ty)] (!p)
- (&uniq{κ} ty).
+ typed_instruction_ty E L [p ◠&uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
Proof.
iIntros (Hκ Hincl tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
@@ -101,8 +97,7 @@ Section borrow.
Lemma type_deref_shr_uniq E L κ κ' p ty :
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
- typed_instruction_ty E L [TCtx_hasty p (&shr{κ} &uniq{κ'} ty)] (!p)
- (&shr{κ} ty).
+ typed_instruction_ty E L [p ◠&shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
Proof.
iIntros (Hκ Hincl tid eq) "#HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 515c2dd4af4090f6bbff2da232c620a12f651e90..22c26a3add6cda55620915dd72a7892826cf69e0 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -9,7 +9,7 @@ Section typing.
(** Jumping to and defining a continuation. *)
Lemma type_jump E L C T k args T' :
- CCtx_iscont k L _ T' ∈ C →
+ (k â—cont(L, T'))%CC ∈ C →
tctx_incl E L T (T' (list_to_vec args)) →
typed_body E L C T (k (of_val <$> args)).
Proof.
@@ -21,9 +21,9 @@ Section typing.
Lemma type_cont E L1 L2 C T argsb econt e2 T' kb :
Closed (kb :b: argsb +b+ []) econt → Closed (kb :b: []) e2 →
- (∀ k args, typed_body E L1 (CCtx_iscont k L1 _ T' :: C) (T' args)
+ (∀ k args, typed_body E L1 (k â—cont(L1, T') :: C) (T' args)
(subst_v (kb::argsb) (k:::args) econt)) →
- (∀ k, typed_body E L2 (CCtx_iscont k L1 _ T' :: C) T (subst' kb k e2)) →
+ (∀ k, typed_body E L2 (k â—cont(L1, T') :: C) T (subst' kb k e2)) →
typed_body E L2 C T (let: kb := Rec kb argsb econt in e2).
Proof.
iIntros (Hc1 Hc2 Hecont He2 tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 4ba6cdfaa048645115c4ab535ffa27b3f27d078b..4a2aca3903b00501b8011cb1156c9e58026df70c 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -16,11 +16,23 @@ Section cont_context_def.
End cont_context_def.
Add Printing Constructor cctx_elt.
+Delimit Scope lrust_cctx_scope with CC.
+Bind Scope lrust_cctx_scope with cctx cctx_elt.
+
+Notation "k â—cont( L , T )" := (CCtx_iscont k L _ T%TC)
+ (at level 70, format "k â—cont( L , T )") : lrust_cctx_scope.
+Notation "a :: b" := (@cons cctx_elt a%CC b%CC)
+ (at level 60, right associativity) : lrust_cctx_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+ (@cons cctx_elt x1%CC (@cons cctx_elt x2%CC
+ (..(@cons cctx_elt xn%CC (@nil cctx_elt))..))) : lrust_cctx_scope.
+Notation "[ x ]" := (@cons cctx_elt x%CC (@nil cctx_elt)) : lrust_cctx_scope.
+
Section cont_context.
Context `{typeG Σ}.
Definition cctx_elt_interp (tid : thread_id) (x : cctx_elt) : iProp Σ :=
- let 'CCtx_iscont k L n T := x in
+ let '(k â—cont(L, T))%CC := x in
(∀ args, na_own tid ⊤ -∗ llctx_interp L 1 -∗ tctx_interp tid (T args) -∗
WP k (of_val <$> (args : list _)) {{ _, cont_postcondition }})%I.
Definition cctx_interp (tid : thread_id) (C : cctx) : iProp Σ :=
@@ -35,7 +47,7 @@ Section cont_context.
Proof.
rewrite /cctx_interp. iIntros "H". iIntros ([k L n T]) "%".
iIntros (args) "HL HT". iMod "H".
- by iApply ("H" $! (CCtx_iscont k L n T) with "[%] * HL HT").
+ by iApply ("H" $! (k â—cont(L, T)%CC) with "[%] * HL HT").
Qed.
Definition cctx_incl (E : elctx) (C1 C2 : cctx): Prop :=
@@ -56,16 +68,16 @@ Section cont_context.
iApply ("H" with "HE * [%]"). by apply HC1C2.
Qed.
- Lemma cctx_incl_cons E k L n T1 T2 C1 C2:
+ Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → _) C1 C2:
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
- cctx_incl E (CCtx_iscont k L n T1 :: C1) (CCtx_iscont k L n T2 :: C2).
+ cctx_incl E (k â—cont(L, T1) :: C1) (k â—cont(L, T2) :: C2).
Proof.
iIntros (HC1C2 HT1T2 ??) "#LFT H HE". rewrite /cctx_interp.
iIntros (x) "Hin". iDestruct "Hin" as %[->|Hin]%elem_of_cons.
- iIntros (args) "Htl HL HT".
iMod (HT1T2 with "LFT HE HL HT") as "(HE & HL & HT)".
iSpecialize ("H" with "HE").
- iApply ("H" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL HT").
+ iApply ("H" $! (_ â—cont(_, _))%CC with "[%] * Htl HL HT").
constructor.
- iApply (HC1C2 with "LFT [H] HE * [%]"); last done.
iIntros "HE". iIntros (x') "%".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index abd45a4eaf2b7c110f8a4c5622e35245ca2a5377..87d4099009e3a70d632116db785897899a21d29c 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -16,7 +16,7 @@ Section fn.
⌜vl = [@RecV fb (kb::xb) e H]⌠∗ ⌜length xb = n⌠∗
□ ▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
typed_body (E x) []
- [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
+ [kâ—cont([], λ v : vec _ 1, [v!!!0 â— ty x])]
(zip_with (TCtx_hasty ∘ of_val) xl (tys x))
(subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
Next Obligation.
@@ -44,7 +44,7 @@ Section typing.
- iIntros "HE". unfold cctx_interp. iIntros (elt) "Helt".
iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
iSpecialize ("HC" with "HE"). unfold cctx_elt_interp.
- iApply ("HC" $! (CCtx_iscont _ _ _ _) with "[%] * Htl HL >").
+ iApply ("HC" $! (_ â—cont(_, _)%CC) with "[%] * Htl HL >").
{ by apply elem_of_list_singleton. }
rewrite /tctx_interp !big_sepL_singleton /=.
iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
@@ -92,7 +92,7 @@ Section typing.
Lemma fn_subtype_lft_incl {A n} E0 L0 E κ κ' (tys : A → vec type n) ty :
lctx_lft_incl E0 L0 κ κ' →
- subtype E0 L0 (fn (λ x, ELCtx_Incl κ κ' :: E x) tys ty) (fn E tys ty).
+ subtype E0 L0 (fn (λ x, (κ ⊑ κ') :: E x)%EL tys ty) (fn E tys ty).
Proof.
intros Hκκ'. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
@@ -107,8 +107,8 @@ Section typing.
Lemma type_call {A} E L E' T T' p (ps : list path)
(tys : A → vec type (length ps)) ty k x :
tctx_incl E L T (zip_with TCtx_hasty ps (tys x) ++ T') → elctx_sat E L (E' x) →
- typed_body E L [CCtx_iscont k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
- (TCtx_hasty p (fn E' tys ty) :: T) (p (of_val k :: ps)).
+ typed_body E L [k â—cont(L, λ v : vec _ 1, (v!!!0 â— ty x) :: T')]
+ ((p â— fn E' tys ty) :: T) (p (of_val k :: ps)).
Proof.
iIntros (HTsat HEsat tid qE) "#HEAP #LFT Htl HE HL HC".
rewrite tctx_interp_cons. iIntros "[Hf HT]".
@@ -116,7 +116,7 @@ Section typing.
iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
iDestruct "HT" as "[Hargs HT']". clear HTsat.
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = kâŒ):::
- vmap (λ ty (v : val), tctx_elt_interp tid (TCtx_hasty v ty)) (tys x))%I
+ vmap (λ ty (v : val), tctx_elt_interp tid (v ◠ty)) (tys x))%I
with "* [Hargs]"); first wp_done.
- rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
clear dependent ty k p.
@@ -151,8 +151,8 @@ Section typing.
T `{!CopyC T, !SendC T} :
Closed (fb :b: kb :b: argsb +b+ []) e →
(∀ x (f : val) k (args : vec val _),
- typed_body (E' x) [] [CCtx_iscont k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
- (TCtx_hasty f (fn E' tys ty) ::
+ typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— ty x])]
+ ((f â— fn E' tys ty) ::
zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
(subst_v (fb :: kb :: argsb) (f ::: k ::: args) e)) →
typed_instruction_ty E L T (Rec fb (kb :: argsb) e) (fn E' tys ty).
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 407ec159786f842ce0abde2e63ac312f41acf911..1da981dfe92974c2f0104fe245add2af5ab48fba 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -24,7 +24,7 @@ Section typing.
Qed.
Lemma type_plus E L p1 p2 :
- typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 + p2) int.
+ typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 + p2) int.
Proof.
iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
@@ -37,7 +37,7 @@ Section typing.
Qed.
Lemma type_minus E L p1 p2 :
- typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 - p2) int.
+ typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 - p2) int.
Proof.
iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
@@ -50,7 +50,7 @@ Section typing.
Qed.
Lemma type_le E L p1 p2 :
- typed_instruction_ty E L [TCtx_hasty p1 int; TCtx_hasty p2 int] (p1 ≤ p2) bool.
+ typed_instruction_ty E L [p1 ◠int; p2 ◠int] (p1 ≤ p2) bool.
Proof.
iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 47bdfeeeaadbe53623cd0785c8664302f6616126..c927125ab1130e346ff7a1d1a3fc093a7236b665 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -3,31 +3,58 @@ From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import fractional.
From lrust.lifetime Require Export derived.
+Inductive elctx_elt : Type :=
+| ELCtx_Alive (κ : lft)
+| ELCtx_Incl (κ κ' : lft).
+Definition elctx := list elctx_elt.
+
+Delimit Scope lrust_elctx_scope with EL.
+Bind Scope lrust_elctx_scope with elctx elctx_elt.
+
+Notation "☀ κ" := (ELCtx_Alive κ) (at level 70) : lrust_elctx_scope.
+Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
+
+Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
+ (at level 60, right associativity) : lrust_elctx_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+ (@cons elctx_elt x1%EL (@cons elctx_elt x2%EL
+ (..(@cons elctx_elt xn%EL (@nil elctx_elt))..))) : lrust_elctx_scope.
+Notation "[ x ]" := (@cons elctx_elt x%EL (@nil elctx_elt)) : lrust_elctx_scope.
+
+Definition llctx_elt : Type := lft * list lft.
+Definition llctx := list llctx_elt.
+
+Delimit Scope lrust_llctx_scope with LL.
+Bind Scope lrust_llctx_scope with llctx llctx_elt.
+
+Notation "κ ⊠κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
+
+Notation "a :: b" := (@cons llctx_elt a%LL b%LL)
+ (at level 60, right associativity) : lrust_llctx_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+ (@cons llctx_elt x1%LL (@cons llctx_elt x2%LL
+ (..(@cons llctx_elt xn%LL (@nil llctx_elt))..))) : lrust_llctx_scope.
+Notation "[ x ]" := (@cons llctx_elt x%LL (@nil llctx_elt)) : lrust_llctx_scope.
+
Section lft_contexts.
Context `{invG Σ, lftG Σ}.
Implicit Type (κ : lft).
(* External lifetime contexts. *)
-
- Inductive elctx_elt : Type :=
- | ELCtx_Alive κ
- | ELCtx_Incl κ κ'.
- Definition elctx := list elctx_elt.
-
Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
match x with
- | ELCtx_Alive κ => q.[κ]
- | ELCtx_Incl κ κ' => κ ⊑ κ'
- end%I.
+ | ☀ κ => q.[κ]%I
+ | κ ⊑ κ' => (κ ⊑ κ')%I
+ end%EL.
Global Instance elctx_elt_interp_fractional x:
Fractional (elctx_elt_interp x).
Proof. destruct x; unfold elctx_elt_interp; apply _. Qed.
Typeclasses Opaque elctx_elt_interp.
Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
match x with
- | ELCtx_Alive κ => True
- | ELCtx_Incl κ κ' => κ ⊑ κ'
- end%I.
+ | ☀ κ => True%I
+ | κ ⊑ κ' => (κ ⊑ κ')%I
+ end%EL.
Global Instance elctx_elt_interp_0_persistent x:
PersistentP (elctx_elt_interp_0 x).
Proof. destruct x; apply _. Qed.
@@ -69,9 +96,6 @@ Section lft_contexts.
(* Local lifetime contexts. *)
- Definition llctx_elt : Type := lft * list lft.
- Definition llctx := list llctx_elt.
-
Definition llctx_elt_interp (x : llctx_elt) (q : Qp) : iProp Σ :=
let κ' := foldr (∪) static (x.2) in
(∃ κ0, ⌜x.1 = κ' ∪ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={⊤,⊤∖↑lftN}▷=∗ [†κ0]))%I.
@@ -141,7 +165,7 @@ Section lft_contexts.
Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
Proof. iIntros "_ _". iApply lft_incl_static. Qed.
- Lemma lctx_lft_incl_local κ κ' κs : (κ, κs) ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
+ Lemma lctx_lft_incl_local κ κ' κs : (κ ⊠κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
Proof.
iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
@@ -151,7 +175,7 @@ Section lft_contexts.
- etrans. done. apply gmultiset_union_subseteq_r.
Qed.
- Lemma lctx_lft_incl_external κ κ' : ELCtx_Incl κ κ' ∈ E → lctx_lft_incl κ κ'.
+ Lemma lctx_lft_incl_external κ κ' : (κ ⊑ κ')%EL ∈ E → lctx_lft_incl κ κ'.
Proof.
iIntros (?) "H _".
rewrite /elctx_interp_0 /elctx_elt_interp_0 big_sepL_elem_of //. done.
@@ -169,7 +193,7 @@ Section lft_contexts.
Qed.
Lemma lctx_lft_alive_local κ κs:
- (κ, κs) ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
+ (κ ⊠κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
Proof.
iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL ?) "HE HL".
iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
@@ -196,7 +220,7 @@ Section lft_contexts.
rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
Qed.
- Lemma lctx_lft_alive_external κ: ELCtx_Alive κ ∈ E → lctx_lft_alive κ.
+ Lemma lctx_lft_alive_external κ: (☀κ)%EL ∈ E → lctx_lft_alive κ.
Proof.
iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
rewrite /elctx_interp /elctx_elt_interp.
@@ -229,7 +253,7 @@ Section lft_contexts.
Qed.
Lemma elctx_sat_alive E' κ :
- lctx_lft_alive κ → elctx_sat E' → elctx_sat (ELCtx_Alive κ :: E').
+ lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E').
Proof.
iIntros (Hκ HE' qE qL F) "% [HE1 HE2] [HL1 HL2]".
iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
@@ -243,7 +267,7 @@ Section lft_contexts.
Qed.
Lemma elctx_sat_incl E' κ κ' :
- lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat (ELCtx_Incl κ κ' :: E').
+ lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E').
Proof.
iIntros (Hκκ' HE' qE qL F) "% HE HL".
iAssert (κ ⊑ κ')%I with "[#]" as "#Hincl". iApply (Hκκ' with "[HE] [HL]").
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 9bec068d45e5ad765f049ddca8f55c2c2babe4a7..367c3ab7e8e5a7c0ab8d99bd70d2b00a324d0356 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -199,7 +199,7 @@ Section typing.
Lemma type_delete E L n ty p :
n = ty.(ty_size) →
- typed_instruction E L [TCtx_hasty p (own n ty)] (delete [ #n; p])%E (λ _, []).
+ typed_instruction E L [p ◠own n ty] (delete [ #n; p])%E (λ _, []).
Proof.
iIntros (-> tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "_ Hown".
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 54eae3a5dadcf94a75edb7e9c594c00c16169a31..82a97ff6b4e1a11bb355f14c0b94234f37311aa8 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -12,7 +12,7 @@ Section product_split.
Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
match tyl with
| [] => []
- | ty :: tyl => TCtx_hasty (p +â‚— #off) (ptr ty) :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
+ | ty :: tyl => (p +â‚— #off â— ptr ty) :: hasty_ptr_offsets p ptr tyl (off + ty.(ty_size))
end.
Lemma hasty_ptr_offsets_offset (l : loc) p (off1 off2 : nat) ptr tyl tid :
@@ -31,12 +31,10 @@ Section product_split.
Lemma tctx_split_ptr_prod E L ptr tyl :
(∀ p ty1 ty2,
- tctx_incl E L [TCtx_hasty p $ ptr $ product2 ty1 ty2]
- [TCtx_hasty p $ ptr $ ty1;
- TCtx_hasty (p +ₗ #ty1.(ty_size)) $ ptr $ ty2]) →
+ tctx_incl E L [p â— ptr $ product2 ty1 ty2]
+ [p ◠ptr ty1; p +ₗ #ty1.(ty_size) ◠ptr ty2]) →
(∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ) →
- ∀ p, tctx_incl E L [TCtx_hasty p $ ptr $ product tyl]
- (hasty_ptr_offsets p ptr tyl 0).
+ ∀ p, tctx_incl E L [p ◠ptr $ product tyl] (hasty_ptr_offsets p ptr tyl 0).
Proof.
iIntros (Hsplit Hloc p tid q1 q2) "#LFT HE HL H". iInduction tyl as [|ty tyl IH] "IH" forall (p).
{ iFrame "HE HL". rewrite tctx_interp_nil. done. }
@@ -44,7 +42,7 @@ Section product_split.
cbn -[tctx_elt_interp]. rewrite tctx_interp_cons tctx_interp_singleton tctx_interp_cons.
iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp.
iDestruct (Hloc with "Hty") as %[l [=->]].
- iAssert (tctx_elt_interp tid (TCtx_hasty (p +â‚— #0) (ptr ty))) with "[Hty]" as "$".
+ iAssert (tctx_elt_interp tid (p +â‚— #0 â— ptr ty)) with "[Hty]" as "$".
{ iExists #l. iSplit; last done. simpl; by rewrite Hp shift_loc_0. }
iMod ("IH" with "* HE HL [Htyl]") as "($ & $ & Htyl)".
{ rewrite tctx_interp_singleton //. }
@@ -52,14 +50,12 @@ Section product_split.
Qed.
Lemma tctx_merge_ptr_prod E L ptr tyl :
- (Proper (eqtype E L ==> eqtype E L ) ptr) → tyl ≠[] →
+ (Proper (eqtype E L ==> eqtype E L ) ptr) → tyl ≠[] →
(∀ p ty1 ty2,
- tctx_incl E L [TCtx_hasty p $ ptr $ ty1;
- TCtx_hasty (p +â‚— #ty1.(ty_size)) $ ptr $ ty2]
- [TCtx_hasty p $ ptr $ product2 ty1 ty2]) →
+ tctx_incl E L [p â— ptr ty1; p +â‚— #ty1.(ty_size) â— ptr ty2]
+ [p ◠ptr $ product2 ty1 ty2]) →
(∀ tid ty vl, (ptr ty).(ty_own) tid vl -∗ ⌜∃ l : loc, vl = [(#l) : val]âŒ) →
- ∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0)
- [TCtx_hasty p $ ptr $ product tyl].
+ ∀ p, tctx_incl E L (hasty_ptr_offsets p ptr tyl 0) [p ◠ptr $ product tyl].
Proof.
iIntros (Hptr Htyl Hmerge Hloc p tid q1 q2) "#LFT HE HL H". iInduction tyl as [|ty tyl IH] "IH" forall (p Htyl); first done.
rewrite product_cons. rewrite /= tctx_interp_singleton tctx_interp_cons.
@@ -85,9 +81,8 @@ Section product_split.
(** Owned pointers *)
Lemma tctx_split_own_prod2 E L p n ty1 ty2 :
- tctx_incl E L [TCtx_hasty p $ own n $ product2 ty1 ty2]
- [TCtx_hasty p $ own n $ ty1;
- TCtx_hasty (p +â‚— #ty1.(ty_size)) $ own n $ ty2].
+ tctx_incl E L [p â— own n $ product2 ty1 ty2]
+ [p â— own n ty1; p +â‚— #ty1.(ty_size) â— own n ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -106,9 +101,8 @@ Section product_split.
Qed.
Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
- tctx_incl E L [TCtx_hasty p $ own n $ ty1;
- TCtx_hasty (p +â‚— #ty1.(ty_size)) $ own n $ ty2]
- [TCtx_hasty p $ own n $ product2 ty1 ty2].
+ tctx_incl E L [p â— own n ty1; p +â‚— #ty1.(ty_size) â— own n ty2]
+ [p â— own n $ product2 ty1 ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -132,7 +126,7 @@ Section product_split.
Qed.
Lemma tctx_split_own_prod E L n tyl p :
- tctx_incl E L [TCtx_hasty p $ own n $ product tyl]
+ tctx_incl E L [p â— own n $ product tyl]
(hasty_ptr_offsets p (own n) tyl 0).
Proof.
apply tctx_split_ptr_prod.
@@ -141,9 +135,9 @@ Section product_split.
Qed.
Lemma tctx_merge_own_prod E L n tyl :
- tyl ≠[] →
+ tyl ≠[] →
∀ p, tctx_incl E L (hasty_ptr_offsets p (own n) tyl 0)
- [TCtx_hasty p $ own n $ product tyl].
+ [p â— own n $ product tyl].
Proof.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
@@ -153,9 +147,8 @@ Section product_split.
(** Unique borrows *)
Lemma tctx_split_uniq_bor_prod2 E L p κ ty1 ty2 :
- tctx_incl E L [TCtx_hasty p $ uniq_bor κ $ product2 ty1 ty2]
- [TCtx_hasty p $ uniq_bor κ $ ty1;
- TCtx_hasty (p +ₗ #ty1.(ty_size)) $ uniq_bor κ $ ty2].
+ tctx_incl E L [p ◠uniq_bor κ $ product2 ty1 ty2]
+ [p ◠uniq_bor κ ty1; p +ₗ #ty1.(ty_size) ◠uniq_bor κ ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -169,9 +162,8 @@ Section product_split.
Qed.
Lemma tctx_merge_uniq_bor_prod2 E L p κ ty1 ty2 :
- tctx_incl E L [TCtx_hasty p $ uniq_bor κ $ ty1;
- TCtx_hasty (p +ₗ #ty1.(ty_size)) $ uniq_bor κ $ ty2]
- [TCtx_hasty p $ uniq_bor κ $ product2 ty1 ty2].
+ tctx_incl E L [p ◠uniq_bor κ ty1; p +ₗ #ty1.(ty_size) ◠uniq_bor κ ty2]
+ [p ◠uniq_bor κ $ product2 ty1 ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -194,7 +186,7 @@ Section product_split.
Qed.
Lemma tctx_split_uniq_bor_prod E L κ tyl p :
- tctx_incl E L [TCtx_hasty p $ uniq_bor κ $ product tyl]
+ tctx_incl E L [p ◠uniq_bor κ $ product tyl]
(hasty_ptr_offsets p (uniq_bor κ) tyl 0).
Proof.
apply tctx_split_ptr_prod.
@@ -203,9 +195,9 @@ Section product_split.
Qed.
Lemma tctx_merge_uniq_bor_prod E L κ tyl :
- tyl ≠[] →
+ tyl ≠[] →
∀ p, tctx_incl E L (hasty_ptr_offsets p (uniq_bor κ) tyl 0)
- [TCtx_hasty p $ uniq_bor κ $ product tyl].
+ [p ◠uniq_bor κ $ product tyl].
Proof.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
@@ -215,9 +207,8 @@ Section product_split.
(** Shared borrows *)
Lemma tctx_split_shr_bor_prod2 E L p κ ty1 ty2 :
- tctx_incl E L [TCtx_hasty p $ shr_bor κ $ product2 ty1 ty2]
- [TCtx_hasty p $ shr_bor κ $ ty1;
- TCtx_hasty (p +ₗ #ty1.(ty_size)) $ shr_bor κ $ ty2].
+ tctx_incl E L [p ◠shr_bor κ $ product2 ty1 ty2]
+ [p ◠shr_bor κ ty1; p +ₗ #ty1.(ty_size) ◠shr_bor κ ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -228,9 +219,8 @@ Section product_split.
Qed.
Lemma tctx_merge_shr_bor_prod2 E L p κ ty1 ty2 :
- tctx_incl E L [TCtx_hasty p $ shr_bor κ $ ty1;
- TCtx_hasty (p +ₗ #ty1.(ty_size)) $ shr_bor κ $ ty2]
- [TCtx_hasty p $ shr_bor κ $ product2 ty1 ty2].
+ tctx_incl E L [p ◠shr_bor κ ty1; p +ₗ #ty1.(ty_size) ◠shr_bor κ ty2]
+ [p ◠shr_bor κ $ product2 ty1 ty2].
Proof.
iIntros (tid q1 q2) "#LFT $ $ H".
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
@@ -251,7 +241,7 @@ Section product_split.
Qed.
Lemma tctx_split_shr_bor_prod E L κ tyl p :
- tctx_incl E L [TCtx_hasty p $ shr_bor κ $ product tyl]
+ tctx_incl E L [p ◠shr_bor κ $ product tyl]
(hasty_ptr_offsets p (shr_bor κ) tyl 0).
Proof.
apply tctx_split_ptr_prod.
@@ -260,14 +250,13 @@ Section product_split.
Qed.
Lemma tctx_merge_shr_bor_prod E L κ tyl :
- tyl ≠[] →
+ tyl ≠[] →
∀ p, tctx_incl E L (hasty_ptr_offsets p (shr_bor κ) tyl 0)
- [TCtx_hasty p $ shr_bor κ $ product tyl].
+ [p ◠shr_bor κ $ product tyl].
Proof.
intros. apply tctx_merge_ptr_prod; try done.
- apply _.
- intros. apply tctx_merge_shr_bor_prod2.
- intros. apply shr_bor_is_ptr.
Qed.
-
End product_split.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 0a3cd6df74588c5338aaada7f384eae0e6019d82..f84f0d1bfe55fd8ffdcbea2cf87014bf3d9865e8 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -11,25 +11,29 @@ Section typing.
(* This is an iProp because it is also used by the function type. *)
Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
- (∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
+ (∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+ elctx_interp E qE -∗ llctx_interp L 1 -∗
(elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
WP e {{ _, cont_postcondition }})%I.
- Global Arguments typed_body _ _ _ _ _%E.
+ Global Arguments typed_body _%EL _%LL _%CC _%TC _%E.
Instance typed_body_llctx_permut E :
Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
Proof.
- intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
+ intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body.
+ by setoid_rewrite HL.
Qed.
Instance typed_body_elctx_permut :
Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> eq ==> (⊢)) typed_body.
Proof.
- intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HE.
+ intros E1 E2 HE L ? <- C ? <- T ? <- e ? <-. rewrite /typed_body.
+ by setoid_rewrite HE.
Qed.
Instance typed_body_mono E L:
- Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
+ Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢))
+ (typed_body E L).
Proof.
intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
@@ -42,9 +46,10 @@ Section typing.
Definition typed_instruction (E : elctx) (L : llctx)
(T1 : tctx) (e : expr) (T2 : val → tctx) : Prop :=
∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
- elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
- WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}.
- Global Arguments typed_instruction _ _ _ _%E _.
+ elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
+ WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗
+ llctx_interp L 1 ∗ tctx_interp tid (T2 v) }}.
+ Global Arguments typed_instruction _%EL _%LL _%TC _%E _.
(** Writing and Reading **)
Definition typed_write (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
@@ -61,12 +66,15 @@ Section typing.
fraction was given). So we go with the definition that is easier to prove. *)
Definition typed_read (E : elctx) (L : llctx) (ty1 ty ty2 : type) : Prop :=
∀ v tid F qE qL, lftE ∪ (↑lrustN) ⊆ F →
- lft_ctx -∗ na_own tid F -∗ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
+ lft_ctx -∗ na_own tid F -∗
+ elctx_interp E qE -∗ llctx_interp L qL -∗ ty1.(ty_own) tid [v] ={F}=∗
∃ (l : loc) vl q, ⌜v = #l⌠∗ l ↦∗{q} vl ∗ ▷ ty.(ty_own) tid vl ∗
- (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
+ (l ↦∗{q} vl ={F}=∗ na_own tid F ∗ elctx_interp E qE ∗
+ llctx_interp L qL ∗ ty2.(ty_own) tid [v]).
End typing.
-Notation typed_instruction_ty E L T1 e ty := (typed_instruction E L T1 e (λ v : val, [TCtx_hasty v ty])).
+Notation typed_instruction_ty E L T1 e ty :=
+ (typed_instruction E L T1 e (λ v : val, [v ◠ty]%TC)).
Section typing_rules.
Context `{typeG Σ}.
@@ -80,13 +88,14 @@ Section typing_rules.
iIntros (Hc He He' tid qE) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
{ iApply (He with "HEAP LFT Htl HE HL HT1"). }
- iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done. iModIntro.
- iApply (He' with "HEAP LFT Htl HE HL HC [HT2 HT]"). rewrite tctx_interp_app. by iFrame.
+ iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
+ iModIntro. iApply (He' with "HEAP LFT Htl HE HL HC [HT2 HT]").
+ rewrite tctx_interp_app. by iFrame.
Qed.
Lemma typed_newlft E L C T κs e :
Closed [] e →
- (∀ κ, typed_body E ((κ, κs) :: L) C T e) →
+ (∀ κ, typed_body E ((κ ⊠κs) :: L) C T e) →
typed_body E L C T (Newlft ;; e).
Proof.
iIntros (Hc He tid qE) "#HEAP #LFT Htl HE HL HC HT".
@@ -101,7 +110,7 @@ Section typing_rules.
Right now, we could take two. *)
Lemma typed_endlft E L C T1 T2 κ κs e :
Closed [] e → UnblockTctx κ T1 T2 →
- typed_body E L C T2 e → typed_body E ((κ, κs) :: L) C T1 (Endlft ;; e).
+ typed_body E L C T2 e → typed_body E ((κ ⊠κs) :: L) C T1 (Endlft ;; e).
Proof.
iIntros (Hc Hub He tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
@@ -113,8 +122,7 @@ Section typing_rules.
Lemma type_assign E L ty1 ty ty1' p1 p2 :
typed_write E L ty1 ty ty1' →
- typed_instruction E L [TCtx_hasty p1 ty1; TCtx_hasty p2 ty] (p1 <- p2)
- (λ _, [TCtx_hasty p1 ty1']).
+ typed_instruction E L [p1 ◠ty1; p2 ◠ty] (p1 <- p2) (λ _, [p1 ◠ty1']%TC).
Proof.
iIntros (Hwrt tid qE) "#HEAP #LFT $ HE HL".
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
@@ -133,12 +141,13 @@ Section typing_rules.
Lemma type_deref E L ty1 ty ty1' p :
ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
- typed_instruction E L [TCtx_hasty p ty1] (!p)
- (λ v, [TCtx_hasty p ty1'; TCtx_hasty v ty]).
+ typed_instruction E L [p ◠ty1] (!p) (λ v, [p ◠ty1'; v ◠ty]%TC).
Proof.
- iIntros (Hsz Hread tid qE) "#HEAP #LFT Htl HE HL Hp". rewrite tctx_interp_singleton.
- wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v) "% Hown".
- iMod (Hread with "* LFT Htl HE HL Hown") as (l vl q) "(% & Hl & Hown & Hclose)"; first done.
+ iIntros (Hsz Hread tid qE) "#HEAP #LFT Htl HE HL Hp".
+ rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
+ iIntros (v) "% Hown".
+ iMod (Hread with "* LFT Htl HE HL Hown") as
+ (l vl q) "(% & Hl & Hown & Hclose)"; first done.
subst v. iAssert (▷⌜length vl = 1%natâŒ)%I with "[#]" as ">%".
{ rewrite -Hsz. iApply ty_size_eq. done. }
destruct vl as [|v [|]]; try done.
@@ -150,15 +159,17 @@ Section typing_rules.
Lemma type_memcpy E L ty1 ty1' ty2 ty2' ty n p1 p2 :
ty.(ty_size) = n → typed_write E L ty1 ty ty1' → typed_read E L ty2 ty ty2' →
- typed_instruction E L [TCtx_hasty p1 ty1; TCtx_hasty p2 ty2] (p1 <-{n} !p2)
- (λ _, [TCtx_hasty p1 ty1'; TCtx_hasty p2 ty2']).
+ typed_instruction E L [p1 â— ty1; p2 â— ty2] (p1 <-{n} !p2)
+ (λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
iIntros (Hsz Hwrt Hread tid qE) "#HEAP #LFT Htl [HE1 HE2] [HL1 HL2]".
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
- iMod (Hwrt with "* LFT HE1 HL1 Hown1") as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
- iMod (Hread with "* LFT Htl HE2 HL2 Hown2") as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
+ iMod (Hwrt with "* LFT HE1 HL1 Hown1")
+ as (l1 vl1) "([% %] & Hl1 & Hcl1)"; first done.
+ iMod (Hread with "* LFT Htl HE2 HL2 Hown2")
+ as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
iAssert (▷⌜length vl2 = ty.(ty_size)âŒ)%I with "[#]" as ">%".
{ by iApply ty_size_eq. } subst v1 v2. iApply wp_fupd.
iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index be0262334a488a58db7a6a0c1402028c340bc320..3496590a3450e04ff322a1f3fd76dc4a42dc8b85 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -55,8 +55,7 @@ Section typing.
Lemma tctx_reborrow_shr E L p ty κ κ' :
lctx_lft_incl E L κ' κ →
- tctx_incl E L [TCtx_hasty p (&shr{κ}ty)]
- [TCtx_hasty p (&shr{κ'}ty); TCtx_blocked p κ (&shr{κ}ty)].
+ tctx_incl E L [p â— &shr{κ}ty] [p â— &shr{κ'}ty; p â—{κ} &shr{κ}ty].
Proof.
iIntros (Hκκ' tid ??) "#LFT HE HL H".
iDestruct (elctx_interp_persist with "HE") as "#HE'".
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 2ba014a3f202798c7b045db93d21d4adab03fd9f..82706f497c404634f5daf5de5ad616dc1c506458 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -7,6 +7,27 @@ From lrust.typing Require Import type lft_contexts.
Definition path := expr.
Bind Scope expr_scope with path.
+(* TODO: Consider making this a pair of a path and the rest. We could
+ then e.g. formulate tctx_elt_hasty_path more generally. *)
+Inductive tctx_elt `{typeG Σ} : Type :=
+| TCtx_hasty (p : path) (ty : type)
+| TCtx_blocked (p : path) (κ : lft) (ty : type).
+
+Definition tctx `{typeG Σ} := list tctx_elt.
+
+Delimit Scope lrust_tctx_scope with TC.
+Bind Scope lrust_tctx_scope with tctx tctx_elt.
+
+Infix "â—" := TCtx_hasty (at level 70) : lrust_tctx_scope.
+Notation "p â—{ κ } ty" := (TCtx_blocked p κ ty)
+ (at level 70, format "p â—{ κ } ty") : lrust_tctx_scope.
+Notation "a :: b" := (@cons tctx_elt a%TC b%TC)
+ (at level 60, right associativity) : lrust_tctx_scope.
+Notation "[ x1 ; x2 ; .. ; xn ]" :=
+ (@cons tctx_elt x1%TC (@cons tctx_elt x2%TC
+ (..(@cons tctx_elt xn%TC (@nil tctx_elt))..))) : lrust_tctx_scope.
+Notation "[ x ]" := (@cons tctx_elt x%TC (@nil tctx_elt)) : lrust_tctx_scope.
+
Section type_context.
Context `{typeG Σ}.
@@ -42,23 +63,18 @@ Section type_context.
Qed.
(** Type context element *)
- (* TODO: Consider mking this a pair of a path and the rest. We could
- then e.g. formulate tctx_elt_hasty_path more generally. *)
- Inductive tctx_elt : Type :=
- | TCtx_hasty (p : path) (ty : type)
- | TCtx_blocked (p : path) (κ : lft) (ty : type).
-
Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
match x with
- | TCtx_hasty p ty => ∃ v, ⌜eval_path p = Some v⌠∗ ty.(ty_own) tid [v]
- | TCtx_blocked p κ ty => ∃ v, ⌜eval_path p = Some v⌠∗
+ | (p ◠ty)%TC => ∃ v, ⌜eval_path p = Some v⌠∗ ty.(ty_own) tid [v]
+ | (p â—{κ} ty)%TC => ∃ v, ⌜eval_path p = Some v⌠∗
([†κ] ={⊤}=∗ ty.(ty_own) tid [v])
end%I.
+
(* Block tctx_elt_interp from reducing with simpl when x is a constructor. *)
Global Arguments tctx_elt_interp : simpl never.
Lemma tctx_hasty_val tid (v : val) ty :
- tctx_elt_interp tid (TCtx_hasty v ty) ⊣⊢ ty.(ty_own) tid [v].
+ tctx_elt_interp tid (v ◠ty) ⊣⊢ ty.(ty_own) tid [v].
Proof.
rewrite /tctx_elt_interp eval_path_of_val. iSplit.
- iIntros "H". iDestruct "H" as (?) "[EQ ?]".
@@ -68,20 +84,19 @@ Section type_context.
Lemma tctx_elt_interp_hasty_path p1 p2 ty tid :
eval_path p1 = eval_path p2 →
- tctx_elt_interp tid (TCtx_hasty p1 ty) ≡
- tctx_elt_interp tid (TCtx_hasty p2 ty).
+ tctx_elt_interp tid (p1 ◠ty) ≡ tctx_elt_interp tid (p2 ◠ty).
Proof. intros Hp. rewrite /tctx_elt_interp /=. setoid_rewrite Hp. done. Qed.
Lemma tctx_hasty_val' tid p (v : val) ty :
eval_path p = Some v →
- tctx_elt_interp tid (TCtx_hasty p ty) ⊣⊢ ty.(ty_own) tid [v].
+ tctx_elt_interp tid (p ◠ty) ⊣⊢ ty.(ty_own) tid [v].
Proof.
intros ?. rewrite -tctx_hasty_val. apply tctx_elt_interp_hasty_path.
rewrite eval_path_of_val. done.
Qed.
Lemma wp_hasty E tid p ty Φ :
- tctx_elt_interp tid (TCtx_hasty p ty) -∗
+ tctx_elt_interp tid (p ◠ty) -∗
(∀ v, ⌜eval_path p = Some v⌠-∗ ty.(ty_own) tid [v] -∗ Φ v) -∗
WP p @ E {{ Φ }}.
Proof.
@@ -91,8 +106,6 @@ Section type_context.
Qed.
(** Type context *)
- Definition tctx := list tctx_elt.
-
Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
([∗ list] x ∈ T, tctx_elt_interp tid x)%I.
@@ -124,7 +137,7 @@ Section type_context.
Proof. rewrite /CopyC. apply _. Qed.
Global Instance tctx_ty_copy T p ty :
- CopyC T → Copy ty → CopyC (TCtx_hasty p ty :: T).
+ CopyC T → Copy ty → CopyC ((p ◠ty) :: T).
Proof.
(* TODO RJ: Should we have instances that PersistentP respects equiv? *)
intros ???. rewrite /PersistentP tctx_interp_cons.
@@ -139,7 +152,7 @@ Section type_context.
Proof. done. Qed.
Global Instance tctx_ty_send T p ty :
- SendC T → Send ty → SendC (TCtx_hasty p ty :: T).
+ SendC T → Send ty → SendC ((p ◠ty) :: T).
Proof.
iIntros (HT Hty ??). rewrite !tctx_interp_cons.
iIntros "[Hty HT]". iSplitR "HT".
@@ -176,14 +189,14 @@ Section type_context.
Qed.
Lemma copy_tctx_incl E L p `{!Copy ty} :
- tctx_incl E L [TCtx_hasty p ty] [TCtx_hasty p ty; TCtx_hasty p ty].
+ tctx_incl E L [p â— ty] [p â— ty; p â— ty].
Proof.
iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
by iIntros "[#$ $]".
Qed.
Lemma subtype_tctx_incl E L p ty1 ty2 :
- subtype E L ty1 ty2 → tctx_incl E L [TCtx_hasty p ty1] [TCtx_hasty p ty2].
+ subtype E L ty1 ty2 → tctx_incl E L [p ◠ty1] [p ◠ty2].
Proof.
iIntros (Hst ???) "#LFT HE HL H". rewrite /tctx_interp !big_sepL_singleton /=.
iDestruct (elctx_interp_persist with "HE") as "#HE'".
@@ -201,7 +214,7 @@ Section type_context.
Global Instance unblock_tctx_cons_unblock T1 T2 p κ ty :
UnblockTctx κ T1 T2 →
- UnblockTctx κ (TCtx_blocked p κ ty::T1) (TCtx_hasty p ty::T2).
+ UnblockTctx κ ((p â—{κ} ty)::T1) ((p â— ty)::T2).
Proof.
iIntros (H12 tid) "#H†". rewrite !tctx_interp_cons. iIntros "[H HT1]".
iMod (H12 with "H†HT1") as "$". iDestruct "H" as (v) "[% H]".
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 3d21619697f3072b5317c85ff3fce5b703bfc1ac..dc509a109b5a553b24f8aee1d34ecfc4794714b5 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -143,7 +143,7 @@ Section typing.
Context `{typeG Σ}.
Lemma tctx_share E L p κ ty :
- lctx_lft_alive E L κ → tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)] [TCtx_hasty p (&shr{κ}ty)].
+ lctx_lft_alive E L κ → tctx_incl E L [p ◠&uniq{κ}ty] [p ◠&shr{κ}ty].
Proof.
iIntros (Hκ ???) "#LFT HE HL Huniq".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
@@ -158,8 +158,7 @@ Section typing.
Lemma tctx_reborrow_uniq E L p ty κ κ' :
lctx_lft_incl E L κ' κ →
- tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
- [TCtx_hasty p (&uniq{κ'}ty); TCtx_blocked p κ (&uniq{κ}ty)].
+ tctx_incl E L [p â— &uniq{κ}ty] [p â— &uniq{κ'}ty; p â—{κ} &uniq{κ}ty].
Proof.
iIntros (Hκκ' tid ??) "#LFT HE HL H".
iDestruct (elctx_interp_persist with "HE") as "#HE'".