A heuristic to add parentheses in the presence of rules such as

Notation "## c" := (S c) (at level 0, c at level 100).

which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.

The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in

Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)

The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.

The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:

Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)

I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.

6 files changed, 41 insertions, 15 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index b8f4f3201..1a2e7074f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -965,7 +965,7 @@ let pr_visibility prglob = function
 (**********************************************************************)
 (* Mapping notations to concrete syntax *)
 
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * precedence * tolerability option
 type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
 let printing_rules =
diff --git a/interp/notation.mli b/interp/notation.mli
index 480979ccc..352c20313 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -194,7 +194,7 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
 (** {6 Printing rules for notations} *)
 
 (** Declare and look for the printing rule for symbolic notations *)
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * precedence * tolerability option
 type extra_unparsing_rules = (string * string) list
 val declare_notation_printing_rule :
   notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1866ca504..7fad6fb9a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -85,8 +85,8 @@ end) = struct
         mt ()
       | UnpMetaVar (_, prec) as unp :: l ->
         let c = pop env in
+        let pp1= pr (n, prec) c in
         let pp2 = aux l in
-        let pp1 = pr (n, prec) c in
         return unp pp1 pp2
       | UnpListMetaVar (_, prec, sl) as unp :: l ->
         let cl = pop envlist in
@@ -95,15 +95,16 @@ end) = struct
         return unp pp1 pp2
       | UnpBinderListMetaVar (_, isopen, sl) as unp :: l ->
         let cl = pop bll in
-        let pp2 = aux l in
         let pp1 = pr_binders (fun () -> aux sl) isopen cl in
+        let pp2 = aux l in
         return unp pp1 pp2
       | UnpTerminal s as unp :: l ->
-        let pp2 = aux l in
         let pp1 = str s in
+        let pp2 = aux l in
         return unp pp1 pp2
       | UnpBox (b,sub) as unp :: l ->
-        let pp1 = ppcmd_of_box b (aux sub) in
+        let pp1 = aux sub in
+        let pp1 = ppcmd_of_box b pp1 in
         let pp2 = aux l in
         return unp pp1 pp2
       | UnpCut cut as unp :: l ->
@@ -114,8 +115,12 @@ end) = struct
     aux unps
 
   let pr_notation pr pr_binders s env =
-    let unpl, level = find_notation_printing_rule s in
-    print_hunks level pr pr_binders env unpl, level
+    let unpl, level, trailing_level = find_notation_printing_rule s in
+    let pp = print_hunks level pr pr_binders env unpl in
+    let level = match trailing_level with
+      | Some (level',_) -> max level level'
+      | _ -> level in
+    pp, level 
 
   let pr_delimiters key strm =
     strm ++ str ("%"^key)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d3837..593a5df84 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,7 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+fun x : nat => (## x) + x
+     : nat -> nat
+fun x : nat => ## x + x
+     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7..d32758375 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,10 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check printing of notations that have arguments at higher level
+   than the notation itself *)
+
+Notation "## a" := (S a) (at level 0, a at level 100).
+Check fun x => (S x) + x.
+Check fun x => S (x + x).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7c1f05cd3..e0cdc1b62 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -479,6 +479,14 @@ let make_hunks etyps symbols from =
 
   in make symbols
 
+let rec trailing_precedence etyps from = function
+  | [] -> assert false
+  | [NonTerminal id|SProdList (id,_)] ->
+     let typ = List.assoc id etyps in
+     Some (precedence_of_entry_type from typ)
+  | [Terminal _|Break _] -> None
+  | _ :: l -> trailing_precedence etyps from l
+
 (* Build default printing rules from explicit format *)
 
 let error_format () = error "The format does not match the notation."
@@ -672,7 +680,7 @@ type syntax_extension = {
   synext_level : Notation.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
-  synext_unparsing : unparsing list;
+  synext_unparsing : unparsing_rule;
   synext_extra : (string * string) list;
 }
 
@@ -691,7 +699,7 @@ let cache_one_syntax_extension se =
     Egramcoq.extend_constr_grammar prec se.synext_notgram;
     (* Declare the printing rule *)
     Notation.declare_notation_printing_rule ntn
-      ~extra:se.synext_extra (se.synext_unparsing, fst prec)
+      ~extra:se.synext_extra se.synext_unparsing
 
 let cache_syntax_extension (_, (_, sy)) =
   List.iter cache_one_syntax_extension sy
@@ -1051,7 +1059,7 @@ exception NoSyntaxRule
 let recover_syntax ntn =
   try
     let prec = Notation.level_of_notation ntn in
-    let pp_rule,_ = Notation.find_notation_printing_rule ntn 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 = Egramcoq.recover_constr_grammar ntn prec in
     { synext_level = prec;
@@ -1085,14 +1093,16 @@ let make_pa_rule i_typs (n,typs,symbols,_) ntn =
     notgram_prods = prod;
     notgram_typs = i_typs; }
 
-let make_pp_rule (n,typs,symbols,fmt) =
-  match fmt with
+let make_pp_rule (n,typs,symbols,fmt) (lev,_) =
+  let unp = match fmt with
   | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
-  | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
+  | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) in
+  let trailingprec = trailing_precedence typs lev symbols in
+  (unp, lev, trailingprec)
 
 let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
   let pa_rule = make_pa_rule i_typs sy_data ntn in
-  let pp_rule = make_pp_rule sy_data in
+  let pp_rule = make_pp_rule sy_data prec in
   let sy = {
     synext_level = prec;
     synext_notation = ntn;