[abbreviation] user syntax to set interp scope of argument

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

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).

doc/sphinx/user-extensions/syntax-extensions.rst

@@ -1181,7 +1181,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
@@ -1373,6 +1373,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
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
@@ -1566,7 +1570,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

doc/tools/docgram/common.edit_mlg

@@ -1410,8 +1410,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: [
@@ -2643,7 +2644,6 @@ SPLICE: [
 | quoted_attributes  (* todo: splice or not? *)
 | printable
 | hint
-| only_parsing
 | record_fields
 | constructor_type
 | record_binder

doc/tools/docgram/fullGrammar

@@ -1401,18 +1401,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"
@@ -1428,8 +1423,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
 ]

doc/tools/docgram/orderedGrammar

@@ -1096,7 +1096,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 "," ")" )
@@ -1540,7 +1540,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

interp/constrexpr_ops.ml

@@ -283,10 +283,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 ->

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;

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

interp/notation_ops.ml

@@ -681,7 +681,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

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 =