Continuing r12485-12486 (cleaning around name generation)

- backtrack on incompatibility introduced in intro while trying to
  simplify the condition about when to restart the subscript of a name
  (the legacy says: find a new name from x0 if the name xN exists in
  the context but find a new name from xN+1 if the name xN does not
  exists in the context but is a global to avoid).
- made the names chosen by "intro" compliant with the ones printed in
  the goal and used for "intros until" (possible source of rare
  incompatibilities) [replaced the use of visibly_occur_id for
  printing the goal into a call to next_name_away_in_goal]
- also made the names internal to T in "T -> U" printed the same in
  the goal as they are while printing T after it is introducted in the
  hypotheses [non contravariant propagation of boolean isgoal in
  detype_binder]
- simplified a bit visibly_occur_id (the Rel and Var cases were useless as
  soon as the avoid list contained the current env); still this function is
  costly with polynomial time in the depth of binders
- see file output/Naming.v for examples

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 107 insertions, 79 deletions

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 027dbb3ff..c4349624f 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -140,40 +140,75 @@ let it_mkLambda_or_LetIn_name env b hyps =
 (**********************************************************************)
 (* Fresh names *)
 
+let default_x = id_of_string "x"
+
+(* Looks for next "good" name by lifting subscript *)
+
 let next_ident_away_from id bad =
   let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in
-  if bad id then
-    let id0 = if not (has_subscript id) then id else
-    (* Ce serait sans doute mieux avec quelque chose inspiré de
-       *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
-    forget_subscript id in
-    name_rec id0
-  else id
+  name_rec id
 
-let next_ident_away id avoid =
-  next_ident_away_from id (fun id -> List.mem id avoid)
+(* Restart subscript from x0 if name starts with xN, or x00 if name
+   starts with x0N, etc *)
 
-let next_name_away_with_default default name avoid =
-  let id = match name with Name id -> id | Anonymous -> id_of_string default in
-  next_ident_away id avoid
+let restart_subscript id =
+  if not (has_subscript id) then id else
+    (* Ce serait sans doute mieux avec quelque chose inspiré de
+     *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+    forget_subscript id
 
-let next_name_away = next_name_away_with_default "H"
+(* Now, there are different renaming strategies... *)
 
-let default_x = id_of_string "x"
+(* 1- Looks for a fresh name for printing in cases pattern *)
 
 let next_name_away_in_cases_pattern na avoid =
   let id = match na with Name id -> id | Anonymous -> default_x in
   next_ident_away_from id (fun id -> List.mem id avoid or is_constructor id)
 
+(* 2- Looks for a fresh name for introduction in goal *)
+
+(* The legacy strategy for renaming introduction variables is not very uniform:
+   - if the name to use is fresh in the context but used as a global
+     name, then a fresh name is taken by finding a free subscript
+     starting from the current subscript;
+   - but if the name to use is not fresh in the current context, the fresh
+     name is taken by finding a free subscript starting from 0 *)
+
 let next_ident_away_in_goal id avoid =
-  let bad id =
-    List.mem id avoid || (is_global id & not (is_section_variable id)) in
+  let id = if List.mem id avoid then restart_subscript id else id in
+  let bad id = List.mem id avoid || (is_global id & not (is_section_variable id)) in
   next_ident_away_from id bad
 
+let next_name_away_in_goal na avoid =
+  let id = match na with Name id -> id | Anonymous -> id_of_string "H" in
+  next_ident_away_in_goal id avoid
+
+(* 3- Looks for next fresh name outside a list that is moreover valid
+   as a global identifier; the legacy algorithm is that if the name is
+   already used in the list, one looks for a name of same base with
+   lower available subscript; if the name is not in the list but is
+   used globally, one looks for a name of same base with lower subscript
+   beyond the current subscript *)
+
 let next_global_ident_away id avoid =
+  let id = if List.mem id avoid then restart_subscript id else id in
   let bad id = List.mem id avoid || is_global id in
   next_ident_away_from id bad
 
+(* 4- Looks for next fresh name outside a list; if name already used,
+   looks for same name with lower available subscript *)
+
+let next_ident_away id avoid =
+  if List.mem id avoid then
+    next_ident_away_from (restart_subscript id) (fun id -> List.mem id avoid)
+  else id
+
+let next_name_away_with_default default na avoid =
+  let id = match na with Name id -> id | Anonymous -> id_of_string default in
+  next_ident_away id avoid
+
+let next_name_away = next_name_away_with_default "H"
+
 let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
@@ -183,8 +218,38 @@ let make_all_name_different env =
        push_rel (Name id,c,t) newenv)
     env
 
+(* 5- Looks for next fresh name outside a list; avoids also to use names that
+   would clash with short name of global references; if name is already used,
+   looks for name of same base with lower available subscript beyond current
+   subscript *)
+
+let visibly_occur_id id c =
+  let rec occur c = match kind_of_term c with
+    | Const _ | Ind _ | Construct _
+	  when shortest_qualid_of_global Idset.empty (global_of_constr c)
+	    = qualid_of_ident id -> raise Occur
+    | _ -> iter_constr occur c
+  in
+  try occur c; false
+  with Occur -> true
+    | Not_found -> false (* Happens when a global is not in the env *)
+
+let next_ident_away_for_default_printing t id avoid =
+  let bad id = List.mem id avoid or visibly_occur_id id t in
+  next_ident_away_from id bad
+
+let next_name_away_for_default_printing t na avoid =
+  let id = match na with
+  | Name id   -> id
+  | Anonymous ->
+      (* In principle, an anonymous name is not dependent and will not be *)
+      (* taken into account by the function compute_displayed_name_in; *)
+      (* just in case, invent a valid name *)
+      id_of_string "H" in
+  next_ident_away_for_default_printing t id avoid
+
 (**********************************************************************)
-(* The algorithm to display distinct bound variables *)
+(* Displaying terms avoiding bound variables clashes *)
 
 (* Renaming strategy introduced in December 1998:
 
@@ -199,84 +264,47 @@ let make_all_name_different env =
    but f and f0 contribute to the list of variables to avoid (knowing
    that f and f0 are how the f's would be named if introduced, assuming
    no other f and f0 are already used).
-
-   The objective was to have the same names in goals before and after intros.
 *)
 
-type avoid_flags = bool option
-
-let is_rel_id_in_env p env id =
-  try lookup_name_of_rel p env = Name id
-  with Not_found -> false (* Unbound indice : may happen in debug *)
-
-let visibly_occur_id nenv id0 c =
-  let rec occur n c = match kind_of_term c with
-    | Var id when  id=id0 -> raise Occur
-    | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur
-    | Ind ind_sp
-	when basename_of_global (IndRef ind_sp) = id0 ->
-        raise Occur
-    | Construct cstr_sp
-	when basename_of_global (ConstructRef cstr_sp) = id0 ->
-        raise Occur
-    | Rel p when p>n & is_rel_id_in_env (p-n) nenv id0 -> 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 *)
+type renaming_flags =
+  | RenamingForCasesPattern
+  | RenamingForGoal
+  | RenamingElsewhereFor of constr
 
