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

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

5 files changed, 31 insertions, 26 deletions

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