Commit ff9307a0 authored by Ralf Jung's avatar Ralf Jung
Browse files

mark Instances as Local/Global

parent 96191ed7
......@@ -16,7 +16,7 @@ test: $(TESTFILES:.v=.vo)
$(SHOW)"Performing some style checks..."
$(HIDE)for FILE in $(VFILES); do \
if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
if egrep '^\s*(Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
if egrep -n '^\s*((Existing\s+|Program\s+)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope)\b' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'/'Scope' (see above)."; echo "Please add 'Global' or 'Local' as appropriate."; echo; exit 1; fi \
done
# Make sure main Iris does not import other Iris packages.
$(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
......
......@@ -86,7 +86,7 @@ Local Instance agree_validN_instance : ValidN (agree A) := λ n x,
end.
Local Instance agree_valid_instance : Valid (agree A) := λ x, n, {n} x.
Program Instance agree_op_instance : Op (agree A) := λ x y,
Local Program Instance agree_op_instance : Op (agree A) := λ x y,
{| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
Local Instance agree_pcore_instance : PCore (agree A) := Some.
......
......@@ -795,7 +795,7 @@ Record rFunctor := RFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (rFunctor_map fg)
}.
Existing Instances rFunctor_map_ne rFunctor_mor.
Global Existing Instances rFunctor_map_ne rFunctor_mor.
Global Instance: Params (@rFunctor_map) 9 := {}.
Declare Scope rFunctor_scope.
......@@ -886,7 +886,7 @@ Record urFunctor := URFunctor {
(fg : (A2 -n> A1) * (B1 -n> B2)) :
CmraMorphism (urFunctor_map fg)
}.
Existing Instances urFunctor_map_ne urFunctor_mor.
Global Existing Instances urFunctor_map_ne urFunctor_mor.
Global Instance: Params (@urFunctor_map) 9 := {}.
Declare Scope urFunctor_scope.
......
......@@ -6,7 +6,7 @@ Record solution (F : oFunctor) := Solution {
solution_cofe : Cofe solution_car;
solution_iso :> ofe_iso (oFunctor_apply F solution_car) solution_car;
}.
Existing Instance solution_cofe.
Global Existing Instance solution_cofe.
Module solver. Section solver.
Context (F : oFunctor) `{Fcontr : oFunctorContractive F}.
......
......@@ -36,12 +36,12 @@ Inductive csum_equiv : Equiv (csum A B) :=
| Cinl_equiv a a' : a a' Cinl a Cinl a'
| Cinr_equiv b b' : b b' Cinr b Cinr b'
| CsumBot_equiv : CsumBot CsumBot.
Existing Instance csum_equiv.
Local Existing Instance csum_equiv.
Inductive csum_dist : Dist (csum A B) :=
| Cinl_dist n a a' : a {n} a' Cinl a {n} Cinl a'
| Cinr_dist n b b' : b {n} b' Cinr b {n} Cinr b'
| CsumBot_dist n : CsumBot {n} CsumBot.
Existing Instance csum_dist.
Local Existing Instance csum_dist.
Global Instance Cinl_ne : NonExpansive (@Cinl A B).
Proof. by constructor. Qed.
......
......@@ -44,7 +44,7 @@ Global Arguments dra_op : simpl never.
Global Arguments dra_valid : simpl never.
Global Arguments dra_mixin : simpl never.
Add Printing Constructor draT.
Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
Global Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
(** Lifting properties from the mixin *)
Section dra_mixin.
......@@ -146,10 +146,10 @@ Local Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
Lemma validity_valid_car_valid z : z validity_car z.
Proof. apply validity_prf. Qed.
Local Hint Resolve validity_valid_car_valid : core.
Program Instance validity_pcore_instance : PCore (validity A) := λ x,
Local Program Instance validity_pcore_instance : PCore (validity A) := λ x,
Some (Validity (core (validity_car x)) ( x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
Program Instance validity_op_instance : Op (validity A) := λ x y,
Local Program Instance validity_op_instance : Op (validity A) := λ x y,
Validity (validity_car x validity_car y)
( x y validity_car x ## validity_car y) _.
Solve Obligations with naive_solver eauto using dra_op_valid.
......
......@@ -29,11 +29,11 @@ Implicit Types x y : excl A.
Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a b Excl a Excl b
| ExclBot_equiv : ExclBot ExclBot.
Existing Instance excl_equiv.
Local Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a {n} b Excl a {n} Excl b
| ExclBot_dist n : ExclBot {n} ExclBot.
Existing Instance excl_dist.
Local Existing Instance excl_dist.
Global Instance Excl_ne : NonExpansive (@Excl A).
Proof. by constructor. Qed.
......
......@@ -535,7 +535,7 @@ Record ofe_mor (A B : ofe) : Type := OfeMor {
}.
Global Arguments OfeMor {_ _} _ {_}.
Add Printing Constructor ofe_mor.
Existing Instance ofe_mor_ne.
Global Existing Instance ofe_mor_ne.
Notation "'λne' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t) _) ..) _)
......@@ -710,7 +710,7 @@ Record oFunctor := OFunctor {
(f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
oFunctor_map (fg, g'f') x oFunctor_map (g,g') (oFunctor_map (f,f') x)
}.
Existing Instance oFunctor_map_ne.
Global Existing Instance oFunctor_map_ne.
Global Instance: Params (@oFunctor_map) 9 := {}.
Declare Scope oFunctor_scope.
......@@ -1329,7 +1329,7 @@ Section iso_cofe_subtype.
Context (g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2).
Let Hgne : NonExpansive g.
Proof. intros n y1 y2. apply g_dist. Qed.
Existing Instance Hgne.
Local Existing Instance Hgne.
Context (gf : x Hx, g (f x Hx) x).
Context (Hlimit : c : chain B, P (compl (chain_map g c))).
Program Definition iso_cofe_subtype : Cofe B :=
......
......@@ -27,7 +27,7 @@ Global Hint Mode IsOp' + ! - - : typeclass_instances.
Global Hint Mode IsOp' + - ! ! : typeclass_instances.
Class IsOp'LR {A : cmra} (a b1 b2 : A) := is_op_lr : IsOp a b1 b2.
Existing Instance is_op_lr | 0.
Global Existing Instance is_op_lr | 0.
Global Hint Mode IsOp'LR + ! - - : typeclass_instances.
Global Instance is_op_lr_op {A : cmra} (a b : A) : IsOp'LR (a b) a b | 0.
Proof. by rewrite /IsOp'LR /IsOp. Qed.
......
......@@ -196,7 +196,7 @@ Implicit Types T : tokens sts.
Inductive sts_equiv : Equiv (car sts) :=
| auth_equiv s T1 T2 : T1 T2 auth s T1 auth s T2
| frag_equiv S1 S2 T1 T2 : T1 T2 S1 S2 frag S1 T1 frag S2 T2.
Existing Instance sts_equiv.
Local Existing Instance sts_equiv.
Local Instance sts_valid_instance : Valid (car sts) := λ x,
match x with
| auth s T => tok s ## T
......@@ -212,7 +212,7 @@ Inductive sts_disjoint : Disjoint (car sts) :=
( s, s S1 S2) T1 ## T2 frag S1 T1 ## frag S2 T2
| auth_frag_disjoint s S T1 T2 : s S T1 ## T2 auth s T1 ## frag S T2
| frag_auth_disjoint s S T1 T2 : s S T1 ## T2 frag S T1 ## auth s T2.
Existing Instance sts_disjoint.
Local Existing Instance sts_disjoint.
Local Instance sts_op_instance : Op (car sts) := λ x1 x2,
match x1, x2 with
| frag S1 T1, frag S2 T2 => frag (S1 S2) (T1 T2)
......
......@@ -29,7 +29,7 @@ Structure gFunctor := GFunctor {
gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.
Global Arguments GFunctor _ {_}.
Existing Instance gFunctor_map_contractive.
Global Existing Instance gFunctor_map_contractive.
Add Printing Constructor gFunctor.
(** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
......
......@@ -32,7 +32,7 @@ Global Hint Mode Affine + ! : typeclass_instances.
Class BiAffine (PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
Global Hint Mode BiAffine ! : typeclass_instances.
Existing Instance absorbing_bi | 0.
Global Existing Instance absorbing_bi | 0.
Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : <affine> (P Q) <affine> P Q.
......
......@@ -9,7 +9,7 @@ Structure biIndex :=
bi_index_inhabited : Inhabited bi_index_type;
bi_index_rel : SqSubsetEq bi_index_type;
bi_index_rel_preorder : PreOrder (@{bi_index_type}) }.
Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
Global Existing Instances bi_index_inhabited bi_index_rel bi_index_rel_preorder.
(* We may want to instantiate monPred with the reflexivity relation in
the case where there is no relevent order. In that case, there is
......
......@@ -62,7 +62,7 @@ Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
Definition twp' := twp_aux.(unseal).
Global Arguments twp' {Λ Σ _}.
Existing Instance twp'.
Global Existing Instance twp'.
Lemma twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
Proof. rewrite -twp_aux.(seal_eq) //. Qed.
......
......@@ -78,7 +78,7 @@ Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
Definition wp' := wp_aux.(unseal).
Global Arguments wp' {Λ Σ _}.
Existing Instance wp'.
Global Existing Instance wp'.
Lemma wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
Proof. rewrite -wp_aux.(seal_eq) //. Qed.
......
......@@ -512,7 +512,7 @@ Global Arguments AsEmpValid {_} _%type _%I.
Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
as_emp_valid_0 : AsEmpValid φ P.
Global Arguments AsEmpValid0 {_} _%type _%I.
Existing Instance as_emp_valid_0 | 0.
Global Existing Instance as_emp_valid_0 | 0.
Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
φ P.
......@@ -570,7 +570,7 @@ Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
(* The typeclass used for the [iInv] tactic.
Input: [Pinv]
Arguments:
Other Arguments:
- [Pinv] is an invariant assertion
- [Pin] is an additional logic assertion needed for opening an invariant
- [φ] is an additional Coq assertion needed for opening an invariant
......
......@@ -931,7 +931,7 @@ Inductive IntoModalIntuitionisticEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 P
| MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
Existing Class IntoModalIntuitionisticEnv.
Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
Global Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
(* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
......@@ -963,7 +963,7 @@ Inductive IntoModalSpatialEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
| MIEnvId_spatial (M : modality PROP2 PROP2) Γ :
IntoModalSpatialEnv M Γ Γ MIEnvId false.
Existing Class IntoModalSpatialEnv.
Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
Global Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
MIEnvTransform_spatial MIEnvClear_spatial MIEnvId_spatial.
Section tac_modal_intro.
......
......@@ -147,7 +147,7 @@ End increment.
Section increment_client.
Context `{!heapG Σ, !spawnG Σ}.
Existing Instance primitive_atomic_heap.
Local Existing Instance primitive_atomic_heap.
Definition incr_client : val :=
λ: "x",
......
......@@ -36,7 +36,7 @@ Global Arguments release {_ _} _.
Global Arguments is_lock {_ _} _ _ _ _.
Global Arguments locked {_ _} _ _.
Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Global Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Global Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) γ lk:
Proper (() ==> ()) (is_lock L γ lk) := ne_proper _.
......@@ -14,7 +14,7 @@ Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
Program Instance loc_infinite : Infinite loc :=
Global Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
Next Obligation. done. Qed.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment