From 680dc403344ab57add0fb9b93e783dc19cc610d8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Feb 2019 18:35:58 +0100
Subject: [PATCH] Bump Iris.
---
opam | 2 +-
theories/lifetime/model/accessors.v | 4 ++--
theories/lifetime/model/creation.v | 4 ++--
theories/lifetime/model/definitions.v | 6 +++---
theories/lifetime/model/faking.v | 8 ++++----
theories/lifetime/model/primitive.v | 10 +++++-----
theories/typing/typing.v | 2 +-
7 files changed, 18 insertions(+), 18 deletions(-)
diff --git a/opam b/opam
index dbbeb23f..3830f036 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-iris" { (= "dev.2019-02-05.0.eb921edd") | (= "dev") }
+ "coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
]
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 14f35f7f..0cd3d78d 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -102,7 +102,7 @@ Proof.
iDestruct (own_bor_valid_2 with "Hinv Hf")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
by destruct INCL as [[=]|(? & ? & [=<-] &
- [[_<-]%lookup_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
+ [[_<-]%lookup_gset_to_gmap_Some [[_ ?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
iDestruct (lft_tok_dead with "Htok H†") as "[]".
Qed.
@@ -206,7 +206,7 @@ Proof.
iDestruct (own_bor_valid_2 with "Hinv Hbor")
as %[(_ & <- & INCL%option_included)%singleton_included _]%auth_valid_discrete_2.
by destruct INCL as [[=]|(? & ? & [=<-] &
- [[_<-]%lookup_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
+ [[_<-]%lookup_gset_to_gmap_Some [[_?%(inj to_agree)]|[]%(exclusive_included _)]])].
- iMod (lft_dead_in_tok with "HA") as "[_ H†]". done.
iDestruct (lft_tok_dead with "Htok H†") as "[]".
Qed.
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 76788cdc..152af548 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -42,7 +42,7 @@ Proof.
iApply fupd_trans. iApply fupd_mask_mono; first by apply union_subseteq_l.
iMod ("Hvs" $! I with "[HI Halive Hbox Hbor] HP Hκ") as "(Hinv & HQ & Hcnt')".
{ rewrite lft_vs_inv_unfold. iFrame. rewrite /lft_bor_dead.
- iExists (dom _ B), P. rewrite !to_gmap_dom -map_fmap_compose.
+ iExists (dom _ B), P. rewrite !gset_to_gmap_dom -map_fmap_compose.
rewrite (map_fmap_ext _ ((1%Qp,) ∘ to_agree) B); last naive_solver.
iFrame. }
rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(?&HI&Halive)".
@@ -63,7 +63,7 @@ Lemma lfts_kill (A : gmap atomic_lft _) (I : gmap lft lft_names) (K K' : gset lf
={↑borN ∪ ↑inhN}=∗ Iinv K' ∗ [∗ set] κ ∈ K, lft_inv_dead κ.
Proof.
intros Iinv. revert K'.
- induction (collection_wf K) as [K _ IH]=> K' HKK' HK HK'.
+ induction (set_wf K) as [K _ IH]=> K' HKK' HK HK'.
iIntros "[HI Halive] HK".
pose (Kalive := filter (lft_alive_in A) K).
destruct (decide (Kalive = ∅)) as [HKalive|].
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index d5b45cfb..580275ad 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -123,13 +123,13 @@ Section defs.
Definition lft_bor_dead (κ : lft) : iProp Σ :=
(∃ (B: gset slice_name) (Pb : iProp Σ),
- own_bor κ (● to_gmap (1%Qp, to_agree Bor_in) B) ∗
- box borN (to_gmap false B) Pb)%I.
+ own_bor κ (● gset_to_gmap (1%Qp, to_agree Bor_in) B) ∗
+ box borN (gset_to_gmap false B) Pb)%I.
Definition lft_inh (κ : lft) (s : bool) (Pi : iProp Σ) : iProp Σ :=
(∃ E : gset slice_name,
own_inh κ (● GSet E) ∗
- box inhN (to_gmap s E) Pi)%I.
+ box inhN (gset_to_gmap s E) Pi)%I.
Definition lft_vs_inv_go (κ : lft) (lft_inv_alive : ∀ κ', κ' ⊂ κ → iProp Σ)
(I : gmap lft lft_names) : iProp Σ :=
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index c00558ab..4dcbb159 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -33,14 +33,14 @@ Proof.
iAssert (own_cnt κ (◯ 0)) with "[Hcnt']" as "Hcnt'".
{ rewrite /own_cnt. iExists γs. by iFrame. }
iAssert (∀ b, lft_inh κ b True)%I with "[Hinh]" as "Hinh".
- { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite to_gmap_empty.
+ { iIntros (b). rewrite /lft_inh. iExists ∅. rewrite gset_to_gmap_empty.
iSplitL; [|iApply box_alloc]. rewrite /own_inh. iExists γs. by iFrame. }
iAssert (lft_inv_dead κ ∧ lft_inv_alive κ)%I
with "[-HA HI Hinv]" as "Hdeadandalive".
{ iSplit.
- rewrite /lft_inv_dead. iExists True%I. iFrame "Hcnt".
iSplitL "Hbor"; last by iApply "Hinh".
- rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !to_gmap_empty.
+ rewrite /lft_bor_dead. iExists ∅, True%I. rewrite !gset_to_gmap_empty.
iSplitL "Hbor". iExists γs. by iFrame. iApply box_alloc.
- rewrite lft_inv_alive_unfold. iExists True%I, True%I. iSplitL "Hbor".
{ rewrite /lft_bor_alive. iExists ∅.
@@ -85,9 +85,9 @@ Proof.
iMod (own_bor_update with "HB●") as "[HB● H◯]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, to_agree Bor_in)); last done.
- by do 2 eapply lookup_to_gmap_None. }
+ by do 2 eapply lookup_gset_to_gmap_None. }
rewrite /bor /raw_bor /idx_bor_own /=. iModIntro. iSplitR "H◯".
- - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !to_gmap_union_singleton. by iFrame.
+ - iExists ({[γ]} ∪ B), (P ∗ Pinh)%I. rewrite !gset_to_gmap_union_singleton. by iFrame.
- iExists γ. iFrame. iExists P. rewrite -bi.iff_refl. eauto.
Qed.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 038aa8d1..25519cbb 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -448,10 +448,10 @@ Proof.
as (γE) "(% & #Hslice & Hbox)".
iMod (own_inh_update with "HE") as "[HE HE◯]".
{ by eapply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[γE]}),
- disjoint_singleton_l, lookup_to_gmap_None. }
+ disjoint_singleton_l, lookup_gset_to_gmap_None. }
iModIntro. iSplitL "Hbox HE".
{ iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
- rewrite to_gmap_union_singleton. iFrame. }
+ rewrite gset_to_gmap_union_singleton. iFrame. }
clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
iDestruct "HE◯" as "[HE◯' HE◯]". iSplitL "HE◯'".
{ iIntros (I) "HI". iApply (own_inh_auth with "HI HE◯'"). }
@@ -462,11 +462,11 @@ Proof.
{ apply auth_update_dealloc, gset_disj_dealloc_local_update. }
iMod (slice_delete_full _ _ true with "Hslice Hbox")
as (Q'') "($ & #? & Hbox)"; first by solve_ndisj.
- { rewrite lookup_to_gmap_Some. set_solver. }
+ { rewrite lookup_gset_to_gmap_Some. set_solver. }
iModIntro. iExists Q''. iSplit; first done.
iNext. rewrite /lft_inh. iExists (PE ∖ {[γE]}). iFrame "HE".
rewrite {1}(union_difference_L {[ γE ]} PE); last set_solver.
- rewrite to_gmap_union_singleton delete_insert // lookup_to_gmap_None.
+ rewrite gset_to_gmap_union_singleton delete_insert // lookup_gset_to_gmap_None.
set_solver.
Qed.
@@ -477,7 +477,7 @@ Proof.
rewrite /lft_inh. iIntros (?) "[Hinh HQ]".
iDestruct "Hinh" as (E') "[Hinh Hbox]".
iMod (box_fill with "Hbox HQ") as "?"=>//.
- rewrite fmap_to_gmap. iModIntro. iExists E'. by iFrame.
+ rewrite fmap_gset_to_gmap. iModIntro. iExists E'. by iFrame.
Qed.
(* View shifts *)
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index cdbc2552..5b61f4b5 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -5,5 +5,5 @@ From lrust.typing Require Export
product_split borrow type_sum.
(* Last, so that we make sure we shadow the defintion of delete for
- collections coming from the prelude. *)
+ sets coming from the prelude. *)
From lrust.lang Require Export new_delete.
--
GitLab