1 files changed, 312 insertions, 0 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
new file mode 100644
index 00000000..7d141faf
--- /dev/null
+++ b/pretyping/namegen.ml
@@ -0,0 +1,312 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+(* Created from contents that was formerly in termops.ml and
+   nameops.ml, Nov 2009 *)
+
+(* This file is about generating new or fresh names and dealing with
+   alpha-renaming *)
+
+open Util
+open Names
+open Term
+open Nametab
+open Nameops
+open Libnames
+open Environ
+open Termops
+
+(**********************************************************************)
+(* Globality of identifiers *)
+
+let rec is_imported_modpath mp =
+  let current_mp,_ = Lib.current_prefix() in
+    match mp with
+      | MPfile dp ->
+	  let rec find_prefix = function
+	    |MPfile dp1 -> not (dp1=dp)
+	    |MPdot(mp,_) -> find_prefix mp
+	    |MPbound(_) -> false
+	  in find_prefix current_mp
+      | p -> false
+
+let is_imported_ref = function
+  | VarRef _ -> false
+  | IndRef (kn,_)
+  | ConstructRef ((kn,_),_) ->
+      let (mp,_,_) = repr_mind kn in is_imported_modpath mp
+  | ConstRef kn ->
+      let (mp,_,_) = repr_con kn in is_imported_modpath mp
+
+let is_global id =
+  try
+    let ref = locate (qualid_of_ident id) in
+    not (is_imported_ref ref)
+  with Not_found ->
+    false
+
+let is_constructor id =
+  try
+    match locate (qualid_of_ident id) with
+      | ConstructRef _ as ref -> not (is_imported_ref ref)
+      | _ -> false
+  with Not_found ->
+    false
+
+(**********************************************************************)
+(* Generating "intuitive" names from its type *)
+
+let lowercase_first_char id = (* First character of a constr *)
+  lowercase_first_char_utf8 (string_of_id id)
+
+let sort_hdchar = function
+  | Prop(_) -> "P"
+  | Type(_) -> "T"
+
+let hdchar env c =
+  let rec hdrec k c =
+    match kind_of_term c with
+    | Prod (_,_,c)    -> hdrec (k+1) c
+    | Lambda (_,_,c)  -> hdrec (k+1) c
+    | LetIn (_,_,_,c) -> hdrec (k+1) c
+    | Cast (c,_,_)    -> hdrec k c
+    | App (f,l)       -> hdrec k f
+    | Const kn -> lowercase_first_char (id_of_label (con_label kn))
+    | Ind x -> lowercase_first_char (basename_of_global (IndRef x))
+    | Construct x -> lowercase_first_char (basename_of_global (ConstructRef x))
+    | Var id  -> lowercase_first_char id
+    | Sort s -> sort_hdchar s
+    | Rel n ->
+	(if n<=k then "p" (* the initial term is flexible product/function *)
+	 else
+	   try match Environ.lookup_rel (n-k) env with
+	     | (Name id,_,_)   -> lowercase_first_char id
+	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
+	   with Not_found -> "y")
+    | Fix ((_,i),(lna,_,_)) ->
+	let id = match lna.(i) with Name id -> id | _ -> assert false in
+	lowercase_first_char id
+    | CoFix (i,(lna,_,_)) ->
+	let id = match lna.(i) with Name id -> id | _ -> assert false in
+	lowercase_first_char id
+    | Meta _|Evar _|Case (_, _, _, _) -> "y"
+  in
+  hdrec 0 c
+
+let id_of_name_using_hdchar env a = function
+  | Anonymous -> id_of_string (hdchar env a)
+  | Name id   -> id
+
+let named_hd env a = function
+  | Anonymous -> Name (id_of_string (hdchar env a))
+  | x         -> x
+
+let mkProd_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
+let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
+
+let lambda_name = mkLambda_name
+let prod_name = mkProd_name
+
+let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
+let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
+
+let name_assumption env (na,c,t) =
+  match c with
+    | None      -> (named_hd env t na, None, t)
+    | Some body -> (named_hd env body na, c, t)
+
+let name_context env hyps =
+  snd
+    (List.fold_left
+       (fun (env,hyps) d ->
+	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+       (env,[]) (List.rev hyps))
+
+let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
+let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+
+let it_mkProd_or_LetIn_name env b hyps =
+  it_mkProd_or_LetIn ~init:b (name_context env hyps)
+let it_mkLambda_or_LetIn_name env b hyps =
+  it_mkLambda_or_LetIn ~init:b (name_context env 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
+  name_rec id
+
+(* Restart subscript from x0 if name starts with xN, or x00 if name
+   starts with x0N, etc *)
+
+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
+
+(* 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 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 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
+    (fun (na,c,t) newenv ->
+       let id = next_name_away na !avoid in
+       avoid := id::!avoid;
+       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 _ | Var _
+	  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
+
+(**********************************************************************)
+(* Displaying terms avoiding bound variables clashes *)
+
+(* Renaming strategy introduced in December 1998:
+
+   - Rule number 1: all names, even if unbound and not displayed, contribute
+     to the list of names to avoid
+   - Rule number 2: only the dependency status is used for deciding if
+     a name is displayed or not
+
+   Example:
+   bool_ind: "forall (P:bool->Prop)(f:(P true))(f:(P false))(b:bool), P b" is
+   displayed "forall P:bool->Prop, P true -> P false -> forall b:bool, P b"
+   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).
+*)
+
+type renaming_flags =
+  | RenamingForCasesPattern
+  | RenamingForGoal
+  | RenamingElsewhereFor of constr
+
+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 flags avoid na c =
+  if na = Anonymous & noccurn 1 c then
+    (Anonymous,avoid)
+  else
+    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::avoid)
+
+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_for_display flags na avoid in
+    (Name fresh_id, fresh_id::avoid)
+
+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 avoid c =
+  let rec rename avoid c =
+    match kind_of_term c with
+    | Prod (na,c1,c2)  ->
+	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 (RenamingElsewhereFor c2) avoid na c2 in
+	mkLetIn (na',c1,t, rename avoid' c2)
+    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
+    | _ -> c
+  in
+  rename avoid c