diff options
Diffstat (limited to 'engine/namegen.ml')
| -rw-r--r-- | engine/namegen.ml | 60 |
1 files changed, 32 insertions, 28 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index 84eb986845..e56ec2877c 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,9 +21,10 @@ open Nameops open Libnames open Globnames open Environ -open Termops open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (**********************************************************************) (* Conventional names *) @@ -76,6 +77,10 @@ let is_constructor id = with Not_found -> false +let is_section_variable id = + try let _ = Global.lookup_named id in true + with Not_found -> false + (**********************************************************************) (* Generating "intuitive" names from its type *) @@ -114,9 +119,9 @@ let hdchar env c = | Rel n -> (if n<=k then "p" (* the initial term is flexible product/function *) else - try match Environ.lookup_rel (n-k) env |> to_tuple with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) + try match Environ.lookup_rel (n-k) env with + | LocalAssum (Name id,_) | LocalDef (Name id,_,_) -> lowercase_first_char id + | LocalAssum (Anonymous,t) | LocalDef (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) with Not_found -> "y") | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> let id = match lna.(i) with Name id -> id | _ -> assert false in @@ -168,7 +173,7 @@ let it_mkLambda_or_LetIn_name env b hyps = (* 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 + let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id (* Restart subscript from x0 if name starts with xN, or x00 if name @@ -180,10 +185,6 @@ let restart_subscript id = *** make_ident id (Some 0) *** but compatibility would be lost... *) forget_subscript id -let rec to_avoid id = function -| [] -> false -| id' :: avoid -> Id.equal id id' || to_avoid id avoid - let visible_ids (nenv, c) = let accu = ref (Refset_env.empty, Int.Set.empty, Id.Set.empty) in let rec visible_ids n c = match kind_of_term c with @@ -205,8 +206,8 @@ let visible_ids (nenv, c) = if p > n && not (Int.Set.mem p vseen) then let vseen = Int.Set.add p vseen in let name = - try Some (lookup_name_of_rel (p - n) nenv) - with Not_found -> + try Some (List.nth nenv (p - n - 1)) + with Invalid_argument _ | Failure _ -> (* Unbound index: may happen in debug and actually also while computing temporary implicit arguments of an inductive type *) @@ -230,8 +231,8 @@ let visible_ids (nenv, c) = let next_name_away_in_cases_pattern env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in let visible = visible_ids env_t in - let bad id = to_avoid id avoid || is_constructor id - || Id.Set.mem id visible in + let bad id = Id.List.mem id avoid || is_constructor id + || Id.Set.mem id visible in next_ident_away_from id bad (* 2- Looks for a fresh name for introduction in goal *) @@ -244,8 +245,8 @@ let next_name_away_in_cases_pattern env_t na avoid = name is taken by finding a free subscript starting from 0 *) let next_ident_away_in_goal id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in + let id = if Id.List.mem id avoid then restart_subscript id else id in + let bad id = 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 = @@ -262,16 +263,16 @@ let next_name_away_in_goal na avoid = beyond the current subscript *) let next_global_ident_away id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || is_global id in + let id = if Id.List.mem id avoid then restart_subscript id else id in + let bad id = 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 to_avoid id avoid then - next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid) + if Id.List.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -292,15 +293,18 @@ let next_name_away_with_default_using_types default na avoid t = let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env = - let avoid = ref (ids_of_named_context (named_context env)) in - process_rel_context + (** FIXME: this is inefficient, but only used in printing *) + let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in + let sign = named_context_val env in + let rels = rel_context env in + let env0 = reset_with_named_context sign env in + Context.Rel.fold_outside (fun decl newenv -> - let (na,_,t) = to_tuple decl in - let na = named_hd newenv t na in + let na = named_hd newenv (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in avoid := id::!avoid; - push_rel (set_name (Name id) decl) newenv) - env + push_rel (RelDecl.set_name (Name id) decl) newenv) + rels ~init:env0 (* 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, @@ -309,7 +313,7 @@ let make_all_name_different env = let next_ident_away_for_default_printing env_t id avoid = let visible = visible_ids env_t in - let bad id = to_avoid id avoid || Id.Set.mem id visible in + let bad id = Id.List.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad let next_name_away_for_default_printing env_t na avoid = @@ -380,12 +384,12 @@ let rename_bound_vars_as_displayed avoid env c = let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkProd (na', c1, rename avoid' (add_name na' env) c2) + mkProd (na', c1, rename avoid' (na' :: env) c2) | LetIn (na,c1,t,c2) -> let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2) + mkLetIn (na',c1,t, rename avoid' (na' :: env) c2) | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) | _ -> c in |