diff options
25 files changed, 288 insertions, 155 deletions
diff --git a/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh new file mode 100644 index 0000000000..decb093b71 --- /dev/null +++ b/dev/ci/user-overlays/13965-gares-syndef-principal-scope.sh @@ -0,0 +1,3 @@ +overlay equations https://github.com/gares/Coq-Equations syndef-principal-scope 13965 +overlay elpi https://github.com/gares/coq-elpi syndef-principal-scope 13965 +overlay paramcoq https://github.com/gares/paramcoq syndef-principal-scope 13965 diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst new file mode 100644 index 0000000000..448dbbe3c7 --- /dev/null +++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst @@ -0,0 +1,12 @@ +- **Added:** + Let the user specify a scope for abbreviation arguments, e.g. + ``Notation abbr X := t (X in scope my_scope)``. + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). +- **Changed:** + The error ``Argument X was previously inferred to be in scope + XXX_scope but is here used in YYY_scope.`` is now the warning + ``[inconsistent-scopes,syntax]`` and can be silenced by + specifying the scope of the argument + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d212256765..f65361bc64 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1182,7 +1182,7 @@ Here are the syntax elements used by the various notation commands. .. prodn:: syntax_modifier ::= at level @natural | in custom @ident {? at level @natural } - | {+, @ident } at @level + | {+, @ident } {| at @level | in scope @ident } | @ident at @level {? @binder_interp } | @ident @explicit_subentry | @ident @binder_interp @@ -1374,6 +1374,10 @@ interpreted in the scope stack extended with the scope bound to :n:`@scope_key`. Removes the delimiting keys associated with a scope. +The arguments of an :ref:`abbreviation <Abbreviations>` can be interpreted +in a scope stack locally extended with a given scope by using the modifier +:n:`{+, @ident } in scope @scope_name`.s + Binding types or coercion classes to a notation scope ++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1567,7 +1571,7 @@ Displaying information about scopes Abbreviations -------------- -.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( only parsing ) } +.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( {+, @syntax_modifier } ) } :name: Notation (abbreviation) .. todo: for some reason, Sphinx doesn't complain about a duplicate name if diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5c211d82e9..48d399dfd3 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1409,8 +1409,9 @@ syntax_modifier: [ | DELETE "in" "custom" IDENT | REPLACE "in" "custom" IDENT; "at" "level" natural | WITH "in" "custom" IDENT OPT ( "at" "level" natural ) -| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level -| WITH LIST1 IDENT SEP "," "at" level +| DELETE IDENT; "in" "scope" IDENT +| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] +| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] ] explicit_subentry: [ @@ -2642,7 +2643,6 @@ SPLICE: [ | quoted_attributes (* todo: splice or not? *) | printable | hint -| only_parsing | record_fields | constructor_type | record_binder diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index fe166524bf..b5a234a86a 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1400,18 +1400,13 @@ syntax: [ | "Undelimit" "Scope" IDENT | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr | "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] -| "Notation" identref LIST0 ident ":=" constr only_parsing +| "Notation" identref LIST0 ident ":=" constr syntax_modifiers | "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ] | "Format" "Notation" STRING STRING STRING | "Reserved" "Infix" ne_lstring syntax_modifiers | "Reserved" "Notation" ne_lstring syntax_modifiers ] -only_parsing: [ -| "(" "only" "parsing" ")" -| -] - level: [ | "level" natural | "next" "level" @@ -1427,8 +1422,9 @@ syntax_modifier: [ | "only" "printing" | "only" "parsing" | "format" STRING OPT STRING -| IDENT; "," LIST1 IDENT SEP "," "at" level +| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ] | IDENT; "at" level OPT binder_interp +| IDENT; "in" "scope" IDENT | IDENT binder_interp | IDENT explicit_subentry ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 2b09263cc4..cd96693bf0 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1095,7 +1095,7 @@ command: [ | "Undelimit" "Scope" scope_name | "Bind" "Scope" scope_name "with" LIST1 class | "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] -| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) | "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] | "Format" "Notation" string string string | "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) @@ -1539,7 +1539,7 @@ class: [ syntax_modifier: [ | "at" "level" natural | "in" "custom" ident OPT ( "at" "level" natural ) -| LIST1 ident SEP "," "at" level +| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ] | ident "at" level OPT binder_interp | ident explicit_subentry | ident binder_interp diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 40fe13784a..ddd689bee0 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -281,10 +281,13 @@ let local_binders_loc bll = match bll with (** Folds and maps *) let is_constructor id = - try Globnames.isConstructRef - (Smartlocate.global_of_extended_global - (Nametab.locate_extended (qualid_of_ident id))) - with Not_found -> false + match + Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id)) + with + | exception Not_found -> false + | None -> false + | Some gref -> Globnames.isConstructRef gref let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with | CPatRecord l -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 958e1408f8..68dd96e44b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -273,40 +273,54 @@ let make_current_scope tmp scopes = match tmp, scopes with | Some tmp_scope, scopes -> tmp_scope :: scopes | None, scopes -> scopes -let pr_scope_stack = function - | [] -> str "the empty scope stack" - | [a] -> str "scope " ++ str a - | l -> str "scope stack " ++ +let pr_scope_stack begin_of_sentence l = + let bstr x = + if begin_of_sentence then str (CString.capitalize_ascii x) else str x in + match l with + | [] -> bstr "the empty scope stack" + | [a] -> bstr "scope " ++ str a + | l -> bstr "scope stack " ++ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" -let error_inconsistent_scope ?loc id scopes1 scopes2 = - user_err ?loc ~hdr:"set_var_scope" - (Id.print id ++ str " is here used in " ++ - pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ - pr_scope_stack scopes1) +let warn_inconsistent_scope = + CWarnings.create ~name:"inconsistent-scopes" ~category:"syntax" + (fun (id,scopes1,scopes2) -> + (str "Argument " ++ Id.print id ++ + strbrk " was previously inferred to be in " ++ + pr_scope_stack false scopes1 ++ + strbrk " but is here used in " ++ + pr_scope_stack false scopes2 ++ + strbrk ". " ++ + pr_scope_stack true scopes1 ++ + strbrk " will be used at parsing time unless you override it by" ++ + strbrk " annotating the argument with an explicit scope of choice.")) let error_expect_binder_notation_type ?loc id = user_err ?loc (Id.print id ++ str " is expected to occur in binding position in the right-hand side.") -let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = +let set_notation_var_scope ?loc id (tmp_scope,subscopes as scopes) ntnvars = try - let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in - if istermvar then begin - (* scopes have no effect on the interpretation of identifiers *) - (match !idscopes with + let _,idscopes,typ = Id.Map.find id ntnvars in + match typ with + | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id + | Notation_term.NtnInternTypeAny principal -> + match !idscopes with | None -> idscopes := Some scopes | Some (tmp_scope', subscopes') -> let s' = make_current_scope tmp_scope' subscopes' in let s = make_current_scope tmp_scope subscopes in - if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s); - (match typ with - | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id - | Notation_term.NtnInternTypeAny -> ()) - end - else - used_as_binder := true + if Option.is_empty principal && not (List.equal String.equal s' s) then + warn_inconsistent_scope ?loc (id,s',s) + with Not_found -> + (* Not in a notation *) + () + +let set_var_is_binder ?loc id ntnvars = + try + let used_as_binder,_,_ = Id.Map.find id ntnvars in + used_as_binder := true with Not_found -> (* Not in a notation *) () @@ -484,7 +498,7 @@ let push_name_env ntnvars implargs env = | { loc; v = Name id } -> if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; - set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; + set_var_is_binder ?loc id ntnvars; let uid = var_uid id in Dumpglob.dump_binding ?loc uid; pure_push_name_env (id,(Variable,implargs,[],uid)) env @@ -1064,7 +1078,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin - if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; + if not (Id.Map.mem id env.impls) then set_notation_var_scope ?loc id (env.tmp_scope,env.scopes) ntnvars; gvar (loc,id) us end else @@ -1130,14 +1144,54 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + +let intern_name_alias = function + | { CAst.v = CRef(qid,u) } -> + let r = + try Some (intern_extended_global_of_qualid qid) + with Not_found -> None + in + Option.bind r Smartlocate.global_of_extended_global |> + Option.map (fun r -> r, intern_instance ~local_univs:empty_local_univs u) + | _ -> None + let intern_projection qid = - try - match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with - | GlobRef.ConstRef c as gr -> - (gr, Structure.find_from_projection c) - | _ -> raise Not_found - with Not_found -> - Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + match + Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) |> + Option.map (function + | GlobRef.ConstRef c as x -> x, Structure.find_from_projection c + | _ -> raise Not_found) + with + | exception Not_found -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + | None -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + | Some x -> x (**********************************************************************) (* Interpreting references *) @@ -1182,37 +1236,6 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] -let intern_sort_name ~local_univs = function - | CSProp -> GSProp - | CProp -> GProp - | CSet -> GSet - | CRawType u -> GRawUniv u - | CType qid -> - let is_id = qualid_is_ident qid in - let local = if not is_id then None - else Id.Map.find_opt (qualid_basename qid) local_univs.bound - in - match local with - | Some u -> GUniv u - | None -> - try GUniv (Univ.Level.make (Nametab.locate_universe qid)) - with Not_found -> - if is_id && local_univs.unb_univs - then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) - else - CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") - -let intern_sort ~local_univs s = - map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s - -let intern_instance ~local_univs us = - Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us - -let try_interp_name_alias = function - | [], { CAst.v = CRef (ref,u) } -> - NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u) - | _ -> raise Not_found - (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1843,7 +1866,7 @@ let rec intern_pat genv ntnvars aliases pat = intern_cstr_with_all_args loc c true [] pl | RCPatAtom (Some ({loc;v=id},scopes)) -> let aliases = merge_aliases aliases (make ?loc @@ Name id) in - set_var_scope ?loc id false scopes ntnvars; + set_var_is_binder ?loc id ntnvars; (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom None -> let { alias_ids = ids; alias_map = asubst; } = aliases in @@ -2561,7 +2584,11 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (function + | (NtnInternTypeAny None | NtnInternTypeOnlyBinder) as typ -> (ref false, ref None, typ) + | NtnInternTypeAny (Some scope) as typ -> + (ref false, ref (Some (Some scope,[])), typ) + ) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env {ids; unb = false; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 65b63962d0..379bd61070 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -147,12 +147,13 @@ val interp_constr_pattern : env -> evar_map -> ?expected_type:typing_constraint -> constr_pattern_expr -> constr_pattern -(** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : qualid -> GlobRef.t +(** Returns None if it's a syndef not bound to a name, raises an error + if not existing *) +val intern_reference : qualid -> GlobRef.t option -(** For syntactic definitions: check if abbreviation to a name - and avoid early insertion of maximal implicit arguments *) -val try_interp_name_alias : 'a list * constr_expr -> notation_constr +(** Returns None if not a reference or a syndef not bound to a name *) +val intern_name_alias : + constr_expr -> (GlobRef.t * Glob_term.glob_level list option) option (** Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> qualid -> glob_constr @@ -174,7 +175,7 @@ val interp_context_evars : (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) -val locate_reference : Libnames.qualid -> GlobRef.t +val locate_reference : Libnames.qualid -> GlobRef.t option val is_global : Id.t -> bool (** Interprets a term as the left-hand side of a notation. The returned map is diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ea95655c18..313a9e85a4 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -680,7 +680,7 @@ let check_variables_and_reversibility nenv str " position as part of a recursive pattern.") in let check_type x typ = match typ with - | NtnInternTypeAny -> + | NtnInternTypeAny _ -> begin try check_pair "term" x (Id.Map.find x recvars) foundrec with Not_found -> check_bound x diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 2979447cf8..ec7165f854 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -91,7 +91,8 @@ type notation_var_instance_type = in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeAny | NtnInternTypeOnlyBinder + | NtnInternTypeAny of scope_name option + | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91d05f7317..56b3cd9815 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -33,7 +33,7 @@ let global_of_extended_global_head = function | _ -> raise Not_found in head_of syn_def -let global_of_extended_global = function +let global_of_extended_global_exn = function | TrueGlobal ref -> ref | SynDef kn -> match search_syntactic_definition kn with @@ -45,11 +45,15 @@ let locate_global_with_alias ?(head=false) qid = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref - else global_of_extended_global ref + else global_of_extended_global_exn ref with Not_found -> user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") +let global_of_extended_global x = + try Some (global_of_extended_global_exn x) + with Not_found -> None + let global_constant_with_alias qid = try match locate_global_with_alias qid with | Names.GlobRef.ConstRef c -> c diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 26f2a4f36d..abf9839c9e 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -19,8 +19,9 @@ open Globnames val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t -(** Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> GlobRef.t +(** Extract a global_reference from a reference that can be an "alias". + If the reference points to a more complex term, we return None *) +val global_of_extended_global : extended_global_reference -> GlobRef.t option (** Locate a reference taking into account possible "alias" notations. May raise [Nametab.GlobalizationError _] for an unknown reference, diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3234d40f73..7d19c443e9 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -930,8 +930,8 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *) let evd', res = Evd.fresh_global (Global.env ()) !evd - (Constrintern.locate_reference - (qualid_of_ident equation_lemma_id)) + (Option.get (Constrintern.locate_reference + (qualid_of_ident equation_lemma_id))) in evd := evd'; let sigma, _ = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 6236a5147d..f1a3cb6af8 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -241,7 +241,7 @@ let change_property_sort evd toSort princ princName = in let evd, princName_as_constr = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident princName))) in let init = let nargs = @@ -408,8 +408,8 @@ let register_struct is_rec fixpoint_exprl = (fun (evd, l) {Vernacexpr.fname} -> let evd, c = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference - (Libnames.qualid_of_ident fname.CAst.v)) + (Option.get (Constrintern.locate_reference + (Libnames.qualid_of_ident fname.CAst.v))) in let cst, u = destConst evd c in let u = EInstance.kind evd u in @@ -427,8 +427,8 @@ let register_struct is_rec fixpoint_exprl = (fun (evd, l) {Vernacexpr.fname} -> let evd, c = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference - (Libnames.qualid_of_ident fname.CAst.v)) + (Option.get (Constrintern.locate_reference + (Libnames.qualid_of_ident fname.CAst.v))) in let cst, u = destConst evd c in let u = EInstance.kind evd u in @@ -1522,7 +1522,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _, lem_cst_constr = Evd.fresh_global (Global.env ()) !evd - (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))) in let lem_cst, _ = EConstr.destConst !evd lem_cst_constr in update_Function {finfo with correctness_lemma = Some lem_cst}) @@ -1592,7 +1592,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) in let _, lem_cst_constr = Evd.fresh_global (Global.env ()) !evd - (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id))) in let lem_cst, _ = destConst !evd lem_cst_constr in update_Function {finfo with completeness_lemma = Some lem_cst}) @@ -1615,7 +1615,7 @@ let derive_inversion fix_names = (fun id (evd, l) -> let evd, c = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference (Libnames.qualid_of_ident id)) + (Option.get (Constrintern.locate_reference (Libnames.qualid_of_ident id))) in let cst, u = EConstr.destConst evd c in (evd, (cst, EConstr.EInstance.kind evd u) :: l)) @@ -1635,8 +1635,8 @@ let derive_inversion fix_names = (fun id (evd, l) -> let evd, id = Evd.fresh_global (Global.env ()) evd - (Constrintern.locate_reference - (Libnames.qualid_of_ident (mk_rel_id id))) + (Option.get (Constrintern.locate_reference + (Libnames.qualid_of_ident (mk_rel_id id)))) in (evd, fst (EConstr.destInd evd id) :: l)) fix_names (evd', []) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 4e0e2dc501..1221ad0bda 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -80,10 +80,12 @@ let functional_induction with_clean c princl pat = (elimination_sort_of_goal gl) in let princ_ref = - try + match Constrintern.locate_reference (Libnames.qualid_of_ident princ_name) - with Not_found -> + with + | Some r -> r + | None -> user_err ( str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') ) diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v index 6ff394bca6..8d7d97d7aa 100644 --- a/test-suite/bugs/closed/bug_3468.v +++ b/test-suite/bugs/closed/bug_3468.v @@ -26,4 +26,5 @@ Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope. Definition test := (& (@4))%my. (* Check inconsistent scopes *) +Set Warnings "+inconsistent-scopes". Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing). diff --git a/test-suite/output/notation_principal_scope.out b/test-suite/output/notation_principal_scope.out new file mode 100644 index 0000000000..5ccee259b0 --- /dev/null +++ b/test-suite/output/notation_principal_scope.out @@ -0,0 +1,20 @@ +The command has indeed failed with message: +Argument X was previously inferred to be in scope function_scope but is here +used in the empty scope stack. Scope function_scope will be used at parsing +time unless you override it by annotating the argument with an explicit scope +of choice. [inconsistent-scopes,syntax] +The command has indeed failed with message: +Simple notations don't support only printing +The command has indeed failed with message: +The reference nonexisting was not found in the current environment. +The command has indeed failed with message: +Notation scope for argument X can be specified only once. +pp I + : True /\ True +The command has indeed failed with message: +Illegal application (Non-functional construction): +The expression "I" of type "True" cannot be applied to the term + "I" : "True" +File "stdin", line 21, characters 0-50: +Warning: This notation will not be used for printing as it is bound to a +single variable. [notation-bound-to-variable,parsing] diff --git a/test-suite/output/notation_principal_scope.v b/test-suite/output/notation_principal_scope.v new file mode 100644 index 0000000000..6bd911501d --- /dev/null +++ b/test-suite/output/notation_principal_scope.v @@ -0,0 +1,23 @@ +Arguments conj {_ _} _ _%function. + +Set Warnings "+inconsistent-scopes". +Fail Notation pp X := (conj X X). + +Fail Notation pp := 1 (only printing). + +Fail Notation pp X := nonexisting. + +Fail Notation pp X := (conj X X) (X, X in scope nat_scope). + +Notation pp X := (conj X X) (X in scope nat_scope). + +Notation "$" := I (only parsing) : nat_scope. +Notation "$" := (I I) (only parsing) : bool_scope. + +Open Scope bool_scope. +Check pp $. +Fail Check pp (id $). + +Notation pp1 X := (X%nat) (X in scope bool_scope). +Notation pp2 X := ((X + X)%type) (X in scope bool_scope). +Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope). diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index f8a28332b1..2343ffc7e7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -52,7 +52,6 @@ let of_type = Entry.create "of_type" let section_subset_expr = Entry.create "section_subset_expr" let scope_delimiter = Entry.create "scope_delimiter" let syntax_modifiers = Entry.create "syntax_modifiers" -let only_parsing = Entry.create "only_parsing" let make_bullet s = let open Proof_bullet in @@ -1160,7 +1159,7 @@ GRAMMAR EXTEND Gram (* Grammar extensions *) GRAMMAR EXTEND Gram - GLOBAL: syntax only_parsing syntax_modifiers; + GLOBAL: syntax syntax_modifiers; syntax: [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> @@ -1181,10 +1180,9 @@ GRAMMAR EXTEND Gram modl = syntax_modifiers; sc = OPT [ ":"; sc = IDENT -> { sc } ] -> { VernacInfix ((op,modl),p,sc) } - | IDENT "Notation"; id = identref; - idl = LIST0 ident; ":="; c = constr; b = only_parsing -> - { VernacSyntacticDefinition - (id,(idl,c),{ onlyparsing = b }) } + | IDENT "Notation"; id = identref; idl = LIST0 ident; + ":="; c = constr; modl = syntax_modifiers -> + { VernacSyntacticDefinition (id,(idl,c), modl) } | IDENT "Notation"; s = lstring; ":="; c = constr; modl = syntax_modifiers; @@ -1207,10 +1205,6 @@ GRAMMAR EXTEND Gram to factorize with other "Print"-based or "Declare"-based vernac entries *) ] ] ; - only_parsing: - [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true } - | -> { false } ] ] - ; level: [ [ IDENT "level"; n = natural -> { NumLevel n } | IDENT "next"; IDENT "level" -> { NextLevel } ] ] @@ -1230,10 +1224,12 @@ GRAMMAR EXTEND Gram { begin match s1, s2 with | { CAst.v = k }, Some s -> SetFormat(k,s) | s, None -> SetFormat ("text",s) end } - | x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at"; - lev = level -> { SetItemLevel (x::l,None,lev) } + | x = IDENT; ","; l = LIST1 IDENT SEP ","; v = + [ "at"; lev = level -> { fun x l -> SetItemLevel (x::l,None,lev) } + | "in"; IDENT "scope"; k = IDENT -> { fun x l -> SetItemScope(x::l,k) } ] -> { v x l } | x = IDENT; "at"; lev = level; b = OPT binder_interp -> { SetItemLevel ([x],b,lev) } + | x = IDENT; "in"; IDENT "scope"; k = IDENT -> { SetItemScope([x],k) } | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) } | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) } ] ] diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f9f65a8c30..c5bfba900c 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -862,6 +862,41 @@ let inSyntaxExtension : syntax_extension_obj -> obj = (* Interpreting user-provided modifiers *) (* XXX: We could move this to the parser itself *) + +module SyndefMods = struct + +type t = { + only_parsing : bool; + scopes : (Id.t * scope_name) list; +} + +let default = { + only_parsing = false; + scopes = []; +} + +end + +let interp_syndef_modifiers modl = let open SyndefMods in + let rec interp skipped acc = function + | [] -> List.rev skipped, acc + | SetOnlyParsing :: l -> + interp skipped { acc with only_parsing = true; } l + | SetItemScope([],_) :: l -> + interp skipped acc l + | SetItemScope(s::ids,k) :: l -> + let scopes = acc.scopes in + let id = Id.of_string s in + if List.mem_assoc id scopes then + user_err (str "Notation scope for argument " ++ str s ++ + str " can be specified only once."); + interp skipped { acc with scopes = (id,k) :: scopes } + (SetItemScope(ids,s) :: l) + | x :: l -> + interp (x :: skipped) acc l + in + interp [] default modl + module NotationMods = struct type notation_modifier = { @@ -872,7 +907,6 @@ type notation_modifier = { subtyps : (Id.t * production_level) list; (* common to syn_data below *) - only_parsing : bool; only_printing : bool; format : lstring option; extra : (string * string) list; @@ -884,7 +918,6 @@ let default = { custom = InConstrEntry; etyps = []; subtyps = []; - only_parsing = false; only_printing = false; format = None; extra = []; @@ -945,8 +978,6 @@ let interp_modifiers modl = let open NotationMods in | SetAssoc a :: l -> if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); interp subtyps { acc with assoc = Some a; } l - | SetOnlyParsing :: l -> - interp subtyps { acc with only_parsing = true; } l | SetOnlyPrinting :: l -> interp subtyps { acc with only_printing = true; } l | SetFormat ("text",s) :: l -> @@ -954,8 +985,10 @@ let interp_modifiers modl = let open NotationMods in interp subtyps { acc with format = Some s; } l | SetFormat (k,s) :: l -> interp subtyps { acc with extra = (k,s.CAst.v)::acc.extra; } l + | (SetOnlyParsing | SetItemScope _) :: _ -> assert false in - let subtyps,mods = interp [] default modl in + let modl, syndef_mods = interp_syndef_modifiers modl 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 *) @@ -965,10 +998,10 @@ let interp_modifiers modl = let open NotationMods in 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 } + syndef_mods, { mods with etyps = extra_etyps@mods.etyps } let check_infix_modifiers modifiers = - let mods = interp_modifiers modifiers in + let _, mods = interp_modifiers modifiers in let t = mods.NotationMods.etyps in let u = mods.NotationMods.subtyps in if not (List.is_empty t) || not (List.is_empty u) then @@ -1036,7 +1069,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder | ETConstr _ | ETBigint | ETGlobal - | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny + | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny None let set_internalization_type typs = List.map (fun (_, e) -> internalization_type_of_entry_type e) typs @@ -1292,23 +1325,25 @@ let check_locality_compatibility local custom i_typs = let compute_syntax_data ~local deprecation df modifiers = let open SynData in + let open SyndefMods in let open NotationMods in - let mods = interp_modifiers modifiers in - let onlyprint = mods.only_printing in - let onlyparse = mods.only_parsing in - if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); + let syndef_mods, mods = interp_modifiers modifiers in + let only_printing = mods.only_printing in + let only_parsing = syndef_mods.only_parsing in + if only_printing && only_parsing then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); + if syndef_mods.scopes <> [] then user_err (str "General notations don't support 'in scope'."); let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in - let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in + let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint:only_printing df in let _ = check_useless_entry_types recvars mainvars mods.etyps in (* Notations for interp and grammar *) - let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols onlyprint in + let msgs,n = find_precedence mods.custom mods.level mods.etyps symbols only_printing in let ntn_for_interp = make_notation_key mods.custom symbols in let symbols_for_grammar = if mods.custom = InConstrEntry then remove_curly_brackets symbols else symbols in let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in let ntn_for_grammar = if need_squash then make_notation_key mods.custom symbols_for_grammar else ntn_for_interp in - if mods.custom = InConstrEntry && not onlyprint then check_rule_productivity symbols_for_grammar; + if mods.custom = InConstrEntry && not only_printing then check_rule_productivity symbols_for_grammar; (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = @@ -1329,8 +1364,8 @@ let compute_syntax_data ~local deprecation df modifiers = (* Return relevant data for interpretation and for parsing/printing *) { info = i_data; - only_parsing = mods.only_parsing; - only_printing = mods.only_printing; + only_parsing; + only_printing; deprecation; format = mods.format; extra = mods.extra; @@ -1793,11 +1828,18 @@ let remove_delimiters local scope = let add_class_scope local scope cl = Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) -let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } = +let add_syntactic_definition ~local deprecation env ident (vars,c) modl = + let open SyndefMods in + let skipped, { only_parsing; scopes } = interp_syndef_modifiers modl in + if skipped <> [] then + user_err (str "Simple notations don't support " ++ Ppvernac.pr_syntax_modifier (List.hd skipped)); + let vars = List.map (fun v -> v, List.assoc_opt v scopes) vars in let acvars,pat,reversibility = - try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible - with Not_found -> - let fold accu id = Id.Map.add id NtnInternTypeAny accu in + match vars, intern_name_alias c with + | [], Some(r,u) -> + Id.Map.empty, NRef(r, u), APrioriReversible + | _ -> + let fold accu (id,scope) = Id.Map.add id (NtnInternTypeAny scope) accu in let i_vars = List.fold_left fold Id.Map.empty vars in let nenv = { ninterp_var_type = i_vars; @@ -1805,11 +1847,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } in interp_notation_constr env nenv c in - let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in + let in_pat (id,_) = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) 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 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 + let onlyparsing = only_parsing || fst (printability None [] false reversibility pat) in Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index dd71817083..3ece04f5f9 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -52,7 +52,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : local:bool -> Deprecation.t option -> env -> - Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit + Id.t -> Id.t list * constr_expr -> syntax_modifier list -> unit (** Print the Camlp5 state of a grammar *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 8e5942440b..be34c563c8 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -468,6 +468,8 @@ let pr_syntax_modifier = let open Gramlib.Gramext in function | SetItemLevel (l,bko,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++ pr_opt pr_constr_as_binder_kind bko + | SetItemScope (l,s) -> + prlist_with_sep sep_v2 str l ++ spc () ++ str"in scope" ++ str s | SetLevel n -> pr_at_level (NumLevel n) | SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n)) | SetAssoc LeftA -> keyword "left associativity" @@ -484,9 +486,6 @@ let pr_syntax_modifiers = function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") -let pr_only_parsing_clause onlyparsing = - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []) - let pr_decl_notation prc decl_ntn = let open Vernacexpr in let @@ -1098,12 +1097,12 @@ let pr_vernac_expr v = ) | VernacHints (dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) -> + | VernacSyntacticDefinition (id,(ids,c),l) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ - pr_only_parsing_clause onlyparsing) + pr_syntax_modifiers l) ) | VernacArguments (q, args, more_implicits, mods) -> return ( diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index 9339803948..d36e61864d 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -13,6 +13,8 @@ val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t +val pr_syntax_modifier : Vernacexpr.syntax_modifier -> Pp.t + (** Prints a fixpoint body *) val pr_rec_definition : Vernacexpr.fixpoint_expr -> Pp.t diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 46acaf7264..9757783d09 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -114,10 +114,6 @@ type import_filter_expr = | ImportAll | ImportNames of one_import_filter_name list -type onlyparsing_flag = { onlyparsing : bool } - (* Some v = Parse only; None = Print also. - If v<>Current, it contains the name of the coq version - which this notation is trying to be compatible with *) type locality_flag = bool (* true = Local *) type option_setting = @@ -135,6 +131,7 @@ type definition_expr = type syntax_modifier = | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level + | SetItemScope of string list * scope_name | SetLevel of int | SetCustomEntry of string * int option | SetAssoc of Gramlib.Gramext.g_assoc @@ -411,8 +408,7 @@ type nonrec vernac_expr = | VernacRemoveHints of string list * qualid list | VernacHints of string list * hints_expr | VernacSyntacticDefinition of - lident * (Id.t list * constr_expr) * - onlyparsing_flag + lident * (Id.t list * constr_expr) * syntax_modifier list | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * |