diff options
48 files changed, 218 insertions, 71 deletions
@@ -10,6 +10,11 @@ Notations - New support for autonomous grammars of terms, called "custom entries" (see chapter "Syntax extensions" of the reference manual). +- New command "Declare Scope" to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is + deprecated. + Tactics - Added toplevel goal selector ! which expects a single focused goal. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index b46382dbbf..4c0e85bdd4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -949,16 +949,25 @@ Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See :ref:`above <NotationSyntax>` for the syntax of notations including the -possibility to declare them in a given scope. Here is a typical example which -declares the notation for conjunction in the scope ``type_scope``. +.. cmd:: Declare Scope @scope + + This adds a new scope named :n:`@scope`. Note that the initial + state of Coq declares by default the following interpretation scopes: + ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, + ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. + +The syntax to associate a notation to a scope is given +:ref:`above <NotationSyntax>`. Here is a typical example which declares the +notation for conjunction in the scope ``type_scope``. .. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. .. note:: A notation not defined in a scope is called a *lonely* - notation. + notation. No example of lonely notations can be found in the + initial state of Coq though. + Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -977,10 +986,6 @@ interpretation: otherwise said, only the order of lonely interpretations and opening of scopes matters, and not the declaration of interpretations within a scope). -The initial state of Coq declares three interpretation scopes and no -lonely notations. These scopes, in opening order, are ``core_scope``, -``type_scope`` and ``nat_scope``. - .. cmd:: Open Scope @scope The command to add a scope to the interpretation scope stack is diff --git a/interp/notation.ml b/interp/notation.ml index 55ead946cb..6b26f66100 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -98,21 +98,40 @@ let init_scope_map () = (**********************************************************************) (* Operations on scopes *) +let warn_undeclared_scope = + CWarnings.create ~name:"undeclared-scope" ~category:"deprecated" + (fun (scope) -> + strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit " + ++ str "\"Declare Scope " ++ str scope ++ str ".\".") + let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> -(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") -let find_scope scope = +let find_scope ?(tolerant=false) scope = try String.Map.find scope !scope_map - with Not_found -> error_unknown_scope scope + with Not_found -> + if tolerant then + (* tolerant mode to be turn off after deprecation phase *) + begin + warn_undeclared_scope scope; + scope_map := String.Map.add scope empty_scope !scope_map; + empty_scope + end + else + error_unknown_scope scope + +let check_scope ?(tolerant=false) scope = + let _ = find_scope ~tolerant scope in () + +let ensure_scope scope = check_scope ~tolerant:true scope -let check_scope sc = let _ = find_scope sc in () +let find_scope scope = find_scope scope (* [sc] might be here a [scope_name] or a [delimiter] (now allowed after Open Scope) *) @@ -418,7 +437,7 @@ type prim_token_infos = { let cache_prim_token_interpretation (_,infos) = let sc = infos.pt_scope in let uid = infos.pt_uid in - declare_scope sc; + check_scope ~tolerant:true sc; prim_token_interp_infos := String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; List.iter (fun r -> prim_token_uninterp_infos := diff --git a/interp/notation.mli b/interp/notation.mli index e5478eff48..6e59c0fd70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -41,6 +41,9 @@ type scopes (** = [scope_name list] *) val declare_scope : scope_name -> unit +(* To be removed after deprecation phase *) +val ensure_scope : scope_name -> unit + val current_scopes : unit -> scopes (** Check where a scope is opened or not in a scope list, or in diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 51b99b9935..da86f4274d 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -8,6 +8,7 @@ *************************************************************************) Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. +Declare Scope Int_scope. Delimit Scope Int_scope with I. (** * Abstract Integers. *) @@ -716,6 +717,7 @@ Inductive term : Set := | Topp : term -> term | Tvar : N -> term. +Declare Scope romega_scope. Bind Scope romega_scope with term. Delimit Scope romega_scope with term. Arguments Tint _%I. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index d9e32dbbf8..ce115f564f 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -19,6 +19,7 @@ Section MakeFieldPol. (* Field elements : R *) Variable R:Type. +Declare Scope R_scope. Bind Scope R_scope with R. Delimit Scope R_scope with ring. Local Open Scope R_scope. @@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth. (* Coefficients : C *) Variable C: Type. +Declare Scope C_scope. Bind Scope C_scope with C. Delimit Scope C_scope with coef. @@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N). (* Polynomial expressions : (PExpr C) *) +Declare Scope PE_scope. Bind Scope PE_scope with PExpr. Delimit Scope PE_scope with poly. diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 523c7b02eb..1ca6227f25 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. - Local Open Scope ZMORPHISM. + Declare Scope ZMORPHISM. + Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b4144aa45e..460bdc6d23 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,6 +86,7 @@ Export SsrSyntax. (* recognize the expansion of the boolean if; using the default printer *) (* avoids a spurrious trailing %GEN_IF. *) +Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. Notation "'if' c 'then' v1 'else' v2" := @@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (* Force boolean interpretation of simple if expressions. *) +Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. Notation "'if' c 'return' t 'then' v1 'else' v2" := @@ -125,6 +127,7 @@ Open Scope boolean_if_scope. (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) (* Lists library) should be loaded before ssreflect so that their notations *) (* do not mask all ssreflect forms. *) +Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b2d5143e36..99ff943e61 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -216,6 +216,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. @@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y) Notation "@^~ x" := (fun f => f x) (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 829ee05e11..9a53e1dd1a 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0). Reserved Notation "( a 'in' b 'in' c )" (at level 0). Reserved Notation "( a 'as' b 'in' c )" (at level 0). +Declare Scope ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + (* Notation to define shortcuts for the "X in t" part of a pattern. *) Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. -Delimit Scope ssrpatternscope with pattern. (* Some shortcuts for recurrent "X in t" parts. *) Notation RHS := (X in _ = X)%pattern. diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2170477938..85babd922b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -168,7 +168,8 @@ let classify_vernac e = | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) - | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacOpenCloseScope _ | VernacDeclareScope _ + | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index bd9240476f..b67ac4f0df 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -10,6 +10,8 @@ Arguments Nat.sub !n !m. About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). +Declare Scope foo_scope. +Declare Scope bar_scope. Delimit Scope foo_scope with F. Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. About pf. diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39e..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -76,6 +76,7 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. +Declare Scope znat_scope. Delimit Scope znat_scope with znat. Open Scope znat_scope. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 66a82008d8..42af3583d4 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -757,6 +757,8 @@ Qed. with lazy behavior (for vm_compute) *) (*****************************************) +Declare Scope lazy_bool_scope. + Notation "a &&& b" := (if a then b else false) (at level 40, left associativity) : lazy_bool_scope. Notation "a ||| b" := (if a then true else b) diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index 03e611f549..c376efef2e 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : crelation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 09b35ca75d..97510578ae 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -87,6 +87,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5217aedb88..516ea12099 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : relation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1858ba76ae..001b7dfdfd 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -88,6 +88,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 2ab3af2029..86a3a88be9 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -357,6 +357,8 @@ Definition predicate_implication {l : Tlist} := (** Notations for pointwise equivalence and implication of predicates. *) +Declare Scope predicate_scope. + Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 3485b9c68d..b0d1824827 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -25,6 +25,7 @@ Unset Strict Implicit. (** Notations and helper lemma about pairs *) +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1e6843d511..76c39f275d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -37,8 +37,8 @@ Inductive bool : Set := Add Printing If bool. +Declare Scope bool_scope. Delimit Scope bool_scope with bool. - Bind Scope bool_scope with bool. (** Basic boolean operators *) @@ -136,6 +136,7 @@ Inductive nat : Set := | O : nat | S : nat -> nat. +Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. Arguments S _%nat. @@ -228,10 +229,13 @@ Inductive list (A : Type) : Type := Arguments nil {A}. Arguments cons {A} a l. -Infix "::" := cons (at level 60, right associativity) : list_scope. + +Declare Scope list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. +Infix "::" := cons (at level 60, right associativity) : list_scope. + Local Open Scope list_scope. Definition length (A : Type) : list A -> nat := diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 1ff00ec11c..537400fb05 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,8 +42,11 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). +Declare Scope dec_uint_scope. Delimit Scope dec_uint_scope with uint. Bind Scope dec_uint_scope with uint. + +Declare Scope dec_int_scope. Delimit Scope dec_int_scope with int. Bind Scope dec_int_scope with int. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 72073bb4f6..8f8e639187 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -108,13 +108,17 @@ End IfNotations. (** Scopes *) -Delimit Scope type_scope with type. -Delimit Scope function_scope with function. +Declare Scope core_scope. Delimit Scope core_scope with core. -Bind Scope type_scope with Sortclass. +Declare Scope function_scope. +Delimit Scope function_scope with function. Bind Scope function_scope with Funclass. +Declare Scope type_scope. +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. + Open Scope core_scope. Open Scope function_scope. Open Scope type_scope. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6afba29a0..db8857df64 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -697,7 +697,7 @@ End Choice_lemmas. Section Dependent_choice_lemmas. - Variables X : Set. + Variable X : Set. Variable R : X -> X -> Prop. Lemma dependent_choice : diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index b966f217aa..aec88f93bf 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -340,6 +340,8 @@ Functional Scheme union_ind := Induction for union Sort Prop. (** Notations and helper lemma about pairs and triples *) +Declare Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index 3ba9d1f5ed..7b6740e94b 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -23,6 +23,7 @@ Inductive positive : Set := | xO : positive -> positive | xH : positive. +Declare Scope positive_scope. Delimit Scope positive_scope with positive. Bind Scope positive_scope with positive. Arguments xO _%positive. @@ -37,6 +38,7 @@ Inductive N : Set := | N0 : N | Npos : positive -> N. +Declare Scope N_scope. Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. @@ -53,6 +55,7 @@ Inductive Z : Set := | Zpos : positive -> Z | Zneg : positive -> Z. +Declare Scope Z_scope. Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 39af62c32f..77ab624ca5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,8 +15,6 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. -Declare ML Module "int31_syntax_plugin". - (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer @@ -50,6 +48,8 @@ Inductive int31 : Type := I31 : digits31 int31. Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. +Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 5a7bd9ab30..a70ecd19d8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -46,6 +46,7 @@ Module ZEuclidProp (** We put notations in a scope, to avoid warnings about redefinitions of notations *) + Declare Scope euclid. Infix "/" := D.div : euclid. Infix "mod" := D.modulo : euclid. Local Open Scope euclid. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 4b2d5c13b5..995d96b314 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,15 +13,18 @@ Require Import NSub ZAxioms. Require Export Ring. +Declare Scope pair_scope. +Local Open Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. Include NSubProp N. End NProp. +Declare Scope NScope. Delimit Scope NScope with N. Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. @@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. +Declare Scope ZScope. Delimit Scope ZScope with Z. Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 3d0c005fd1..acebfcf1d2 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -220,8 +220,10 @@ End NZDomainProp. Module NZOfNat (Import NZ:NZDomainSig'). Definition ofnat (n : nat) : t := (S^n) 0. -Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. + +Declare Scope ofnat. Local Open Scope ofnat. +Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. Lemma ofnat_zero : [O] == 0. Proof. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index f55093ed48..c2316689fc 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) := Hint Unfold compose. +Declare Scope program_scope. + Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 78c36dc7d1..c51cacac68 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -20,12 +20,13 @@ Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) (x ident, y ident, at level 10) : type_scope. +Declare Scope program_scope. +Delimit Scope program_scope with prg. + (** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _) : program_scope. -Delimit Scope program_scope with prg. - (** Abbreviation for first projection and hiding of proofs of subset objects. *) Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 35706e7fa2..139c4bf432 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -18,6 +18,7 @@ Require Export Morphisms Setoid Bool. Record Q : Set := Qmake {Qnum : Z; Qden : positive}. +Declare Scope Q_scope. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. Arguments Qmake _%Z _%positive. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 1510a7b825..81c318138e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -18,6 +18,7 @@ Require Import Eqdep_dec. Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. +Declare Scope Qc_scope. Delimit Scope Qc_scope with Qc. Bind Scope Qc_scope with Qc. Arguments Qcmake this%Q _. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 36ac738ca6..9f8039ec9d 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -28,6 +28,7 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x. Definition comp f1 f2 (x:R) : R := f1 (f2 x). Definition inv_fct f (x:R) : R := / f x. +Declare Scope Rfun_scope. Delimit Scope Rfun_scope with F. Arguments plus_fct (f1 f2)%F x%R. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 6019d4faf1..a2818371e9 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -14,6 +14,7 @@ Require Export ZArith_base. Require Export Rdefinitions. +Declare Scope R_scope. Local Open Scope R_scope. (*********************************************************) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 857b4ec33b..932fcddaf5 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,12 +12,15 @@ (** Definitions for the axiomatization *) (*********************************************************) -Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. -(* Declare Scope positive_scope with Key R *) +(* Declare primitive numeral notations for Scope R_scope *) +Declare Scope R_scope. +Declare ML Module "r_syntax_plugin". + +(* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 31a7fb8ad6..3f676c1888 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -13,7 +13,6 @@ Adapted to Coq V8 by the Coq Development Team *) Require Import Bool BinPos BinNat PeanoNat Nnat. -Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) @@ -21,6 +20,8 @@ Declare ML Module "ascii_syntax_plugin". Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). +Declare Scope char_scope. +Declare ML Module "ascii_syntax_plugin". Delimit Scope char_scope with char. Bind Scope char_scope with ascii. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index be9a10c6dc..b27474ef25 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -15,7 +15,6 @@ Require Import Arith. Require Import Ascii. Require Import Bool. -Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) @@ -25,6 +24,8 @@ Inductive string : Set := | EmptyString : string | String : ascii -> string -> string. +Declare Scope string_scope. +Declare ML Module "string_syntax_plugin". Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 87df6b479d..60c64d306b 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -132,6 +132,7 @@ Module OrderedTypeFacts (Import O: OrderedType'). Module OrderTac := OT_to_OrderTac O. Ltac order := OrderTac.order. + Declare Scope order. Notation "x <= y" := (~lt y x) : order. Infix "?=" := compare (at level 70, no associativity) : order. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index ba3e411091..390ca78c0e 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -305,6 +305,7 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni End VECTORLIST. Module VectorNotations. +Declare Scope vector_scope. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 2f3bf9a32a..1e35370d29 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -17,6 +17,7 @@ *) Require Import BinInt. +Declare Scope Int_scope. Delimit Scope Int_scope with I. Local Open Scope Int_scope. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74516e320c..44c0159d1b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram info = hint_info -> { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + (* Should be in syntax, but camlp5 would not factorize *) + | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> + { VernacDeclareScope sc } + (* System directory *) | IDENT "Pwd" -> { VernacChdir None } | IDENT "Cd" -> { VernacChdir None } @@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] -> { VernacSyntaxExtension (false, (s,l)) } - (* "Print" "Grammar" should be here but is in "command" entry in order - to factorize with other "Print"-based vernac entries *) + (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order + to factorize with other "Print"-based or "Declare"-based vernac entries *) ] ] ; only_parsing: diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d66a121437..2e5e11bb09 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1306,8 +1306,18 @@ type notation_obj = { notobj_notation : notation * notation_location; } -let load_notation _ (_, nobj) = - Option.iter Notation.declare_scope nobj.notobj_scope +let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = + (* When the default shall be to require that a scope already exists *) + (* the call to ensure_scope will have to be removed *) + if silently_define_scope_if_undefined then + (* Don't warn if the scope is not defined: *) + (* there was already a warning at "cache" time *) + Option.iter Notation.declare_scope nobj.notobj_scope + else + Option.iter Notation.ensure_scope nobj.notobj_scope + +let load_notation = + load_notation_common true let open_notation i (_, nobj) = let scope = nobj.notobj_scope in @@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) = end let cache_notation o = - load_notation 1 o; + load_notation_common false 1 o; open_notation 1 o let subst_notation (subst, nobj) = @@ -1566,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = add_notation local env c (df,modifiers) sc (**********************************************************************) -(* Delimiters and classes bound to scopes *) +(* Scopes, delimiters and classes bound to scopes *) type scope_command = - | ScopeDelim of string + | ScopeDeclare + | ScopeDelimAdd of string + | ScopeDelimRemove | ScopeClasses of scope_class list - | ScopeRemove - -let load_scope_command _ (_,(scope,dlm)) = - Notation.declare_scope scope -let open_scope_command i (_,(scope,o)) = +let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) = + let declare_scope_if_needed = + if silently_define_scope_if_undefined then Notation.declare_scope + else Notation.ensure_scope in + match o with + | ScopeDeclare -> Notation.declare_scope scope + (* When the default shall be to require that a scope already exists *) + (* the call to declare_scope_if_needed will have to be removed below *) + | ScopeDelimAdd dlm -> declare_scope_if_needed scope + | ScopeDelimRemove -> declare_scope_if_needed scope + | ScopeClasses cl -> declare_scope_if_needed scope + +let load_scope_command = + load_scope_command_common true + +let open_scope_command i (_,(local,scope,o)) = if Int.equal i 1 then match o with - | ScopeDelim dlm -> Notation.declare_delimiters scope dlm + | ScopeDeclare -> () + | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm + | ScopeDelimRemove -> Notation.remove_delimiters scope | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl - | ScopeRemove -> Notation.remove_delimiters scope let cache_scope_command o = - load_scope_command 1 o; + load_scope_command_common false 1 o; open_scope_command 1 o -let subst_scope_command (subst,(scope,o as x)) = match o with +let subst_scope_command (subst,(local,scope,o as x)) = match o with | ScopeClasses cl -> let cl' = List.map_filter (subst_scope_class subst) cl in let cl' = if List.for_all2eq (==) cl cl' then cl else cl' in - scope, ScopeClasses cl' + local, scope, ScopeClasses cl' | _ -> x -let inScopeCommand : scope_name * scope_command -> obj = +let classify_scope_command (local, _, _ as o) = + if local then Dispose else Substitute o + +let inScopeCommand : locality_flag * scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; - classify_function = (fun obj -> Substitute obj)} + classify_function = classify_scope_command} + +let declare_scope local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare)) -let add_delimiters scope key = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let add_delimiters local scope key = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key)) -let remove_delimiters scope = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) +let remove_delimiters local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove)) -let add_class_scope scope cl = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) +let add_class_scope local scope cl = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) (* Check if abbreviation to a name and avoid early insertion of maximal implicit arguments *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 73bee7121b..38dbdf7e41 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr -> val add_notation_extra_printing_rule : string -> string -> string -> unit -(** Declaring delimiter keys and default scopes *) +(** Declaring scopes, delimiter keys and default scopes *) -val add_delimiters : scope_name -> string -> unit -val remove_delimiters : scope_name -> unit -val add_class_scope : scope_name -> scope_class list -> unit +val declare_scope : locality_flag -> scope_name -> unit +val add_delimiters : locality_flag -> scope_name -> string -> unit +val remove_delimiters : locality_flag -> scope_name -> unit +val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 93e4e89a12..63e9e4fe49 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -635,6 +635,10 @@ open Pputils keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) + | VernacDeclareScope sc -> + return ( + keyword "Declare Scope" ++ spc () ++ str sc + ) | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 385e28f64b..681dce3ca3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -403,17 +403,24 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension atts infix l = +let vernac_syntax_extension ~atts infix l = let local = enforce_module_locality atts.locality in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l -let vernac_delimiters sc = function - | Some lr -> Metasyntax.add_delimiters sc lr - | None -> Metasyntax.remove_delimiters sc +let vernac_declare_scope ~atts sc = + let local = enforce_module_locality atts.locality in + Metasyntax.declare_scope local sc + +let vernac_delimiters ~atts sc action = + let local = enforce_module_locality atts.locality in + match action with + | Some lr -> Metasyntax.add_delimiters local sc lr + | None -> Metasyntax.remove_delimiters local sc -let vernac_bind_scope sc cll = - Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) +let vernac_bind_scope ~atts sc cll = + let local = enforce_module_locality atts.locality in + Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll) let vernac_open_close_scope ~atts (b,s) = let local = enforce_section_locality atts.locality in @@ -2093,9 +2100,10 @@ let interp ?proof ~atts ~st c = (* Syntax *) | VernacSyntaxExtension (infix, sl) -> - vernac_syntax_extension atts infix sl - | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr - | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl + vernac_syntax_extension ~atts infix sl + | VernacDeclareScope sc -> vernac_declare_scope ~atts sc + | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr + | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> @@ -2232,6 +2240,7 @@ let check_vernac_supports_locality c l = | Some _, ( VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _ | VernacDeclareCustomEntry _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 8fb74e6d78..11b2a7d802 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -325,6 +325,7 @@ type nonrec vernac_expr = (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name + | VernacDeclareScope of scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of (lstring * syntax_modifier list) * |