Adding support for an "only parsing" modifier in "where"-based notations.

Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>

10 files changed, 57 insertions, 34 deletions

diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
new file mode 100644
index 0000000000..1d30d16664
--- /dev/null
+++ b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Notations declared with the ``where`` clause in the declaration of
+  inductive types, coinductive types, record fields, fixpoints and
+  cofixpoints now support the ``only parsing`` modifier
+  (`#11602 <https://github.com/coq/coq/pull/11602>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 6c1d83b3b8..b9e181dd94 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -24,7 +24,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
      record         : `record_keyword` `record_body` with … with `record_body`
      record_keyword : Record | Inductive | CoInductive
      record_body    : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }.
-     field          : `ident` [ `binders` ] : `type` [ where `notation` ]
+     field          : `ident` [ `binders` ] : `type` [ `decl_notations` ]
                     : `ident` [ `binders` ] [: `type` ] := `term`
 
 .. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition }
@@ -35,8 +35,10 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is
    omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of
    fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`.
-   Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the
-   order of the fields is important. Finally, :token:`binders` are parameters of the record.
+   Notice that the type of a particular identifier may depend on a previously-given identifier. Thus the
+   order of the fields is important. The record can depend as a whole on parameters :token:`binders`
+   and each field can also depend on its own :token:`binders`. Finally, notations can be attached to
+   fields using the :n:`decl_notations` annotation.
 
    :cmd:`Record` and :cmd:`Structure` are synonyms.
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 9b4d7cf5fa..fd95a5cef4 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -909,10 +909,10 @@ notations are given below. The optional :production:`scope` is described in
    notation      : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`].
                  : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`].
                  : [Local] Reserved Notation `string` [(`modifiers`)] .
-                 : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
-                 : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`].
-                 : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
-                 : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`].
+                 : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`].
+                 : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`].
+                 : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`].
+                 : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`].
                  : [Local] Declare Custom Entry `ident`.
    modifiers     : `modifier`, … , `modifier`
    modifier      : at level `num`
@@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in
 
 .. prodn::
    decl_notations ::= where @decl_notation {* and @decl_notation }
-   decl_notation ::= @string := @term1_extended {? : @ident }
+   decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident }
 
 .. note:: No typing of the denoted expression is performed at definition
           time. Type checking is done only at the time of use of the notation.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 8ff571ae55..ff2556c5dc 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 Arguments foo _%type_scope
 Arguments Foo _%type_scope
+myprod unit bool
+     : Set
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 9eec9a7dad..db1276cb6c 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set :=
 (* Check printing of let-ins *)
 #[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo.
 Print foo.
+
+(* Check where clause *)
+Reserved Notation "x ** y" (at level 40, left associativity).
+Inductive myprod A B :=
+  mypair : A -> B -> A ** B
+  where "A ** B" := (myprod A B) (only parsing).
+
+Check unit ** bool.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 37b584f8d9..f2a533fdb2 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -44,11 +44,12 @@ let quoted_attributes = Entry.create "vernac:quoted_attributes"
 let class_rawexpr = Entry.create "vernac:class_rawexpr"
 let thm_token = Entry.create "vernac:thm_token"
 let def_body = Entry.create "vernac:def_body"
-let decl_notation = Entry.create "vernac:decl_notation"
+let decl_notations = Entry.create "vernac:decl_notations"
 let record_field = Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
 let section_subset_expr = Entry.create "vernac:section_subset_expr"
 let scope_delimiter = Entry.create "vernac:scope_delimiter"
+let only_parsing = Entry.create "vernac:only_parsing"
 
 let make_bullet s =
   let open Proof_bullet in
@@ -176,7 +177,7 @@ let name_of_ident_decl : ident_decl -> name_decl =
 (* Gallina declarations *)
 GRAMMAR EXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    record_field decl_notation rec_definition ident_decl univ_decl;
+    record_field decl_notations rec_definition ident_decl univ_decl;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -376,15 +377,15 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "Eval"; r = red_expr; "in" -> { Some r }
       | -> { None } ] ]
   ;
-  one_decl_notation:
-    [ [ ntn = ne_lstring; ":="; c = constr;
-        scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,scopt) } ] ]
+  decl_notation:
+    [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing;
+        scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,b,scopt) } ] ]
   ;
   decl_sep:
     [ [ IDENT "and" -> { () } ] ]
   ;
