diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-08 12:07:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:45 +0200 |
| commit | dbe29599c2e9bf49368c7a92fe00259aa9cbbe15 (patch) | |
| tree | 7c737eed6064ab403cec16fe1ff4c02d554758b7 /interp/notation.mli | |
| parent | 5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 (diff) | |
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.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |