From 8d27b12365a1d8b3f1670a055537dd3724583baf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 30 Aug 2020 08:20:29 +0200
Subject: Notations: reworking the treatment of only-parsing and only-printing
 notations.

The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.

Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.

The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.

Additionally, we anticipate the ability to selectively
activate/deactivate each of those.

This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.

Rules for importing are not changed (see forthcoming #12984 though).

We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.

Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
---
 test-suite/output/bug_12908.out |  5 +++++
 test-suite/output/bug_12908.v   |  7 +++++++
 test-suite/output/bug_13112.out |  4 ++++
 test-suite/output/bug_13112.v   |  5 +++++
 test-suite/output/bug_9682.out  |  9 +++++++++
 test-suite/output/bug_9682.v    | 10 ++++++++++
 6 files changed, 40 insertions(+)
 create mode 100644 test-suite/output/bug_13112.out
 create mode 100644 test-suite/output/bug_13112.v

(limited to 'test-suite')

diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out
index fca6dde704..54c4f98422 100644
--- a/test-suite/output/bug_12908.out
+++ b/test-suite/output/bug_12908.out
@@ -1,2 +1,7 @@
 forall m n : nat, m * n = (2 * m * n)%nat
      : Prop
+File "stdin", line 11, characters 0-31:
+Warning: Notation "_ * _" was already used in scope nat_scope.
+[notation-overridden,parsing]
+forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n
+     : Prop
diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v
index 558c9f9f6a..6f7be22fa0 100644
--- a/test-suite/output/bug_12908.v
+++ b/test-suite/output/bug_12908.v
@@ -1,6 +1,13 @@
 Definition mult' m n := 2 * m * n.
+
 Module A.
 (* Test hiding of a scoped notation by a lonely notation *)
 Infix "*" := mult'.
 Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
 End A.
+
+Module B.
+(* Test that an overriden scoped notation is deactivated *)
+Infix "*" := mult' : nat_scope.
+Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n.
+End B.
diff --git a/test-suite/output/bug_13112.out b/test-suite/output/bug_13112.out
new file mode 100644
index 0000000000..a8a98d6b68
--- /dev/null
+++ b/test-suite/output/bug_13112.out
@@ -0,0 +1,4 @@
+0 + 0
+     : nat
+HI
+     : nat
diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v
new file mode 100644
index 0000000000..9fee5e09d8
--- /dev/null
+++ b/test-suite/output/bug_13112.v
@@ -0,0 +1,5 @@
+Reserved Notation "'HI'".
+Notation "'HI'" := (O + O) (only parsing).
+Check HI. (* 0 + 0 : nat *)
+Notation "'HI'" := (O + O) (only printing).
+Check HI. (* 0 + 0 : nat *)
diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out
index e69de29bb2..45d9e4cad1 100644
--- a/test-suite/output/bug_9682.out
+++ b/test-suite/output/bug_9682.out
@@ -0,0 +1,9 @@
+mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x
+return M (x = x) with
+| 1
+end
+     : unit
+#
+     : True
+##
+     : True
diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v
index 3630142126..fa30d323ef 100644
--- a/test-suite/output/bug_9682.v
+++ b/test-suite/output/bug_9682.v
@@ -16,3 +16,13 @@ Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
     (at level 200, ls at level 91, p at level 10, only printing,
      format "'[  ' mmatch  '/' x ']'  '/' '[  ' in  '/' T ']'  '/' '[  ' as  '/' y ']'  '/' '[  ' return  M  p ']'  with  '//' '[' ls ']'  '//' end"
      ).
+(* Check use of "mmatch" *)
+Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end).
+
+(* 2nd example *)
+Notation "#" := I (at level 0, only parsing).
+Notation "#" := I (at level 0, only printing).
+Check #.
+Notation "##" := I (at level 0, only printing).
+Notation "##" := I (at level 0, only parsing).
+Check ##.
-- 
cgit v1.2.3


From 4c090da84c1cf2c4e37b9ddd5b2321c474f19e60 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 4 Sep 2020 19:04:38 +0200
Subject: New spacing/formatting in Locate Notation, Print Scopes, Print
 Visibility.

---
 test-suite/output/Notations3.out | 17 +++++++----------
 test-suite/output/bug_9180.out   |  3 +--
 test-suite/output/locate.out     |  5 ++---
 3 files changed, 10 insertions(+), 15 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index abada44da7..bd22d45059 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -231,16 +231,13 @@ fun l : list nat => match l with
      : list nat -> list nat
 
 Arguments foo _%list_scope
-Notation
-"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
-(default interpretation)
-"'exists' ! x .. y , p" := ex
-                             (unique
-                                (fun x => .. (ex (unique (fun y => p))) ..))
-: type_scope (default interpretation)
-Notation
-"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
-(default interpretation)
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+  : type_scope (default interpretation)
+Notation "'exists' ! x .. y , p" :=
+  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope
+  (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
+  (default interpretation)
 1 subgoal
   
   ============================
diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out
index ed4892b389..f035d0252a 100644
--- a/test-suite/output/bug_9180.out
+++ b/test-suite/output/bug_9180.out
@@ -1,4 +1,3 @@
-Notation
-"n .+1" := S n : nat_scope (default interpretation)
+Notation "n .+1" := (S n) : nat_scope (default interpretation)
 forall x : nat, x.+1 = x.+1
      : Prop
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 473db2d312..93d9d6cf7b 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,3 +1,2 @@
-Notation
-"b1 && b2" := if b1 then b2 else false (default interpretation)
-"x && y" := andb x y : bool_scope
+Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
+Notation "x && y" := (andb x y) : bool_scope
-- 
cgit v1.2.3