From 704ca98e3efa8731558d6908d89362d4fb54d686 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Jun 2021 12:24:11 +0200
Subject: [PATCH] Rename our own typeclasses to follow new naming scheme
---
theories/lang/adequacy.v | 16 ++---
theories/lang/lib/arc.v | 4 +-
theories/lang/lib/lock.v | 2 +-
theories/lang/lib/memcpy.v | 2 +-
theories/lang/lib/new_delete.v | 2 +-
theories/lang/lib/spawn.v | 2 +-
theories/lang/lib/swap.v | 2 +-
theories/lang/lib/tests.v | 2 +-
theories/lang/lifting.v | 12 ++--
theories/lang/proofmode.v | 10 +--
theories/lifetime/at_borrow.v | 6 +-
theories/lifetime/frac_borrow.v | 8 +--
theories/lifetime/lifetime.v | 2 +-
theories/lifetime/lifetime_sig.v | 34 ++++-----
theories/lifetime/meta.v | 4 +-
theories/lifetime/model/accessors.v | 2 +-
theories/lifetime/model/borrow.v | 2 +-
theories/lifetime/model/borrow_sep.v | 2 +-
theories/lifetime/model/creation.v | 2 +-
theories/lifetime/model/definitions.v | 16 ++---
theories/lifetime/model/faking.v | 2 +-
theories/lifetime/model/primitive.v | 8 +--
theories/lifetime/model/reborrow.v | 2 +-
theories/lifetime/na_borrow.v | 4 +-
theories/typing/bool.v | 4 +-
theories/typing/borrow.v | 2 +-
theories/typing/cont.v | 2 +-
theories/typing/cont_context.v | 4 +-
theories/typing/examples/get_x.v | 2 +-
theories/typing/examples/init_prod.v | 2 +-
theories/typing/examples/lazy_lft.v | 2 +-
theories/typing/examples/nonlexical.v | 2 +-
theories/typing/examples/rebor.v | 2 +-
theories/typing/examples/unbox.v | 2 +-
theories/typing/fixpoint.v | 8 +--
theories/typing/function.v | 4 +-
theories/typing/int.v | 4 +-
theories/typing/lft_contexts.v | 4 +-
theories/typing/lib/arc.v | 2 +-
theories/typing/lib/brandedvec.v | 4 +-
theories/typing/lib/cell.v | 4 +-
theories/typing/lib/diverging_static.v | 2 +-
theories/typing/lib/fake_shared.v | 2 +-
theories/typing/lib/ghostcell.v | 2 +-
theories/typing/lib/join.v | 2 +-
theories/typing/lib/mutex/mutex.v | 4 +-
theories/typing/lib/mutex/mutexguard.v | 4 +-
theories/typing/lib/option.v | 2 +-
theories/typing/lib/panic.v | 2 +-
theories/typing/lib/rc/rc.v | 4 +-
theories/typing/lib/rc/weak.v | 4 +-
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/ref_code.v | 2 +-
theories/typing/lib/refcell/refcell.v | 4 +-
theories/typing/lib/refcell/refcell_code.v | 2 +-
theories/typing/lib/refcell/refmut.v | 2 +-
theories/typing/lib/refcell/refmut_code.v | 2 +-
theories/typing/lib/rwlock/rwlock.v | 4 +-
theories/typing/lib/rwlock/rwlock_code.v | 2 +-
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
.../typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 2 +-
.../typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
theories/typing/lib/spawn.v | 4 +-
theories/typing/lib/swap.v | 2 +-
theories/typing/lib/take_mut.v | 2 +-
theories/typing/own.v | 8 +--
theories/typing/product.v | 4 +-
theories/typing/product_split.v | 2 +-
theories/typing/programs.v | 8 +--
theories/typing/shr_bor.v | 4 +-
theories/typing/soundness.v | 16 ++---
theories/typing/sum.v | 2 +-
theories/typing/type.v | 72 +++++++++----------
theories/typing/type_context.v | 4 +-
theories/typing/type_sum.v | 2 +-
theories/typing/uninit.v | 2 +-
theories/typing/uniq_bor.v | 4 +-
theories/typing/util.v | 2 +-
79 files changed, 198 insertions(+), 198 deletions(-)
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index e86deef4..8ce55710 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -4,21 +4,21 @@ From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation.
Set Default Proof Using "Type".
-Class lrustPreG Σ := HeapGpreS {
- lrust_preG_irig :> invGpreS Σ;
- lrust_preG_heap :> inG Σ (authR heapUR);
- lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
+Class lrustGpreS Σ := HeapGpreS {
+ lrustGpreS_irig :> invGpreS Σ;
+ lrustGpreS_heap :> inG Σ (authR heapUR);
+ lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR)
}.
Definition lrustΣ : gFunctors :=
#[invΣ;
GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
+Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
Proof. solve_inG. Qed.
-Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
- (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌠}}) →
+Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
+ (∀ `{!lrustGS Σ}, True ⊢ WP e {{ v, ⌜φ v⌠}}) →
adequate NotStuck e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
@@ -29,5 +29,5 @@ Proof.
set (Hheap := HeapGS _ _ _ vγ fγ).
iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
{ iExists ∅. by iFrame. }
- by iApply (Hwp (LRustG _ _ Hheap)).
+ by iApply (Hwp (LRustGS _ _ Hheap)).
Qed.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 06f2a7af..528ea5c1 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -114,7 +114,7 @@ Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
Proof. solve_inG. Qed.
Section def.
- Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
+ Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) (P2 : iProp Σ) (N : namespace).
Definition arc_tok γ q : iProp Σ :=
own γ (◯ (Some $ Cinl (q, 1%positive, None), 0%nat)).
@@ -158,7 +158,7 @@ Section arc.
this is the lifetime token), and P2 is the thing that is owned by the
protocol when only weak references are left (in practice, P2 is the
ownership of the underlying memory incl. deallocation). *)
- Context `{!lrustG Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
+ Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
(P2 : iProp Σ) (N : namespace).
Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index ae421b61..364aba41 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -16,7 +16,7 @@ Definition release : val := λ: ["l"], "l" <-ˢᶜ #false.
their cancelling view shift has a non-empty mask, and it would have to be
executed in the consequence view shift of a borrow. *)
Section proof.
- Context `{!lrustG Σ}.
+ Context `{!lrustGS Σ}.
Definition lock_proto (l : loc) (R : iProp Σ) : iProp Σ :=
(∃ b : bool, l ↦ #b ∗ if b then True else R)%I.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 1897f020..3b70cb90 100644
--- a/theories/lang/lib/memcpy.v
+++ b/theories/lang/lib/memcpy.v
@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
(at level 80, n, i at next level,
format "e1 <-{ n ,Σ i } ! e2") : expr_scope.
-Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
+Lemma wp_memcpy `{!lrustGS Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
diff --git a/theories/lang/lib/new_delete.v b/theories/lang/lib/new_delete.v
index 6a4be069..3e049e44 100644
--- a/theories/lang/lib/new_delete.v
+++ b/theories/lang/lib/new_delete.v
@@ -13,7 +13,7 @@ Definition delete : val :=
else Free "n" "loc".
Section specs.
- Context `{!lrustG Σ}.
+ Context `{!lrustGS Σ}.
Lemma wp_new E n:
0 ≤ n →
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 55feed47..c603babc 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -36,7 +36,7 @@ Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
-Context `{!lrustG Σ, !spawnG Σ} (N : namespace).
+Context `{!lrustGS Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γf γj : gname) (c : loc) (Ψ : val → iProp Σ) : iProp Σ :=
(own γf (Excl ()) ∗ own γj (Excl ()) ∨
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index d182c900..e6997bbe 100644
--- a/theories/lang/lib/swap.v
+++ b/theories/lang/lib/swap.v
@@ -10,7 +10,7 @@ Definition swap : val :=
"p2" <- "x";;
"swap" ["p1" +â‚— #1 ; "p2" +â‚— #1 ; "len" - #1].
-Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
+Lemma wp_swap `{!lrustGS Σ} E l1 l2 vl1 vl2 (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
{{{ l1 ↦∗ vl1 ∗ l2 ↦∗ vl2 }}}
swap [ #l1; #l2; #n] @ E
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
index 8f414deb..82b76da0 100644
--- a/theories/lang/lib/tests.v
+++ b/theories/lang/lib/tests.v
@@ -4,7 +4,7 @@ From lrust.lang Require Import lang proofmode notation.
Set Default Proof Using "Type".
Section tests.
- Context `{!lrustG Σ}.
+ Context `{!lrustGS Σ}.
Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
{{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 9f869980..38567f42 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -6,13 +6,13 @@ From lrust.lang Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Class lrustG Σ := LRustG {
- lrustG_invG : invGS Σ;
- lrustG_gen_heapG :> heapGS Σ
+Class lrustGS Σ := LRustGS {
+ lrustGS_invGS : invGS Σ;
+ lrustGS_heapGS :> heapGS Σ
}.
-Instance lrustG_irisG `{!lrustG Σ} : irisGS lrust_lang Σ := {
- iris_invG := lrustG_invG;
+Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+ iris_invG := lrustGS_invGS;
state_interp σ _ κs _ := heap_ctx σ;
fork_post _ := True%I;
num_laters_per_step _ := 0%nat;
@@ -63,7 +63,7 @@ Instance do_subst_vec xl (vsl : vec val (length xl)) e :
Proof. by rewrite /DoSubstL subst_v_eq. Qed.
Section lifting.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types e : expr.
Implicit Types ef : option expr.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index ef5c8bd7..3ea0ab9f 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -6,14 +6,14 @@ From lrust.lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
-Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{!lrustGS Σ} Δ E Φ e v :
IntoVal e v →
envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
-Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!lrustGS Σ} K Δ Δ' E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| _ => fail "wp_pure: not a 'wp'"
end.
-Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
+Lemma tac_wp_eq_loc `{!lrustGS Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' →
envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
@@ -67,7 +67,7 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
Tactic Notation "wp_if" := wp_pure (If _ _ _).
Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
-Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
+Lemma tac_wp_bind `{!lrustGS Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
@@ -89,7 +89,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
end.
Section heap.
-Context `{!lrustG Σ}.
+Context `{!lrustGS Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 04bd55a8..84d0c052 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
(** Atomic persistent bors *)
(* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invGS Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
+Definition at_bor `{!invGS Σ, !lftGS Σ userE} κ N (P : iProp Σ) :=
(∃ i, &{κ,i}P ∗
(⌜N ## lftN⌠∗ inv N (idx_bor_own 1 i) ∨
⌜N = lftN⌠∗ inv N (∃ q, idx_bor_own q i)))%I.
Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
Section atomic_bors.
- Context `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
+ Context `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) (N : namespace).
Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
Qed.
End atomic_bors.
-Lemma at_bor_acc_lftN `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) E κ :
↑lftN ⊆ E →
lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
[†κ] ∗ |={E∖↑lftN,E}=> True.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 2874a660..6c88d97e 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -6,16 +6,16 @@ Set Default Proof Using "Type".
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
-Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ userE, !frac_borG Σ}
+Local Definition frac_bor_inv `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ}
(φ : Qp → iProp Σ) γ κ' :=
(∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌠∨ ∃ q', ⌜(q + q' = 1)%Qp⌠∗ q'.[κ']))%I.
-Definition frac_bor `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
(∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
Section frac_bor.
- Context `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
+ Context `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
Implicit Types E : coPset.
Global Instance frac_bor_contractive κ n :
@@ -155,7 +155,7 @@ Section frac_bor.
Qed.
End frac_bor.
-Lemma frac_bor_lft_incl `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ} κ κ' q:
lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 098a789e..1a8a9b3a 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,7 +26,7 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
Infix "⊑ˢʸâ¿" := lft_incl_syntactic (at level 40) : stdpp_scope.
Section derived.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
Lemma lft_create E :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 84ed70d6..345b819a 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -13,29 +13,29 @@ Module Type lifetime_sig.
have aliases here. *)
(** userE is a (disjoint) mask that is available in the "consequence" view
shift of borrow accessors. *)
- Parameter lftG' : ∀ (Σ : gFunctors) (userE : coPset), Set.
- Global Notation lftG := lftG'.
- Existing Class lftG'.
- Parameter lftPreG' : gFunctors → Set.
- Global Notation lftPreG := lftPreG'.
- Existing Class lftPreG'.
+ Parameter lftGS' : ∀ (Σ : gFunctors) (userE : coPset), Set.
+ Global Notation lftGS := lftGS'.
+ Existing Class lftGS'.
+ Parameter lftGpreS' : gFunctors → Set.
+ Global Notation lftGpreS := lftGpreS'.
+ Existing Class lftGpreS'.
(** * Definitions *)
Parameter lft : Type.
Parameter static : lft.
Declare Instance lft_intersect : Meet lft.
- Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ userE}, iProp Σ.
+ Parameter lft_ctx : ∀ `{!invGS Σ, !lftGS Σ userE}, iProp Σ.
- Parameter lft_tok : ∀ `{!lftG Σ userE} (q : Qp) (κ : lft), iProp Σ.
- Parameter lft_dead : ∀ `{!lftG Σ userE} (κ : lft), iProp Σ.
+ Parameter lft_tok : ∀ `{!lftGS Σ userE} (q : Qp) (κ : lft), iProp Σ.
+ Parameter lft_dead : ∀ `{!lftGS Σ userE} (κ : lft), iProp Σ.
- Parameter lft_incl : ∀ `{!invGS Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
- Parameter bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
+ Parameter lft_incl : ∀ `{!invGS Σ, !lftGS Σ userE} (κ κ' : lft), iProp Σ.
+ Parameter bor : ∀ `{!invGS Σ, !lftGS Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
Parameter bor_idx : Type.
- Parameter idx_bor_own : ∀ `{!lftG Σ userE} (q : frac) (i : bor_idx), iProp Σ.
- Parameter idx_bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+ Parameter idx_bor_own : ∀ `{!lftGS Σ userE} (q : frac) (i : bor_idx), iProp Σ.
+ Parameter idx_bor : ∀ `{!invGS Σ, !lftGS Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
(** Our lifetime creation lemma offers allocating a lifetime that is defined
by a [positive] in some given infinite set. This operation converts the
@@ -53,7 +53,7 @@ Module Type lifetime_sig.
Infix "⊑" := lft_incl (at level 70) : bi_scope.
Section properties.
- Context `{!invGS Σ, !lftG Σ userE}.
+ Context `{!invGS Σ, !lftGS Σ userE}.
(** * Instances *)
Global Declare Instance lft_inhabited : Inhabited lft.
@@ -170,9 +170,9 @@ Module Type lifetime_sig.
End properties.
Parameter lftΣ : gFunctors.
- Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
+ Global Declare Instance subG_lftGpreS Σ : subG lftΣ Σ → lftGpreS Σ.
- Parameter lft_init : ∀ `{!invGS Σ, !lftPreG Σ} E userE,
+ Parameter lft_init : ∀ `{!invGS Σ, !lftGpreS Σ} E userE,
↑lftN ⊆ E → ↑lftN ## userE →
- ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
+ ⊢ |={E}=> ∃ _ : lftGS Σ userE, lft_ctx.
End lifetime_sig.
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 62421fce..5872acd5 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -21,12 +21,12 @@ we need. In other words, we use [own_unit] instead of [own_alloc]. As a result
we can just hard-code an arbitrary name here. *)
Local Definition lft_meta_gname : gname := 42%positive.
-Definition lft_meta `{!lftG Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
+Definition lft_meta `{!lftGS Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iProp Σ :=
∃ p : positive, ⌜κ = positive_to_lft p⌠∗
own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
Section lft_meta.
- Context `{!invGS Σ, !lftG Σ userE, lft_metaG Σ}.
+ Context `{!invGS Σ, !lftGS Σ userE, lft_metaG Σ}.
Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
Proof. apply _. Qed.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index bc460359..58054f9c 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
Set Default Proof Using "Type".
Section accessors.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
(* Helper internal lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 982cc8d5..aea3fa11 100644
--- a/theories/lifetime/model/borrow.v
+++ b/theories/lifetime/model/borrow.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
Lemma raw_bor_create E κ P :
diff --git a/theories/lifetime/model/borrow_sep.v b/theories/lifetime/model/borrow_sep.v
index 9213e161..e01b8f51 100644
--- a/theories/lifetime/model/borrow_sep.v
+++ b/theories/lifetime/model/borrow_sep.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index ac782d8f..dbfdff98 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section creation.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 1a1f85e5..2fc9c8bd 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -40,7 +40,7 @@ Definition ilftUR := gmapUR lft (agreeR lft_namesO).
Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
Definition inhUR := gset_disjUR slice_name.
-Class lftG Σ (userE : coPset) := LftG {
+Class lftGS Σ (userE : coPset) := LftG {
lft_box :> boxG Σ;
alft_inG :> inG Σ (authR alftUR);
alft_name : gname;
@@ -51,9 +51,9 @@ Class lftG Σ (userE : coPset) := LftG {
lft_inh_inG :> inG Σ (authR inhUR);
userE_lftN_disj : ↑lftN ## userE;
}.
-Definition lftG' := lftG.
+Definition lftGS' := lftGS.
-Class lftPreG Σ := LftPreG {
+Class lftGpreS Σ := LftGPreS {
lft_preG_box :> boxG Σ;
alft_preG_inG :> inG Σ (authR alftUR);
ilft_preG_inG :> inG Σ (authR ilftUR);
@@ -61,13 +61,13 @@ Class lftPreG Σ := LftPreG {
lft_preG_cnt_inG :> inG Σ (authR natUR);
lft_preG_inh_inG :> inG Σ (authR inhUR);
}.
-Definition lftPreG' := lftPreG.
+Definition lftGpreS' := lftGpreS.
Definition lftΣ : gFunctors :=
#[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftPreG Σ :
- subG lftΣ Σ → lftPreG Σ.
+Instance subG_lftGpreS Σ :
+ subG lftΣ Σ → lftGpreS Σ.
Proof. solve_inG. Qed.
Definition bor_filled (s : bor_state) : bool :=
@@ -80,7 +80,7 @@ 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 `{!invGS Σ, !lftG Σ userE}.
+ Context `{!invGS Σ, !lftGS Σ userE}.
Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -224,7 +224,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
idx_bor_own idx_bor raw_bor bor.
Section basic_properties.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
(* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 1e996cd1..1500524e 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section faking.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index eaaf4991..798d8d0e 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -6,13 +6,13 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Lemma lft_init `{!invGS Σ, !lftPreG Σ} E userE :
- ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
+Lemma lft_init `{!invGS Σ, !lftGpreS Σ} E userE :
+ ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftGS Σ userE, lft_ctx.
Proof.
iIntros (? HuserE). rewrite /lft_ctx.
iMod (own_alloc (◠∅ : authR alftUR)) as (γa) "Ha"; first by apply auth_auth_valid.
iMod (own_alloc (◠∅ : authR ilftUR)) as (γi) "Hi"; first by apply auth_auth_valid.
- set (HlftG := LftG _ _ _ _ γa _ γi _ _ _ HuserE). iExists HlftG.
+ set (HlftGS := LftG _ _ _ _ γa _ γi _ _ _ HuserE). iExists HlftGS.
iMod (inv_alloc _ _ lfts_inv with "[Ha Hi]") as "$"; last done.
iModIntro. rewrite /lfts_inv /own_alft_auth /own_ilft_auth. iExists ∅, ∅.
rewrite /to_alftUR /to_ilftUR !fmap_empty. iFrame.
@@ -20,7 +20,7 @@ Proof.
Qed.
Section primitive.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index a77e597a..7b0bce86 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section reborrow.
-Context `{!invGS Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftGS Σ userE}.
Implicit Types κ : lft.
(* Notice that taking lft_inv for both κ and κ' already implies
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index fec690bc..729cc576 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Definition na_bor `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
(κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
(∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
(format "&na{ κ , tid , N }") : bi_scope.
Section na_bor.
- Context `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
+ Context `{!invGS Σ, !lftGS Σ userE, !na_invG Σ}
(tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 19c04dd6..6c1e4f83 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs.
Set Default Proof Using "Type".
Section bool.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Program Definition bool : type :=
{| st_own tid vl :=
@@ -22,7 +22,7 @@ Section bool.
End bool.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
Proof.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index baf447ff..ad909c54 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
concurrently. *)
Section borrow.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma tctx_borrow E L p n ty κ :
tctx_incl E L [p â— own_ptr n ty] [p â— &uniq{κ}ty; p â—{κ} own_ptr n ty].
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 2d7d99ac..1cca2081 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs.
Set Default Proof Using "Type".
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(** Jumping to and defining a continuation. *)
Lemma type_jump args argsv E L C T k T' :
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b76fdf65..ff78d9db 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import type lft_contexts type_context.
Set Default Proof Using "Type".
Section cont_context_def.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition cont_postcondition : iProp Σ := True%I.
@@ -20,7 +20,7 @@ Notation "k â—cont( L , T )" := (CCtx_iscont k L _ T)
(at level 70, format "k â—cont( L , T )").
Section cont_context.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition cctx_elt_interp (tid : thread_id) (qmax: Qp) (x : cctx_elt) : iProp Σ :=
let '(k â—cont(L, T)) := x in
diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 3da2f4ac..95486f6e 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section get_x.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition get_x : val :=
fn: ["p"] :=
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 2da36073..ee0bc5ba 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section init_prod.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition init_prod : val :=
fn: ["x"; "y"] :=
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index ca5b804e..b9bf7354 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section lazy_lft.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition lazy_lft : val :=
fn: [] :=
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 64ad88b1..2718f2e8 100644
--- a/theories/typing/examples/nonlexical.v
+++ b/theories/typing/examples/nonlexical.v
@@ -13,7 +13,7 @@ From lrust.typing Require Import typing lib.option.
*)
Section non_lexical.
- Context `{!typeG Σ} (HashMap K V : type)
+ Context `{!typeGS Σ} (HashMap K V : type)
`{!TyWf hashmap, !TyWf K, !TyWf V, !Copy K}
(defaultv get_mut insert: val).
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 1dbac6ce..4b5cda26 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section rebor.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition rebor : val :=
fn: ["t1"; "t2"] :=
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 843b715f..b1a13d01 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section unbox.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition unbox : val :=
fn: ["b"] :=
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index cec43a3b..b35258a6 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
Import uPred.
Section fixpoint_def.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Context (T : type → type) {HT: TypeContractive T}.
Global Instance type_inhabited : Inhabited type := populate bool.
@@ -37,13 +37,13 @@ Section fixpoint_def.
{| ty_lfts := lfts; ty_wf_E := wf_E |}.
End fixpoint_def.
-Lemma type_fixpoint_ne `{!typeG Σ} (T1 T2 : type → type)
+Lemma type_fixpoint_ne `{!typeGS Σ} (T1 T2 : type → type)
`{!TypeContractive T1, !TypeContractive T2} n :
(∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
Section fixpoint.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Context (T : type → type) {HT: TypeContractive T}.
Global Instance fixpoint_copy :
@@ -98,7 +98,7 @@ Section fixpoint.
End fixpoint.
Section subtyping.
- Context `{!typeG Σ} (E : elctx) (L : llctx).
+ Context `{!typeGS Σ} (E : elctx) (L : llctx).
(* TODO : is there a way to declare these as a [Proper] instances ? *)
Lemma fixpoint_mono T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4e9a4f4c..9eed7c5e 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import own programs cont.
Set Default Proof Using "Type".
Section fn.
- Context `{!typeG Σ} {A : Type} {n : nat}.
+ Context `{!typeGS Σ} {A : Type} {n : nat}.
Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
@@ -142,7 +142,7 @@ Notation "'fn(' E ')' '→' R" :=
Instance elctx_empty : Empty (lft → elctx) := λ Ï, [].
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
(∀ x Ï, let EE := E0 ++ (fp' x).(fp_E) Ï in
diff --git a/theories/typing/int.v b/theories/typing/int.v
index c710360d..4ec16f6d 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import bool programs.
Set Default Proof Using "Type".
Section int.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Program Definition int : type :=
{| st_own tid vl :=
@@ -22,7 +22,7 @@ Section int.
End int.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma type_int_instr (z : Z) : typed_val #z int.
Proof.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index f869d85e..0dc89dcf 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -23,7 +23,7 @@ Notation llctx := (list llctx_elt).
Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
Section lft_contexts.
- Context `{!invGS Σ, !lftG Σ lft_userE}.
+ Context `{!invGS Σ, !lftGS Σ lft_userE}.
Implicit Type (κ : lft).
(* External lifetime contexts. *)
@@ -415,7 +415,7 @@ Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
-Lemma elctx_sat_submseteq `{!invGS Σ, !lftG Σ lft_userE} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftGS Σ lft_userE} E E' L :
E' ⊆+ E → elctx_sat E L E'.
Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index c85c868c..7eed83f4 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -13,7 +13,7 @@ Definition arc_shrN := arcN .@ "shr".
Definition arc_endN := arcN .@ "end".
Section arc.
- Context `{!typeG Σ, !arcG Σ}.
+ Context `{!typeGS Σ, !arcG Σ}.
(* Preliminary definitions. *)
Let P1 ν q := (q.[ν])%I.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 8a12af76..979b61d8 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -21,7 +21,7 @@ Definition brandidxN := lrustN .@ "brandix".
Definition brandvecN := lrustN .@ "brandvec".
Section brandedvec.
- Context `{!typeG Σ, !brandidxG Σ}.
+ Context `{!typeGS Σ, !brandidxG Σ}.
Implicit Types (q : Qp) (α : lft) (γ : gname) (n m : nat).
Local Notation iProp := (iProp Σ).
@@ -158,7 +158,7 @@ Section brandedvec.
End brandedvec.
Section typing.
- Context `{!typeG Σ, !brandidxG Σ}.
+ Context `{!typeGS Σ, !brandidxG Σ}.
Implicit Types (q : Qp) (α : lft) (γ : gname) (n m : nat).
Local Notation iProp := (iProp Σ).
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index 213fa339..9645ecbd 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section cell.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Program Definition cell (ty : type) :=
{| ty_size := ty.(ty_size);
@@ -79,7 +79,7 @@ Section cell.
End cell.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(** The next couple functions essentially show owned-type equalities, as they
are all different types for the identity function. *)
diff --git a/theories/typing/lib/diverging_static.v b/theories/typing/lib/diverging_static.v
index 1c985a36..abbedcab 100644
--- a/theories/typing/lib/diverging_static.v
+++ b/theories/typing/lib/diverging_static.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section diverging_static.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* Show that we can convert any live borrow to 'static with an infinite
loop. *)
diff --git a/theories/typing/lib/fake_shared.v b/theories/typing/lib/fake_shared.v
index 0b3db02b..d10fe83f 100644
--- a/theories/typing/lib/fake_shared.v
+++ b/theories/typing/lib/fake_shared.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section fake_shared.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition fake_shared_box : val :=
fn: ["x"] := Skip ;; return: ["x"].
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index cbdc1d38..7085874b 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -93,7 +93,7 @@ Definition ghosttoken_st_to_R (st : ghosttoken_st) : ghosttoken_stR :=
end).
Section ghostcell.
- Context `{!typeG Σ, !ghostcellG Σ}.
+ Context `{!typeGS Σ, !ghostcellG Σ}.
Implicit Types (α β: lft) (γ: gname) (q: Qp) (ty: type) (l: loc).
Local Instance ghosttoken_fractional γ κ' :
diff --git a/theories/typing/lib/join.v b/theories/typing/lib/join.v
index 9de2211b..fc593c24 100644
--- a/theories/typing/lib/join.v
+++ b/theories/typing/lib/join.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Definition joinN := lrustN .@ "join".
Section join.
- Context `{!typeG Σ, !spawnG Σ}.
+ Context `{!typeGS Σ, !spawnG Σ}.
(* This model is very far from rayon::join, which uses a persistent
work-stealing thread-pool. Still, the important bits are right:
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index f6a5a350..ca3cd06d 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
Definition mutexN := lrustN .@ "mutex".
Section mutex.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(*
pub struct Mutex<T: ?Sized> {
@@ -126,7 +126,7 @@ Section mutex.
End mutex.
Section code.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition mutex_new ty : val :=
fn: ["x"] :=
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 2ca7e007..960c7464 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -16,7 +16,7 @@ Set Default Proof Using "Type".
*)
Section mguard.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(*
pub struct MutexGuard<'a, T: ?Sized + 'a> {
@@ -143,7 +143,7 @@ Section mguard.
End mguard.
Section code.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma mutex_acc E l ty tid q α κ :
↑lftN ⊆ E → ↑mutexN ⊆ E →
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 66c6d79b..6f7a4b5f 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -3,7 +3,7 @@ From lrust.typing Require Import typing lib.panic.
Set Default Proof Using "Type".
Section option.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition option (τ : type) := Σ[unit; τ]%T.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index f5564c57..fe40d55b 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -11,7 +11,7 @@ Set Default Proof Using "Type".
[take_mut]. *)
Section panic.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition panic : val :=
fn: [] := #☠.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e2ed4647..2f725829 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -25,7 +25,7 @@ Definition rc_invN := rcN .@ "inv".
Definition rc_shrN := rcN .@ "shr".
Section rc.
- Context `{!typeG Σ, !rcG Σ}.
+ Context `{!typeGS Σ, !rcG Σ}.
(* The RC can be in four different states :
- The living state, meaning that some strong reference exists. The
@@ -236,7 +236,7 @@ Section rc.
End rc.
Section code.
- Context `{!typeG Σ, !rcG Σ}.
+ Context `{!typeGS Σ, !rcG Σ}.
Lemma rc_check_unique ty F tid (l : loc) :
↑rc_invN ⊆ F →
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index dfea77e5..a218e1de 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -8,7 +8,7 @@ From lrust.typing.lib Require Export rc.
Set Default Proof Using "Type".
Section weak.
- Context `{!typeG Σ, !rcG Σ}.
+ Context `{!typeGS Σ, !rcG Σ}.
Program Definition weak (ty : type) :=
{| ty_size := 1;
@@ -103,7 +103,7 @@ Section weak.
End weak.
Section code.
- Context `{!typeG Σ, !rcG Σ}.
+ Context `{!typeGS Σ, !rcG Σ}.
Definition rc_upgrade : val :=
fn: ["w"] :=
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index e146334c..7ee34cc9 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
Definition refcell_refN := refcellN .@ "ref".
Section ref.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
(* The Rust type looks as follows (after some unfolding):
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index a77c45b8..9df46b27 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell ref.
Set Default Proof Using "Type".
Section ref_functions.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
Lemma refcell_inv_reading_inv tid l γ α ty q ν :
refcell_inv tid l γ α ty -∗
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 72219bfa..15ffbb55 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -40,7 +40,7 @@ Definition refcellN := lrustN .@ "refcell".
Definition refcell_invN := refcellN .@ "inv".
Section refcell_inv.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
Definition refcell_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
(∃ st, l ↦ #(Z_of_refcell_st st) ∗ own γ (◠(refcell_st_to_R st)) ∗
@@ -94,7 +94,7 @@ Section refcell_inv.
End refcell_inv.
Section refcell.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
(* Original Rust type:
pub struct RefCell<T: ?Sized> {
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 17320a49..a4e20122 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell ref refmut.
Set Default Proof Using "Type".
Section refcell_functions.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
(* Constructing a refcell. *)
Definition refcell_new ty : val :=
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index ff6e32e0..b405995b 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell.
Set Default Proof Using "Type".
Section refmut.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
(* The Rust type looks as follows (after some unfolding):
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4dc1d3bd..680c7d77 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.refcell Require Import refcell refmut.
Set Default Proof Using "Type".
Section refmut_functions.
- Context `{!typeG Σ, !refcellG Σ}.
+ Context `{!typeGS Σ, !refcellG Σ}.
(* Turning a refmut into a shared borrow. *)
Definition refmut_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index e658e08d..ad9ef92c 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -28,7 +28,7 @@ Definition writing_st : rwlock_stR :=
Definition rwlockN := lrustN .@ "rwlock".
Section rwlock_inv.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
Definition rwlock_inv tid_own tid_shr (l : loc) (γ : gname) (α : lft) ty
: iProp Σ :=
@@ -103,7 +103,7 @@ Section rwlock_inv.
End rwlock_inv.
Section rwlock.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
(* Original Rust type (we ignore poisoning):
pub struct RwLock<T: ?Sized> {
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 0a86013d..2f0f3fcf 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwritegu
Set Default Proof Using "Type".
Section rwlock_functions.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
(* Constructing a rwlock. *)
Definition rwlock_new ty : val :=
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index d94c4ab8..51df1e84 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock.
Set Default Proof Using "Type".
Section rwlockreadguard.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
(* Original Rust type:
pub struct RwLockReadGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index e5ac1c55..e2c0553d 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
Set Default Proof Using "Type".
Section rwlockreadguard_functions.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
(* Turning a rwlockreadguard into a shared borrow. *)
Definition rwlockreadguard_deref : val :=
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index f6ba19e9..702201bc 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock.
Set Default Proof Using "Type".
Section rwlockwriteguard.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
(* Original Rust type (we ignore poisoning):
pub struct RwLockWriteGuard<'a, T: ?Sized + 'a> {
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 8dfc9891..beda5f49 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -7,7 +7,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
Set Default Proof Using "Type".
Section rwlockwriteguard_functions.
- Context `{!typeG Σ, !rwlockG Σ}.
+ Context `{!typeGS Σ, !rwlockG Σ}.
(* Turning a rwlockwriteguard into a shared borrow. *)
Definition rwlockwriteguard_deref : val :=
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index f2d2859e..421bb191 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Definition spawnN := lrustN .@ "spawn".
Section join_handle.
- Context `{!typeG Σ, !spawnG Σ}.
+ Context `{!typeGS Σ, !spawnG Σ}.
Definition join_inv (ty : type) (v : val) :=
(∀ tid, (box ty).(ty_own) tid [v])%I.
@@ -65,7 +65,7 @@ Section join_handle.
End join_handle.
Section spawn.
- Context `{!typeG Σ, !spawnG Σ}.
+ Context `{!typeGS Σ, !spawnG Σ}.
Definition spawn (call_once : val) : val :=
fn: ["f"] :=
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index b6d4cb18..d920a7d2 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section swap.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition swap ty : val :=
fn: ["p1"; "p2"] :=
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 9adb5ff7..8c9f2155 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Section code.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition take ty (call_once : val) : val :=
fn: ["x"; "f"] :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index a03beedf..757e883c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import util uninit type_context programs.
Set Default Proof Using "Type".
Section own.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
match sz, n return _ with
@@ -146,7 +146,7 @@ Section own.
End own.
Section box.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Definition box ty := own_ptr ty.(ty_size) ty.
@@ -183,7 +183,7 @@ Section box.
End box.
Section util.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma ownptr_own n ty tid v :
(own_ptr n ty).(ty_own) tid [v] ⊣⊢
@@ -214,7 +214,7 @@ Section util.
End util.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(** Typing *)
Lemma write_own {E L} ty ty' n :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 90f273cd..57e1e108 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
Set Default Proof Using "Type".
Section product.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* TODO: Find a better spot for this. *)
Lemma Z_nat_add (n1 n2 : nat) : Z.to_nat (n1 + n2) = (n1 + n2)%nat.
@@ -195,7 +195,7 @@ End product.
Notation Î := product.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Global Instance prod2_assoc E L : Assoc (eqtype E L) product2.
Proof.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 3dc9c1ce..150710d3 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import shr_bor.
Set Default Proof Using "Type".
Section product_split.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(** General splitting / merging for pointer types *)
Fixpoint hasty_ptr_offsets (p : path) (ptr: type → type) tyl (off : nat) : tctx :=
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index d3e564c7..f0448ba9 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type lft_contexts type_context cont_context.
Set Default Proof Using "Type".
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(** Function Body *)
(* This is an iProp because it is also used by the function type. *)
@@ -101,17 +101,17 @@ Section typing.
Proof. rewrite typed_read_eq. apply _. Qed.
End typing.
-Definition typed_instruction_ty `{!typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+Definition typed_instruction_ty `{!typeGS Σ} (E : elctx) (L : llctx) (T : tctx)
(e : expr) (ty : type) : iProp Σ :=
typed_instruction E L T e (λ v, [v ◠ty]).
Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
-Definition typed_val `{!typeG Σ} (v : val) (ty : type) : Prop :=
+Definition typed_val `{!typeGS Σ} (v : val) (ty : type) : Prop :=
∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
Arguments typed_val _ _ _%V _%T.
Section typing_rules.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* This lemma is helpful when switching from proving unsafe code in Iris
back to proving it in the type system. *)
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index e6042d95..0fb7bf7f 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import lft_contexts type_context programs.
Set Default Proof Using "Type".
Section shr_bor.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Program Definition shr_bor (κ : lft) (ty : type) : type :=
{| st_own tid vl :=
@@ -61,7 +61,7 @@ End shr_bor.
Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma shr_mono' E L κ1 κ2 ty1 ty2 :
lctx_lft_incl E L κ2 κ1 → subtype E L ty1 ty2 →
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 4280bcf9..4ef123dc 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -7,25 +7,25 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
-Class typePreG Σ := PreTypeG {
- type_preG_lrustG :> lrustPreG Σ;
- type_preG_lftG :> lftPreG Σ;
+Class typeGpreS Σ := PreTypeG {
+ type_preG_lrustGS :> lrustGpreS Σ;
+ type_preG_lftGS :> lftGpreS Σ;
type_preG_na_invG :> na_invG Σ;
type_preG_frac_borG :> frac_borG Σ
}.
Definition typeΣ : gFunctors :=
#[lrustΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
-Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Instance subG_typeGpreS {Σ} : subG typeΣ Σ → typeGpreS Σ.
Proof. solve_inG. Qed.
Section type_soundness.
Definition exit_cont : val := λ: [<>], #☠.
- Definition main_type `{!typeG Σ} := (fn(∅) → unit)%T.
+ Definition main_type `{!typeGS Σ} := (fn(∅) → unit)%T.
- Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
- (∀ `{!typeG Σ}, typed_val main main_type) →
+ Theorem type_soundness `{!typeGpreS Σ} (main : val) σ t :
+ (∀ `{!typeGS Σ}, typed_val main main_type) →
rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
nonracing_threadpool t σ ∧
(∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
@@ -63,7 +63,7 @@ End type_soundness.
(* Soundness theorem when no other CMRA is needed. *)
Theorem type_soundness_closed (main : val) σ t :
- (∀ `{!typeG typeΣ}, typed_val main main_type) →
+ (∀ `{!typeGS typeΣ}, typed_val main main_type) →
rtc erased_step ([main [exit_cont]%E], ∅) (t, σ) →
nonracing_threadpool t σ ∧
(∀ e, e ∈ t → is_Some (to_val e) ∨ reducible e σ).
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e68edb4f..0bfaa42a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -6,7 +6,7 @@ From lrust.typing Require Export type.
Set Default Proof Using "Type".
Section sum.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* We define the actual empty type as being the empty sum, so that it is
convertible to it---and in particular, we can pattern-match on it
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 09cb325c..ea9fa413 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -6,9 +6,9 @@ From lrust.typing Require Export base.
From lrust.typing Require Import lft_contexts.
Set Default Proof Using "Type".
-Class typeG Σ := TypeG {
- type_lrustG :> lrustG Σ;
- type_lftG :> lftG Σ lft_userE;
+Class typeGS Σ := TypeG {
+ type_lrustGS :> lrustGS Σ;
+ type_lftGS :> lftGS Σ lft_userE;
type_na_invG :> na_invG Σ;
type_frac_borrowG :> frac_borG Σ
}.
@@ -18,7 +18,7 @@ Definition shrN := lrustN .@ "shr".
Definition thread_id := na_inv_pool_name.
-Record type `{!typeG Σ} :=
+Record type `{!typeGS Σ} :=
{ ty_size : nat;
ty_own : thread_id → list val → iProp Σ;
ty_shr : lft → thread_id → loc → iProp Σ;
@@ -52,14 +52,14 @@ Instance: Params (@ty_shr) 2 := {}.
Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
-Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
+Class TyWf `{!typeGS Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
Arguments ty_lfts {_ _} _ {_}.
Arguments ty_wf_E {_ _} _ {_}.
-Definition ty_outlives_E `{!typeG Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
+Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
(λ α, κ ⊑ₑ α) <$> ty.(ty_lfts).
-Lemma ty_outlives_E_elctx_sat `{!typeG Σ} E L ty `{!TyWf ty} α β :
+Lemma ty_outlives_E_elctx_sat `{!typeGS Σ} E L ty `{!TyWf ty} α β :
ty_outlives_E ty β ⊆+ E →
lctx_lft_incl E L α β →
elctx_sat E L (ty_outlives_E ty α).
@@ -73,34 +73,34 @@ Proof.
Qed.
(* Lift TyWf to lists. We cannot use `Forall` because that one is restricted to Prop. *)
-Inductive ListTyWf `{!typeG Σ} : list type → Type :=
+Inductive ListTyWf `{!typeGS Σ} : list type → Type :=
| list_ty_wf_nil : ListTyWf []
| list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
Existing Class ListTyWf.
Existing Instances list_ty_wf_nil list_ty_wf_cons.
-Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeGS Σ} tyl {WF : ListTyWf tyl} : list lft :=
match WF with
| list_ty_wf_nil => []
| list_ty_wf_cons ty [] => ty.(ty_lfts)
| list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
end.
-Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeGS Σ} tyl {WF : ListTyWf tyl} : elctx :=
match WF with
| list_ty_wf_nil => []
| list_ty_wf_cons ty [] => ty.(ty_wf_E)
| list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
end.
-Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeGS Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
match WF with
| list_ty_wf_nil => []
| list_ty_wf_cons ty [] => ty_outlives_E ty κ
| list_ty_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
end.
-Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : ListTyWf tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeGS Σ} E L tyl {WF : ListTyWf tyl} α β :
tyl_outlives_E tyl β ⊆+ E →
lctx_lft_incl E L α β →
elctx_sat E L (tyl_outlives_E tyl α).
@@ -112,14 +112,14 @@ Proof.
(etrans; [|done]); solve_typing.
Qed.
-Record simple_type `{!typeG Σ} :=
+Record simple_type `{!typeGS Σ} :=
{ st_own : thread_id → list val → iProp Σ;
st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%natâŒ;
st_own_persistent tid vl : Persistent (st_own tid vl) }.
Existing Instance st_own_persistent.
Instance: Params (@st_own) 2 := {}.
-Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
+Program Definition ty_of_st `{!typeGS Σ} (st : simple_type) : type :=
{| ty_size := 1; ty_own := st.(st_own);
(* [st.(st_own) tid vl] needs to be outside of the fractured
borrow, otherwise I do not know how to prove the shr part of
@@ -149,7 +149,7 @@ Bind Scope lrust_type_scope with type.
(* OFE and COFE structures on types and simple types. *)
Section ofe.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Inductive type_equiv' (ty1 ty2 : type) : Prop :=
Type_equiv :
@@ -260,7 +260,7 @@ End ofe.
(** Special metric for type-nonexpansive and Type-contractive functions. *)
Section type_dist2.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* Size and shr are n-equal, but own is only n-1-equal.
We need this to express what shr has to satisfy on a Type-NE-function:
@@ -328,7 +328,7 @@ Notation TypeNonExpansive T := (∀ n, Proper (type_dist2 n ==> type_dist2 n) T)
Notation TypeContractive T := (∀ n, Proper (type_dist2_later n ==> type_dist2 n) T).
Section type_contractive.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma type_ne_dist_later T :
TypeNonExpansive T → ∀ n, Proper (type_dist2_later n ==> type_dist2_later n) T.
@@ -389,7 +389,7 @@ Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
| S n => ↑shrN.@l ∪ shr_locsE (l +ₗ 1%nat) n
end.
-Class Copy `{!typeG Σ} (t : type) := {
+Class Copy `{!typeGS Σ} (t : type) := {
copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
copy_shr_acc κ tid E F l q :
↑lftN ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
@@ -402,34 +402,34 @@ Class Copy `{!typeG Σ} (t : type) := {
Existing Instances copy_persistent.
Instance: Params (@Copy) 2 := {}.
-Class ListCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Class ListCopy `{!typeGS Σ} (tys : list type) := lst_copy : Forall Copy tys.
Instance: Params (@ListCopy) 2 := {}.
-Global Instance lst_copy_nil `{!typeG Σ} : ListCopy [] := List.Forall_nil _.
-Global Instance lst_copy_cons `{!typeG Σ} ty tys :
+Global Instance lst_copy_nil `{!typeGS Σ} : ListCopy [] := List.Forall_nil _.
+Global Instance lst_copy_cons `{!typeGS Σ} ty tys :
Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
-Class Send `{!typeG Σ} (t : type) :=
+Class Send `{!typeGS Σ} (t : type) :=
send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
Instance: Params (@Send) 2 := {}.
-Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Class ListSend `{!typeGS Σ} (tys : list type) := lst_send : Forall Send tys.
Instance: Params (@ListSend) 2 := {}.
-Global Instance lst_send_nil `{!typeG Σ} : ListSend [] := List.Forall_nil _.
-Global Instance lst_send_cons `{!typeG Σ} ty tys :
+Global Instance lst_send_nil `{!typeGS Σ} : ListSend [] := List.Forall_nil _.
+Global Instance lst_send_cons `{!typeGS Σ} ty tys :
Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
-Class Sync `{!typeG Σ} (t : type) :=
+Class Sync `{!typeGS Σ} (t : type) :=
sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
Instance: Params (@Sync) 2 := {}.
-Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Class ListSync `{!typeGS Σ} (tys : list type) := lst_sync : Forall Sync tys.
Instance: Params (@ListSync) 2 := {}.
-Global Instance lst_sync_nil `{!typeG Σ} : ListSync [] := List.Forall_nil _.
-Global Instance lst_sync_cons `{!typeG Σ} ty tys :
+Global Instance lst_sync_nil `{!typeGS Σ} : ListSync [] := List.Forall_nil _.
+Global Instance lst_sync_cons `{!typeGS Σ} ty tys :
Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
Section type.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(** Copy types *)
Lemma shr_locsE_shift l n m :
@@ -532,30 +532,30 @@ Section type.
Qed.
End type.
-Definition type_incl `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+Definition type_incl `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
Instance: Params (@type_incl) 2 := {}.
(* Typeclasses Opaque type_incl. *)
-Definition type_equal `{!typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+Definition type_equal `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
(⌜ty1.(ty_size) = ty2.(ty_size)⌠∗
(□ ∀ tid vl, ty1.(ty_own) tid vl ∗-∗ ty2.(ty_own) tid vl) ∗
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
Instance: Params (@type_equal) 2 := {}.
-Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition subtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
Instance: Params (@subtype) 4 := {}.
(* TODO: The prelude should have a symmetric closure. *)
-Definition eqtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition eqtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
Instance: Params (@eqtype) 4 := {}.
Section subtyping.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Global Instance type_incl_ne : NonExpansive2 type_incl.
Proof.
@@ -742,7 +742,7 @@ Section subtyping.
End subtyping.
Section type_util.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma heap_mapsto_ty_own l ty tid :
l ↦∗: ty_own ty tid ⊣⊢ ∃ (vl : vec val ty.(ty_size)), l ↦∗ vl ∗ ty_own ty tid vl.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index b0fb3cb2..45da5647 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -7,7 +7,7 @@ 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 :=
+Inductive tctx_elt `{!typeGS Σ} : Type :=
| TCtx_hasty (p : path) (ty : type)
| TCtx_blocked (p : path) (κ : lft) (ty : type).
@@ -18,7 +18,7 @@ Notation "p â—{ κ } ty" := (TCtx_blocked p κ ty)
(at level 70, format "p â—{ κ } ty").
Section type_context.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Implicit Types T : tctx.
Fixpoint eval_path (p : path) : option val :=
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 5e3dedaf..4bb4ab17 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import lft_contexts type_context programs product.
Set Default Proof Using "Type".
Section case.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* FIXME : have an Iris version of Forall2. *)
Lemma type_case_own' E L C T p n tyl el :
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index e45318a9..23637fd5 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import product.
Set Default Proof Using "Type".
Section uninit.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Program Definition uninit_1 : type :=
{| st_own tid vl := ⌜length vl = 1%natâŒ%I |}.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index f5ca1e03..3813dd68 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import util lft_contexts type_context programs.
Set Default Proof Using "Type".
Section uniq_bor.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Program Definition uniq_bor (κ:lft) (ty:type) :=
{| ty_size := 1;
@@ -113,7 +113,7 @@ End uniq_bor.
Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
Section typing.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 6bf47379..5edf38b7 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -3,7 +3,7 @@ From lrust.typing Require Export type.
Set Default Proof Using "Type".
Section util.
- Context `{!typeG Σ}.
+ Context `{!typeGS Σ}.
(* Delayed sharing is used by various types; in particular own and uniq.
It comes in two flavors: Borrows of "later something" and borrows of
--
GitLab