From 83e22b5abc05902d1468d1cf033251dae46b69bc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 17 Mar 2020 10:37:30 +0100 Subject: Renaming "ident" into "name" in grammar entries, to prevent confusions. We use a deprecation phase where: - "ident" means "name" (as it used to mean), except in custom coercion entries where it already meant "ident". - "ident" will be made again available (outside situation of coercions) to mean "ident" at the end of deprecation phase. Also renaming "as ident" into "as name". Co-authored-by: Jim Fehrle --- ...istinguishing-ident-name-in-grammar-entries.rst | 13 +++++++++ interp/constrintern.ml | 13 +++++++-- interp/notation.ml | 3 +- interp/notation_ops.ml | 4 +-- interp/notation_term.ml | 5 +++- parsing/extend.ml | 2 ++ parsing/extend.mli | 2 ++ vernac/egramcoq.ml | 11 ++++++++ vernac/g_vernac.mlg | 17 ++++++++++-- vernac/metasyntax.ml | 32 ++++++++++++++++------ vernac/ppvernac.ml | 5 +++- 11 files changed, 87 insertions(+), 20 deletions(-) create mode 100644 doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst new file mode 100644 index 0000000000..8d681361e8 --- /dev/null +++ b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst @@ -0,0 +1,13 @@ +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 `_, + fixes `#9514 `_, + by Hugo Herbelin). diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8bd77abc4a..0645636255 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -976,6 +976,9 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) +let cases_pattern_of_id {loc;v=id} = + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + let cases_pattern_of_name {loc;v=na} = let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) @@ -991,16 +994,20 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> + let a,terms = match terms with a::terms -> a,terms | _ -> assert false in + let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder NtnBinderParsedAsConstr AsName -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> - let onlyident = (x = NtnParsedAsIdent) in + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> + let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in let binders,binders' = bind id (onlyident,scl) binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> diff --git a/interp/notation.ml b/interp/notation.ml index b5951a9c59..c35ba44aa5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -62,10 +62,11 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsName, NtnParsedAsName -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 | NtnParsedAsBinder, NtnParsedAsBinder -> true -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false +| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f51d3bfdfb..036970ce37 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -881,7 +881,7 @@ let is_onlybinding_meta id metas = let is_onlybinding_pattern_like_meta isvar id metas = try match Id.List.assoc id metas with | _,NtnTypeBinder (NtnBinderParsedAsConstr - (AsIdentOrPattern | AsStrictPattern)) -> true + (AsNameOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) | _,NtnTypeBinder NtnParsedAsBinder -> not isvar | _ -> false @@ -1533,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) = let v = glob_constr_of_cases_pattern (Global.env()) pat in (((vars,v),scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 29db23cc54..c541a19bfd 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes type constr_as_binder_kind = | AsIdent - | AsIdentOrPattern + | AsName + | AsNameOrPattern | AsStrictPattern type notation_binder_source = @@ -76,6 +77,8 @@ type notation_binder_source = | NtnParsedAsPattern of bool (* This accepts only ident *) | NtnParsedAsIdent + (* This accepts only name *) + | NtnParsedAsName (* This accepts ident, or pattern, or both *) | NtnBinderParsedAsConstr of constr_as_binder_kind (* This accepts ident, _, and quoted pattern *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 94c3768116..7d2ed9aed0 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -32,6 +32,7 @@ let production_level_eq lev1 lev2 = type 'a constr_entry_key_gen = | ETIdent + | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *) | ETGlobal | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) @@ -55,6 +56,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list type binder_target = ForBinder | ForTerm type constr_prod_entry_key = + | ETProdIdent (* Parsed as an ident *) | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) diff --git a/parsing/extend.mli b/parsing/extend.mli index b698415fd6..3cea45c3f5 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -27,6 +27,7 @@ val production_level_eq : production_level -> production_level -> bool type 'a constr_entry_key_gen = | ETIdent + | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *) | ETGlobal | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) @@ -50,6 +51,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list type binder_target = ForBinder | ForTerm type constr_prod_entry_key = + | ETProdIdent (* Parsed as an ident *) | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index ad6ac8d3f3..9fe3e2f7ab 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -246,6 +246,7 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = +| TTIdent : ('self, lident) entry | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry @@ -364,6 +365,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p)) | TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder)) | TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false) +| TTIdent -> MayRecNo (Pcoq.Symbol.nterm Prim.identref) | TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name) | TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder) | TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder) @@ -372,6 +374,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global) let interp_entry forpat e = match e with +| ETProdIdent -> TTAny TTIdent | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint @@ -382,6 +385,9 @@ let interp_entry forpat e = match e with | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) +let cases_pattern_expr_of_id { CAst.loc; v = id } = + CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) + let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None | Name id -> CPatAtom (Some (qualid_of_ident ?loc id)) @@ -398,6 +404,11 @@ let push_constr subst v = { subst with constrs = v :: subst.constrs } let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> match e with | TTConstr _ -> push_constr subst v +| TTIdent -> + begin match forpat with + | ForConstr -> { subst with binders = (cases_pattern_expr_of_id v, Glob_term.Explicit) :: subst.binders } + | ForPattern -> push_constr subst (cases_pattern_expr_of_id v) + end | TTName -> begin match forpat with | ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 116cfc6413..5c329f60a9 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -531,6 +531,10 @@ let warn_deprecated_include_type = CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" (fun () -> strbrk "Include Type is deprecated; use Include instead") +let warn_deprecated_as_ident_kind = + CWarnings.create ~name:"deprecated-as-ident-kind" ~category:"deprecated" + (fun () -> strbrk "grammar kind \"as ident\" no longer accepts \"_\"; use \"as name\" instead to accept \"_\", too, or silence the warning if you actually intended to accept only identifiers.") + } (* Modules and Sections *) @@ -1242,7 +1246,13 @@ GRAMMAR EXTEND Gram ] ] ; explicit_subentry: - [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } + [ [ (* Warning to be turn into an error at the end of deprecation phase (for 8.14) *) + IDENT "ident" -> { ETName false } + (* To be activated at the end of transitory phase (for 8.15) + | IDENT "ident" -> { ETIdent } + *) + | IDENT "name" -> { ETName true } (* Boolean to remove at the end of transitory phase *) + | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } @@ -1261,8 +1271,9 @@ GRAMMAR EXTEND Gram | -> { DefaultLevel } ] ] ; binder_interp: - [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent } - | "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern } + [ [ "as"; IDENT "ident" -> { warn_deprecated_as_ident_kind (); Notation_term.AsIdent } + | "as"; IDENT "name" -> { Notation_term.AsName } + | "as"; IDENT "pattern" -> { Notation_term.AsNameOrPattern } | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ] ; END diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8759798331..06eb330958 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -340,11 +340,11 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec,side = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint -> + | ETConstr _ | ETGlobal | ETBigint | ETIdent -> UnpMetaVar (prec,side) - | ETPattern _ | ETIdent -> + | ETPattern _ | ETName _ -> UnpBinderMetaVar (prec,NotQuotedPattern) - | ETBinder _ -> + | ETBinder isopen -> UnpBinderMetaVar (prec,QuotedPattern) (* Heuristics for building default printing rules *) @@ -631,7 +631,8 @@ let include_possible_similar_trailing_pattern typ etyps sl l = try_aux 0 l let prod_entry_type = function - | ETIdent -> ETProdName + | ETIdent -> ETProdIdent + | ETName _ -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint | ETBinder o -> ETProdOneBinder o @@ -891,6 +892,11 @@ let default = { end +(* To be turned into a fatal warning in 8.14 *) +let warn_deprecated_ident_entry = + CWarnings.create ~name:"deprecated-ident-entry" ~category:"deprecated" + (fun () -> strbrk "grammar entry \"ident\" permitted \"_\" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use \"name\" instead.") + let interp_modifiers modl = let open NotationMods in let rec interp subtyps acc = function | [] -> subtyps, acc @@ -952,6 +958,13 @@ let interp_modifiers modl = let open NotationMods in let subtyps,mods = interp [] default modl in (* interpret item levels wrt to main entry *) let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in + (* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *) + let mods = + { mods with etyps = List.map (function + | (id,ETName false) -> + if mods.custom = InConstrEntry then (warn_deprecated_ident_entry (); (id,ETName true)) + else (id,ETIdent) + | x -> x) mods.etyps } in { mods with etyps = extra_etyps@mods.etyps } let check_infix_modifiers modifiers = @@ -1000,7 +1013,7 @@ let set_entry_type from n etyps (x,typ) = | ETConstr (s,bko,n), InternalProd -> ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x + | (ETIdent | ETName _ | ETBigint | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> ETConstr (from,None,(make_lev n from,typ)) in (x,typ) @@ -1023,7 +1036,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder | ETConstr _ | ETBigint | ETGlobal - | ETIdent | ETPattern _ -> NtnInternTypeAny + | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = List.map (fun (_, e) -> internalization_type_of_entry_type e) typs @@ -1043,6 +1056,7 @@ let make_interpretation_type isrec isonlybinding default_if_binding = function | ETConstr (_,None,_) -> NtnTypeConstr (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent + | ETName _ -> NtnTypeBinder NtnParsedAsName | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> @@ -1063,7 +1077,7 @@ let subentry_of_constr_prod_entry from_level = function | _ -> InConstrEntrySomeLevel let make_interpretation_vars - (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent) + (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsName) recvars level allvars typs = let eq_subscope (sc1, l1) (sc2, l2) = Option.equal String.equal sc1 sc2 && @@ -1159,7 +1173,7 @@ let find_precedence custom lev etyps symbols onlyprint = user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () - | (ETIdent | ETBigint | ETGlobal), _ -> + | (ETIdent | ETName _ | ETBigint | ETGlobal), _ -> begin match lev with | None -> ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0) @@ -1798,7 +1812,7 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing interp_notation_constr env nenv c in let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in - let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in + let interp = make_interpretation_vars ~default_if_binding:AsNameOrPattern [] 0 acvars (List.map in_pat vars) in let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in let also_in_cases_pattern = has_no_binders_type vars in let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 4cee4f7a47..00a5727af6 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -187,13 +187,16 @@ let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel let pr_constr_as_binder_kind = let open Notation_term in function | AsIdent -> spc () ++ keyword "as ident" - | AsIdentOrPattern -> spc () ++ keyword "as pattern" + | AsName -> spc () ++ keyword "as name" + | AsNameOrPattern -> spc () ++ keyword "as pattern" | AsStrictPattern -> spc () ++ keyword "as strict pattern" let pr_strict b = if b then str "strict " else mt () let pr_set_entry_type pr = function | ETIdent -> str"ident" + | ETName false -> str"ident" (* temporary *) + | ETName true -> str"name" | ETGlobal -> str"global" | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko -- cgit v1.2.3 From 5ee4141e04696fe82f4291723a9574a4830479a2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 Jul 2020 17:37:36 +0200 Subject: Uniformizing indentation in ppvernac.ml. --- vernac/ppvernac.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 00a5727af6..01873918aa 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -271,9 +271,9 @@ let pr_reference_or_constr pr_c = function | HintsConstr c -> pr_c c let pr_hint_mode = let open Hints in function - | ModeInput -> str"+" - | ModeNoHeadEvar -> str"!" - | ModeOutput -> str"-" + | ModeInput -> str"+" + | ModeNoHeadEvar -> str"!" + | ModeOutput -> str"-" let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } = pr_opt (fun x -> str"|" ++ int x) pri ++ -- cgit v1.2.3 From df8b5c7d83ad6e88af34d29bcc32c85bd42c2712 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 17 Mar 2020 11:16:09 +0100 Subject: Adapting standard library, doc and test suite to ident->name renaming. --- doc/sphinx/language/extensions/canonical.rst | 4 +-- test-suite/bugs/closed/bug_9517.v | 1 + test-suite/output/Notations2.v | 8 +++--- test-suite/output/Notations3.v | 2 +- test-suite/output/Notations4.v | 1 + theories/Init/Logic.v | 10 +++---- theories/Logic/Hurkens.v | 16 +++++------ theories/Program/Utils.v | 2 +- theories/ssr/ssrbool.v | 26 ++++++++--------- theories/ssr/ssreflect.v | 2 +- theories/ssr/ssrfun.v | 42 ++++++++++++++-------------- 11 files changed, 58 insertions(+), 56 deletions(-) diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index f7ce7f1c6c..aa754ab63d 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -490,10 +490,10 @@ We need some infrastructure for that. Definition id {T} {t : T} (x : phantom t) := x. Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v index bb43edbe74..93ed94df39 100644 --- a/test-suite/bugs/closed/bug_9517.v +++ b/test-suite/bugs/closed/bug_9517.v @@ -2,6 +2,7 @@ Declare Custom Entry expr. Declare Custom Entry stmt. Notation "x" := x (in custom stmt, x ident). Notation "x" := x (in custom expr, x ident). +Notation "'_'" := _ (in custom expr). Notation "1" := 1 (in custom expr). diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index bcb2468792..05712eaac7 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -62,7 +62,7 @@ Check `(∀ n p : A, n=p). Notation "'let'' f x .. y := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (f ident, x closed binder, y closed binder, at level 200, + (f name, x closed binder, y closed binder, at level 200, right associativity). Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. @@ -93,7 +93,7 @@ End A. Notation "'mylet' f [ x ; .. ; y ] := t 'in' u":= (let f := fun x => .. (fun y => t) .. in u) - (f ident, x closed binder, y closed binder, at level 200, + (f name, x closed binder, y closed binder, at level 200, right associativity). Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. @@ -104,7 +104,7 @@ Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2. (* Old request mentioned again on coq-club 20/1/2012 *) Notation "# x : T => t" := (fun x : T => t) - (at level 0, t at level 200, x ident). + (at level 0, t at level 200, x name). Check # x : nat => x. Check # _ : nat => 2. @@ -116,7 +116,7 @@ Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). Check (exist (Q x) y conj). (* Check bug #4854 *) -Notation "% i" := (fun i : nat => i) (at level 0, i ident). +Notation "% i" := (fun i : nat => i) (at level 0, i name). Check %i. Check %j. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 04a91c14d9..6c714fc624 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -305,7 +305,7 @@ Module E. Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop := myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q. Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q)) - (at level 200, x ident, A at level 200, p at level 200, right associativity, + (at level 200, x name, A at level 200, p at level 200, right associativity, format "'[' 'myexists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ebc1426fc8..ce488fe18d 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -327,6 +327,7 @@ Module P. Module NotationMixedTermBinderAsIdent. + Set Warnings "-deprecated-ident-entry". (* We do want ident! *) Notation "▢_ n P" := (pseudo_force n (fun n => P)) (at level 0, n ident, P at level 9, format "▢_ n P"). Check exists p, ▢_p (p >= 1). diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 023705e169..5247c7b56a 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -309,9 +309,9 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) : type_scope. Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) - (at level 200, x ident, p at level 200, right associativity) : type_scope. + (at level 200, x name, p at level 200, right associativity) : type_scope. Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q)) - (at level 200, x ident, A at level 200, p at level 200, right associativity, + (at level 200, x name, A at level 200, p at level 200, right associativity, format "'[' 'exists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'") : type_scope. @@ -489,18 +489,18 @@ Module EqNotations. := (match H as p in (_ = y) return P with | eq_refl => H' end) - (at level 10, H' at level 10, y ident, p ident, + (at level 10, H' at level 10, y name, p name, format "'[' 'rew' 'dependent' [ 'fun' y p => P ] '/ ' H in '/' H' ']'"). Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'" := (match H as p in (_ = y) return P with | eq_refl => H' end) - (at level 10, H' at level 10, y ident, p ident, only parsing). + (at level 10, H' at level 10, y name, p name, only parsing). Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'" := (match eq_sym H as p in (_ = y) return P with | eq_refl => H' end) - (at level 10, H' at level 10, y ident, p ident, + (at level 10, H' at level 10, y name, p name, format "'[' 'rew' 'dependent' <- [ 'fun' y p => P ] '/ ' H in '/' H' ']'"). Notation "'rew' 'dependent' [ P ] H 'in' H'" := (match H as p in (_ = y) return P y p with diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 84d40035bf..1a2c4ba171 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -96,19 +96,19 @@ Module Generic. (* begin hide *) (* Notations used in the proof. Hidden in coqdoc. *) -Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity). +Reserved Notation "'∀₁' x : A , B" (at level 200, x name, A at level 200,right associativity). Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200). -Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'λ₁' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₁' x" (at level 5, left associativity). -Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity). -Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'∀₂' A , F" (at level 200, A name, right associativity). +Reserved Notation "'λ₂' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity). -Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity). +Reserved Notation "'∀₀' x : A , B" (at level 200, x name, A at level 200,right associativity). Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200). -Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'λ₀' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₀' x" (at level 5, left associativity). -Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity). -Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity). +Reserved Notation "'∀₀¹' A : U , F" (at level 200, A name, right associativity). +Reserved Notation "'λ₀¹' x , u" (at level 200, x name, right associativity). Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity). (* end hide *) diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 9c8508bf39..b2bdd8099a 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -18,7 +18,7 @@ Set Implicit Arguments. Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) - (x ident, y ident, at level 10) : type_scope. + (x name, y name, at level 10) : type_scope. Declare Scope program_scope. Delimit Scope program_scope with prg. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index d1cefeb552..a563dcbf95 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -335,19 +335,19 @@ Reserved Notation "[ 'predType' 'of' T ]" (at level 0, Reserved Notation "[ 'pred' : T | E ]" (at level 0, format "'[hv' [ 'pred' : T | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x | E ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x | E ]" (at level 0, x name, format "'[hv' [ 'pred' x | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x name, format "'[hv' [ 'pred' x : T | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x name, format "'[hv' [ 'pred' x | '/ ' E1 & '/ ' E2 ] ']'"). -Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x name, format "'[hv' [ 'pred' x : T | '/ ' E1 & E2 ] ']'"). -Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x name, format "'[hv' [ 'pred' x 'in' A ] ']'"). -Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x name, format "'[hv' [ 'pred' x 'in' A | '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x ident, +Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x name, format "'[hv' [ 'pred' x 'in' A | '/ ' E1 & '/ ' E2 ] ']'"). Reserved Notation "[ 'qualify' x | P ]" (at level 0, x at level 99, @@ -363,17 +363,17 @@ Reserved Notation "[ 'qualify' 'an' x | P ]" (at level 0, x at level 99, Reserved Notation "[ 'qualify' 'an' x : T | P ]" (at level 0, x at level 99, format "'[hv' [ 'qualify' 'an' x : T | '/ ' P ] ']'"). -Reserved Notation "[ 'rel' x y | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A & B ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x ident, y ident, +Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x name, y name, format "'[hv' [ 'rel' x y 'in' A ] ']'"). Reserved Notation "[ 'mem' A ]" (at level 0, format "[ 'mem' A ]"). diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index d0508bef2e..dc81b5cca7 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -110,7 +110,7 @@ Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200, Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200, c, R, vT, vF at level 200). Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200, - c, R, vT, vF at level 200, x ident). + c, R, vT, vF at level 200, x name). Reserved Notation "x : T" (at level 100, right associativity, format "'[hv' x '/ ' : T ']'"). diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v index e1442e1da2..ba66e04e4a 100644 --- a/theories/ssr/ssrfun.v +++ b/theories/ssr/ssrfun.v @@ -236,19 +236,19 @@ Reserved Notation "'fun' => E" (at level 200, format "'fun' => E"). Reserved Notation "[ 'fun' : T => E ]" (at level 0, format "'[hv' [ 'fun' : T => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x => E ]" (at level 0, - x ident, format "'[hv' [ 'fun' x => '/ ' E ] ']'"). + x name, format "'[hv' [ 'fun' x => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x : T => E ]" (at level 0, - x ident, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'"). + x name, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x y => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' x y => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' x y => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x y : T => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'"). Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'"). Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0, - x ident, y ident, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'"). + x name, y name, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'"). Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0, - x ident, y ident, format "[ 'fun' ( x : T ) ( y : U ) => E ]" ). + x name, y name, format "[ 'fun' ( x : T ) ( y : U ) => E ]" ). Reserved Notation "f =1 g" (at level 70, no associativity). Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90). @@ -259,33 +259,33 @@ Reserved Notation "f \; g" (at level 60, right associativity, format "f \; '/ ' g"). Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99, - x ident, format "{ 'morph' f : x / a >-> r }"). + x name, format "{ 'morph' f : x / a >-> r }"). Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99, - x ident, format "{ 'morph' f : x / a }"). + x name, format "{ 'morph' f : x / a }"). Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99, - x ident, y ident, format "{ 'morph' f : x y / a >-> r }"). + x name, y name, format "{ 'morph' f : x y / a >-> r }"). Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'morph' f : x y / a }"). + x name, y name, format "{ 'morph' f : x y / a }"). Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99, - x ident, format "{ 'homo' f : x / a >-> r }"). + x name, format "{ 'homo' f : x / a >-> r }"). Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99, - x ident, format "{ 'homo' f : x / a }"). + x name, format "{ 'homo' f : x / a }"). Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99, - x ident, y ident, format "{ 'homo' f : x y / a >-> r }"). + x name, y name, format "{ 'homo' f : x y / a >-> r }"). Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'homo' f : x y / a }"). + x name, y name, format "{ 'homo' f : x y / a }"). Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'homo' f : x y /~ a }"). + x name, y name, format "{ 'homo' f : x y /~ a }"). Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99, - x ident, format "{ 'mono' f : x / a >-> r }"). + x name, format "{ 'mono' f : x / a >-> r }"). Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99, - x ident, format "{ 'mono' f : x / a }"). + x name, format "{ 'mono' f : x / a }"). Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99, - x ident, y ident, format "{ 'mono' f : x y / a >-> r }"). + x name, y name, format "{ 'mono' f : x y / a >-> r }"). Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'mono' f : x y / a }"). + x name, y name, format "{ 'mono' f : x y / a }"). Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99, - x ident, y ident, format "{ 'mono' f : x y /~ a }"). + x name, y name, format "{ 'mono' f : x y /~ a }"). Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T"). Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'"). -- cgit v1.2.3 From 87c46c50506089ba16bdd7afd7e795ee21033319 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 14 Jul 2020 18:23:31 +0200 Subject: Updating doc wrt addition of grammar subentry "name" and deprecation of "ident". For constr, this means clarifying that "ident" is deprecated and to be replaced by "name". Here, some cleaning shall have to be done at the end of deprecation phase, when "ident" will take its literal meaning. For custom notations, this is about documenting the effect of "ident" and "global" which was yet undocumented. Note that we anticipate an example in constr working with the literal meaning of "ident" (temporarily silencing the warning). Co-authored-by: Théo Zimmermann Co-authored-by: Jim Fehrle --- doc/sphinx/user-extensions/syntax-extensions.rst | 91 ++++++++++++++++++++---- doc/tools/docgram/fullGrammar | 2 + doc/tools/docgram/orderedGrammar | 2 + 3 files changed, 82 insertions(+), 13 deletions(-) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5cbd2e400e..df73de846f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -603,7 +603,7 @@ Here is the basic example of a notation using a binder: .. coqtop:: in Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) - (at level 200, x ident, A at level 200, right associativity). + (at level 200, x name, A at level 200, right associativity). The binding variables in the right-hand side that occur as a parameter of the notation (here :g:`x`) dynamically bind all the occurrences @@ -616,8 +616,9 @@ application of the notation: Check sigma z : nat, z = 0. -Note the :n:`@syntax_modifier x ident` in the declaration of the -notation. It tells to parse :g:`x` as a single identifier. +Note the :n:`@syntax_modifier x name` in the declaration of the +notation. It tells to parse :g:`x` as a single identifier (or as the +unnamed variable :g:`_`). Binders bound in the notation and parsed as patterns ++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -655,7 +656,7 @@ variable. Here is an example showing the difference: Notation "'subset_bis' ' p , P" := (sig (fun p => P)) (at level 200, p strict pattern). Notation "'subset_bis' p , P " := (sig (fun p => P)) - (at level 200, p ident). + (at level 200, p name). .. coqtop:: all @@ -675,18 +676,19 @@ the following: .. coqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) - (at level 0, x at level 99 as ident). + (at level 0, x at level 99 as name). This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the constant :g:`sumbool` (see :ref:`specification`). -Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning +Then, in the rule, ``x name`` is replaced by ``x at level 99 as name`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for -:g:`sumbool`), but that this term has actually to be an identifier. +:g:`sumbool`), but that this term has actually to be a name, i.e. an +identifier or :g:`_`. The notation :g:`{ x | P }` is already defined in the standard -library with the ``as ident`` :n:`@syntax_modifier`. We cannot redefine it but +library with the ``as name`` :n:`@syntax_modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. @@ -702,12 +704,12 @@ Then, the following works: Check {(x,y) such that x+y=0}. To enforce that the pattern should not be used for printing when it -is just an identifier, one could have said +is just a name, one could have said ``p at level 99 as strict pattern``. -Note also that in the absence of a ``as ident``, ``as strict pattern`` or +Note also that in the absence of a ``as name``, ``as strict pattern`` or ``as pattern`` :n:`@syntax_modifier`\s, the default is to consider sub-expressions occurring -in binding position and parsed as terms to be ``as ident``. +in binding position and parsed as terms to be ``as name``. Binders bound in the notation and parsed as general binders +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -768,7 +770,7 @@ binding position. Here is an example: Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. Notation "▢_ n P" := (force n (fun n => P)) - (at level 0, n ident, P at level 9, format "▢_ n P"). + (at level 0, n name, P at level 9, format "▢_ n P"). .. coqtop:: all @@ -946,16 +948,31 @@ position of :g:`x`: (at level 10, f global, a1, an at level 9). In addition to ``global``, one can restrict the syntax of a -sub-expression by using the entry names ``ident`` or ``pattern`` +sub-expression by using the entry names ``ident``, ``name`` or ``pattern`` already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: + .. todo: these two Set Warnings and the note should be removed when + ident is reactivated with its literal meaning. + +.. coqtop:: none + + Set Warnings "-deprecated-ident-entry". + .. coqtop:: in Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +.. coqtop:: none + + Set Warnings "+deprecated-ident-entry". + +.. note:: As of version 8.13, the entry ``ident`` is a deprecated + alias for ``name``. In the future, it is planned to strictly + parse an identifier (excluding :g:`_`). + .. _custom-entries: Custom entries @@ -1113,6 +1130,31 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. +Another special situation is when parsing global references or +identifiers. To indicate that a custom entry should parse identifiers, +use the following form: + +.. coqtop:: none + + Reset Initial. + Declare Custom Entry expr. + +.. coqtop:: in + + Notation "x" := x (in custom expr at level 0, x ident). + +Similarly, to indicate that a custom entry should parse global references +(i.e. qualified or non qualified identifiers), use the following form: + +.. coqtop:: none + + Reset Initial. + Declare Custom Entry expr. + +.. coqtop:: in + + Notation "x" := x (in custom expr at level 0, x global). + .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar @@ -1142,6 +1184,7 @@ Here are the syntax elements used by the various notation commands. | only printing | format @string {? @string } explicit_subentry ::= ident + | name | global | bigint | strict pattern {? at level @natural } @@ -1151,6 +1194,7 @@ Here are the syntax elements used by the various notation commands. | custom @ident {? at @level } {? @binder_interp } | pattern {? at level @natural } binder_interp ::= as ident + | as name | as pattern | as strict pattern level ::= level @natural @@ -1188,6 +1232,27 @@ Here are the syntax elements used by the various notation commands. due to legacy notation in the Coq standard library. It can be turned on with the ``-w disj-pattern-notation`` flag. +.. note:: + + As of version 8.13, the entry ``ident`` is a deprecated alias for + ``name``. In the future, it is planned to strictly parse an + identifier (to the exclusion of :g:`_`). If the intent was to use + ``ident`` as an identifier (excluding :g:`_`), just silence the warning with + :n:`Set Warnings "-deprecated-ident-entry"` and it should automatically + get its intended meaning in version 8.15. + + Similarly, ``as ident`` is a deprecated alias for ``as name``, which + will only accept an identifier in the future. If the + intent was to use ``as ident`` as an identifier + (excluding :g:`_`), just silence the warning with + :n:`Set Warnings "-deprecated-as-ident-kind"`. + + However, this deprecation does not apply to custom entries, where it + already denotes an identifier, as expected. + + .. todo: the note above should be removed at the end of deprecation + phase of ident + .. .. _Scopes: Notation scopes diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 03a20d621b..e23925d1f7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1420,6 +1420,7 @@ syntax_modifiers: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "binder" @@ -1440,6 +1441,7 @@ at_level_opt: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 0209cf762a..1948d48dbd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1574,6 +1574,7 @@ syntax_modifier: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "strict" "pattern" OPT ( "at" "level" natural ) @@ -1586,6 +1587,7 @@ explicit_subentry: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] -- cgit v1.2.3