Partial fix to #4592 (notation requiring alpha-conversion for printing).

5 files changed, 101 insertions, 3 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 4a507b37e..2cace1ed9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -616,7 +616,9 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
      glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the
      choice of exact variable be done there; but again, this would be a non-trivial
      refinement *)
-  if alpmetas != [] then raise No_match;
+  let v =
+    if alpmetas == [] then v
+    else try rename_glob_vars alpmetas v with Not_found -> raise No_match in
   (* TODO: handle the case of multiple occs in different scopes *)
   ((var,v)::terms,onlybinders,termlists,binderlists)
 
@@ -669,6 +671,19 @@ let bind_termlist_env (terms,onlybinders,termlists,binderlists as sigma) var vl
     add_termlist_env sigma var vl
   with Not_found -> add_termlist_env sigma var vl
 
+let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+  try
+    match Id.List.assoc var terms with
+    | GVar (_,id') ->
+       (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
+       sigma
+    | _ -> anomaly (str "A term which can be a binder has to be a variable")
+  with Not_found ->
+    (* The matching against a term allowing to find the instance has not been found yet *)
+    (* If it will be a different name, we shall unfortunately fail *)
+    (* TODO: look at the consequences for alp *)
+    alp, add_env alp sigma var (GVar (Loc.ghost,id))
+
 let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
     let v' = Id.List.assoc var onlybinders in
@@ -772,8 +787,8 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
       bind_binding_env alp sigma id2 na1
   | (Name id1,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs and hence reason up to *)
-      (* alpha-conversion for the given occurrence of the name (see #)) *)
-      (fst alp,(id1,id2)::snd alp), sigma
+      (* alpha-conversion for the given occurrence of the name (see #4592)) *)
+      bind_term_as_binding_env alp sigma id2 id1
   | (Anonymous,Name id2) when is_term_meta id2 metas ->
       (* We let the non-binding occurrence define the rhs *)
       alp, sigma
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5c8060996..244f013e3 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -470,6 +470,68 @@ let loc_of_glob_constr = function
   | GCast (loc,_,_) -> loc
 
 (**********************************************************************)
+(* Alpha-renaming                                                     *)
+
+let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
+let test_id l id = if collide_id l id then raise Not_found
+let test_na l na = name_iter (test_id l) na
+
+let update_subst na l =
+  let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in
+  let l' = name_fold Id.List.remove_assoc na l in
+  name_fold
+    (fun id _ ->
+     if in_range id l' then
+       let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in
+       Name id', (id,id')::l
+     else na,l)
+    na (na,l)
+
+let rec rename_glob_vars l = function
+  | GVar (loc,id) as r ->
+     (try GVar (loc,Id.List.assoc id l)
+      with Not_found ->
+      if List.exists (fun (_,id') -> Id.equal id id') l then raise Not_found
+      else r)
+  | GRef (_,VarRef id,_) as r ->
+      if List.exists (fun (_,id') -> Id.equal id id') l then raise Not_found
+      else r
+  | GProd (loc,na,bk,t,c) ->
+      let na',l' = update_subst na l in
+      GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLambda (loc,na,bk,t,c) ->
+      let na',l' = update_subst na l in
+      GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLetIn (loc,na,b,c) ->
+      let na',l' = update_subst na l in
+      GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c)
+  (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
+  | GCases (loc,ci,po,tomatchl,cls) ->
+      let test_pred_pat (na,ino) =
+        test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in
+      let test_clause idl = List.iter (test_id l) idl in
+      let po = Option.map (rename_glob_vars l) po in
+      let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
+      let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in
+      GCases (loc,ci,po,tomatchl,cls)
+  | GLetTuple (loc,nal,(na,po),c,b) ->
+     List.iter (test_na l) (na::nal);
+     GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po),
+                rename_glob_vars l c,rename_glob_vars l b)
+  | GIf (loc,c,(na,po),b1,b2) ->
+     test_na l na;
+     GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
+          rename_glob_vars l b1,rename_glob_vars l b2)
+  | GRec (loc,k,idl,decls,bs,ts) ->
+     Array.iter (test_id l) idl;
+     GRec (loc,k,idl,
+           Array.map (List.map (fun (na,k,bbd,bty) ->
+             test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
+           Array.map (rename_glob_vars l) bs,
+           Array.map (rename_glob_vars l) ts)
+  | r -> map_glob_constr (rename_glob_vars l) r
+
+(**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
 let rec cases_pattern_of_glob_constr na = function
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c2b27ca6a..dcc6ef88b 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -44,6 +44,8 @@ val bound_glob_vars : glob_constr -> Id.Set.t
 val loc_of_glob_constr : glob_constr -> Loc.t
 val glob_visible_short_qualid : glob_constr -> Id.t list
 
+val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr
+
 (** [map_pattern_binders f m c] applies [f] to all the binding names
     in a pattern-matching expression ({!Glob_term.GCases}) represented
     here by its relevant components [m] and [c]. It is used to
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 64317a9f8..6b2177830 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -32,3 +32,9 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f
        forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))}
 where
 ?T : [x : nat * (bool * unit) |- Type] 
+forall n : nat, {#n | 1 > n}
+     : Prop
+forall x : nat, {|x | x > 0|}
+     : Prop
+exists2 x : nat, x = 1 & x = 2
+     : Prop
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 655a01c2d..f6e0d2d9d 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -36,3 +36,16 @@ Check ETA x y, le_S.
 
 Notation "'CURRY' x .. y , f" := (fun x => .. (fun y => f (x, .. (y,tt) ..)) ..) (at level 200, x binder, y binder).
 Check fun f => CURRY (x:nat) (y:bool), f.
+
+(**********************************************************************)
+(* Notations with variables bound both as a term and as a binder      *)
+(* This is #4592 *)
+
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
+Check forall n:nat, {# n | 1 > n}.
+
+Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
+Notation "{| x | P |}" := (foo x (fun x => P)).
+Check forall x:nat, {| x | x > 0 |}.
+
+Check ex2 (fun x => x=1) (fun x0 => x0=2).