-let next_name_not_occurring avoid_flags name l env_names t =
-  let rec next id =
-    if List.mem id l or visibly_occur_id env_names id t or
-      (* Further restrictions ? *)
-      match avoid_flags with None -> false | Some not_only_cstr ->
-      (if not_only_cstr then
-	(* To be consistent with the intro mechanism *)
-	is_global id & not (is_section_variable id)
-      else
-	(* To avoid constructors in pattern-matchings *)
-	is_constructor id)
-    then next (lift_subscript id)
-    else id
-  in
-  match name with
-  | Name id   -> next id
-  | Anonymous ->
-      (* In principle, an anonymous name is not dependent and will not be *)
-      (* taken into account by the function compute_displayed_name_in; *)
-      (* just in case, invent a valid name *)
-      next (id_of_string "H")
+let next_name_for_display flags =
+  match flags with
+  | RenamingForCasesPattern -> next_name_away_in_cases_pattern
+  | RenamingForGoal -> next_name_away_in_goal
+  | RenamingElsewhereFor t -> next_name_away_for_default_printing t
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in avoid_flags l env_names n c =
-  if n = Anonymous & noccurn 1 c then
-    (Anonymous,l)
+let compute_displayed_name_in flags avoid na c =
+  if na = Anonymous & noccurn 1 c then
+    (Anonymous,avoid)
   else
-    let fresh_id = next_name_not_occurring avoid_flags n l env_names c in
+    let fresh_id = next_name_for_display flags na avoid in
     let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
-    (idopt, fresh_id::l)
+    (idopt, fresh_id::avoid)
 
-let compute_and_force_displayed_name_in avoid_flags l env_names n c =
-  if n = Anonymous & noccurn 1 c then
-    (Anonymous,l)
+let compute_and_force_displayed_name_in flags avoid na c =
+  if na = Anonymous & noccurn 1 c then
+    (Anonymous,avoid)
   else
-    let fresh_id = next_name_not_occurring avoid_flags n l env_names c in
-    (Name fresh_id, fresh_id::l)
+    let fresh_id = next_name_for_display flags na avoid in
+    (Name fresh_id, fresh_id::avoid)
 
-let compute_displayed_let_name_in avoid_flags l env_names n c =
-  let fresh_id = next_name_not_occurring avoid_flags n l env_names c in
-  (Name fresh_id, fresh_id::l)
+let compute_displayed_let_name_in flags avoid na c =
+  let fresh_id = next_name_for_display flags na avoid in
+  (Name fresh_id, fresh_id::avoid)
 
-let rec rename_bound_vars_as_displayed env avoid c =
-  let env_names = names_of_rel_context env in
+let rec rename_bound_vars_as_displayed avoid c =
   let rec rename avoid c =
     match kind_of_term c with
     | Prod (na,c1,c2)  ->
-	let na',avoid' = compute_displayed_name_in None avoid env_names na c2 in
+	let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in
 	mkProd (na', c1, rename avoid' c2)
     | LetIn (na,c1,t,c2) ->
-	let na',avoid' = compute_displayed_let_name_in None avoid env_names na c2 in
+	let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in
 	mkLetIn (na',c1,t, rename avoid' c2)
     | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
     | _ -> c