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.

1 files changed, 11 insertions, 6 deletions

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)