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.

0 files changed, 0 insertions, 0 deletions