From 53c9d30c7fcb1ed75d509d14ce884bee5aebbe98 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 22 Feb 2019 18:44:52 +0100
Subject: [PATCH] never genrealize without a !
---
theories/lang/adequacy.v | 4 +-
theories/lang/heap.v | 4 +-
theories/lang/lang.v | 2 +-
theories/lang/lib/memcpy.v | 2 +-
theories/lang/lib/new_delete.v | 2 +-
theories/lang/lib/swap.v | 2 +-
theories/lang/lifting.v | 4 +-
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 | 18 +++---
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 | 4 +-
theories/lifetime/model/faking.v | 2 +-
theories/lifetime/model/primitive.v | 2 +-
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 | 20 +++---
theories/typing/function.v | 8 +--
theories/typing/int.v | 4 +-
theories/typing/lft_contexts.v | 4 +-
theories/typing/lib/cell.v | 4 +-
theories/typing/lib/fake_shared.v | 2 +-
theories/typing/lib/option.v | 2 +-
theories/typing/lib/panic.v | 2 +-
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/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 | 8 +--
theories/typing/sum.v | 2 +-
theories/typing/type.v | 64 +++++++++----------
theories/typing/type_context.v | 4 +-
theories/typing/type_sum.v | 2 +-
theories/typing/uninit.v | 2 +-
theories/typing/uniq_bor.v | 4 +-
65 files changed, 150 insertions(+), 150 deletions(-)
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 7ea33f07..05315b8c 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -17,8 +17,8 @@ Definition lrustΣ : gFunctors :=
Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
Proof. solve_inG. Qed.
-Definition lrust_adequacy Σ `{lrustPreG Σ} e σ φ :
- (∀ `{lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌠}}) →
+Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
+ (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌠}}) →
adequate NotStuck e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 590b23f7..38b14062 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
qs.2 ≠∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
Section definitions.
- Context `{heapG Σ}.
+ Context `{!heapG Σ}.
Definition heap_mapsto_st (st : lock_state)
(l : loc) (q : Qp) (v: val) : iProp Σ :=
@@ -106,7 +106,7 @@ Section to_heap.
End to_heap.
Section heap.
- Context `{heapG Σ}.
+ Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types σ : state.
Implicit Types E : coPset.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index cd64baa2..c302a1c3 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -91,7 +91,7 @@ Proof. rewrite /Closed. apply _. Qed.
Inductive val :=
| LitV (l : base_lit)
-| RecV (f : binder) (xl : list binder) (e : expr) `{Closed (f :b: xl +b+ []) e}.
+| RecV (f : binder) (xl : list binder) (e : expr) `{!Closed (f :b: xl +b+ []) e}.
Bind Scope val_scope with val.
diff --git a/theories/lang/lib/memcpy.v b/theories/lang/lib/memcpy.v
index 6cf5ee8c..1897f020 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 `{!lrustG Σ} 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 1feb16e7..6a4be069 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 `{!lrustG Σ}.
Lemma wp_new E n:
0 ≤ n →
diff --git a/theories/lang/lib/swap.v b/theories/lang/lib/swap.v
index 8550d80b..d182c900 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 `{!lrustG Σ} 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/lifting.v b/theories/lang/lifting.v
index 2da5f05e..4bac7690 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -11,7 +11,7 @@ Class lrustG Σ := LRustG {
lrustG_gen_heapG :> heapG Σ
}.
-Instance lrustG_irisG `{lrustG Σ} : irisG lrust_lang Σ := {
+Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
iris_invG := lrustG_invG;
state_interp σ κs _ := heap_ctx σ;
fork_post _ := True%I;
@@ -61,7 +61,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 `{!lrustG Σ}.
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 4abc2eaa..a1b3db3e 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -6,14 +6,14 @@ From iris.program_logic Require Import lifting.
Set Default Proof Using "Type".
Import uPred.
-Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{!lrustG Σ} Δ 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 `{!lrustG Σ} 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 `{!lrustG Σ} 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 `{!lrustG Σ} 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 `{!lrustG Σ}.
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 3373c818..e982eb17 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 `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
+Definition at_bor `{!invG Σ, !lftG Σ} κ 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 `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
+ Context `{!invG Σ, !lftG Σ} (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 `{invG Σ, lftG Σ} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ} (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 489ed417..e844bbda 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -7,13 +7,13 @@ Set Default Proof Using "Type".
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
-Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invG Σ, !lftG Σ, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
(∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (∃ q, φ q ∗ own γ q ∗
(⌜q = 1%Qp⌠∨ ∃ q', ⌜(q + q' = 1)%Qp⌠∗ q'.[κ'])))%I.
Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
Section frac_bor.
- Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp → iProp Σ).
+ Context `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp → iProp Σ).
Implicit Types E : coPset.
Global Instance frac_bor_contractive κ n :
@@ -112,7 +112,7 @@ Section frac_bor.
iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
Qed.
- Lemma frac_bor_acc E q κ `{Fractional _ φ} :
+ Lemma frac_bor_acc E q κ `{!Fractional φ} :
↑lftN ⊆ E →
lft_ctx -∗ &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
Proof.
@@ -134,7 +134,7 @@ Section frac_bor.
Qed.
End frac_bor.
-Lemma frac_bor_lft_incl `{invG Σ, lftG Σ, frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 735ae6d1..fe1429b7 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -23,7 +23,7 @@ Instance lft_inhabited : Inhabited lft := populate static.
Canonical lftC := leibnizC lft.
Section derived.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma bor_acc_atomic_cons E κ P :
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index fe4827cd..eb1d9569 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -23,17 +23,17 @@ Module Type lifetime_sig.
Parameter static : lft.
Parameter lft_intersect : lft → lft → lft.
- Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
+ Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ}, iProp Σ.
- Parameter lft_tok : ∀ `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
- Parameter lft_dead : ∀ `{lftG Σ} (κ : lft), iProp Σ.
+ Parameter lft_tok : ∀ `{!lftG Σ} (q : Qp) (κ : lft), iProp Σ.
+ Parameter lft_dead : ∀ `{!lftG Σ} (κ : lft), iProp Σ.
- Parameter lft_incl : ∀ `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
- Parameter bor : ∀ `{invG, lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
+ Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ} (κ κ' : lft), iProp Σ.
+ Parameter bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
Parameter bor_idx : Type.
- Parameter idx_bor_own : ∀ `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
- Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+ Parameter idx_bor_own : ∀ `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
+ Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
(** Notation *)
Notation "q .[ κ ]" := (lft_tok q κ)
@@ -47,7 +47,7 @@ Module Type lifetime_sig.
Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
Section properties.
- Context `{invG, lftG Σ}.
+ Context `{!invG Σ, !lftG Σ}.
(** Instances *)
Global Declare Instance lft_inhabited : Inhabited lft.
@@ -155,6 +155,6 @@ Module Type lifetime_sig.
Parameter lftΣ : gFunctors.
Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
- Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
+ Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
(|={E}=> ∃ _ : lftG Σ, lft_ctx)%I.
End lifetime_sig.
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index 0cd3d78d..573c4456 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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
(* Helper internal lemmas *)
diff --git a/theories/lifetime/model/borrow.v b/theories/lifetime/model/borrow.v
index 8138b837..03ff321d 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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
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 45ba12f1..70b98634 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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma bor_sep E κ P Q :
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 152af548..9c336443 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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
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 ae52a295..8342a18c 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -79,7 +79,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 `{invG Σ, lftG Σ}.
+ Context `{!invG Σ, !lftG Σ}.
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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
(* Unfolding lemmas *)
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 4dcbb159..decf7ad3 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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma ilft_create A I κ :
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 19ca418d..c633f1dd 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Import uPred.
Section primitive.
-Context `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
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 b0c84dd1..d7e2e4b0 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 `{invG Σ, lftG Σ}.
+Context `{!invG Σ, !lftG Σ}.
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 41551687..7af98c9e 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 `{invG Σ, lftG Σ, na_invG Σ}
+Definition na_bor `{!invG Σ, !lftG Σ, !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 `{invG Σ, lftG Σ, na_invG Σ}
+ Context `{!invG Σ, !lftG Σ, !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 4a4d6a15..3375a9cb 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 `{!typeG Σ}.
Program Definition bool : type :=
{| st_own tid vl :=
@@ -22,7 +22,7 @@ Section bool.
End bool.
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
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 6ab60442..7557c5de 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 `{!typeG Σ}.
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 02ef7650..1011aa94 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 `{!typeG Σ}.
(** 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 a86297a4..c29c7315 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 `{!typeG Σ}.
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 `{!typeG Σ}.
Definition cctx_elt_interp (tid : thread_id) (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 3052ba5a..e71c3dec 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 `{!typeG Σ}.
Definition get_x : val :=
funrec: <> ["p"] :=
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index 77b4de91..49723aed 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 `{!typeG Σ}.
Definition init_prod : val :=
funrec: <> ["x"; "y"] :=
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index 1efdcf94..0bc054bc 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 `{!typeG Σ}.
Definition lazy_lft : val :=
funrec: <> [] :=
diff --git a/theories/typing/examples/nonlexical.v b/theories/typing/examples/nonlexical.v
index 6510eff8..2666af36 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 `{!typeG Σ} (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 c8b0b127..e761beeb 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 `{!typeG Σ}.
Definition rebor : val :=
funrec: <> ["t1"; "t2"] :=
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index cb63526d..b27bbd92 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 `{!typeG Σ}.
Definition unbox : val :=
funrec: <> ["b"] :=
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index f93012b0..58a14e00 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 `{!typeG Σ}.
Context (T : type → type) {HT: TypeContractive T}.
Global Instance type_inhabited : Inhabited type := populate bool.
@@ -25,7 +25,7 @@ Section fixpoint_def.
I believe this gives the right sets for all types that we can define in
Rust, but I do not have any proof of this.
TODO : investigate this in more detail. *)
- Global Instance type_fixpoint_wf `{∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
+ Global Instance type_fixpoint_wf `{!∀ `{!TyWf ty}, TyWf (T ty)} : TyWf type_fixpoint :=
let lfts :=
let _ : TyWf type_fixpoint := {| ty_lfts := []; ty_wf_E := [] |} in
(T type_fixpoint).(ty_lfts)
@@ -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 `{!typeG Σ} (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 `{!typeG Σ}.
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 `{!typeG Σ} (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} :
@@ -114,7 +114,7 @@ Section subtyping.
apply bi.limit_preserving_entails; solve_proper.
Qed.
- Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
+ Lemma fixpoint_proper T1 `{!TypeContractive T1} T2 `{!TypeContractive T2} :
(∀ ty1 ty2, eqtype E L ty1 ty2 → eqtype E L (T1 ty1) (T2 ty2)) →
eqtype E L (type_fixpoint T1) (type_fixpoint T2).
Proof.
@@ -127,16 +127,16 @@ Section subtyping.
apply bi.limit_preserving_entails; solve_proper.
Qed.
- Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
+ Lemma fixpoint_unfold_subtype_l ty T `{!TypeContractive T} :
subtype E L ty (T (type_fixpoint T)) → subtype E L ty (type_fixpoint T).
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
- Lemma fixpoint_unfold_subtype_r ty T `{TypeContractive T} :
+ Lemma fixpoint_unfold_subtype_r ty T `{!TypeContractive T} :
subtype E L (T (type_fixpoint T)) ty → subtype E L (type_fixpoint T) ty.
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
- Lemma fixpoint_unfold_eqtype_l ty T `{TypeContractive T} :
+ Lemma fixpoint_unfold_eqtype_l ty T `{!TypeContractive T} :
eqtype E L ty (T (type_fixpoint T)) → eqtype E L ty (type_fixpoint T).
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
- Lemma fixpoint_unfold_eqtype_r ty T `{TypeContractive T} :
+ Lemma fixpoint_unfold_eqtype_r ty T `{!TypeContractive T} :
eqtype E L (T (type_fixpoint T)) ty → eqtype E L (type_fixpoint T) ty.
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
End subtyping.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 73aed282..6fe52645 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 `{!typeG Σ} {A : Type} {n : nat}.
Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
@@ -141,7 +141,7 @@ Notation "'fn(' E ')' '→' R" :=
Instance elctx_empty : Empty (lft → elctx) := λ Ï, [].
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Lemma fn_subtype {A n} E0 L0 (fp fp' : A → fn_params n) :
(∀ x Ï, let EE := E0 ++ (fp' x).(fp_E) Ï in
@@ -390,7 +390,7 @@ Section typing.
Qed.
Lemma type_rec {A} E L fb (argsb : list binder) ef e n
- (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+ (fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
IntoVal ef (funrec: fb argsb := e) →
n = length argsb →
â–¡ (∀ x Ï (f : val) k (args : vec val (length argsb)),
@@ -413,7 +413,7 @@ Section typing.
Qed.
Lemma type_fn {A} E L (argsb : list binder) ef e n
- (fp : A → fn_params n) T `{!CopyC T, !SendC T, Closed _ e} :
+ (fp : A → fn_params n) T `{!CopyC T, !SendC T, !Closed _ e} :
IntoVal ef (funrec: <> argsb := e) →
n = length argsb →
â–¡ (∀ x Ï k (args : vec val (length argsb)),
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 5f94433c..0b3d8e1c 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 `{!typeG Σ}.
Program Definition int : type :=
{| st_own tid vl :=
@@ -22,7 +22,7 @@ Section int.
End int.
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
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 12913694..eead3bd4 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -22,7 +22,7 @@ Notation llctx := (list llctx_elt).
Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
Section lft_contexts.
- Context `{invG Σ, lftG Σ}.
+ Context `{!invG Σ, !lftG Σ}.
Implicit Type (κ : lft).
(* External lifetime contexts. *)
@@ -308,7 +308,7 @@ Arguments elctx_sat {_ _ _} _ _ _.
Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
-Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
+Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} 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/cell.v b/theories/typing/lib/cell.v
index dea59d49..c3c80027 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 `{!typeG Σ}.
Program Definition cell (ty : type) :=
{| ty_size := ty.(ty_size);
@@ -79,7 +79,7 @@ Section cell.
End cell.
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
(** 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/fake_shared.v b/theories/typing/lib/fake_shared.v
index 7d50663f..384b44cf 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 `{!typeG Σ}.
Definition fake_shared_box : val :=
funrec: <> ["x"] := Skip ;; return: ["x"].
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 8ac02855..b7d0b2fd 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 `{!typeG Σ}.
Definition option (τ : type) := Σ[unit; τ]%T.
diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 5296c6c4..f6a6b094 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 `{!typeG Σ}.
Definition panic : val :=
funrec: <> [] := #☠.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index 91852456..6f403685 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 `{!typeG Σ, !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 b791f605..181d9dde 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell ref.
Set Default Proof Using "Type".
Section ref_functions.
- Context `{typeG Σ, refcellG Σ}.
+ Context `{!typeG Σ, !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 f8ad3495..ebb22eba 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 `{!typeG Σ, !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 `{!typeG Σ, !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 8c10eb20..a70435da 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -9,7 +9,7 @@ From lrust.typing.lib.refcell Require Import refcell ref refmut.
Set Default Proof Using "Type".
Section refcell_functions.
- Context `{typeG Σ, refcellG Σ}.
+ Context `{!typeG Σ, !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 a00a34f9..c8e0f46c 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 `{!typeG Σ, !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 fa5374c6..719970bd 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.refcell Require Import refcell refmut.
Set Default Proof Using "Type".
Section refmut_functions.
- Context `{typeG Σ, refcellG Σ}.
+ Context `{!typeG Σ, !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 2ee4f34a..4d4e1a47 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 `{!typeG Σ, !rwlockG Σ}.
Definition rwlock_inv tid (l : loc) (γ : gname) (α : lft) ty : iProp Σ :=
(∃ st, l ↦ #(Z_of_rwlock_st st) ∗ own γ (◠st) ∗
@@ -83,7 +83,7 @@ Section rwlock_inv.
End rwlock_inv.
Section rwlock.
- Context `{typeG Σ, rwlockG Σ}.
+ Context `{!typeG Σ, !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 22876856..964ecea9 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -9,7 +9,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwritegu
Set Default Proof Using "Type".
Section rwlock_functions.
- Context `{typeG Σ, rwlockG Σ}.
+ Context `{!typeG Σ, !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 692a354e..e8878646 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 `{!typeG Σ, !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 c0e61e1b..fccc7cea 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
Set Default Proof Using "Type".
Section rwlockreadguard_functions.
- Context `{typeG Σ, rwlockG Σ}.
+ Context `{!typeG Σ, !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 e48927ad..ef2e9d2b 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 `{!typeG Σ, !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 9b15a6c8..b9c9010a 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -8,7 +8,7 @@ From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
Set Default Proof Using "Type".
Section rwlockwriteguard_functions.
- Context `{typeG Σ, rwlockG Σ}.
+ Context `{!typeG Σ, !rwlockG Σ}.
(* Turning a rwlockwriteguard into a shared borrow. *)
Definition rwlockwriteguard_deref : val :=
diff --git a/theories/typing/lib/swap.v b/theories/typing/lib/swap.v
index b1aef757..2b631d86 100644
--- a/theories/typing/lib/swap.v
+++ b/theories/typing/lib/swap.v
@@ -4,7 +4,7 @@ From lrust.lang.lib Require Import swap.
Set Default Proof Using "Type".
Section swap.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Definition swap ty : val :=
funrec: <> ["p1"; "p2"] :=
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 2e075ad5..b051af66 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 `{!typeG Σ}.
Definition take ty (call_once : val) : val :=
funrec: <> ["x"; "f"] :=
diff --git a/theories/typing/own.v b/theories/typing/own.v
index c3c8dcfc..7280e94c 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import util uninit type_context programs.
Set Default Proof Using "Type".
Section own.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Program Definition freeable_sz (n : nat) (sz : nat) (l : loc) : iProp Σ :=
match sz, n return _ with
@@ -147,7 +147,7 @@ Section own.
End own.
Section box.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Definition box ty := own_ptr ty.(ty_size) ty.
@@ -184,7 +184,7 @@ Section box.
End box.
Section util.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Lemma ownptr_own n ty tid v :
(own_ptr n ty).(ty_own) tid [v] ⊣⊢
@@ -215,7 +215,7 @@ Section util.
End util.
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
(** Typing *)
Lemma write_own {E L} ty ty' n :
diff --git a/theories/typing/product.v b/theories/typing/product.v
index fbc9fdfb..7076ceaa 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 `{!typeG Σ}.
(* 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 `{!typeG Σ}.
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 8130c5ae..ac417767 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -5,7 +5,7 @@ From lrust.typing Require Import type_context lft_contexts product own uniq_bor
Set Default Proof Using "Type".
Section product_split.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
(** 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 5a298fa4..a5bea9a8 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 `{!typeG Σ}.
(** Function Body *)
(* This is an iProp because it is also used by the function type. *)
@@ -77,17 +77,17 @@ Section typing.
Global Arguments typed_read _ _ _%T _%T _%T.
End typing.
-Definition typed_instruction_ty `{typeG Σ} (E : elctx) (L : llctx) (T : tctx)
+Definition typed_instruction_ty `{!typeG Σ} (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 `{!typeG Σ} (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 `{!typeG Σ}.
(* 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 b3a58cbf..4a447451 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 `{!typeG Σ}.
Program Definition shr_bor (κ : lft) (ty : type) : type :=
{| st_own tid vl :=
@@ -60,7 +60,7 @@ End shr_bor.
Notation "&shr{ κ }" := (shr_bor κ) (format "&shr{ κ }") : lrust_type_scope.
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
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 096937a6..84f4c4d3 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -22,10 +22,10 @@ Proof. solve_inG. Qed.
Section type_soundness.
Definition exit_cont : val := λ: [<>], #☠.
- Definition main_type `{typeG Σ} := (fn(∅) → unit)%T.
+ Definition main_type `{!typeG Σ} := (fn(∅) → unit)%T.
- Theorem type_soundness `{typePreG Σ} (main : val) σ t :
- (∀ `{typeG Σ}, typed_val main main_type) →
+ Theorem type_soundness `{!typePreG Σ} (main : val) σ t :
+ (∀ `{!typeG Σ}, 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 σ).
@@ -60,7 +60,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) →
+ (∀ `{!typeG 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 97b9abfa..2e690507 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -5,7 +5,7 @@ From lrust.typing Require Export type.
Set Default Proof Using "Type".
Section sum.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
(* 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 88a28ae5..9f2a0c37 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -18,7 +18,7 @@ Definition shrN := lrustN .@ "shr".
Definition thread_id := na_inv_pool_name.
-Record type `{typeG Σ} :=
+Record type `{!typeG Σ} :=
{ 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 `{!typeG Σ} (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 `{!typeG Σ} 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 `{!typeG Σ} 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 TyWfLst `{typeG Σ} : list type → Type :=
+Inductive TyWfLst `{!typeG Σ} : list type → Type :=
| tyl_wf_nil : TyWfLst []
| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
Existing Class TyWfLst.
Existing Instances tyl_wf_nil tyl_wf_cons.
-Fixpoint tyl_lfts `{typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
match WF with
| tyl_wf_nil => []
| tyl_wf_cons ty [] => ty.(ty_lfts)
| tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
end.
-Fixpoint tyl_wf_E `{typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
match WF with
| tyl_wf_nil => []
| tyl_wf_cons ty [] => ty.(ty_wf_E)
| tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
end.
-Fixpoint tyl_outlives_E `{typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
match WF with
| tyl_wf_nil => []
| tyl_wf_cons ty [] => ty_outlives_E ty κ
| tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
end.
-Lemma tyl_outlives_E_elctx_sat `{typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : TyWfLst 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 `{!typeG Σ} :=
{ 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 `{!typeG Σ} (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
@@ -148,7 +148,7 @@ Bind Scope lrust_type_scope with type.
(* OFE and COFE structures on types and simple types. *)
Section ofe.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Inductive type_equiv' (ty1 ty2 : type) : Prop :=
Type_equiv :
@@ -259,7 +259,7 @@ End ofe.
(** Special metric for type-nonexpansive and Type-contractive functions. *)
Section type_dist2.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
(* 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:
@@ -327,7 +327,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 `{!typeG Σ}.
Lemma type_ne_dist_later T :
TypeNonExpansive T → ∀ n, Proper (type_dist2_later n ==> type_dist2_later n) T.
@@ -388,7 +388,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 `{!typeG Σ} (t : type) := {
copy_persistent tid vl : Persistent (t.(ty_own) tid vl);
copy_shr_acc κ tid E F l q :
lftE ∪ ↑shrN ⊆ E → shr_locsE l (t.(ty_size) + 1) ⊆ F →
@@ -401,34 +401,34 @@ Class Copy `{typeG Σ} (t : type) := {
Existing Instances copy_persistent.
Instance: Params (@Copy) 2 := {}.
-Class LstCopy `{typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Class LstCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
Instance: Params (@LstCopy) 2 := {}.
-Global Instance lst_copy_nil `{typeG Σ} : LstCopy [] := List.Forall_nil _.
-Global Instance lst_copy_cons `{typeG Σ} ty tys :
+Global Instance lst_copy_nil `{!typeG Σ} : LstCopy [] := List.Forall_nil _.
+Global Instance lst_copy_cons `{!typeG Σ} ty tys :
Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _.
-Class Send `{typeG Σ} (t : type) :=
+Class Send `{!typeG Σ} (t : type) :=
send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
Instance: Params (@Send) 2 := {}.
-Class LstSend `{typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Class LstSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
Instance: Params (@LstSend) 2 := {}.
-Global Instance lst_send_nil `{typeG Σ} : LstSend [] := List.Forall_nil _.
-Global Instance lst_send_cons `{typeG Σ} ty tys :
+Global Instance lst_send_nil `{!typeG Σ} : LstSend [] := List.Forall_nil _.
+Global Instance lst_send_cons `{!typeG Σ} ty tys :
Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _.
-Class Sync `{typeG Σ} (t : type) :=
+Class Sync `{!typeG Σ} (t : type) :=
sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
Instance: Params (@Sync) 2 := {}.
-Class LstSync `{typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Class LstSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
Instance: Params (@LstSync) 2 := {}.
-Global Instance lst_sync_nil `{typeG Σ} : LstSync [] := List.Forall_nil _.
-Global Instance lst_sync_cons `{typeG Σ} ty tys :
+Global Instance lst_sync_nil `{!typeG Σ} : LstSync [] := List.Forall_nil _.
+Global Instance lst_sync_cons `{!typeG Σ} ty tys :
Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _.
Section type.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
(** Copy types *)
Lemma shr_locsE_shift l n m :
@@ -519,24 +519,24 @@ Section type.
Qed.
End type.
-Definition type_incl `{typeG Σ} (ty1 ty2 : type) : iProp Σ :=
+Definition type_incl `{!typeG Σ} (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 subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+Definition subtype `{!typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
∀ qL, llctx_interp 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 `{!typeG Σ} (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 `{!typeG Σ}.
Global Instance type_incl_ne : NonExpansive2 type_incl.
Proof.
@@ -670,7 +670,7 @@ Section subtyping.
End subtyping.
Section type_util.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
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 bc169ec8..e56f40df 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 `{!typeG Σ} : 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 `{!typeG Σ}.
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 c4fceaee..cf00d06c 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 `{!typeG Σ}.
(* FIXME : have a 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 28875d50..214c359f 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 `{!typeG Σ}.
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 0b6923af..d796d3f8 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 `{!typeG Σ}.
Program Definition uniq_bor (κ:lft) (ty:type) :=
{| ty_size := 1;
@@ -98,7 +98,7 @@ End uniq_bor.
Notation "&uniq{ κ }" := (uniq_bor κ) (format "&uniq{ κ }") : lrust_type_scope.
Section typing.
- Context `{typeG Σ}.
+ Context `{!typeG Σ}.
Lemma uniq_mono' E L κ1 κ2 ty1 ty2 :
lctx_lft_incl E L κ2 κ1 → eqtype E L ty1 ty2 →
--
GitLab