-  decl_notation:
-    [ [ "where"; l = LIST1 one_decl_notation SEP decl_sep -> { l }
+  decl_notations:
+    [ [ "where"; l = LIST1 decl_notation SEP decl_sep -> { l }
     | -> { [] } ] ]
   ;
   (* Inductives and records *)
@@ -396,7 +397,7 @@ GRAMMAR EXTEND Gram
     [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
         extrapar = OPT [ "|"; p = binders -> { p } ];
         c = OPT [ ":"; c = lconstr -> { c } ];
-        lc=opt_constructors_or_fields; ntn = decl_notation ->
+        lc=opt_constructors_or_fields; ntn = decl_notations ->
            { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
   ;
   constructor_list_or_record_decl:
@@ -423,14 +424,14 @@ GRAMMAR EXTEND Gram
     [ [ id_decl = ident_decl;
         bl = binders_fixannot;
         rtype = type_cstr;
-        body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation ->
+        body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations ->
           { let binders, rec_order = bl in
             {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
           } ] ]
   ;
   corec_definition:
     [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
-        body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation ->
+        body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
         { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
         } ]]
   ;
@@ -466,7 +467,7 @@ GRAMMAR EXTEND Gram
   record_field:
   [ [ attr = LIST0 quoted_attributes ;
       bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
-      rf_notation = decl_notation -> {
+      rf_notation = decl_notations -> {
       let rf_canonical = attr |> List.flatten |> parse canonical_field in
       let rf_subclass, rf_decl = bd in
       rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
@@ -1145,7 +1146,7 @@ GRAMMAR EXTEND Gram
 (* Grammar extensions *)
 
 GRAMMAR EXTEND Gram
-  GLOBAL: syntax;
+  GLOBAL: syntax only_parsing;
 
   syntax:
    [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index fedebc9700..7a150e021b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1654,13 +1654,13 @@ let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
 
 (* Notations with only interpretation *)
 
-let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
-  let df' = add_notation_interpretation_core ~local:false df env c sc false false None in
+let add_notation_interpretation env ({CAst.loc;v=df},c,onlyparse,sc) =
+  let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in
   Dumpglob.dump_notation (loc,df') sc true
 
-let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
+let set_notation_for_interpretation env impls ({CAst.v=df},c,onlyparse,sc) =
   (try ignore
-    (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ());
+    (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ());
   with NoSyntaxRule ->
     user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index e3e733a4b7..d76820b033 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -37,12 +37,12 @@ val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit
 (** Add only the interpretation of a notation that already has pa/pp rules *)
 
 val add_notation_interpretation :
-  env -> (lstring * constr_expr * scope_name option) -> unit
+  env -> decl_notation -> unit
 
 (** Add a notation interpretation for supporting the "where" clause *)
 
-val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
-  (lstring * constr_expr * scope_name option) -> unit
+val set_notation_for_interpretation :
+  env -> Constrintern.internalization_env -> decl_notation -> unit
 
 (** Add only the parsing/printing rule of a notation *)
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 33d9e3d98a..48961fd271 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -297,11 +297,6 @@ open Pputils
     | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
     | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
 
-  let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
-    fnl () ++ keyword "where " ++ qs ntn ++ str " := "
-    ++ Flags.without_option Flags.beautify prc c ++
-      pr_opt (fun sc -> str ": " ++ str sc) scopt
-
   let pr_binders_arg =
     let env = Global.env () in
     let sigma = Evd.from_env env in
@@ -418,6 +413,15 @@ let string_of_theorem_kind = let open Decls in 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 ({loc; v=ntn},c,onlyparsing, scopt) =
+    fnl () ++ keyword "where " ++ qs ntn ++ str " := "
+    ++ Flags.without_option Flags.beautify prc c
+    ++ pr_only_parsing_clause onlyparsing
+    ++ pr_opt (fun sc -> str ": " ++ str sc) scopt
+
   let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
     let env = Global.env () in
     let sigma = Evd.from_env env in
@@ -1057,7 +1061,7 @@ let string_of_definition_object_kind = let open Decls in function
           hov 2
             (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
                prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
-               pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
+               pr_only_parsing_clause onlyparsing)
         )
       | VernacArguments (q, args, more_implicits, mods) ->
         return (
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 22aaab2a68..b6514487e8 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -128,7 +128,7 @@ type definition_expr =
   | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
-type decl_notation = lstring * constr_expr * scope_name option
+type decl_notation = lstring * constr_expr * bool * scope_name option
 
 type 'a fix_expr_gen =
   { fname : lident