Fixing the essence of naming bug #3204: use same strategy for naming

cases pattern variables than for naming forall/fun binders (but still
avoiding constructor names).

Note in passing: such as it is implemented, the general strategy is in
O(n²) in the number of nested binders, because, when computing the
name for each 'fun x => c" (or forall, or a pattern name), the names
from the outside c and visibly occurring in c are computed.

5 files changed, 40 insertions, 37 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8bff91602..bdec8307a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -223,7 +223,7 @@ let update_name na ((_,e),c) =
       na
 
 let rec decomp_branch ndecls nargs nal b (avoid,env as e) c =
-  let flag = if b then RenamingForGoal else RenamingForCasesPattern in
+  let flag = if b then RenamingForGoal else RenamingForCasesPattern (env,c) in
   if Int.equal ndecls 0 then (List.rev nal,(e,c))
   else
     let na,c,f,nargs' =
@@ -536,12 +536,13 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
     if force_wildcard () && noccurn 1 b then
       PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
     else
-      let id = next_name_away_in_cases_pattern x avoid in
-      PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids
+      let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (env,b) in
+      let na,avoid' = compute_displayed_name_in flag avoid x b in
+      PatVar (dl,na),avoid',(add_name na env),add_vname ids na
   in
   let rec buildrec ids patlist avoid env n b =
     if Int.equal n 0 then
-      (dl, ids,
+      (dl, Id.Set.elements ids,
        [PatCstr(dl, constr, List.rev patlist,Anonymous)],
        detype isgoal avoid env b)
     else
@@ -566,7 +567,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
 	    buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
 
   in
-  buildrec [] [] avoid env construct_nargs branch
+  buildrec Id.Set.empty [] avoid env construct_nargs branch
 
 and detype_binder isgoal bk avoid env na ty c =
   let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 16ba03ad7..8e1b51a7d 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -183,13 +183,38 @@ let rec to_avoid id = function
 | [] -> false
 | id' :: avoid -> Id.equal id id' || to_avoid id avoid
 
+let occur_rel p env id =
+  try
+    let name = lookup_name_of_rel p env in
+    begin match name with
+    | Name id' -> Id.equal id' id
+    | Anonymous -> false
+    end
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let visibly_occur_id id (nenv,c) =
+  let rec occur n c = match kind_of_term c with
+    | Const _ | Ind _ | Construct _ | Var _
+      when
+        let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in
+        qualid_eq short (qualid_of_ident id) ->
+      raise Occur
+    | Rel p when p>n && occur_rel (p-n) nenv id -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
+  in
+  try occur 1 c; false
+  with Occur -> true
+    | Not_found -> false (* Happens when a global is not in the env *)
+
 (* Now, there are different renaming strategies... *)
 
 (* 1- Looks for a fresh name for printing in cases pattern *)
 
-let next_name_away_in_cases_pattern na avoid =
+let next_name_away_in_cases_pattern env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
-  next_ident_away_from id (fun id -> to_avoid id avoid || is_constructor id)
+  let bad id = to_avoid id avoid || is_constructor id
+                                 || visibly_occur_id id env_t in
+  next_ident_away_from id bad
 
 (* 2- Looks for a fresh name for introduction in goal *)
 
@@ -262,29 +287,6 @@ let make_all_name_different env =
    looks for name of same base with lower available subscript beyond current
    subscript *)
 
-let occur_rel p env id =
-  try
-    let name = lookup_name_of_rel p env in
-    begin match name with
-    | Name id' -> Id.equal id' id
-    | Anonymous -> false
-    end
-  with Not_found -> false (* Unbound indice : may happen in debug *)
-
-let visibly_occur_id id (nenv,c) =
-  let rec occur n c = match kind_of_term c with
-    | Const _ | Ind _ | Construct _ | Var _
-      when
-        let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in
-        qualid_eq short (qualid_of_ident id) ->
-      raise Occur
-    | Rel p when p>n && occur_rel (p-n) nenv id -> raise Occur
-    | _ -> iter_constr_with_binders succ occur n c
-  in
-  try occur 1 c; false
-  with Occur -> true
-    | Not_found -> false (* Happens when a global is not in the env *)
-
 let next_ident_away_for_default_printing env_t id avoid =
   let bad id = to_avoid id avoid || visibly_occur_id id env_t in
   next_ident_away_from id bad
@@ -318,13 +320,13 @@ let next_name_away_for_default_printing env_t na avoid =
 *)
 
 type renaming_flags =
-  | RenamingForCasesPattern
+  | RenamingForCasesPattern of (Name.t list * constr)
   | RenamingForGoal
   | RenamingElsewhereFor of (Name.t list * constr)
 
 let next_name_for_display flags =
   match flags with
-  | RenamingForCasesPattern -> next_name_away_in_cases_pattern
+  | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t
   | RenamingForGoal -> next_name_away_in_goal
   | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t
 
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 88ce43f8e..e1f55be6e 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -64,7 +64,7 @@ val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
 val next_global_ident_away : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a constructor name already used in current module *)
-val next_name_away_in_cases_pattern : Name.t -> Id.t list -> Id.t
+val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t
 
 (** Default is [default_non_dependent_ident] *)
 val next_name_away  : Name.t -> Id.t list -> Id.t
@@ -81,7 +81,7 @@ val set_reserved_typed_name : (types -> Name.t) -> unit
    Making name distinct for displaying *)
 
 type renaming_flags =
-  | RenamingForCasesPattern (** avoid only global constructors *)
+  | RenamingForCasesPattern of (Name.t list * constr) (** avoid only global constructors *)
   | RenamingForGoal (** avoid all globals (as in intro) *)
   | RenamingElsewhereFor of (Name.t list * constr)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5f7e2916b..34fac5e75 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1193,8 +1193,8 @@ let indirect_dependency d decls =
   pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls))
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) =
-  let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
-  in Evd.evar_universe_context sigma, nf_evar sigma c
+(*  let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma
+in*) Evd.evar_universe_context sigma, nf_evar sigma c
 
 let default_matching_flags sigma = {
   modulo_conv_on_closed_terms = Some empty_transparent_state;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 274bfc33c..4df08b6a1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -135,7 +135,7 @@ let make_cases s =
 	     let rec rename avoid = function
 	       | [] -> []
 	       | (n,_)::l ->
-		   let n' = Namegen.next_name_away_in_cases_pattern n avoid in
+		   let n' = Namegen.next_name_away_in_cases_pattern ([],mkMeta 0) n avoid in
 		   Id.to_string n' :: rename (n'::avoid) l in
 	     let al' = rename [] al in
 	     (Id.to_string consname :: al') :: l)