Allowing variables used in recursive notation to occur several times in pattern.

This allows for instance to support recursive notations of the form:

Notation "! x .. y # A #" :=
  (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
  (at level 200, x binder).

4 files changed, 66 insertions, 4 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index bedf932b0..7411c7e35 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -697,7 +697,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     | t ->
       glob_constr_of_notation_constr_with_binders ?loc
         (traverse_binder subst avoid) (aux subst') subinfos t
-  and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
+  and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
     (* of the notations *)
     try
@@ -705,6 +705,14 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       intern {env with tmp_scope = scopt;
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
+    try
+      match binderopt with
+      | Some (x,binder) when Id.equal x id ->
+         let terms = terms_of_binders [binder] in
+         assert (List.length terms = 1);
+         intern env (List.hd terms)
+      | _ -> raise Not_found
+    with Not_found ->
     DAst.make ?loc (
     try
       GVar (Id.Map.find id renaming)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 73b5100ca..ac65f6875 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -284,7 +284,9 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | None ->
         let () = diff := Some (x, y, RecursiveTerms lassoc) in
         true
-      | Some _ -> false
+      | Some (x', y', RecursiveTerms lassoc')
+      | Some (x', y', RecursiveBinders (lassoc',_,_)) ->
+        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
       end
   | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
   | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) ->
@@ -295,7 +297,11 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | None ->
         let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
         aux c term
-      | Some _ -> false
+      | Some (x', y', RecursiveBinders (lassoc',_,_)) ->
+        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
+      | Some (x', y', RecursiveTerms lassoc') ->
+        let () = diff := Some (x, y, RecursiveBinders (lassoc,t_x,t_y)) in
+        Id.equal x x' && Id.equal y y' && lassoc = lassoc'
       end
   | _ ->
       mk_glob_constr_eq aux c1 c2 in
@@ -327,10 +333,21 @@ let compare_recursive_parts found f f' (iterator,subc) =
                                recursive_term_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_term_vars };
         NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,RecursiveBinders (lassoc,t_x,t_y)) ->
+        let toadd,x,y,lassoc =
+          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_term_vars ||
+             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (!found).recursive_binders_vars
+          then
+            None,x,y,lassoc
+          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_term_vars ||
+                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (!found).recursive_binders_vars
+          then
+            None,y,x,not lassoc
+          else
+            Some (x,y),x,y,lassoc in
         let iterator = f' (if lassoc then iterator else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
         (* found have been collected by compare_constr *)
         found := { !found with vars = List.remove Id.equal y (!found).vars;
-                               recursive_binders_vars = (x,y) :: (!found).recursive_binders_vars };
+                               recursive_binders_vars = Option.fold_right (fun a l -> a::l) toadd (!found).recursive_binders_vars };
         check_is_hole x t_x;
         check_is_hole y t_y;
         NBinderList (x,y,iterator,f (Option.get !terminator),lassoc)
@@ -976,6 +993,8 @@ let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin las
         match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
       in
       let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
+      (* In case y is bound not only to a binder but also to a term *)
+      let sigma = remove_sigma y sigma in
       aux sigma (b::bl) rest
     with No_match when not (List.is_empty bl) ->
       bl, rest, sigma in
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e114ea894..5bfdec989 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -163,3 +163,13 @@ exists_true (x : nat) (A : Type) (R : A -> A -> Prop)
      : Prop
 {{{{True, nat -> True}}, nat -> True}}
      : Prop * Prop * Prop
+{{D 1, 2}}
+     : nat * nat * (nat * nat * (nat * nat))
+! a b : nat # True #
+     : Prop * (Prop * Prop)
+!!!! a b : nat # True #
+     : Prop * Prop * (Prop * Prop * Prop)
+@@ a b : nat # a = b # b = a #
+     : Prop * Prop
+exists_non_null x y z t : nat , x = y /\ z = t
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index a7fed3561..c7e32f733 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -282,3 +282,28 @@ End G.
 (* Allows recursive patterns for binders to be associative on the left *)
 Notation "!! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
 Check !! a b : nat # True #.
+
+(* Examples where the recursive pattern refer several times to the recursive variable *)
+
+Notation "{{D  x , .. , y }}" := ((x,x), .. ((y,y),(0,0)) ..).
+Check {{D 1, 2 }}.
+
+Notation "! x .. y # A #" :=
+  ((forall x, x=x), .. ((forall y, y=y), A) ..)
+  (at level 200, x binder).
+Check ! a b : nat # True #.
+
+Notation "!!!! x .. y # A #" :=
+  (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
+  (at level 200, x binder).
+Check !!!! a b : nat # True #.
+
+Notation "@@ x .. y # A # B #" :=
+  ((forall x, .. (forall y, A) ..), (forall x, .. (forall y, B) ..))
+  (at level 200, x binder).
+Check @@ a b : nat # a=b # b=a #.
+
+Notation "'exists_non_null' x .. y  , P" :=
+  (ex (fun x => x <> 0 /\ .. (ex (fun y => y <> 0 /\ P)) ..))
+  (at level 200, x binder).
+Check exists_non_null x y z t , x=y/\z=t.