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).

2 files changed, 31 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