Merge PR #7477: Support for notations with autonomous only-parsing and only-printing declarations.

5 files changed, 47 insertions, 26 deletions

diff --git a/CHANGES b/CHANGES
index 68cc495f5..cdc1ff6a6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -33,6 +33,14 @@ Tactic language
   called by OCaml-defined tactics.
 - Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
+Changes from 8.8.0 to 8.8.1
+===========================
+
+Notations
+
+- Fixed unexpected collision between only-parsing and only-printing
+  notations (issue #7462).
+
 Changes from 8.8+beta1 to 8.8.0
 ===============================
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 4a6d2a154..20e46bfe3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,7 +49,6 @@ type notation_location = (DirPath.t * DirPath.t) * string
 type notation_data = {
   not_interp : interpretation;
   not_location : notation_location;
-  not_onlyprinting : bool;
 }
 
 type scope = {
@@ -430,13 +429,15 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
 
 (* Uninterpreted notation levels *)
 
-let declare_notation_level ntn level =
+let declare_notation_level ?(onlyprint=false) ntn level =
   if String.Map.mem ntn !notation_level_map then
     anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
-  notation_level_map := String.Map.add ntn level !notation_level_map
+  notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
 
-let level_of_notation ntn =
-  String.Map.find ntn !notation_level_map
+let level_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+  if onlyprint' && not onlyprint then raise Not_found;
+  level
 
 (* The mapping between notations and their interpretation *)
 
@@ -449,20 +450,21 @@ let warn_notation_overridden =
 let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
-  let () =
-    if String.Map.mem ntn sc.notations then
-    let which_scope = match scopt with
-    | None -> mt ()
-    | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
-    warn_notation_overridden (ntn,which_scope)
-  in
-  let notdata = {
-    not_interp = pat;
-    not_location = df;
-    not_onlyprinting = onlyprint;
-  } in
-  let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
-  let () = scope_map := String.Map.add scope sc !scope_map in
+  if not onlyprint then begin
+    let () =
+      if String.Map.mem ntn sc.notations then
+      let which_scope = match scopt with
+      | None -> mt ()
+      | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+      warn_notation_overridden (ntn,which_scope)
+    in
+    let notdata = {
+      not_interp = pat;
+      not_location = df;
+    } in
+    let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
+    scope_map := String.Map.add scope sc !scope_map
+  end;
   begin match scopt with
   | None -> scope_stack := SingleNotation ntn :: !scope_stack
   | Some _ -> ()
@@ -487,7 +489,6 @@ let rec find_interpretation ntn find = function
 
 let find_notation ntn sc =
   let n = String.Map.find ntn (find_scope sc).notations in
-  let () = if n.not_onlyprinting then raise Not_found in
   (n.not_interp, n.not_location)
 
 let notation_of_prim_token = function
@@ -631,7 +632,6 @@ let exists_notation_in_scope scopt ntn onlyprint r =
   try
     let sc = String.Map.find scope !scope_map in
     let n = String.Map.find ntn sc.notations in
-    onlyprint = n.not_onlyprinting && 
     interpretation_eq n.not_interp r
   with Not_found -> false
 
diff --git a/interp/notation.mli b/interp/notation.mli
index eac87414f..ccc67fe49 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -137,8 +137,8 @@ val availability_of_notation : scope_name option * notation -> local_scopes ->
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val declare_notation_level : notation -> level -> unit
-val level_of_notation : notation -> level (** raise [Not_found] if no level *)
+val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
+val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
 
 (** {6 Miscellaneous} *)
 
diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v
new file mode 100644
index 000000000..40ca39e38
--- /dev/null
+++ b/test-suite/bugs/closed/7462.v
@@ -0,0 +1,13 @@
+(* Adding an only-printing notation should not override existing
+   interpretations for the same notation. *)
+
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *)
+
+(* Adding an only-printing notation should not let believe
+   that a parsing rule has been given *)
+
+Notation "$ x" := (@id bool x) (only printing, at level 0).
+Notation "$ x" := (@id nat x) (only parsing, at level 0).
+Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index feeca6075..76958b05f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -738,12 +738,12 @@ let cache_one_syntax_extension se =
   let prec = se.synext_level in
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
   try
-    let oldprec = Notation.level_of_notation ntn in
+    let oldprec = Notation.level_of_notation ~onlyprint ntn in
     if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
   with Not_found ->
     if is_active_compat se.synext_compat then begin
       (* Reserve the notation level *)
-      Notation.declare_notation_level ntn prec;
+      Notation.declare_notation_level ntn prec ~onlyprint;
       (* Declare the parsing rule *)
       if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
       (* Declare the notation rule *)
@@ -1274,7 +1274,7 @@ exception NoSyntaxRule
 
 let recover_notation_syntax ntn =
   try
-    let prec = Notation.level_of_notation ntn in
+    let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
     let pp_rule,_ = Notation.find_notation_printing_rule ntn in
     let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
     let pa_rule = Notation.find_notation_parsing_rules ntn in