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

6 files changed, 153 insertions, 116 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index fe84141eef..aa58a08082 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -32,6 +32,7 @@ open Coercion.Default
 (* Abbreviations *)
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
+let pf_hyps gls = named_context_of_val gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
 let pf_concl gl = gl.it.evar_concl
 
@@ -146,7 +147,8 @@ let mk_clenv_from_n gls n (c,cty) =
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
 let mk_clenv_rename_from_n gls n (c,t) =
-  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed (pf_env gls) [] t)
+  let ids = collect_visible_vars t in
+  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed ids t)
 
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c152f3ca8b..f1da217a60 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -171,27 +171,23 @@ let computable p k =
 let avoid_flag isgoal = if isgoal then Some true else None
 
 let lookup_name_as_displayed env t s =
-  let rec lookup avoid env_names n c = match kind_of_term c with
+  let rec lookup avoid n c = match kind_of_term c with
     | Prod (name,_,c') ->
-	(match compute_displayed_name_in (Some true) avoid env_names name c' with
-           | (Name id,avoid') ->
-	       if id=s then (Some n)
-	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
-	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
+	(match compute_displayed_name_in RenamingForGoal avoid name c' with
+           | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c'
+	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-	(match compute_displayed_name_in (Some true) avoid env_names name c' with
-           | (Name id,avoid') ->
-	       if id=s then (Some n)
-	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
-	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
-    | Cast (c,_,_) -> lookup avoid env_names n c
+	(match compute_displayed_name_in RenamingForGoal avoid name c' with
+           | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c'
+	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
+    | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
-  in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
+  in lookup (ids_of_named_context (named_context env)) 1 t
 
 let lookup_index_as_renamed env t n =
   let rec lookup n d c = match kind_of_term c with
     | Prod (name,_,c') ->
-	  (match compute_displayed_name_in (Some true) [] empty_names_context name c' with
+	  (match compute_displayed_name_in RenamingForGoal [] name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if n=0 then
@@ -201,7 +197,7 @@ let lookup_index_as_renamed env t n =
 		 else
 		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match compute_displayed_name_in (Some true) [] empty_names_context name c' with
+	  (match compute_displayed_name_in RenamingForGoal [] name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if n=0 then
@@ -226,6 +222,7 @@ let update_name na ((_,e),c) =
       na
 
 let rec decomp_branch n nal b (avoid,env as e) c =
+  let flag = if b then RenamingForGoal else RenamingForCasesPattern in
   if n=0 then (List.rev nal,(e,c))
   else
     let na,c,f =
@@ -235,7 +232,7 @@ let rec decomp_branch n nal b (avoid,env as e) c =
 	| _ ->
 	    Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])),
 	    compute_displayed_name_in in
-    let na',avoid' = f (Some b) avoid env na c in
+    let na',avoid' = f flag avoid na c in
     decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
 
 let rec build_tree na isgoal e ci cl =
@@ -533,16 +530,15 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
   buildrec [] [] avoid env construct_nargs branch
 
 and detype_binder isgoal bk avoid env na ty c =
+  let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
   let na',avoid' =
-    if bk = BLetIn then
-      compute_displayed_let_name_in (avoid_flag isgoal) avoid env na c
-    else
-      compute_displayed_name_in (avoid_flag isgoal) avoid env na c in
+    if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
+    else compute_displayed_name_in flag avoid na c in
   let r =  detype isgoal avoid' (add_name na' env) c in
   match bk with
-  | BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r)
-  | BLambda -> RLambda (dl, na',Explicit,detype isgoal avoid env ty, r)
-  | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
+  | BProd -> RProd (dl, na',Explicit,detype false avoid env ty, r)
+  | BLambda -> RLambda (dl, na',Explicit,detype false avoid env ty, r)
+  | BLetIn -> RLetIn (dl, na',detype false avoid env ty, r)
 
 let rec detype_rel_context where avoid env sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
@@ -553,8 +549,10 @@ let rec detype_rel_context where avoid env sign =
 	match where with
 	| None -> na,avoid
 	| Some c ->
-	    if b<>None then compute_displayed_let_name_in None avoid env na c
-	    else compute_displayed_name_in None avoid env na c in
+	    if b<>None then
+	      compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+	    else
+	      compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 027dbb3ff1..c4349624fe 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
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 0587b886b2..096c09b511 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -61,20 +61,17 @@ val next_name_away_with_default : string -> name -> identifier list ->
 (**********************************************************************)
 (* Making name distinct for displaying *)
 
-type avoid_flags = bool option
- (* Some true = avoid all globals (as in intro);
-    Some false = avoid only global constructors;
-    None = don't avoid globals *)
+type renaming_flags =
+  | RenamingForCasesPattern (* avoid only global constructors *)
+  | RenamingForGoal (* avoid all globals (as in intro) *)
+  | RenamingElsewhereFor of constr
 
 val make_all_name_different : env -> env
 
 val compute_displayed_name_in :
-  avoid_flags -> identifier list -> name list -> name -> constr ->
-    name * identifier list
+  renaming_flags -> identifier list -> name -> constr -> name * identifier list
 val compute_and_force_displayed_name_in :
-  avoid_flags -> identifier list -> name list -> name -> constr ->
-    name * identifier list
+  renaming_flags -> identifier list -> name -> constr -> name * identifier list
 val compute_displayed_let_name_in :
-  avoid_flags -> identifier list -> name list -> name -> constr ->
-    name * identifier list
-val rename_bound_vars_as_displayed : env -> identifier list -> types -> types
+  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+val rename_bound_vars_as_displayed : identifier list -> types -> types
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 4de4bde2cb..07ac5df215 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -523,6 +523,17 @@ let collect_metas c =
   in
   List.rev (collrec [] c)
 
+(* collects all visible var occurences (does not include indirect
+   dependencies of section variables via global references) *)
+
+let collect_visible_vars c =
+  let rec collrec acc c =
+    match kind_of_term c with
+    | Var id -> list_add_set id acc
+    | _      -> fold_constr collrec acc c
+  in
+  List.rev (collrec [] c)
+
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 59f7750d3f..44a96b613c 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -109,6 +109,7 @@ val free_rels : constr -> Intset.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val collect_metas : constr -> int list
+val collect_visible_vars : constr -> identifier list
 val occur_term : constr -> constr -> bool (* Synonymous
  of dependent *)
 (* Substitution of metavariables *)