From 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 13 Aug 2017 18:17:32 +0200
Subject: Fixing/improving notations with recursive patterns.

- The "terminator" of a recursive notation is now interpreted in the
  environment in which it occurs rather than the environment at the
  beginning of the recursive patterns.

  Note that due to a tolerance in checking unbound variables of
  notations, a variable unbound in the environment was still working
  ok as long as no user-given variable was shadowing a private
  variable of the notation - see the "exists_mixed" example in
  test-suite.

  Conversely, in a notation such as:

    Notation "!! x .. y # A #" :=
      ((forall x, True), .. ((forall y, True), A) ..)
      (at level 200, x binder).
    Check !! a b # a=b #.

  The unbound "a" was detected only at pretyping and not as expected
  at internalizing time, due to "a=b" interpreted in context
  containing a and b.

- Similarly, each binder is now interpreted in the environment in
  which it occurs rather than as if the sequence of binders was
  dependent from the left to the right (such a dependency was ok for
  "forall" or "exists" but not in general).

  For instance, in:

    Notation "!! x .. y # A #" :=
      ((forall x, True), .. ((forall y, True), A) ..)
      (at level 200, x binder).
    Check !! (a:nat) (b:a=a) # True #.

  The illegal dependency of the type of b in a was detected only at
  pretyping time.

- If a let-in occurs in the sequence of binders of a notation with a
  recursive pattern, it is now inserted in between the occurrences of
  the iterator rather than glued with the forall/fun of the iterator.
  For instance, in:

    Notation "'exists_true' x .. y , P" :=
      (exists x, True /\ .. (exists y, True /\ P) ..)
      (at level 200, x binder).
    Check exists_true '(x,y) (u:=0), x=y.

  We now get

    exists '(x, y), True /\ (let u := 0 in True /\ x = y)

  while we had before the let-in breaking the repeated pattern:

    exists '(x, y), (let u := 0 in True /\ x = y)

  This is more compositional, and, in particular, the printer algorithm
  now recognizes the pattern which is otherwise broken.
---
 test-suite/output/Notations3.out | 21 +++++++++++++++++++++
 test-suite/output/Notations3.v   | 20 ++++++++++++++++++++
 2 files changed, 41 insertions(+)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index bd24f3f61..cf69874ca 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -140,3 +140,24 @@ alist = [0; 1; 2]
      : list nat
 ! '{{x, y}}, x + y = 0
      : Prop
+exists x : nat,
+  nat ->
+  exists y : nat,
+    nat ->
+    exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0
+     : Prop
+exists x : nat,
+  nat ->
+  exists y : nat,
+    nat ->
+    exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0
+     : Prop
+exists_true '{{x, y}},
+(let u := 0 in exists_true '{{z, t}}, x + y = 0 /\ z + t = 0)
+     : Prop
+exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
+(forall x : A, R x x)
+     : Prop
+exists_true (x : nat) (A : Type) (R : A -> A -> Prop) 
+(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 773241f90..3e07fbce9 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -258,3 +258,23 @@ End B.
 (* for isolated "forall" (was not working already in 8.6) *)
 Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
 Check ! '(x,y), x+y=0.
+
+(* Check that the terminator of a recursive pattern is interpreted in
+   the correct environment of bindings *)
+Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun y => forall z:nat, z=0 /\ P)) ..)) (at level 200, x binder).
+Check exists_mixed x y '(u,t), x+y=0/\u+t=0.
+Check exists_mixed x y '(z,t), x+y=0/\z+t=0.
+
+(* Check that intermediary let-in are inserted inbetween instances of
+   the repeated pattern *)
+Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder).
+Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0.
+
+(* Check that generalized binders are correctly interpreted *)
+
+Module G.
+Generalizable Variables A R.
+Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
+Check exists_true `{Reflexive A R}, forall x, R x x.
+Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
+End G.
-- 
cgit v1.2.3