From dbe29599c2e9bf49368c7a92fe00259aa9cbbe15 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 8 Apr 2016 12:07:57 +0200
Subject: 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.
---
 test-suite/output/Notations2.out | 4 ++++
 test-suite/output/Notations2.v   | 7 +++++++
 2 files changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d38372..593a5df84c 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 4e0d135d7d..d32758375f 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).
-- 
cgit v1.2.3