From 039b2423cf7b85f2f5960dde6a1586f0f07cf9d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Sep 2019 00:06:19 +0200
Subject: Addressing #6082 and #7766 (overriding format of notation).

We do two changes:
- We distinguish between a notion of format generically attached to
  notations and a new notion of format attached to interpreted
  notations. "Reserved Notation" attaches a format
  generically. "Notation" attaches the format specifically to the given
  interpretation, and additionally, attaches it generically if it is the
  first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
  a specific format.
---
 test-suite/output/Notations4.out | 32 ++++++++++++++++
 test-suite/output/Notations4.v   | 81 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 113 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 1c8f237bb8..66b54b629f 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,3 +77,35 @@ Entry constr:expr is
 [ "201" RIGHTA
   [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
 
+fun x : nat => [ x ]
+     : nat -> nat
+fun x : nat => [x]
+     : nat -> nat
+∀ x : nat, x = x
+     : Prop
+File "stdin", line 222, characters 0-160:
+Warning: Notation "∀ _ .. _ , _" was already defined with a different format
+in scope type_scope. [notation-incompatible-format,parsing]
+∀x : nat,x = x
+     : Prop
+File "stdin", line 235, characters 0-60:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 239, characters 0-64:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 244, characters 0-62:
+Warning: Lonely notation "_ %%%% _" was already defined with a different
+format. [notation-incompatible-format,parsing]
+3  %%  4
+     : nat
+3  %%  4
+     : nat
+3   %%   4
+     : nat
+File "stdin", line 272, characters 0-61:
+Warning: The format modifier is irrelevant for only parsing rules.
+[irrelevant-format-only-parsing,parsing]
+File "stdin", line 276, characters 0-63:
+Warning: The only parsing modifier has no effect in Reserved Notation.
+[irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..a6503a8bf3 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -195,3 +195,84 @@ Notation "{ p }" := (p) (in custom expr at level 201, p constr).
 Print Custom Grammar expr.
 
 End Bug11331.
+
+Module Bug_6082.
+
+Declare Scope foo.
+Notation "[ x ]" := (S x) (format "[  x  ]") : foo.
+Open Scope foo.
+Check fun x => S x.
+
+Declare Scope bar.
+Notation "[ x ]" := (S x) (format "[ x ]") : bar.
+Open Scope bar.
+
+Check fun x => S x.
+
+End Bug_6082.
+
+Module Bug_7766.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' ∀  x  ..  y ']' ,  P") : type_scope.
+
+Check forall (x : nat), x = x.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+   format "∀ x .. y , P") : type_scope.
+
+Check forall (x : nat), x = x.
+
+End Bug_7766.
+
+Module N.
+
+(* Other tests about generic and specific formats *)
+
+Reserved Notation "x %%% y" (format "x  %%%  y", at level 35).
+Reserved Notation "x %%% y" (format "x %%% y", at level 35).
+
+(* Not using the reserved format, we warn *)
+
+Notation "x %%% y" := (x+y) (format "x   %%%   y", at level 35).
+
+(* Same scope (here lonely): we warn *)
+
+Notation "x %%%% y" := (x+y) (format "x  %%%%  y", at level 35).
+Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35).
+
+(* Test if the format for a specific notation becomes the default
+   generic format or if the generic format, in the absence of a
+   Reserved Notation, is the one canonically obtained from the
+   notation *)
+
+Declare Scope foo_scope.
+Declare Scope bar_scope.
+Declare Scope bar'_scope.
+Notation "x %% y" := (x+y) (at level 47, format "x   %%   y") : foo_scope.
+Open Scope foo_scope.
+Check 3 %% 4.
+
+(* No scope, we inherit the initial format *)
+
+Notation "x %% y" := (x*y) : bar_scope. (* Inherit the format *)
+Open Scope bar_scope.
+Check 3 %% 4.
+
+(* Different scope and no reserved notation, we don't warn *)
+
+Notation "x %% y" := (x*y) (at level 47, format "x    %%    y") : bar'_scope.
+Open Scope bar'_scope.
+Check 3 %% 4.
+
+(* Warn for combination of "only parsing" and "format" *)
+
+Notation "###" := 0 (at level 0, only parsing, format "###").
+
+(* In reserved notation, warn only for the "only parsing" *)
+
+Reserved Notation "##" (at level 0, only parsing, format "##").
+
+End N.
-- 
cgit v1.2.3