diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 0efccc1614f7ad134586e8fbb2f2c71f48bb9829..a2439938202aa5d985f61186901aa5cb16ae5221 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -5,6 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Module Export lifetime : lifetime_sig.
+ Definition lft := gmultiset positive.
Include definitions.
Include primitive.
Include borrow.
@@ -14,6 +15,8 @@ Module Export lifetime : lifetime_sig.
Include creation.
End lifetime.
+Instance lft_inhabited : Inhabited lft := populate static.
+
Canonical lftC := leibnizC lft.
Section derived.
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 54cddeac8f82078d5dff603ff8b5f2152afff2cf..5245d4e8f77b8af2eb545a07592c496507029a3a 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -9,13 +9,10 @@ Definition borN : namespace := lftN .@ "bor".
Definition inhN : namespace := lftN .@ "inh".
Definition mgmtN : namespace := lftN .@ "mgmt".
-Definition atomic_lft := positive.
-Notation lft := (gmultiset positive).
-Definition static : lft := ∅.
-
Module Type lifetime_sig.
(** CMRAs needed by the lifetime logic *)
- (* We can't instantie the module parameters with inductive types, so we have aliases here. *)
+ (* We can't instantie the module parameters with inductive types, so we
+ have aliases here. *)
Parameter lftG' : gFunctors → Set.
Global Notation lftG := lftG'.
Existing Class lftG'.
@@ -24,6 +21,10 @@ Module Type lifetime_sig.
Existing Class lftPreG'.
(** Definitions *)
+ Parameter lft : Type.
+ Parameter static : lft.
+ Parameter lft_intersect : lft → lft → lft.
+
Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
@@ -47,11 +48,19 @@ Module Type lifetime_sig.
(format "&{ κ , i } P", at level 20, right associativity) : uPred_scope.
Infix "⊑" := lft_incl (at level 70) : uPred_scope.
+ Infix "⊓" := lft_intersect (at level 40) : C_scope.
Section properties.
Context `{invG, lftG Σ}.
(** Instances *)
+ Global Declare Instance lft_intersect_comm : Comm eq lft_intersect.
+ Global Declare Instance lft_intersect_assoc : Assoc eq lft_intersect.
+ Global Declare Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ).
+ Global Declare Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ).
+ Global Declare Instance lft_intersect_left_id : LeftId eq static lft_intersect.
+ Global Declare Instance lft_intersect_right_id : RightId eq static lft_intersect.
+
Global Declare Instance lft_ctx_persistent : PersistentP lft_ctx.
Global Declare Instance lft_dead_persistent κ : PersistentP (lft_dead κ).
Global Declare Instance lft_incl_persistent κ κ' : PersistentP (κ ⊑ κ').
@@ -79,8 +88,8 @@ Module Type lifetime_sig.
AsFractional (idx_bor_own q i) (λ q, idx_bor_own q i)%I q.
(** Laws *)
- Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
- Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ∪ κ2].
+ Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
+ Parameter lft_dead_or : ∀ κ1 κ2, [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ⊓ κ2].
Parameter lft_tok_dead : ∀ q κ, q.[κ] -∗ [†κ] -∗ False.
Parameter lft_tok_static : ∀ q, q.[static]%I.
Parameter lft_dead_static : [†static] -∗ False.
@@ -103,7 +112,7 @@ Module Type lifetime_sig.
Parameter rebor : ∀ E κ κ' P,
↑lftN ⊆ E → lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Parameter bor_unnest : ∀ E κ κ' P,
- ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+ ↑lftN ⊆ E → lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
Parameter bor_unfold_idx : ∀ κ P, &{κ}P ⊣⊢ ∃ i, &{κ,i}P ∗ idx_bor_own 1 i.
@@ -128,14 +137,15 @@ Module Type lifetime_sig.
(* Because Coq's module system is horrible, we have to repeat properties of lft_incl here
unless we want to prove them twice (both here and in model.primitive) *)
- Parameter lft_glb_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
- ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
- Parameter lft_le_incl : ∀ κ κ', κ' ⊆ κ → (κ ⊑ κ')%I.
+ Parameter lft_intersect_acc : ∀ κ κ' q q', q.[κ] -∗ q'.[κ'] -∗
+ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
+ Parameter lft_intersect_incl_l : ∀ κ κ', (κ ⊓ κ' ⊑ κ)%I.
+ Parameter lft_intersect_incl_r : ∀ κ κ', (κ ⊓ κ' ⊑ κ')%I.
Parameter lft_incl_refl : ∀ κ, (κ ⊑ κ)%I.
Parameter lft_incl_trans : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
- Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
- Parameter lft_glb_mono : ∀ κ1 κ1' κ2 κ2',
- κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+ Parameter lft_incl_glb : ∀ κ κ' κ'', κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
+ Parameter lft_intersect_mono : ∀ κ1 κ1' κ2 κ2',
+ κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ⊓ κ2 ⊑ κ1' ⊓ κ2'.
Parameter lft_incl_acc : ∀ E κ κ' q,
↑lftN ⊆ E → κ ⊑ κ' -∗ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
Parameter lft_incl_dead : ∀ E κ κ', ↑lftN ⊆ E → κ ⊑ κ' -∗ [†κ'] ={E}=∗ [†κ].
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 77e8b58838c19d1e037370566254aca845dadee1..94d545f501c7ae9e74c56a166a88071923895695 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -136,9 +136,9 @@ Lemma bor_combine E κ P Q :
Proof.
iIntros (?) "#LFT HP HQ". rewrite {1 2}/bor.
iDestruct "HP" as (κ1) "[#Hκ1 Hbor1]". iDestruct "HQ" as (κ2) "[#Hκ2 Hbor2]".
- iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor1") as "[Hbor1 _]".
+ iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor1") as "[Hbor1 _]".
done. by apply gmultiset_union_subseteq_l.
- iMod (raw_rebor _ _ (κ1 ∪ κ2) with "LFT Hbor2") as "[Hbor2 _]".
+ iMod (raw_rebor _ _ (κ1 ⊓ κ2) with "LFT Hbor2") as "[Hbor2 _]".
done. by apply gmultiset_union_subseteq_r.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose". unfold raw_bor, idx_bor_own.
iDestruct "Hbor1" as (j1) "[Hbor1 Hslice1]". iDestruct "Hbor2" as (j2) "[Hbor2 Hslice2]".
@@ -177,7 +177,7 @@ Proof.
-fmap_None -lookup_fmap !fmap_delete //. }
rewrite own_bor_op. iDestruct "Hbor" as "[Hâ— Hâ—¯]".
iAssert (&{κ}(P ∗ Q))%I with "[H◯ Hslice]" as "$".
- { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ∪ κ2).
+ { rewrite /bor /raw_bor /idx_bor_own. iExists (κ1 ⊓ κ2).
iSplit; first by iApply (lft_incl_glb with "Hκ1 Hκ2").
iExists γ. iFrame. iExists _. iFrame. iNext. iAlways.
by iSplit; iIntros "[HP HQ]"; iSplitL "HP"; (iApply "HPP'" || iApply "HQQ'"). }
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 9c81827977c89c8191b22f8961516d4061be3fab..7ee2738816323458d685fedf126842a133d8fe6d 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -6,6 +6,19 @@ From lrust.lifetime Require Export lifetime_sig.
Set Default Proof Using "Type".
Import uPred.
+Definition atomic_lft := positive.
+(* HACK : We need to make sure this is not in the top-level context,
+ so that it does not conflict with the *definition* of [lft] that we
+ use in lifetime.v. *)
+Module Export lft_notation.
+ Notation lft := (gmultiset atomic_lft).
+End lft_notation.
+
+Definition static : lft := (∅ : gmultiset _).
+Definition lft_intersect (κ κ' : lft) : lft := κ ∪ κ'.
+
+Infix "⊓" := lft_intersect (at level 40) : C_scope.
+
Inductive bor_state :=
| Bor_in
| Bor_open (q : frac)
@@ -67,7 +80,6 @@ Definition to_alftUR : gmap atomic_lft bool → alftUR := fmap to_lft_stateR.
Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,) ∘ to_agree).
-
Section defs.
Context `{invG Σ, lftG Σ}.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index cc70c535dc8759fe1a6b15aa14a3e189d3d1102e..1d64078131b75ffdc53ffdbb8597bb3ddc9b12d0 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -218,7 +218,7 @@ Qed.
Lemma lft_dead_in_insert_false' A κ Λ : Λ ∈ κ → lft_dead_in (<[Λ:=false]> A) κ.
Proof. exists Λ. by rewrite lookup_insert. Qed.
Lemma lft_dead_in_alive_in_union A κ κ' :
- lft_dead_in A (κ ∪ κ') → lft_alive_in A κ → lft_dead_in A κ'.
+ lft_dead_in A (κ ⊓ κ') → lft_alive_in A κ → lft_dead_in A κ'.
Proof.
intros (Λ & [Hin|Hin]%elem_of_union & HΛ) Halive.
- contradict HΛ. rewrite (Halive _ Hin). done.
@@ -261,13 +261,20 @@ Proof.
Qed.
(** Basic rules about lifetimes *)
-Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ∪ κ2].
+Instance lft_intersect_comm : Comm eq lft_intersect := _.
+Instance lft_intersect_assoc : Assoc eq lft_intersect := _.
+Instance lft_intersect_inj_1 κ : Inj eq eq (lft_intersect κ) := _.
+Instance lft_intersect_inj_2 κ : Inj eq eq (λ κ', lft_intersect κ' κ) := _.
+Instance lft_intersect_left_id : LeftId eq static lft_intersect := _.
+Instance lft_intersect_right_id : RightId eq static lft_intersect := _.
+
+Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
Proof. by rewrite /lft_tok -big_sepMS_union. Qed.
-Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ∪ κ2].
+Lemma lft_dead_or κ1 κ2 : [†κ1] ∨ [†κ2] ⊣⊢ [†κ1 ⊓ κ2].
Proof.
rewrite /lft_dead -or_exist. apply exist_proper=> Λ.
- rewrite -sep_or_r -pure_or. do 2 f_equiv. set_solver.
+ rewrite -sep_or_r -pure_or. do 2 f_equiv. unfold lft_intersect. set_solver.
Qed.
Lemma lft_tok_dead q κ : q.[κ] -∗ [†κ] -∗ False.
@@ -325,16 +332,19 @@ Lemma lft_incl_intro κ κ' :
(lft_dead κ' ={↑lftN}=∗ lft_dead κ)) -∗ κ ⊑ κ'.
Proof. reflexivity. Qed.
-Lemma lft_le_incl κ κ' : κ' ⊆ κ → (κ ⊑ κ')%I.
+Lemma lft_intersect_incl_l κ κ': (κ ⊓ κ' ⊑ κ)%I.
Proof.
- iIntros (->%gmultiset_union_difference) "!#". iSplitR.
+ iIntros "!#". iSplitR.
- iIntros (q). rewrite <-lft_tok_sep. iIntros "[H Hf]". iExists q. iFrame.
rewrite <-lft_tok_sep. by iIntros "!>{$Hf}$".
- iIntros "? !>". iApply lft_dead_or. auto.
Qed.
+Lemma lft_intersect_incl_r κ κ': (κ ⊓ κ' ⊑ κ')%I.
+Proof. rewrite comm. apply lft_intersect_incl_l. Qed.
+
Lemma lft_incl_refl κ : (κ ⊑ κ)%I.
-Proof. by apply lft_le_incl. Qed.
+Proof. iIntros "!#"; iSplitR; auto 10 with iFrame. Qed.
Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' -∗ κ' ⊑ κ'' -∗ κ ⊑ κ''.
Proof.
@@ -347,8 +357,8 @@ Proof.
- iIntros "H†". iMod ("H2†" with "H†"). by iApply "H1†".
Qed.
-Lemma lft_glb_acc κ κ' q q' :
- q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ∪ κ'] ∗ (q''.[κ ∪ κ'] -∗ q.[κ] ∗ q'.[κ']).
+Lemma lft_intersect_acc κ κ' q q' :
+ q.[κ] -∗ q'.[κ'] -∗ ∃ q'', q''.[κ ⊓ κ'] ∗ (q''.[κ ⊓ κ'] -∗ q.[κ] ∗ q'.[κ']).
Proof.
iIntros "Hκ Hκ'".
destruct (Qp_lower_bound q q') as (qq & q0 & q'0 & -> & ->).
@@ -356,27 +366,25 @@ Proof.
iDestruct "Hκ" as "[$$]". iDestruct "Hκ'" as "[$$]". auto.
Qed.
-Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ∪ κ''.
+Lemma lft_incl_glb κ κ' κ'' : κ ⊑ κ' -∗ κ ⊑ κ'' -∗ κ ⊑ κ' ⊓ κ''.
Proof.
rewrite /lft_incl. iIntros "#[H1 H1†] #[H2 H2†]!#". iSplitR.
- iIntros (q) "[Hκ'1 Hκ'2]".
iMod ("H1" with "Hκ'1") as (q') "[Hκ' Hclose']".
iMod ("H2" with "Hκ'2") as (q'') "[Hκ'' Hclose'']".
- iDestruct (lft_glb_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
+ iDestruct (lft_intersect_acc with "Hκ' Hκ''") as (qq) "[Hqq Hclose]".
iExists qq. iFrame. iIntros "!> Hqq".
iDestruct ("Hclose" with "Hqq") as "[Hκ' Hκ'']".
iMod ("Hclose'" with "Hκ'") as "$". by iApply "Hclose''".
- rewrite -lft_dead_or. iIntros "[H†|H†]". by iApply "H1†". by iApply "H2†".
Qed.
-Lemma lft_glb_mono κ1 κ1' κ2 κ2' :
- κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ∪ κ2 ⊑ κ1' ∪ κ2'.
+Lemma lft_intersect_mono κ1 κ1' κ2 κ2' :
+ κ1 ⊑ κ1' -∗ κ2 ⊑ κ2' -∗ κ1 ⊓ κ2 ⊑ κ1' ⊓ κ2'.
Proof.
iIntros "#H1 #H2". iApply (lft_incl_glb with "[]").
- - iApply (lft_incl_trans with "[] H1").
- iApply lft_le_incl. apply gmultiset_union_subseteq_l.
- - iApply (lft_incl_trans with "[] H2").
- iApply lft_le_incl. apply gmultiset_union_subseteq_r.
+ - iApply (lft_incl_trans with "[] H1"). iApply lft_intersect_incl_l.
+ - iApply (lft_incl_trans with "[] H2"). iApply lft_intersect_incl_r.
Qed.
(** Basic rules about borrows *)
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 14b4c53de88002d58dfea60fa8e033eeccfd64e6..22c8f50333fcb4bcdd755f66156bfa308227c36f 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -27,10 +27,10 @@ Lemma rebor E κ κ' P :
lft_ctx -∗ κ' ⊑ κ -∗ &{κ}P ={E}=∗ &{κ'}P ∗ ([†κ'] ={E}=∗ &{κ}P).
Proof.
iIntros (?) "#LFT #H⊑". rewrite {1}/bor; iDestruct 1 as (κ'') "[#H⊑' Hκ'']".
- iMod (raw_rebor _ _ (κ' ∪ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
+ iMod (raw_rebor _ _ (κ' ⊓ κ'') with "LFT Hκ''") as "[Hκ'' Hclose]"; first done.
{ apply gmultiset_union_subseteq_r. }
iModIntro. iSplitL "Hκ''".
- - rewrite /bor. iExists (κ' ∪ κ''). iFrame "Hκ''".
+ - rewrite /bor. iExists (κ' ⊓ κ''). iFrame "Hκ''".
iApply (lft_incl_glb with "[]"); first iApply lft_incl_refl.
by iApply (lft_incl_trans with "H⊑").
- iIntros "Hκ†". iMod ("Hclose" with "[Hκ†]") as "Hκ''".
@@ -40,7 +40,7 @@ Qed.
Lemma bor_unnest E κ κ' P :
↑lftN ⊆ E →
- lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ∪ κ'} P.
+ lft_ctx -∗ &{κ'} &{κ} P ={E, E∖↑lftN}▷=∗ &{κ ⊓ κ'} P.
Proof.
iIntros (?) "#LFT Hκ". rewrite {2}/bor.
iMod (bor_exists with "LFT Hκ") as (κ0) "Hκ"; first done.
@@ -50,7 +50,7 @@ Proof.
{ iModIntro. iNext. iMod "Hclose" as "_". iApply (bor_fake with "LFT"); first done.
iApply lft_dead_or. iRight. done. }
iMod ("Hclose" with "Hκ⊑") as "_".
- set (κ'' := κ0 ∪ κ0').
+ set (κ'' := κ0 ⊓ κ0').
iMod (raw_rebor _ _ κ'' with "LFT Hκ") as "[Hκ _]"; first done.
{ apply gmultiset_union_subseteq_r. }
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
@@ -68,7 +68,7 @@ Proof.
iNext. iMod "Hclose" as "_".
iApply (bor_fake with "LFT >"); first done.
iApply (lft_incl_dead with "[] H†"); first done.
- by iApply (lft_glb_mono with "Hκ⊑"). }
+ by iApply (lft_intersect_mono with "Hκ⊑"). }
rewrite {1}/raw_bor /idx_bor_own /=; iDestruct "Hκ" as (i) "[Hi #Hislice]".
iDestruct "Hislice" as (P') "[#HPP' Hislice]".
rewrite lft_inv_alive_unfold;
@@ -100,6 +100,6 @@ Proof.
iFrame. rewrite /lft_inv lft_inv_alive_unfold. iLeft.
iFrame "%". iExists Pb'', Pi. iFrame. }
iModIntro. rewrite /bor. iExists κ''. iFrame. subst κ''.
- by iApply (lft_glb_mono with "Hκ⊑").
+ by iApply (lft_intersect_mono with "Hκ⊑").
Qed.
End reborrow.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 90bda2528a158dbbadb9ca20005e2d6d0bb8bea1..65b4e4fcce33b9742805dd504c2f3a2831fa36fd 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -144,7 +144,7 @@ Section borrow.
wp_apply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hshr"; try done.
iDestruct "Hshr" as (l') "[H↦ Hown]".
iMod (frac_bor_acc with "LFT H↦ Htok1") as (q'') "[>H↦ Hclose']". done.
- iAssert (κ ⊑ κ' ∪ κ)%I as "#Hincl'".
+ iAssert (κ ⊑ κ' ⊓ κ)%I as "#Hincl'".
{ iApply (lft_incl_glb with "Hincl []"). iApply lft_incl_refl. }
iMod (lft_incl_acc with "Hincl' Htok2") as (q2) "[Htok2 Hclose'']". solve_ndisj.
iApply (wp_fupd_step _ (_∖_) with "[Hown Htok2]"); try done.
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 99ceda8626896827b87f2f7b34229e80cc42767e..1eabd4e3b07504b63bc5d67d016c50a7ce5096ee 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -12,7 +12,7 @@ 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. *)
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index f1e7aaa443fdd1ca5991d043b96d1290a17dd313..b9b5734349158ee2b98410293564479866e26e48 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -12,7 +12,7 @@ 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.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index eb1d163e141832ab4309373a00c1262b558759db..b09e8af19d3c4cdce5a834ec74a6f9f55d3517fb 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -8,40 +8,66 @@ Set Default Proof Using "Type".
Section fn.
Context `{typeG Σ} {A : Type} {n : nat}.
- Program Definition fn (E : A → elctx)
- (tys : A → vec type n) (ty : A → type) : type :=
+ Record fn_params := FP { fp_tys : vec type n; fp_ty : type; fp_E : elctx }.
+
+ Program Definition fn (fp : A → fn_params) : type :=
{| st_own tid vl := (∃ fb kb xb e H,
⌜vl = [@RecV fb (kb::xb) e H]⌠∗ ⌜length xb = n⌠∗
▷ ∀ (x : A) (k : val) (xl : vec val (length xb)),
- â–¡ typed_body (E x) []
- [kâ—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
+ â–¡ typed_body (fp x).(fp_E) []
+ [kâ—cont([], λ v : vec _ 1, [v!!!0 â— box (fp x).(fp_ty)])]
(zip_with (TCtx_hasty ∘ of_val) xl
- (box <$> (vec_to_list (tys x))))
+ (box <$> (vec_to_list (fp x).(fp_tys))))
(subst_v (fb::kb::xb) (RecV fb (kb::xb) e:::k:::xl) e))%I |}.
Next Obligation.
- iIntros (E tys ty tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
+ iIntros (fp tid vl) "H". iDestruct "H" as (fb kb xb e ?) "[% _]". by subst.
Qed.
- Global Instance fn_send E tys ty : Send (fn E tys ty).
+ Global Instance fn_send fp : Send (fn fp).
Proof. iIntros (tid1 tid2 vl). done. Qed.
- Lemma fn_type_contractive n' E :
- Proper (pointwise_relation A (B := vec type n) (Forall2 (type_dist2_later n')) ==>
- pointwise_relation A (type_dist2_later n') ==> type_dist2 n') (fn E).
+ Definition fn_params_rel (ty_rel : relation type) : relation fn_params :=
+ λ fp1 fp2,
+ Forall2 ty_rel fp2.(fp_tys) fp1.(fp_tys) ∧ ty_rel fp1.(fp_ty) fp2.(fp_ty) ∧
+ fp1.(fp_E) = fp2.(fp_E).
+
+ Global Instance fp_tys_proper R :
+ Proper (flip (fn_params_rel R) ==> (Forall2 R : relation (vec _ _))) fp_tys.
+ Proof. intros ?? HR. apply HR. Qed.
+ Global Instance fp_tys_proper_flip R :
+ Proper (fn_params_rel R ==> flip (Forall2 R : relation (vec _ _))) fp_tys.
+ Proof. intros ?? HR. apply HR. Qed.
+
+ Global Instance fp_ty_proper R :
+ Proper (fn_params_rel R ==> R) fp_ty.
+ Proof. intros ?? HR. apply HR. Qed.
+
+ Global Instance fp_E_proper R :
+ Proper (fn_params_rel R ==> eq) fp_E.
+ Proof. intros ?? HR. apply HR. Qed.
+
+ Global Instance FP_proper R :
+ Proper (flip (Forall2 R : relation (vec _ _)) ==> R ==> eq ==> fn_params_rel R) FP.
+ Proof. by split; [|split]. Qed.
+
+ Global Instance fn_type_contractive n' :
+ Proper (pointwise_relation A (fn_params_rel (type_dist2_later n')) ==>
+ type_dist2 n') fn.
Proof.
- intros ?? Htys ?? Hty. apply ty_of_st_type_ne. destruct n'; first done.
+ intros fp1 fp2 Hfp. apply ty_of_st_type_ne. destruct n'; first done.
constructor; simpl.
(* TODO: 'f_equiv' is slow here because reflexivity is slow. *)
(* The clean way to do this would be to have a metric on type contexts. Oh well. *)
intros tid vl. unfold typed_body.
- do 12 f_equiv. f_contractive. do 17 f_equiv.
+ do 12 f_equiv. f_contractive. do 17 (apply Hfp || f_equiv).
+ - f_equiv. apply Hfp.
- rewrite !cctx_interp_singleton /=. do 5 f_equiv.
- rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hty || f_equiv).
+ rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hfp || f_equiv).
- rewrite /tctx_interp !big_sepL_zip_with /=. do 3 f_equiv.
cut (∀ n tid p i, Proper (dist n ==> dist n)
(λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌠→ tctx_elt_interp tid (p ◠ty))%I).
{ intros Hprop. apply Hprop, list_fmap_ne; last first.
- - eapply Forall2_impl; first exact: Htys. intros.
+ - symmetry. eapply Forall2_impl; first apply Hfp. intros.
apply dist_later_dist, type_dist2_dist_later. done.
- apply _. }
clear. intros n tid p i x y. rewrite list_dist_lookup=>Hxy.
@@ -57,52 +83,65 @@ Section fn.
* iIntros "H". by iApply "H".
* iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
Qed.
- Global Existing Instance fn_type_contractive.
- Global Instance fn_ne n' E :
- Proper (pointwise_relation A (dist n') ==>
- pointwise_relation A (dist n') ==> dist n') (fn E).
+ Global Instance fn_ne n' :
+ Proper (pointwise_relation A (fn_params_rel (dist n')) ==> dist n') fn.
Proof.
- intros ?? H1 ?? H2. apply dist_later_dist, type_dist2_dist_later.
- apply fn_type_contractive=>u; simpl.
- - eapply Forall2_impl; first exact: H1. intros. simpl.
+ intros ?? Hfp. apply dist_later_dist, type_dist2_dist_later.
+ apply fn_type_contractive=>u. split; last split.
+ - eapply Forall2_impl; first apply Hfp. intros. simpl.
apply type_dist_dist2. done.
- - apply type_dist_dist2. apply H2.
+ - apply type_dist_dist2. apply Hfp.
+ - apply Hfp.
Qed.
End fn.
-(* TODO: Once we depend on 8.6pl1, extend this to recursive binders so that
- patterns like '(a, b) can be used. *)
-Notation "'fn(∀' x ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
- (fn (λ x, E%EL) (λ x, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ x, R%T))
- (at level 99, R at level 200,
- format "'fn(∀' x ',' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
-Notation "'fn(∀' x ',' E ')' '→' R" :=
- (fn (λ x, E%EL) (λ x, Vector.nil) (λ x, R%T))
- (at level 99, R at level 200,
- format "'fn(∀' x ',' E ')' '→' R") : lrust_type_scope.
+Arguments fn_params {_ _} _.
+
+(* The parameter of [FP] are in the wrong order in order to make sure
+ that type-checking is done in that order, so that the [ELCtx_Alive]
+ is taken as a coercion. We reestablish the intuitive order with
+ [FP'] *)
+Notation FP' E tys ty := (FP tys ty E).
+
+(* We use recursive notation for binders as well, to allow patterns
+ like '(a, b) to be used. In practice, only one binder is ever used,
+ but using recursive binders is the only way to make Coq accept
+ patterns. *)
+(* FIXME : because of a bug in Coq, such patterns only work for
+ printing. Once on 8.6pl1, this should work. *)
+Notation "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R" :=
+ (fn (λ x, (.. (λ x',
+ FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T R%T)..)))
+ (at level 99, R at level 200, x binder, x' binder,
+ format "'fn(∀' x .. x' ',' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
+Notation "'fn(∀' x .. x' ',' E ')' '→' R" :=
+ (fn (λ x, (.. (λ x', FP' E%EL Vector.nil R%T)..)))
+ (at level 99, R at level 200, x binder, x' binder,
+ format "'fn(∀' x .. x' ',' E ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R" :=
- (fn (λ _:(), E%EL) (λ _, (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..)%T) (λ _, R%T))
+ (fn (λ _:(), FP' E%EL (Vector.cons T1 .. (Vector.cons TN Vector.nil) ..) R%T))
(at level 99, R at level 200,
format "'fn(' E ';' T1 ',' .. ',' TN ')' '→' R") : lrust_type_scope.
Notation "'fn(' E ')' '→' R" :=
- (fn (λ _:(), E%EL) (λ _, Vector.nil) (λ _, R%T))
+ (fn (λ _:(), FP' E%EL Vector.nil R%T))
(at level 99, R at level 200,
format "'fn(' E ')' '→' R") : lrust_type_scope.
Section typing.
Context `{typeG Σ}.
- Lemma fn_subtype_full {A n} E0 L0 E E' (tys tys' : A → vec type n) ty ty' :
- (∀ x, elctx_incl E0 L0 (E x) (E' x)) →
- (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys' x) (tys x)) →
- (∀ x, subtype (E0 ++ E x) L0 (ty x) (ty' x)) →
- subtype E0 L0 (fn E' tys ty) (fn E tys' ty').
+ Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
+ (∀ x, elctx_incl E0 L0 (fp' x).(fp_E) (fp x).(fp_E)) →
+ (∀ x, Forall2 (subtype (E0 ++ (fp' x).(fp_E)) L0)
+ (fp' x).(fp_tys) (fp x).(fp_tys)) →
+ (∀ x, subtype (E0 ++ (fp' x).(fp_E)) L0 (fp x).(fp_ty) (fp' x).(fp_ty)) →
+ subtype E0 L0 (fn fp) (fn fp').
Proof.
intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
iIntros "#HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
- rewrite /typed_body. iIntros "* !# * #LFT Htl HE HL HC HT".
+ rewrite /typed_body. iIntros (x k xl) "!# * #LFT Htl HE HL HC HT".
iDestruct (elctx_interp_persist with "HE") as "#HEp".
iMod (HE with "HE0 HL0 HE") as (qE') "[HE' Hclose]". done.
iApply ("Hf" with "LFT Htl HE' HL [HC Hclose] [HT]").
@@ -114,14 +153,15 @@ Section typing.
{ by apply elem_of_list_singleton. }
rewrite /tctx_interp !big_sepL_singleton /=.
iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
- assert (Hst : subtype (E0 ++ E x) L0 (box (ty x)) (box (ty' x)))
+ assert (Hst : subtype (E0 ++ (fp' x).(fp_E)) L0
+ (box (fp x).(fp_ty)) (box (fp' x).(fp_ty)))
by by rewrite ->Hty.
iDestruct (Hst with "[HE0 HEp] HL0") as "(_ & Hty & _)".
{ rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
by iApply "Hty".
- rewrite /tctx_interp
- -(fst_zip (tys x) (tys' x)) ?vec_to_list_length //
- -{1}(snd_zip (tys x) (tys' x)) ?vec_to_list_length //
+ -(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+ -{1}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
!zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
iApply big_sepL_impl. iSplit; last done. iIntros "{HT}!#".
iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
@@ -129,58 +169,43 @@ Section typing.
rewrite !lookup_zip_with.
iDestruct "Hzip" as %(? & ? & ([? ?] & (? & Hty'1 &
(? & Hty'2 & [=->->])%bind_Some)%bind_Some & [=->->->])%bind_Some)%bind_Some.
- specialize (Htys x). eapply Forall2_lookup_lr in Htys; try done.
- assert (Hst : subtype (E0 ++ E x) L0 (box ty2') (box ty1'))
+ eapply Forall2_lookup_lr in Htys; try done.
+ assert (Hst : subtype (E0 ++ (fp' x).(fp_E)) L0 (box ty2') (box ty1'))
by by rewrite ->Htys.
iDestruct (Hst with "[] []") as "(_ & #Ho & _)"; [ |done|].
{ rewrite /elctx_interp_0 big_sepL_app. by iSplit. }
by iApply "Ho".
Qed.
- Lemma fn_subtype_ty {A n} E0 L0 E (tys1 tys2 : A → vec type n) ty1 ty2 :
- (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x) (tys1 x)) →
- (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
- subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
- Proof. intros. by apply fn_subtype_full. Qed.
-
(* This proper and the next can probably not be inferred, but oh well. *)
- Global Instance fn_subtype_ty' {A n} E0 L0 E :
- Proper (flip (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (subtype E0 L0) v1 v2)) ==>
- pointwise_relation A (subtype E0 L0) ==> subtype E0 L0) (fn E).
+ Global Instance fn_subtype' {A n} E0 L0 :
+ Proper (pointwise_relation A (fn_params_rel (n:=n) (subtype E0 L0)) ==>
+ subtype E0 L0) fn.
Proof.
- intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
- - intros. eapply Forall2_impl; first eapply Htys. intros ??.
+ intros fp1 fp2 Hfp. apply fn_subtype=>x; destruct (Hfp x) as (Htys & Hty & HE).
+ - by rewrite HE.
+ - eapply Forall2_impl; first eapply Htys. intros ??.
eapply subtype_weaken; last done. by apply submseteq_inserts_r.
- - intros. eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
- Qed.
-
- Global Instance fn_eqtype_ty' {A n} E0 L0 E :
- Proper (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (eqtype E0 L0) v1 v2) ==>
- pointwise_relation A (eqtype E0 L0) ==> eqtype E0 L0) (fn E).
- Proof.
- intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty);
- intros x; (apply Forall2_flip + idtac); (eapply Forall2_impl; first by eapply (Htys x)); by intros ??[].
- Qed.
-
- Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
- (∀ x, elctx_sat (E x) [] (E' x)) →
- subtype E0 L0 (fn E' tys ty) (fn E tys ty).
- Proof.
- intros. apply fn_subtype_full; try done. by intros; apply elctx_sat_incl.
+ - eapply subtype_weaken, Hty; last done. by apply submseteq_inserts_r.
Qed.
- 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, (κ ⊑ κ') :: E x)%EL tys ty) (fn E tys ty).
+ Global Instance fn_eqtype' {A n} E0 L0 :
+ Proper (pointwise_relation A (fn_params_rel (n:=n) (eqtype E0 L0)) ==>
+ eqtype E0 L0) fn.
Proof.
- intros Hκκ'. apply fn_subtype_full; try done. intros.
- apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
- iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
- rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[$ _]".
+ intros fp1 fp2 Hfp. split; eapply fn_subtype=>x; destruct (Hfp x) as (Htys & Hty & HE).
+ - by rewrite HE.
+ - eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
+ eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
+ - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
+ - by rewrite HE.
+ - symmetry in Htys. eapply Forall2_impl; first eapply Htys. intros t1 t2 Ht.
+ eapply subtype_weaken; last apply Ht; last done. by apply submseteq_inserts_r.
+ - eapply subtype_weaken; last apply Hty; last done. by apply submseteq_inserts_r.
Qed.
- Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :
- subtype E0 L0 (fn (n:=n) E tys ty) (fn (E ∘ σ) (tys ∘ σ) (ty ∘ σ)).
+ Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 fp :
+ subtype E0 L0 (fn (n:=n) fp) (fn (fp ∘ σ)).
Proof.
apply subtype_simple_type=>//= _ vl.
iIntros "_ _ Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
@@ -188,12 +213,12 @@ Section typing.
rewrite /typed_body. iNext. iIntros "*". iApply "Hf".
Qed.
- Lemma type_call' {A} E L E' T p (ps : list path)
- (tys : A → vec type (length ps)) ty k x :
- elctx_sat E L (E' x) →
- typed_body E L [k â—cont(L, λ v : vec _ 1, (v!!!0 â— box (ty x)) :: T)]
- ((p â— fn E' tys ty) ::
- zip_with TCtx_hasty ps (box <$> (vec_to_list (tys x))) ++
+ Lemma type_call' {A} E L T p (ps : list path)
+ (fp : A → fn_params (length ps)) k x :
+ elctx_sat E L (fp x).(fp_E) →
+ typed_body E L [k â—cont(L, λ v : vec _ 1, (v!!!0 â— box (fp x).(fp_ty)) :: T)]
+ ((p â— fn fp) ::
+ zip_with TCtx_hasty ps (box <$> (vec_to_list (fp x).(fp_tys))) ++
T)
(call: p ps → k).
Proof.
@@ -201,10 +226,10 @@ Section typing.
rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = kâŒ):::
- vmap (λ ty (v : val), tctx_elt_interp tid (v ◠box ty)) (tys x))%I
+ vmap (λ ty (v : val), tctx_elt_interp tid (v ◠box ty)) (fp x).(fp_tys))%I
with "[Hargs]"); first wp_done.
- rewrite /= big_sepL_cons. iSplitR "Hargs"; first by iApply wp_value'.
- clear dependent ty k p.
+ clear dependent k p.
rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
(zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
@@ -212,8 +237,8 @@ Section typing.
- simpl. change (@length expr ps) with (length ps).
iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
- iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl tys.
- rewrite <-EQl=>vl tys. iApply wp_rec; try done.
+ iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl fp HE.
+ rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
{ rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
iNext. iSpecialize ("Hf" $! x k vl).
@@ -231,14 +256,14 @@ Section typing.
iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
Qed.
- Lemma type_call {A} x E L E' C T T' T'' p (ps : list path)
- (tys : A → vec type (length ps)) ty k :
- (p ◠fn E' tys ty)%TC ∈ T →
- elctx_sat E L (E' x) →
+ Lemma type_call {A} x E L C T T' T'' p (ps : list path)
+ (fp : A → fn_params (length ps)) k :
+ (p ◠fn fp)%TC ∈ T →
+ elctx_sat E L (fp x).(fp_E) →
tctx_extract_ctx E L (zip_with TCtx_hasty ps
- (box <$> vec_to_list (tys x))) T T' →
+ (box <$> vec_to_list (fp x).(fp_tys))) T T' →
(k â—cont(L, T''))%CC ∈ C →
- (∀ ret : val, tctx_incl E L ((ret ◠box (ty x))::T') (T'' [# ret])) →
+ (∀ ret : val, tctx_incl E L ((ret ◠box (fp x).(fp_ty))::T') (T'' [# ret])) →
typed_body E L C T (call: p ps → k).
Proof.
intros Hfn HE HTT' HC HT'T''.
@@ -249,18 +274,18 @@ Section typing.
apply copy_elem_of_tctx_incl; last done. apply _.
Qed.
- Lemma type_letcall {A} x E L E' C T T' p (ps : list path)
- (tys : A → vec type (length ps)) ty b e :
+ Lemma type_letcall {A} x E L C T T' p (ps : list path)
+ (fp : A → fn_params (length ps)) b e :
Closed (b :b: []) e → Closed [] p → Forall (Closed []) ps →
- (p ◠fn E' tys ty)%TC ∈ T →
- elctx_sat E L (E' x) →
+ (p ◠fn fp)%TC ∈ T →
+ elctx_sat E L (fp x).(fp_E) →
tctx_extract_ctx E L (zip_with TCtx_hasty ps
- (box <$> vec_to_list (tys x))) T T' →
- (∀ ret : val, typed_body E L C ((ret ◠box (ty x))::T') (subst' b ret e)) -∗
+ (box <$> vec_to_list (fp x).(fp_tys))) T T' →
+ (∀ ret : val, typed_body E L C ((ret ◠box (fp x).(fp_ty))::T') (subst' b ret e)) -∗
typed_body E L C T (letcall: b := p ps in e).
Proof.
iIntros (?? Hpsc ???) "He".
- iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◠box (ty x)) :: T')%TC).
+ iApply (type_cont_norec [_] _ (λ r, (r!!!0 ◠box (fp x).(fp_ty)) :: T')%TC).
- (* TODO : make [solve_closed] work here. *)
eapply is_closed_weaken; first done. set_solver+.
- (* TODO : make [solve_closed] work here. *)
@@ -283,19 +308,19 @@ Section typing.
apply incl_cctx_incl. set_solver+.
Qed.
- Lemma type_rec {A} E L E' fb (argsb : list binder) ef e n
- (tys : A → vec type n) ty
- T `{!CopyC T, !SendC T} :
+ Lemma type_rec {A} E L fb (argsb : list binder) ef e n
+ (fp : A → fn_params n) T `{!CopyC T, !SendC T} :
ef = (funrec: fb argsb := e)%E →
n = length argsb →
Closed (fb :b: "return" :b: argsb +b+ []) e →
□ (∀ x (f : val) k (args : vec val (length argsb)),
- typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
- ((f â— fn E' tys ty) ::
+ typed_body (fp x).(fp_E) []
+ [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (fp x).(fp_ty)])]
+ ((f â— fn fp) ::
zip_with (TCtx_hasty ∘ of_val) args
- (box <$> vec_to_list (tys x)) ++ T)
+ (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
(subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) -∗
- typed_instruction_ty E L T ef (fn E' tys ty).
+ typed_instruction_ty E L T ef (fn fp).
Proof.
iIntros (-> -> Hc) "#Hbody". iIntros (tid qE) " #LFT $ $ $ #HT". iApply wp_value.
{ simpl. rewrite ->(decide_left Hc). done. }
@@ -308,23 +333,23 @@ Section typing.
by iApply sendc_change_tid.
Qed.
- Lemma type_fn {A} E L E' (argsb : list binder) ef e n
- (tys : A → vec type n) ty
- T `{!CopyC T, !SendC T} :
+ Lemma type_fn {A} E L (argsb : list binder) ef e n
+ (fp : A → fn_params n) T `{!CopyC T, !SendC T} :
ef = (funrec: <> argsb := e)%E →
n = length argsb →
Closed ("return" :b: argsb +b+ []) e →
□ (∀ x k (args : vec val (length argsb)),
- typed_body (E' x) [] [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (ty x)])]
+ typed_body (fp x).(fp_E) []
+ [k â—cont([], λ v : vec _ 1, [v!!!0 â— box (fp x).(fp_ty)])]
(zip_with (TCtx_hasty ∘ of_val) args
- (box <$> vec_to_list (tys x)) ++ T)
+ (box <$> vec_to_list (fp x).(fp_tys)) ++ T)
(subst_v (BNamed "return" :: argsb) (k ::: args) e)) -∗
- typed_instruction_ty E L T ef (fn E' tys ty).
+ typed_instruction_ty E L T ef (fn fp).
Proof.
iIntros (???) "#He". iApply type_rec; try done. iIntros "!# *".
- (iApply typed_body_mono; last by iApply "He"); try done.
+ iApply typed_body_mono; last iApply "He"; try done.
eapply contains_tctx_incl. by constructor.
Qed.
End typing.
-Hint Resolve fn_subtype_full : lrust_typing.
+Hint Resolve fn_subtype : lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 0cd42e35de775dd360a44a12485826dc9ff79a1b..9ee1956b82c9f16dd453f4d91a7a73a1cfaeb6d2 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -16,7 +16,7 @@ Delimit Scope lrust_elctx_scope with EL.
notations, so we have to use [Arguments] everywhere. *)
Bind Scope lrust_elctx_scope with elctx_elt.
-Notation "☀ κ" := (ELCtx_Alive κ) (at level 70) : lrust_elctx_scope.
+Coercion ELCtx_Alive : lft >-> elctx_elt.
Infix "⊑" := ELCtx_Incl (at level 70) : lrust_elctx_scope.
Notation "a :: b" := (@cons elctx_elt a%EL b%EL)
@@ -48,7 +48,7 @@ Section lft_contexts.
(* External lifetime contexts. *)
Definition elctx_elt_interp (x : elctx_elt) (q : Qp) : iProp Σ :=
match x with
- | ☀ κ => q.[κ]%I
+ | ELCtx_Alive κ => q.[κ]%I
| κ ⊑ κ' => (κ ⊑ κ')%I
end%EL.
Global Instance elctx_elt_interp_fractional x:
@@ -57,7 +57,7 @@ Section lft_contexts.
Typeclasses Opaque elctx_elt_interp.
Definition elctx_elt_interp_0 (x : elctx_elt) : iProp Σ :=
match x with
- | ☀ κ => True%I
+ | ELCtx_Alive κ => True%I
| κ ⊑ κ' => (κ ⊑ κ')%I
end%EL.
Global Instance elctx_elt_interp_0_persistent x:
@@ -104,8 +104,8 @@ Section lft_contexts.
(* Local lifetime contexts. *)
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.
+ let κ' := foldr lft_intersect static (x.2) in
+ (∃ κ0, ⌜x.1 = κ' ⊓ κ0⌠∗ q.[κ0] ∗ □ (1.[κ0] ={↑lftN,∅}▷=∗ [†κ0]))%I.
Global Instance llctx_elt_interp_fractional x :
Fractional (llctx_elt_interp x).
Proof.
@@ -115,13 +115,13 @@ Section lft_contexts.
- iDestruct "H" as "[Hq Hq']".
iDestruct "Hq" as (κ0) "(% & Hq & #?)".
iDestruct "Hq'" as (κ0') "(% & Hq' & #?)". simpl in *.
- rewrite (inj (union (foldr (∪) static κs)) κ0' κ0); last congruence.
+ rewrite (inj (lft_intersect (foldr lft_intersect static κs)) κ0' κ0); last congruence.
iExists κ0. by iFrame "∗%".
Qed.
Typeclasses Opaque llctx_elt_interp.
Definition llctx_elt_interp_0 (x : llctx_elt) : Prop :=
- let κ' := foldr (∪) static (x.2) in (∃ κ0, x.1 = κ' ∪ κ0).
+ let κ' := foldr lft_intersect static (x.2) in (∃ κ0, x.1 = κ' ⊓ κ0).
Lemma llctx_elt_interp_persist x q :
llctx_elt_interp x q -∗ ⌜llctx_elt_interp_0 xâŒ.
Proof.
@@ -164,8 +164,7 @@ Section lft_contexts.
iMod (bor_fracture (λ q, (qL * q).[_])%I with "LFT [Hκ]") as "#Hκ"; first done.
{ rewrite Qp_mult_1_r. done. }
iModIntro. subst κ1. iSplit.
- - iApply lft_le_incl.
- rewrite <-!gmultiset_union_subseteq_l. done.
+ - iApply lft_incl_trans; iApply lft_intersect_incl_l.
- iApply (lft_incl_glb with "[]"); first iApply (lft_incl_glb with "[]").
+ iApply lft_incl_refl.
+ iApply lft_incl_static.
@@ -212,10 +211,10 @@ Section lft_contexts.
Proof.
iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
- iApply lft_le_incl. etrans; last by apply gmultiset_union_subseteq_l.
+ iApply lft_incl_trans; first iApply lft_intersect_incl_l.
clear -Hκ'κs. induction Hκ'κs.
- - apply gmultiset_union_subseteq_l.
- - etrans. done. apply gmultiset_union_subseteq_r.
+ - iApply lft_intersect_incl_l.
+ - iApply lft_incl_trans; last done. iApply lft_intersect_incl_r.
Qed.
Lemma lctx_lft_incl_local' κ κ' κ'' κs :
@@ -250,8 +249,8 @@ Section lft_contexts.
iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
iDestruct (big_sepL_lookup_acc with "HL2") as "[Hκ Hclose]". done.
iDestruct "Hκ" as (κ0) "(EQ & Htok & #Hend)". simpl. iDestruct "EQ" as %->.
- iAssert (∃ q', q'.[foldr union static κs] ∗
- (q'.[foldr union static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
+ iAssert (∃ q', q'.[foldr lft_intersect static κs] ∗
+ (q'.[foldr lft_intersect static κs] ={F}=∗ elctx_interp E qE ∗ llctx_interp L (qL / 2)))%I
with ">[HE HL1]" as "H".
{ move:(qL/2)%Qp=>qL'. clear HL. iClear "Hend".
iInduction Hκs as [|κ κs Hκ ?] "IH" forall (qE qL').
@@ -271,7 +270,7 @@ Section lft_contexts.
rewrite /llctx_interp /llctx_elt_interp. iApply "Hclose". iExists κ0. iFrame. auto.
Qed.
- Lemma lctx_lft_alive_external κ: (☀κ)%EL ∈ E → lctx_lft_alive κ.
+ Lemma lctx_lft_alive_external κ: (ELCtx_Alive κ) ∈ E → lctx_lft_alive κ.
Proof.
iIntros ([i HE]%elem_of_list_lookup_1 F qE qL ?) "HE $ !>".
rewrite /elctx_interp /elctx_elt_interp.
@@ -292,7 +291,7 @@ Section lft_contexts.
Qed.
Lemma lctx_lft_alive_external' κ κ':
- (☀κ)%EL ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
+ (ELCtx_Alive κ) ∈ E → (κ ⊑ κ')%EL ∈ E → lctx_lft_alive κ'.
Proof.
intros. eapply lctx_lft_alive_incl, lctx_lft_incl_external; last done.
by apply lctx_lft_alive_external.
@@ -311,7 +310,7 @@ Section lft_contexts.
Qed.
Lemma elctx_sat_alive E' κ :
- lctx_lft_alive κ → elctx_sat E' → elctx_sat ((☀κ) :: E')%EL.
+ lctx_lft_alive κ → elctx_sat E' → elctx_sat (κ :: E')%EL.
Proof.
iIntros (Hκ HE' qE qL F ?) "[HE1 HE2] [HL1 HL2]".
iMod (Hκ with "HE1 HL1") as (q) "[Htok Hclose]". done.
@@ -431,7 +430,7 @@ Section elctx_incl.
Qed.
Lemma elctx_incl_lft_alive E1 E2 κ :
- lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
+ lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 (κ :: E2).
Proof.
intros Hκ HE2. rewrite (elctx_incl_dup E1).
apply (elctx_incl_app_proper _ [_]); last done.
@@ -482,7 +481,7 @@ Hint Opaque elctx_incl elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
- elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
+ elctx_incl E L (κ :: E1) (κ' :: E2).
Proof.
move=> ? /elctx_incl_lft_incl -> //.
apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index dcbc8431edb0c9147f19048fbaf03ac433204be9..bfbe7e4a91905491e35bf52c7e601dbf53a4a711 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -109,7 +109,7 @@ Section typing.
funrec: <> ["x"] := "return" ["x"].
Lemma cell_get_mut_type ty :
- typed_val cell_get_mut (fn(∀ α, [☀α]; &uniq{α} (cell ty)) → &uniq{α} ty).
+ typed_val cell_get_mut (fn(∀ α, [α]; &uniq{α} (cell ty)) → &uniq{α} ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -126,7 +126,7 @@ Section typing.
delete [ #1; "x"];; "return" ["r"].
Lemma cell_get_type `(!Copy ty) :
- typed_val (cell_get ty) (fn(∀ α, [☀α]; &shr{α} (cell ty)) → ty).
+ typed_val (cell_get ty) (fn(∀ α, [α]; &shr{α} (cell ty)) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -146,7 +146,7 @@ Section typing.
delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
Lemma cell_replace_type 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. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>c x. simpl_subst.
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index fedb4a378512c896faea3d4a87ec04b211ce52ad..b0dc67a558d4accbdd0ba5fb31421beda63448f4 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -11,9 +11,8 @@ Section fake_shared_box.
Lemma cell_replace_type ty :
typed_val fake_shared_box
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &shr{α}(&shr{β} ty)]%T)
- (fun '(α, β) => &shr{α}box ty)%T).
+ (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.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 279a0e79457bce404b93ac7a83eb93a0e42677c9..10e930a39231a85d2f813aa7aec005decd8d81c4 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -19,7 +19,7 @@ Section option.
Lemma option_as_mut_type Ï„ :
typed_val
- option_as_mut (fn(∀ α, [☀α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
+ option_as_mut (fn(∀ α, [α]; &uniq{α} (option τ)) → option (&uniq{α}τ)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
inv_vec p=>o. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 9fe6e746df7a57d49015b129963d21c956123759..839c173b979cbaf85a5ebb76675a9496d68d3c2f 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -24,7 +24,7 @@ Section ref.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
- ∃ ν q γ β ty', ty.(ty_shr) (α ∪ ν) tid lv ∗
+ ∃ ν q γ β ty', ty.(ty_shr) (α ⊓ ν) tid lv ∗
α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
q.[ν] ∗ own γ (◯ reading_st q ν)
| _ => False
@@ -32,7 +32,7 @@ Section ref.
ty_shr κ tid l :=
∃ ν q γ β ty' (lv lrc : loc),
κ ⊑ ν ∗ &frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
- ▷ ty.(ty_shr) (α ∪ ν) tid lv ∗
+ ▷ ty.(ty_shr) (α ⊓ ν) tid lv ∗
▷ (α ⊑ β) ∗ ▷ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
&na{κ, tid, refcell_refN}(own γ (◯ reading_st q ν)) |}%I.
Next Obligation. iIntros (???[|[[]|][|[[]|][]]]) "?"; auto. Qed.
@@ -85,12 +85,12 @@ Section ref.
iDestruct "H" as (ν q γ β ty') "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
iExists ν, q, γ, β, ty'. iFrame "∗#". iSplit.
+ iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H". iDestruct "H" as (ν q γ β ty' lv lrc) "H".
iExists ν, q, γ, β, ty', lv, lrc. iDestruct "H" as "#($&$&?&?&$&$)". iSplit.
+ iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
Qed.
Global Instance ref_mono_flip E L :
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e2858d9359a39e60df0553583f85bc11f7718334..c1012db9e85a6547a405cad6804de80b72e5f486 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -15,7 +15,7 @@ Section ref_functions.
own γ (◯ reading_st q ν) -∗
∃ (q' : Qp) n, l ↦ #(Zpos n) ∗ ⌜(q ≤ q')%Qc⌠∗
own γ (◠Some (to_agree ν, Cinr (q', n)) ⋅ ◯ reading_st q ν) ∗
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
((1).[ν] ={↑lftN,∅}▷=∗ &{α} shift_loc l 1 ↦∗: ty_own ty tid) ∗
∃ q'', ⌜(q' + q'' = 1)%Qp⌠∗ q''.[ν].
Proof.
@@ -56,8 +56,7 @@ Section ref_functions.
See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
Lemma ref_clone_type ty :
typed_val ref_clone
- (fn (fun '(α, β) => [☀α; ☀β])%EL (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
- (fun '(α, β) => ref β ty)%T).
+ (fn (fun '(α, β) => FP' [α; β]%EL [# &shr{α}(ref β ty)]%T (ref β ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -117,9 +116,7 @@ Section ref_functions.
Lemma ref_deref_type ty :
typed_val ref_deref
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &shr{α}(ref β ty)]%T)
- (fun '(α, β) => &shr{α}ty)%T).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -156,7 +153,7 @@ Section ref_functions.
let: "r" := new [ #0] in "return" ["r"].
Lemma ref_drop_type ty :
- typed_val ref_drop (fn(∀ α, [☀α]; ref α ty) → unit).
+ typed_val ref_drop (fn(∀ α, [α]; ref α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -221,7 +218,8 @@ Section ref_functions.
Lemma ref_map_type ty1 ty2 envty E :
typed_val ref_map
- (fn(∀ β, [☀β] ++ E; ref β ty1, fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
+ (fn(∀ β, [β]%EL ++ E;
+ ref β ty1, fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2, envty)
→ ref β ty2).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret arg).
@@ -240,10 +238,10 @@ Section ref_functions.
iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
- iApply (type_type ((☀ (α ∪ ν)) :: E)%EL []
- [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&shr{α ∪ ν}ty2)])]%CC
- [ f ◠box (fn(∀ α, [☀α] ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
- #lref ◠own_ptr 2 (&shr{α ∪ ν}ty1); env ◠box envty ]%TC
+ iApply (type_type ((α ⊓ ν) :: E)%EL []
+ [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&shr{α ⊓ ν}ty2)])]%CC
+ [ f ◠box (fn(∀ α, [α]%EL ++ E; envty, &shr{α}ty1) → &shr{α}ty2);
+ #lref ◠own_ptr 2 (&shr{α ⊓ ν}ty1); env ◠box envty ]%TC
with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index aa8ee23e2da8bb2a90f5ad154dc0c26fd27287e2..9523a646d1cc8b399bc36c815a3313c4b5f68848 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -43,7 +43,7 @@ Section refcell_inv.
match st with
| Cinr (q, n) =>
(* Immutably borrowed. *)
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
∃ q', ⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]
| _ => (* Mutably borrowed. *) True
end
@@ -51,8 +51,9 @@ Section refcell_inv.
Global Instance refcell_inv_type_ne n tid l γ α :
Proper (type_dist2 n ==> dist n) (refcell_inv tid l γ α).
- Proof.
- solve_proper_core ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
+ Proof.
+ solve_proper_core
+ ltac:(fun _ => exact: type_dist2_S || f_type_equiv || f_contractive || f_equiv).
Qed.
Global Instance refcell_inv_ne tid l γ α : NonExpansive (refcell_inv tid l γ α).
@@ -135,9 +136,9 @@ Section refcell.
iMod (own_alloc (◠Some (to_agree ν, Cinr ((1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
- iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ { iApply lft_intersect_incl_l. }
+ iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _. iIntros "{$Hshr}".
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index d807fb209e78c4ec6f2a3bf6c5cafea4a587c043..f5e4931519f6d41333b7e0cb38a90c9037609a92 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -20,8 +20,7 @@ Section refcell_functions.
delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
Lemma refcell_new_type ty :
- typed_val (refcell_new ty)
- (fn (λ _, []) (λ _, [# ty]) (λ _:(), refcell ty)).
+ typed_val (refcell_new ty) (fn([]; ty) → refcell ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -58,8 +57,7 @@ Section refcell_functions.
delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
Lemma refcell_into_inner_type ty :
- typed_val (refcell_into_inner ty)
- (fn (λ _, []) (λ _, [# refcell ty]) (λ _:(), ty)).
+ typed_val (refcell_into_inner ty) (fn([]; refcell ty) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -93,8 +91,7 @@ Section refcell_functions.
"return" ["x"].
Lemma refcell_get_mut_type ty :
- typed_val refcell_get_mut
- (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (refcell ty)])%T (λ α, &uniq{α} ty)%T).
+ typed_val refcell_get_mut (fn(∀ α, [α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -143,8 +140,7 @@ Section refcell_functions.
delete [ #1; "x"];; "return" ["r"].
Lemma refcell_try_borrow_type ty :
- typed_val refcell_try_borrow
- (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (ref α ty))%T).
+ typed_val refcell_try_borrow (fn(∀ α, [α] ; &shr{α}(refcell ty)) → option (ref α ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -178,7 +174,7 @@ Section refcell_functions.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iDestruct "Hlref" as "[Hlref0 Hlref1]". wp_op. wp_write. wp_op. wp_write.
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
- ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
+ ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
own γ (◯ reading_st qν ν) ∗ refcell_inv tid lx γ β ty)%I
with ">[Hlx Hownst Hst Hβtok2]" as (q' ν) "(Hβtok2 & Hν & Hshr & Hreading & INV)".
{ destruct st as [[agν [|[q n]|]]|]; try done.
@@ -201,10 +197,10 @@ Section refcell_functions.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
- iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+ iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". done.
+ { iApply lft_intersect_incl_l. }
iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". done. iFrame "Hshr".
iDestruct ("Hclose" with "Htok") as "[$ Htok2]". iExists _. iFrame.
iExists _. iSplitR; first done. iFrame "Hshr". iSplitR "Htok2".
@@ -220,7 +216,7 @@ Section refcell_functions.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. iExists _, _, _, _, _. iFrame "∗#". iApply ty_shr_mono; try by auto.
- iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono. done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [unit; ref α ty]); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
@@ -249,7 +245,7 @@ Section refcell_functions.
Lemma refcell_try_borrow_mut_type ty :
typed_val refcell_try_borrow_mut
- (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(refcell ty)]%T) (λ α, option (refmut α ty))%T).
+ (fn(∀ α, [α]; &shr{α}(refcell ty)) → option (refmut α ty))%T.
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -279,8 +275,8 @@ Section refcell_functions.
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ (writing_st ν)). }
iApply fupd_wp. iApply (fupd_mask_mono (↑lftN)); first done.
- iMod (rebor _ _ (β ∪ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hb") as "[Hb Hbh]". done.
+ { iApply lft_intersect_incl_l. }
iModIntro. iMod ("Hclose'" with "[Hlx Hownst Hbh] Hna") as "[Hβtok Hna]".
{ iExists _. iFrame. iExists ν. iSplit; first by auto. iNext. iSplitL; last by auto.
iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
@@ -292,7 +288,7 @@ Section refcell_functions.
rewrite tctx_hasty_val' //. rewrite /= freeable_sz_full. iFrame.
iExists [_; _]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
iFrame. iExists _, _, _, _. iFrame "#∗". iApply (bor_shorten with "[] [$Hb]").
- iApply lft_glb_mono; first done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [unit; refmut α ty]); [solve_typing..|].
simpl. iApply type_delete; [solve_typing..|].
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index bc9e076c94dd1cbde4ff947d818b54d47cf5355c..a5f90e56a84653914110efa55ed94d6e2da3a961 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -24,7 +24,7 @@ Section refmut.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc lv); #(LitLoc lrc) ] =>
- ∃ ν γ β ty', &{α ∪ ν}(lv ↦∗: ty.(ty_own) tid) ∗
+ ∃ ν γ β ty', &{α ⊓ ν}(lv ↦∗: ty.(ty_own) tid) ∗
α ⊑ β ∗ &na{β, tid, refcell_invN}(refcell_inv tid lrc γ β ty') ∗
1.[ν] ∗ own γ (◯ writing_st ν)
| _ => False
@@ -32,8 +32,8 @@ Section refmut.
ty_shr κ tid l :=
∃ (lv lrc : loc),
&frac{κ} (λ q, l↦∗{q} [ #lv; #lrc]) ∗
- □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ∪ κ]
- ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α ∪ κ) tid lv ∗ q.[α ∪ κ] |}%I.
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ]
+ ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (α ⊓ κ) tid lv ∗ q.[α ⊓ κ] |}%I.
Next Obligation.
iIntros (???[|[[]|][|[[]|][]]]); try iIntros "[]". by iIntros "_".
Qed.
@@ -58,7 +58,7 @@ Section refmut.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _, _. iFrame "H↦". rewrite {1}bor_unfold_idx.
iDestruct "Hb" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ∪ κ) tid lv)%I
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ⊓ κ) tid lv)%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". clear HE.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
@@ -68,7 +68,7 @@ Section refmut.
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
{ iApply bor_shorten; last done. rewrite -assoc.
- iApply lft_glb_mono; first by iApply lft_incl_refl.
+ iApply lft_intersect_mono; first by iApply lft_incl_refl.
iApply lft_incl_glb; first done. iApply lft_incl_refl. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
@@ -80,10 +80,10 @@ Section refmut.
- by iApply frac_bor_shorten.
- iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. iApply lft_incl_refl. done. }
+ { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
Global Instance refmut_type_contractive α : TypeContractive (refmut α).
@@ -104,17 +104,17 @@ Section refmut.
iDestruct "H" as (ν γ β ty') "(Hb & #H⊑ & #Hinv & Hν & Hown)".
iExists ν, γ, β, ty'. iFrame "∗#". iSplit.
+ iApply bor_shorten; last iApply bor_iff; last done.
- * iApply lft_glb_mono; first done. iApply lft_incl_refl.
+ * iApply lft_intersect_mono; first done. iApply lft_incl_refl.
* iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
+ by iApply lft_incl_trans.
- iIntros (κ tid l) "H". iDestruct "H" as (lv lrc) "H". iExists lv, lrc.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
by iApply "Hs".
Qed.
Global Instance refmut_mono_flip E L :
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index b0c55bedc7514eaf7204bfd00d1530865a5294cc..8c6fd2351e90af488c32071ee188e05e3cff6be5 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -20,9 +20,7 @@ Section refmut_functions.
Lemma refmut_deref_type ty :
typed_val refmut_deref
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &shr{α}(refmut β ty)]%T)
- (fun '(α, β) => &shr{α}ty)%T).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -35,7 +33,7 @@ Section refmut_functions.
iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
- iDestruct (lft_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+ iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
[done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_let.
@@ -62,10 +60,9 @@ Section refmut_functions.
Lemma refmut_derefmut_type ty :
typed_val refmut_derefmut
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
- (fun '(α, β) => &uniq{α}ty)%T).
- Proof.
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL [# &uniq{α}(refmut β ty)]%T
+ (&uniq{α}ty)%T)).
+ Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
@@ -117,7 +114,7 @@ Section refmut_functions.
let: "r" := new [ #0] in "return" ["r"].
Lemma refmut_drop_type ty :
- typed_val refmut_drop (fn(∀ α, [☀α]; refmut α ty) → unit).
+ typed_val refmut_drop (fn(∀ α, [α]; refmut α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -171,9 +168,9 @@ Section refmut_functions.
Lemma refmut_map_type ty1 ty2 envty E :
typed_val refmut_map
- (fn(∀ β, [☀β] ++ E; refmut β ty1,
- fn(∀ α, [☀α] ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
- envty)
+ (fn(∀ β, [β]%EL ++ E; refmut β ty1,
+ fn(∀ α, [α]%EL ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
+ envty)
→ refmut β ty2).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
@@ -193,10 +190,10 @@ Section refmut_functions.
iDestruct "HE" as "[HE HE']". iDestruct "Hν" as "[Hν Hν']".
remember (RecV "k" [] (ret [ LitV lref])%E)%V as k eqn:EQk.
iApply (wp_let' _ _ _ _ k). { subst. solve_to_val. } simpl_subst.
- iApply (type_type ((☀ (α ∪ ν)) :: E)%EL []
- [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&uniq{α ∪ ν}ty2)])]%CC
- [ f ◠box (fn(∀ α, [☀α] ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
- #lref ◠own_ptr 2 (&uniq{α ∪ ν}ty1); env ◠box envty ]%TC
+ iApply (type_type ((α ⊓ ν) :: E)%EL []
+ [k â—cont([], λ _:vec val 0, [ #lref â— own_ptr 2 (&uniq{α ⊓ ν}ty2)])]%CC
+ [ f ◠box (fn(∀ α, [α]%EL ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2);
+ #lref ◠own_ptr 2 (&uniq{α ⊓ ν}ty1); env ◠box envty ]%TC
with "[] LFT Hna [HE Hν] HL [Hk HE' Hν' Href↦2 Hγ Href†2]"); first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iFrame. iApply tctx_hasty_val'. done. iFrame. iExists [_].
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 38985be130abe0a7ee0bce88901c4a23647c4f01..1c3421925f4b2ba24b85650b32abc6668bdc7e50 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -41,7 +41,7 @@ Section rwlock_inv.
∃ (ν : lft) q', agν ≡ to_agree ν ∗
□ (1.[ν] ={↑lftN,∅}▷=∗ [†ν]) ∗
([†ν] ={↑lftN}=∗ &{α}(shift_loc l 1 ↦∗: ty.(ty_own) tid)) ∗
- ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
⌜(q + q')%Qp = 1%Qp⌠∗ q'.[ν]
| _ => (* Locked for write. *) True
end)%I.
@@ -131,9 +131,9 @@ Section rwlock.
- iMod (lft_create with "LFT") as (ν) "[[Htok1 Htok2] #Hhν]". done.
iMod (own_alloc (◠Some (Cinr (to_agree ν, (1/2)%Qp, n)))) as (γ) "Hst".
{ by apply auth_auth_valid. }
- iMod (rebor _ _ (κ ∪ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
- iDestruct (lft_glb_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
+ iMod (rebor _ _ (κ ⊓ ν) with "LFT [] Hvl") as "[Hvl Hh]". done.
+ { iApply lft_intersect_incl_l. }
+ iDestruct (lft_intersect_acc with "Htok' Htok1") as (q') "[Htok Hclose]".
iMod (ty_share with "LFT Hvl Htok") as "[Hshr Htok]". done.
iDestruct ("Hclose" with "Htok") as "[$ Htok]".
iExists γ, _. iFrame "Hst Hn". iExists _, _. iIntros "{$Hshr}".
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index bb3f04008457d83d24e8a4b46321cd282e26fdbe..2a6caa17c1cfb08d21ca1a7ca236e7b5aa2368a5 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -20,7 +20,7 @@ Section rwlock_functions.
delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
Lemma rwlock_new_type ty :
- typed_val (rwlock_new ty) (fn (λ _, []) (λ _, [# ty]) (λ _:(), rwlock ty)).
+ typed_val (rwlock_new ty) (fn([]; ty) → rwlock ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -56,8 +56,7 @@ Section rwlock_functions.
delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
Lemma rwlock_into_inner_type ty :
- typed_val (rwlock_into_inner ty)
- (fn (λ _, []) (λ _, [# rwlock ty]) (λ _:(), ty)).
+ typed_val (rwlock_into_inner ty) (fn([] ; rwlock ty) → ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (_ ret arg). inv_vec arg=>x. simpl_subst.
@@ -91,8 +90,7 @@ Section rwlock_functions.
"return" ["x"].
Lemma rwlock_get_mut_type ty :
- typed_val rwlock_get_mut
- (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (rwlock ty)])%T (λ α, &uniq{α} ty)%T).
+ typed_val rwlock_get_mut (fn(∀ α, [α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -141,8 +139,7 @@ Section rwlock_functions.
Lemma rwlock_try_read_type ty :
typed_val rwlock_try_read
- (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
- (λ α, option (rwlockreadguard α ty))%T).
+ (fn(∀ α, [α]; &shr{α}(rwlock ty)) → option (rwlockreadguard α ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
@@ -183,7 +180,7 @@ Section rwlock_functions.
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
+ iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
iAssert (∃ qν ν, (qβ / 2).[β] ∗ (qν).[ν] ∗
- ty_shr ty (β ∪ ν) tid (shift_loc lx 1) ∗
+ ty_shr ty (β ⊓ ν) tid (shift_loc lx 1) ∗
own γ (◯ reading_st qν ν) ∗ rwlock_inv tid lx γ β ty ∗
((1).[ν] ={↑lftN,∅}▷=∗ [†ν]))%I
with ">[Hlx Hownst Hst Hβtok2]"
@@ -207,10 +204,10 @@ Section rwlock_functions.
iMod (own_update with "Hownst") as "[Hownst Hreading]"; first by apply
auth_update_alloc, (op_local_update_discrete _ _ (reading_st (1/2)%Qp ν)).
rewrite right_id. iExists _, _. iFrame "Htok1 Hreading".
- iDestruct (lft_glb_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
+ iDestruct (lft_intersect_acc with "Hβtok2 Htok2") as (q) "[Htok Hclose]".
iApply (fupd_mask_mono (↑lftN)). solve_ndisj.
- iMod (rebor _ _ (β ∪ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
- { iApply lft_le_incl. apply gmultiset_union_subseteq_l. }
+ iMod (rebor _ _ (β ⊓ ν) with "LFT [] Hst") as "[Hst Hh]". solve_ndisj.
+ { iApply lft_intersect_incl_l. }
iMod (ty_share with "LFT Hst Htok") as "[#Hshr Htok]". solve_ndisj.
iFrame "#". iDestruct ("Hclose" with "Htok") as "[$ Htok2]".
iExists _. iFrame. iExists _, _. iSplitR; first done. iFrame "#∗".
@@ -226,7 +223,7 @@ Section rwlock_functions.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val
tctx_hasty_val' //. iFrame.
iExists _, _, _, _. iFrame "∗#". iApply ty_shr_mono; last done.
- iApply lft_glb_mono; first done. iApply lft_incl_refl. }
+ iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
{ rewrite {1}/elctx_interp big_sepL_singleton //. }
iApply (type_sum_assign [unit; rwlockreadguard α ty]); [solve_typing..|].
simpl. iApply (type_jump [_]); solve_typing.
@@ -257,8 +254,7 @@ Section rwlock_functions.
Lemma rwlock_try_write_type ty :
typed_val rwlock_try_write
- (fn (λ α, [☀α])%EL (λ α, [# &shr{α}(rwlock ty)]%T)
- (λ α, option (rwlockwriteguard α ty))%T).
+ (fn(∀ α, [α]; &shr{α}(rwlock ty)) → option (rwlockwriteguard α ty)).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 6a61a4adfb58401b16dc58c96b658ae69d2f47a4..d14f88a4827e900a82487900a7d9732affc84d42 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -20,7 +20,7 @@ Section rwlockreadguard.
ty_own tid vl :=
match vl return _ with
| [ #(LitLoc l) ] =>
- ∃ ν q γ β, ty.(ty_shr) (α ∪ ν) tid (shift_loc l 1) ∗
+ ∃ ν q γ β, ty.(ty_shr) (α ⊓ ν) tid (shift_loc l 1) ∗
α ⊑ β ∗ &shr{β,rwlockN}(rwlock_inv tid l γ β ty) ∗
q.[ν] ∗ own γ (◯ reading_st q ν) ∗
(1.[ν] ={↑lftN,∅}▷=∗ [†ν])
@@ -29,7 +29,7 @@ Section rwlockreadguard.
ty_shr κ tid l :=
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
- ▷ ty.(ty_shr) (α ∪ κ) tid (shift_loc l' 1) |}%I.
+ ▷ ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) |}%I.
Next Obligation. intros α ty tid [|[[]|] []]; auto. Qed.
Next Obligation.
iIntros (α ty E κ l tid q ?) "#LFT Hb Htok".
@@ -52,12 +52,12 @@ Section rwlockreadguard.
iDestruct (frac_bor_lft_incl with "LFT >[Hκν]") as "#Hκν".
{ iApply bor_fracture; try done. by rewrite Qp_mult_1_r. }
iExists _. iFrame "#". iApply ty_shr_mono; last done.
- iApply lft_glb_mono; last done. iApply lft_incl_refl.
+ iApply lft_intersect_mono; last done. iApply lft_incl_refl.
Qed.
Next Obligation.
iIntros (α ty κ κ' tid l) "#Hκ'κ H". iDestruct "H" as (l') "[#Hf #Hshr]".
iExists l'. iSplit; first by iApply frac_bor_shorten.
- iApply ty_shr_mono; last done. iApply lft_glb_mono; last done.
+ iApply ty_shr_mono; last done. iApply lft_intersect_mono; last done.
iApply lft_incl_refl.
Qed.
@@ -84,13 +84,13 @@ Section rwlockreadguard.
iDestruct "H" as (ν q γ β) "(#Hshr & #H⊑ & #Hinv & Htok & Hown)".
iExists ν, q, γ, β. iFrame "∗#". iSplit; last iSplit.
+ iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
+ by iApply lft_incl_trans.
+ iApply (shr_bor_iff with "[] Hinv").
iIntros "!>!#"; iSplit; iIntros "H"; by iApply rwlock_inv_proper.
- iIntros (κ tid l) "H". iDestruct "H" as (l') "[Hf Hshr]". iExists l'.
iFrame. iApply ty_shr_mono; last by iApply "Hs".
- iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply lft_intersect_mono. done. iApply lft_incl_refl.
Qed.
Global Instance rwlockreadguard_mono_flip E L :
Proper (lctx_lft_incl E L ==> eqtype E L ==> flip (subtype E L))
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 12ececef0f687202b63dbe1847280ad196c85e24..c2eaab6779ab658e48c8efbb1cead75bd23504ee 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -20,9 +20,8 @@ Section rwlockreadguard_functions.
Lemma rwlockreadguard_deref_type ty :
typed_val rwlockreadguard_deref
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &shr{α}(rwlockreadguard β ty)]%T)
- (fun '(α, β) => &shr{α}ty)%T).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &shr{α}(rwlockreadguard β ty)] (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -62,7 +61,7 @@ Section rwlockreadguard_functions.
Lemma rwlockreadguard_drop_type ty :
typed_val rwlockreadguard_drop
- (fn(∀ α, [☀α]; rwlockreadguard α ty) → unit).
+ (fn(∀ α, [α]; rwlockreadguard α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index ac8397324fa5f678bb4c09b0609245ad3cc3c034..e8a02e85f33cb48edcbb81eed0bc2940d33fc538 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -29,8 +29,8 @@ Section rwlockwriteguard.
ty_shr κ tid l :=
∃ (l' : loc),
&frac{κ} (λ q, l↦∗{q} [ #l']) ∗
- □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ∪ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
- ty.(ty_shr) (α ∪ κ) tid (shift_loc l' 1) ∗ q.[α ∪ κ] |}%I.
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[α ⊓ κ] ={F, F∖↑shrN∖↑lftN}▷=∗
+ ty.(ty_shr) (α ⊓ κ) tid (shift_loc l' 1) ∗ q.[α ⊓ κ] |}%I.
Next Obligation. by iIntros (???[|[[]|][]]) "?". Qed.
Next Obligation.
iIntros (α ty E κ l tid q HE) "#LFT Hb Htok".
@@ -46,7 +46,7 @@ Section rwlockwriteguard.
iMod (bor_persistent_tok with "LFT Hαβ Htok") as "[#Hαβ $]". done.
iExists _. iFrame "H↦". rewrite {1}bor_unfold_idx.
iDestruct "Hb" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ∪ κ) tid (shift_loc l' 1))%I
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (α ⊓ κ) tid (shift_loc l' 1))%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". clear HE.
iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
@@ -55,7 +55,7 @@ Section rwlockwriteguard.
{ iApply bor_unfold_idx. eauto. }
iModIntro. iNext. iMod "Hb".
iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]". solve_ndisj.
- { iApply (bor_shorten with "[] Hb"). iApply lft_glb_mono. done.
+ { iApply (bor_shorten with "[] Hb"). iApply lft_intersect_mono. done.
iApply lft_incl_refl. }
iMod ("Hclose" with "[]") as "_"; auto.
- iMod ("Hclose" with "[]") as "_". by eauto.
@@ -67,10 +67,10 @@ Section rwlockwriteguard.
- by iApply frac_bor_shorten.
- iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. iApply lft_incl_refl. done. }
+ { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. iApply lft_incl_refl. done.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. iApply lft_incl_refl. done.
Qed.
Global Instance rwlockwriteguard_type_contractive α : TypeContractive (rwlockwriteguard α).
@@ -103,10 +103,10 @@ Section rwlockwriteguard.
- iIntros (κ tid l) "H". iDestruct "H" as (l') "H". iExists l'.
iDestruct "H" as "[$ #H]". iIntros "!# * % Htok".
iMod (lft_incl_acc with "[] Htok") as (q') "[Htok Hclose]". set_solver.
- { iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
iMod ("H" with "[] Htok") as "Hshr". done. iModIntro. iNext.
iMod "Hshr" as "[Hshr Htok]". iMod ("Hclose" with "Htok") as "$".
- iApply ty_shr_mono; try done. iApply lft_glb_mono. done. iApply lft_incl_refl.
+ iApply ty_shr_mono; try done. iApply lft_intersect_mono. done. iApply lft_incl_refl.
by iApply "Hs".
Qed.
Global Instance rwlockwriteguard_mono_flip E L :
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 620771766340a8c965323346c3152002836c9597..0ebe26120cc2200c39602b83bc33c2b6eb33e077 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -20,9 +20,8 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_deref_type ty :
typed_val rwlockwriteguard_deref
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &shr{α}(rwlockwriteguard β ty)]%T)
- (fun '(α, β) => &shr{α}ty)%T).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &shr{α}(rwlockwriteguard β ty)] (&shr{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -35,7 +34,7 @@ Section rwlockwriteguard_functions.
iDestruct "HE" as "([Hα1 Hα2] & Hβ & #Hαβ)".
iMod (frac_bor_acc with "LFT Hfrac Hα1") as (qlx') "[H↦ Hcloseα1]". done.
rewrite heap_mapsto_vec_singleton.
- iDestruct (lft_glb_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
+ iDestruct (lft_intersect_acc with "Hβ Hα2") as (qβα) "[Hα2β Hcloseβα2]".
wp_bind (!(LitV lx'))%E. iApply (wp_fupd_step with "[Hα2β]");
[done| |by iApply ("Hshr" with "[] Hα2β")|]; first done.
iMod "H↦" as "[H↦1 H↦2]". wp_read. iIntros "[#Hshr' Hα2β]!>". wp_op. wp_let.
@@ -63,9 +62,8 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_derefmut_type ty :
typed_val rwlockwriteguard_derefmut
- (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
- (fun '(α, β) => [# &uniq{α}(rwlockwriteguard β ty)]%T)
- (fun '(α, β) => &uniq{α}ty)%T).
+ (fn (fun '(α, β) => FP' [α; β; α ⊑ β]%EL
+ [# &uniq{α}(rwlockwriteguard β ty)] (&uniq{α}ty))).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ret arg). inv_vec arg=>x. simpl_subst.
@@ -111,7 +109,7 @@ Section rwlockwriteguard_functions.
Lemma rwlockwriteguard_drop_type ty :
typed_val rwlockwriteguard_drop
- (fn(∀ α, [☀α]; rwlockwriteguard α ty) → unit).
+ (fn(∀ α, [α]; rwlockwriteguard α ty) → unit).
Proof.
intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 0874f490422c4842c03562cfa9653c7b1062bf27..e19b166b782ef60d39631fe302502b7a7ba0bf86 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -84,8 +84,7 @@ Section spawn.
iIntros "?". iExists retty. iFrame. iApply type_incl_refl. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
(* FIXME this is horrible. *)
- assert (Hcall := type_call' [] [] (λ _:(), []) [] f' [env:expr]
- (λ _, [# envty]) (λ _, retty)).
+ assert (Hcall := type_call' [] [] [] f' [env:expr] (λ _:(), FP' [] [# envty] retty)).
specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
erewrite of_val_unlock in Hcall; last done.
iApply (Hcall $! _ 1%Qp with "LFT Htl [] [] [Hfin]").
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index b18f281951eaf2622dbac2bbd772d16f361e4b58..28a52c0e56bba92acff74ac66f49cc3693522477 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -154,8 +154,8 @@ Section typing_rules.
Proof.
iIntros (Hc) "He". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
- set (κ' := foldr (∪) static κs). wp_seq.
- iApply ("He" $! (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
+ set (κ' := foldr lft_intersect static κs). wp_seq.
+ iApply ("He" $! (κ' ⊓ Λ) with "LFT Htl HE [HL Htk] HC HT").
rewrite /llctx_interp big_sepL_cons. iFrame "HL".
iExists Λ. iSplit; first done. iFrame. done.
Qed.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 1537f6b34456c036b268a930ab04ca703f34883e..401a207842d2b5a2bf7ba065543d13150e4426e6 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -17,8 +17,8 @@ Section uniq_bor.
end%I;
ty_shr κ' tid l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
- □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ∪κ']
- ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid l' ∗ q.[κ∪κ'])%I
+ □ ∀ F q, ⌜↑shrN ∪ lftE ⊆ F⌠-∗ q.[κ⊓κ']
+ ={F, F∖↑shrN∖↑lftN}▷=∗ ty.(ty_shr) (κ⊓κ') tid l' ∗ q.[κ⊓κ'])%I
|}.
Next Obligation. by iIntros (q ty tid [|[[]|][]]) "H". Qed.
Next Obligation.
@@ -29,7 +29,7 @@ Section uniq_bor.
iFrame. iExists l'. subst. rewrite heap_mapsto_vec_singleton.
iMod (bor_fracture (λ q, l ↦{q} #l')%I with "LFT Hb1") as "$". set_solver.
rewrite {1}bor_unfold_idx. iDestruct "Hb2" as (i) "[#Hpb Hpbown]".
- iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ∪κ') tid l')%I
+ iMod (inv_alloc shrN _ (idx_bor_own 1 i ∨ ty_shr ty (κ⊓κ') tid l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!> !# * % Htok". iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
@@ -43,8 +43,8 @@ Section uniq_bor.
Qed.
Next Obligation.
intros κ0 ty κ κ' tid l. iIntros "#Hκ #H".
- iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0∪κ' ⊑ κ0∪κ)%I as "#Hκ0".
- { iApply lft_glb_mono. iApply lft_incl_refl. done. }
+ iDestruct "H" as (l') "[Hfb Hvs]". iAssert (κ0⊓κ' ⊑ κ0⊓κ)%I as "#Hκ0".
+ { iApply lft_intersect_mono. iApply lft_incl_refl. done. }
iExists l'. iSplit. by iApply (frac_bor_shorten with "[]").
iIntros "!# * % Htok".
iApply (step_fupd_mask_mono F _ _ (F∖↑shrN∖↑lftN)); try set_solver.
@@ -64,8 +64,8 @@ Section uniq_bor.
iApply (bor_shorten with "Hκ"). iApply bor_iff; last done.
iSplit; iIntros "!>!# H"; iDestruct "H" as (vl) "[??]";
iExists vl; iFrame; by iApply "Ho".
- - iIntros (κ ??) "H". iAssert (κ2 ∪ κ ⊑ κ1 ∪ κ)%I as "#Hincl'".
- { iApply lft_glb_mono. done. iApply lft_incl_refl. }
+ - iIntros (κ ??) "H". iAssert (κ2 ⊓ κ ⊑ κ1 ⊓ κ)%I as "#Hincl'".
+ { iApply lft_intersect_mono. done. iApply lft_incl_refl. }
iDestruct "H" as (l') "[Hbor #Hupd]". iExists l'. iIntros "{$Hbor}!# %%% Htok".
iMod (lft_incl_acc with "Hincl' Htok") as (q') "[Htok Hclose]"; first set_solver.
iMod ("Hupd" with "[%] Htok") as "Hupd'"; try done. iModIntro. iNext.