Notations: Avoiding computing parsing rule when in onlyprinting mode.

In particular, this fixes #9741.

6 files changed, 54 insertions, 29 deletions

diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 9f133ca9d4..ffc92fa53a 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -37,7 +37,4 @@ type one_notation_grammar = {
   notgram_prods : grammar_constr_prod_item list list;
 }
 
-type notation_grammar = {
-  notgram_onlyprinting : bool;
-  notgram_rules : one_notation_grammar list
-}
+type notation_grammar = one_notation_grammar list
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 661f9c5cad..a84d2a4cb0 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -15,16 +15,16 @@ open Notation
 open Notation_gram
 
 (* Register the level of notation for parsing and printing
-   (we also register a precomputed parsing rule) *)
+   (also register the parsing rule if not onlyprinting) *)
 
 let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
-let declare_notation_level ntn ~onlyprint parsing_rule level =
+let declare_notation_level ntn parsing_rule level =
   try
     let _ = NotationMap.find ntn !notation_level_map in
     anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
+  notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map
 
 let level_of_notation ntn =
   NotationMap.find ntn !notation_level_map
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index d5711569f0..7c676fbb10 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -16,8 +16,8 @@ val level_eq : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit
-val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+val declare_notation_level : notation -> notation_grammar option -> level -> unit
+val level_of_notation : notation -> notation_grammar option * level
   (** raise [Not_found] if not declared *)
 
 (** Returns notations with defined parsing/printing rules *)
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 92f44faec8..0277e79adb 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -59,7 +59,8 @@ let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
   | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
      UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
 
-(* Concrete syntax for symbolic-extension table *)
+(* Register generic and specific printing rules *)
+
 let generic_notation_printing_rules =
   Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
 
diff --git a/test-suite/bugs/closed/bug_9741.v b/test-suite/bugs/closed/bug_9741.v
new file mode 100644
index 0000000000..247155d8b3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9741.v
@@ -0,0 +1,21 @@
+(* This was failing at parsing *)
+
+Notation "'a'" := tt (only printing).
+Goal True. let a := constr:(1+1) in idtac a. Abort.
+
+(* Idem *)
+
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+Open Scope string_scope.
+
+Axiom Ox: string -> Z.
+
+Axiom isMMIOAddr: Z -> Prop.
+
+Notation "'Ox' a" := (Ox a) (only printing, at level 10, format "'Ox' a").
+
+Goal False.
+  set (f := isMMIOAddr).
+  set (x := f (Ox "0018")).
+Abort.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 69d9bd4c41..b0b8a7612e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -788,7 +788,7 @@ let warn_incompatible_format =
 type syntax_parsing_extension = {
   synext_level : Notation_gram.level;
   synext_notation : notation;
-  synext_notgram : notation_grammar;
+  synext_notgram : notation_grammar option;
 }
 
 type syntax_printing_extension = {
@@ -833,29 +833,30 @@ let check_and_extend_constr_grammar ntn rule =
     let ntn_for_grammar = rule.notgram_notation in
     if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
-    let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
-    if not (Notgram_ops.level_eq prec oldprec) && not oldonlyprint then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
-    if oldonlyprint then raise Not_found
+    let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
+    if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+    if oldparsing = None then raise Not_found
   with Not_found ->
     Egramcoq.extend_constr_grammar rule
 
 let cache_one_syntax_extension (pa_se,pp_se) =
   let ntn = pa_se.synext_notation in
   let prec = pa_se.synext_level in
-  let onlyprint = pa_se.synext_notgram.notgram_onlyprinting in
   (* Check and ensure that the level and the precomputed parsing rule is declared *)
-  let parsing_to_activate =
+  let oldparsing =
     try
-      let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn in
-      if not (Notgram_ops.level_eq prec oldprec) && (not oldonlyprint || onlyprint) then error_incompatible_level ntn oldprec prec;
-      oldonlyprint && not onlyprint
+      let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in
+      if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec;
+      oldparsing
     with Not_found ->
       (* Declare the level and the precomputed parsing rule *)
-      let _ = Notgram_ops.declare_notation_level ntn ~onlyprint pa_se.synext_notgram prec in
-      not onlyprint in
+      let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in
+      None in
   (* Declare the parsing rule *)
-  if parsing_to_activate then
-    List.iter (check_and_extend_constr_grammar ntn) pa_se.synext_notgram.notgram_rules;
+  begin match oldparsing, pa_se.synext_notgram with
+  | None, Some grams -> List.iter (check_and_extend_constr_grammar ntn) grams
+  | _ -> (* The grammars rules are canonically derived from the string and the precedence*) ()
+  end;
   (* Printing *)
   match pp_se with
   | None -> ()
@@ -875,7 +876,7 @@ let subst_printing_rule subst x = x
 
 let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
   (local, ({ pa_sy with
-    synext_notgram = { pa_sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) pa_sy.synext_notgram.notgram_rules }},
+    synext_notgram = Option.map (List.map (subst_parsing_rule subst)) pa_sy.synext_notgram },
     Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy)
   )
 
@@ -1486,7 +1487,7 @@ exception NoSyntaxRule
 let recover_notation_syntax ntn =
   let pa =
     try
-      let _,pa_rule,prec = Notgram_ops.level_of_notation ntn in
+      let pa_rule,prec = Notgram_ops.level_of_notation ntn in
       { synext_level = prec;
         synext_notation = ntn;
         synext_notgram = pa_rule }
@@ -1505,7 +1506,9 @@ let recover_notation_syntax ntn =
 
 let recover_squash_syntax sy =
   let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
-  sy :: sq.synext_notgram.notgram_rules
+  match sq.synext_notgram with
+  | Some gram -> sy :: gram
+  | None -> raise NoSyntaxRule
 
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
@@ -1538,10 +1541,13 @@ let make_pp_rule level (typs,symbols) fmt =
 
 let make_parsing_rules (sd : SynData.syn_data) = let open SynData in
   let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
-  let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in {
+  let pa_rule =
+    if sd.only_printing then None
+    else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash)
+  in {
     synext_level    = sd.level;
     synext_notation = fst sd.info;
-    synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
+    synext_notgram  = pa_rule;
   }
 
 let warn_irrelevant_format =
@@ -1610,7 +1616,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
     let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
     let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (* If the only printing flag has been explicitly requested, put it back *)
-    let onlyprint = onlyprint || pa_sy.synext_notgram.notgram_onlyprinting in
+    let onlyprint = onlyprint || pa_sy.synext_notgram = None in
     let _,_,_,typs = pa_sy.synext_level in
     Some pa_sy.synext_level, typs, onlyprint, pp_sy
   end else None, [], false, None in