diff options
Diffstat (limited to 'pretyping/namegen.ml')
-rw-r--r-- | pretyping/namegen.ml | 186 |
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 |