Module Namegen

This file features facilities to generate fresh names.

type intro_pattern_naming_expr =
| IntroIdentifier of Names.Id.t
| IntroFresh of Names.Id.t
| IntroAnonymous

General evar naming using intro patterns

val intro_pattern_naming_eq : intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool

Equalities on intro_pattern_naming

val default_prop_ident : Names.Id.t
val default_small_ident : Names.Id.t
val default_type_ident : Names.Id.t
val default_non_dependent_ident : Names.Id.t
val default_dependent_ident : Names.Id.t
val lowercase_first_char : Names.Id.t -> string
val sort_hdchar : Sorts.t -> string
val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string
val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t
val named_hd : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Name.t
val head_name : Evd.evar_map -> EConstr.types -> Names.Id.t option
val mkProd_name : Environ.env -> Evd.evar_map -> (Names.Name.t Context.binder_annot * EConstr.types * EConstr.types) -> EConstr.types
val mkLambda_name : Environ.env -> Evd.evar_map -> (Names.Name.t Context.binder_annot * EConstr.types * EConstr.constr) -> EConstr.constr
val prod_name : Environ.env -> Evd.evar_map -> (Names.Name.t Context.binder_annot * EConstr.types * EConstr.types) -> EConstr.types

Deprecated synonyms of mkProd_name and mkLambda_name

val lambda_name : Environ.env -> Evd.evar_map -> (Names.Name.t Context.binder_annot * EConstr.types * EConstr.constr) -> EConstr.constr
val prod_create : Environ.env -> Evd.evar_map -> (Sorts.relevance * EConstr.types * EConstr.types) -> EConstr.constr
val lambda_create : Environ.env -> Evd.evar_map -> (Sorts.relevance * EConstr.types * EConstr.constr) -> EConstr.constr
val name_assumption : Environ.env -> Evd.evar_map -> EConstr.rel_declaration -> EConstr.rel_declaration
val name_context : Environ.env -> Evd.evar_map -> EConstr.rel_context -> EConstr.rel_context
val mkProd_or_LetIn_name : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.rel_declaration -> EConstr.types
val mkLambda_or_LetIn_name : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.rel_declaration -> EConstr.constr
val it_mkProd_or_LetIn_name : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.rel_context -> EConstr.types
val it_mkLambda_or_LetIn_name : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.rel_context -> EConstr.constr
val next_ident_away_from : Names.Id.t -> (Names.Id.t -> bool) -> Names.Id.t

Avoid clashing with a name satisfying some predicate

val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

next_ident_away original_id unwanted_ids returns a new identifier as close as possible to the original_id while avoiding all unwanted_ids.

In particular:

  • if original_id does not appear in the list of unwanted_ids, then original_id is returned.

  • if original_id appears in the list of unwanted_ids, then this function returns a new id that:

    • has the same root as the original_id,
    • does not occur in the list of unwanted_ids,
    • has the smallest possible subscript.

where by subscript of some identifier we mean last part of it that is composed only from (decimal) digits and by root of some identifier we mean the whole identifier except for the subscript.

E.g. if we take foo42, then 42 is the subscript, and foo is the root.

val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Avoid clashing with a name already used in current module

val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t

Avoid clashing with a name already used in current module but tolerate overwriting section variables, as in goals

val next_name_away : Names.Name.t -> Names.Id.Set.t -> Names.Id.t

Default is default_non_dependent_ident

val next_name_away_with_default : string -> Names.Name.t -> Names.Id.Set.t -> Names.Id.t
val next_name_away_with_default_using_types : string -> Names.Name.t -> Names.Id.Set.t -> EConstr.types -> Names.Id.t
val set_reserved_typed_name : (EConstr.types -> Names.Name.t) -> unit
type renaming_flags =
| RenamingForCasesPattern of Names.Name.t list * EConstr.constr

avoid only global constructors

| RenamingForGoal

avoid all globals (as in intro)

| RenamingElsewhereFor of Names.Name.t list * EConstr.constr
val make_all_name_different : Environ.env -> Evd.evar_map -> Environ.env
val compute_displayed_name_in : Evd.evar_map -> renaming_flags -> Names.Id.Set.t -> Names.Name.t -> EConstr.constr -> Names.Name.t * Names.Id.Set.t
val compute_and_force_displayed_name_in : Evd.evar_map -> renaming_flags -> Names.Id.Set.t -> Names.Name.t -> EConstr.constr -> Names.Name.t * Names.Id.Set.t
val compute_displayed_let_name_in : Evd.evar_map -> renaming_flags -> Names.Id.Set.t -> Names.Name.t -> 'a -> Names.Name.t * Names.Id.Set.t
val rename_bound_vars_as_displayed : Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types
val compute_displayed_name_in_gen : (Evd.evar_map -> int -> 'a -> bool) -> Evd.evar_map -> Names.Id.Set.t -> Names.Name.t -> 'a -> Names.Name.t * Names.Id.Set.t