Module Evd

This file defines the pervasive unification state used everywhere in Coq tactic engine. It is very low-level and most of the functions exported here are irrelevant to the standard API user. Consider using Evarutil or Proofview instead.

A unification state (of type evar_map) is primarily a finite mapping from existential variables to records containing the type of the evar (evar_concl), the context under which it was introduced (evar_hyps) and its definition (evar_body). evar_extra is used to add any other kind of information.

It also contains conversion constraints, debugging information and information about meta variables.

type econstr
type etypes = econstr
type esorts
type erelevance
Existential variables and unification states
Evar filters
module Filter : sig ... end
module Abstraction : sig ... end
Evar infos
type defined = [
| `defined
]
type undefined = [
| `undefined
]
type _ evar_body =
| Evar_empty : undefined evar_body
| Evar_defined : econstr -> defined evar_body
type 'a evar_info
type any_evar_info =
| EvarInfo : 'a evar_info -> any_evar_info
Projections from evar infos
val evar_concl : undefined evar_info -> econstr

Type of the evar.

val evar_context : 'a evar_info -> (econstr, etypes, erelevance) Context.Named.pt

Context of the evar.

val evar_hyps : 'a evar_info -> Environ.named_context_val

Context of the evar.

val evar_body : 'a evar_info -> 'a evar_body

Optional content of the evar.

val evar_candidates : undefined evar_info -> econstr list option

List of possible solutions when known that it is a finite list

val evar_source : 'a evar_info -> Evar_kinds.t Loc.located
val evar_filter : 'a evar_info -> Filter.t

Boolean mask over evar_hyps. Should have the same length. When filtered out, the corresponding variable is not allowed to occur in the solution

val evar_abstract_arguments : undefined evar_info -> Abstraction.t

Boolean information over evar_hyps, telling if an hypothesis instance can be imitated or should stay abstract in HO unification problems and inversion (see second_order_matching_with_args for its use).

val evar_relevance : 'a evar_info -> erelevance

Relevance of the conclusion of the evar.

Derived projections
val evar_filtered_context : 'a evar_info -> (econstr, etypes, erelevance) Context.Named.pt
val evar_filtered_hyps : 'a evar_info -> Environ.named_context_val
val evar_env : Environ.env -> 'a evar_info -> Environ.env
val evar_filtered_env : Environ.env -> 'a evar_info -> Environ.env
val evar_identity_subst : 'a evar_info -> econstr SList.t
val map_evar_body : (econstr -> econstr) -> 'a evar_body -> 'a evar_body
val map_evar_info : (econstr -> econstr) -> 'a evar_info -> 'a evar_info
Unification state

*

type evar_map

Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction.

val empty : evar_map

The empty evar map.

val from_env : ?binders:Names.lident list -> Environ.env -> evar_map

The empty evar map with given universe context, taking its initial universes from env, possibly with initial universe binders. This is the main entry point at the beginning of the process of interpreting a declaration (e.g. before entering the interpretation of a Theorem statement).

val from_ctx : UState.t -> evar_map

The empty evar map with given universe context. This is the main entry point when resuming from a already interpreted declaration (e.g. after having interpreted a Theorem statement and preparing to open a goal).

val is_empty : evar_map -> bool

Whether an evarmap is empty.

val has_undefined : evar_map -> bool

has_undefined sigma is true if and only if there are uninstantiated evars in sigma.

val has_given_up : evar_map -> bool

has_given_up sigma is true if and only if there are given up evars in sigma.

val has_shelved : evar_map -> bool

has_shelved sigma is true if and only if there are shelved evars in sigma.

val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?relevance:erelevance -> ?abstract_arguments:Abstraction.t -> ?candidates:econstr list -> ?name:Names.Id.t -> ?typeclass_candidate:bool -> ?principal:bool -> Environ.named_context_val -> evar_map -> etypes -> evar_map * Evar.t

Low-level interface to create an evar.

  • parameter src

    User-facing source for the evar

  • parameter filter

    See Evd.Filter, must be the same length as named_context_val

  • parameter name

    A name for the evar

  • parameter principal

    Whether the evar is the principal goal

  • parameter named_context_val

    The context of the evar

  • parameter types

    The type of conclusion of the evar

val add : evar_map -> Evar.t -> 'a evar_info -> evar_map

add sigma ev info adds ev with evar info info in sigma. Precondition: ev must not preexist in sigma.

val find_defined : evar_map -> Evar.t -> defined evar_info option
val find : evar_map -> Evar.t -> any_evar_info

Recover the data associated to an evar.

val find_undefined : evar_map -> Evar.t -> undefined evar_info

Same as find but restricted to undefined evars. For efficiency reasons.

val remove : evar_map -> Evar.t -> evar_map

Remove an evar from an evar map. Use with caution.

val undefine : evar_map -> Evar.t -> etypes -> evar_map

Remove the body of an evar. Only there for backward compat, do not use.

val mem : evar_map -> Evar.t -> bool

Whether an evar is present in an evarmap.

val fold : (Evar.t -> any_evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

Apply a function to all evars and their associated info in an evarmap.

val fold_undefined : (Evar.t -> undefined evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

Same as fold, but restricted to undefined evars. For efficiency reasons.

type map = {
map : r. Evar.t -> 'r evar_info -> 'r evar_info;
}
val raw_map : map -> evar_map -> evar_map

Apply the given function to all evars in the map. Beware: this function expects the argument function to preserve the kind of evar_body, i.e. it must send Evar_empty to Evar_empty and Evar_defined c to some Evar_defined c'.

val raw_map_undefined : (Evar.t -> undefined evar_info -> undefined evar_info) -> evar_map -> evar_map

Same as raw_map, but restricted to undefined evars. For efficiency reasons.

val define : Evar.t -> econstr -> evar_map -> evar_map

Set the body of an evar to the given constr. It is expected that:

  • The evar is already present in the evarmap.
  • The evar is not defined in the evarmap yet.
  • All the evars present in the constr should be present in the evar map.
val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map

Same as define ev body evd, except the body must be an existential variable ev'. This additionally makes ev' inherit the obligation and typeclass flags of ev.

val cmap : (econstr -> econstr) -> evar_map -> evar_map

Map the function on all terms in the evar map.

val is_evar : evar_map -> Evar.t -> bool

Alias for mem.

val is_defined : evar_map -> Evar.t -> bool

Whether an evar is defined in an evarmap.

val is_undefined : evar_map -> Evar.t -> bool

Whether an evar is not defined in an evarmap.

val add_constraints : evar_map -> Univ.Constraints.t -> evar_map

Add universe constraints in an evar map.

val add_quconstraints : evar_map -> Sorts.QUConstraints.t -> evar_map
val undefined_map : evar_map -> undefined evar_info Evar.Map.t

Access the undefined evar mapping directly.

val drop_all_defined : evar_map -> evar_map
val drop_new_defined : original:evar_map -> evar_map -> evar_map

Drop the defined evars in the second evar map which did not exist in the first.

val is_maybe_typeclass_hook : (evar_map -> Constr.constr -> bool) Hook.t
Instantiating partial terms
exception NotInstantiatedEvar
val existential_value : evar_map -> econstr Constr.pexistential -> econstr

existential_value sigma ev raises NotInstantiatedEvar if ev has no body and Not_found if it does not exist in sigma

val existential_value0 : evar_map -> Constr.existential -> Constr.constr
val existential_type_opt : evar_map -> econstr Constr.pexistential -> etypes option
val existential_type : evar_map -> econstr Constr.pexistential -> etypes
val existential_type0 : evar_map -> Constr.existential -> Constr.types
val existential_opt_value : evar_map -> econstr Constr.pexistential -> econstr option

Same as existential_value but returns an option instead of raising an exception.

val existential_opt_value0 : evar_map -> Constr.existential -> Constr.constr option
val evar_handler : evar_map -> CClosure.evar_handler
val expand_existential : evar_map -> econstr Constr.pexistential -> econstr list

Returns the full evar instance with implicit default variables turned into explicit Var nodes.

val expand_existential0 : evar_map -> Constr.constr Constr.pexistential -> Constr.constr list
val instantiate_evar_array : evar_map -> 'a evar_info -> econstr -> econstr SList.t -> econstr
Misc
val restrict : Evar.t -> Filter.t -> ?candidates:econstr list -> ?src:Evar_kinds.t Loc.located -> evar_map -> evar_map * Evar.t

Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates (candidates are filtered according to the filter)

val update_source : evar_map -> Evar.t -> Evar_kinds.t Loc.located -> evar_map

To update the source a posteriori, e.g. when an evar type of another evar has to refer to this other evar, with a mutual dependency

val get_aliased_evars : evar_map -> Evar.t Evar.Map.t

The map of aliased evars

val is_aliased_evar : evar_map -> Evar.t -> Evar.t option

Tell if an evar has been aliased to another evar, and if yes, which

val max_undefined_with_candidates : evar_map -> Evar.t option

If any, the evar with highest id with a non-empty list of candidates.

val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map

Mark the given set of evars as available for resolution.

Precondition: they should indeed refer to undefined typeclass evars.

val get_typeclass_evars : evar_map -> Evar.Set.t

The set of undefined typeclass evars

val is_typeclass_evar : evar_map -> Evar.t -> bool

Is the evar declared resolvable for typeclass resolution

val get_obligation_evars : evar_map -> Evar.Set.t

The set of obligation evars

val set_obligation_evar : evar_map -> Evar.t -> evar_map

Declare an evar as an obligation

val is_obligation_evar : evar_map -> Evar.t -> bool

Is the evar declared as an obligation

val get_impossible_case_evars : evar_map -> Evar.Set.t

Set of undefined evars with ImpossibleCase evar source.

val downcast : Evar.t -> etypes -> evar_map -> evar_map

Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller

val evar_ident : Evar.t -> evar_map -> Names.Id.t option
val rename : Evar.t -> Names.Id.t -> evar_map -> evar_map
val evar_key : Names.Id.t -> evar_map -> Evar.t
val evar_names : evar_map -> Nameops.Fresh.t
val evar_source_of_meta : Constr.metavariable -> evar_map -> Evar_kinds.t Loc.located
val dependent_evar_ident : Evar.t -> evar_map -> Names.Id.t
Side-effects
type side_effect_role =
| Schema of Names.inductive * string
type side_effects = {
seff_private : Safe_typing.private_constants;
seff_roles : side_effect_role Names.Cmap.t;
}
val empty_side_effects : side_effects
val concat_side_effects : side_effects -> side_effects -> side_effects
val emit_side_effects : side_effects -> evar_map -> evar_map

Push a side-effect into the evar map.

val eval_side_effects : evar_map -> side_effects

Return the effects contained in the evar map.

val drop_side_effects : evar_map -> evar_map

This should not be used. For hacking purposes.

Future goals
val declare_future_goal : Evar.t -> evar_map -> evar_map

Adds an existential variable to the list of future goals. For internal uses only.

val declare_principal_goal : Evar.t -> evar_map -> evar_map

Adds an existential variable to the list of future goals and make it principal. Only one existential variable can be made principal, an error is raised otherwise. For internal uses only.

module FutureGoals : sig ... end
val push_future_goals : evar_map -> evar_map
val pop_future_goals : evar_map -> FutureGoals.t * evar_map
val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
val remove_future_goal : evar_map -> Evar.t -> evar_map
val pr_future_goals_stack : evar_map -> Pp.t
val push_shelf : evar_map -> evar_map
val pop_shelf : evar_map -> Evar.t list * evar_map
val filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map
val give_up : Evar.t -> evar_map -> evar_map
val shelve : evar_map -> Evar.t list -> evar_map
val unshelve : evar_map -> Evar.t list -> evar_map
val given_up : evar_map -> Evar.Set.t
val shelf : evar_map -> Evar.t list
val pr_shelf : evar_map -> Pp.t
Sort variables

Evar maps also keep track of the universe constraints defined at a given point. This section defines the relevant manipulation functions.

exception UniversesDiffer
val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map

Add the given universe unification constraints to the evar map.

  • raises UniversesDiffer

    in case a first-order unification fails.

  • raises UniverseInconsistency

    .

Extra data

Evar maps can contain arbitrary data, allowing to use an extensible state. As evar maps are theoretically used in a strict state-passing style, such additional data should be passed along transparently. Some old and bug-prone code tends to drop them nonetheless, so you should keep cautious.

module Store : Store.S

Datatype used to store additional information in evar maps.

val get_extra_data : evar_map -> Store.t
val set_extra_data : Store.t -> evar_map -> evar_map
Enriching with evar maps
type 'a sigma = {
it : 'a;(*

The base object.

*)
sigma : evar_map;(*

The added unification state.

*)
}

The type constructor 'a sigma adds an evar map to an object of type 'a.

val sig_it : 'a sigma -> 'a
val sig_sig : 'a sigma -> evar_map
val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b
The state monad with state an evar map
module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map
Meta machinery

These functions are almost deprecated. They were used before the introduction of the full-fledged evar calculus. In an ideal world, they should be removed. Alas, some parts of the code still use them. Do not use in newly-written code.

module Metaset : Util.Set.S with type elt = Constr.metavariable
module Metamap : Util.Map.ExtS with type key = Constr.metavariable and module Set := Metaset
type 'a freelisted = {
rebus : 'a;
freemetas : Metaset.t;
}
val metavars_of : econstr -> Metaset.t
val mk_freelisted : econstr -> econstr freelisted
val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted

Status of an instance found by unification wrt to the meta it solves:

type instance_constraint =
| IsSuperType
| IsSubType
| Conv
val eq_instance_constraint : instance_constraint -> instance_constraint -> bool

Status of the unification of the type of an instance against the type of the meta it instantiates:

type instance_typing_status =
| CoerceToType
| TypeNotProcessed
| TypeProcessed

Status of an instance together with the status of its type unification

Clausal environments

type conv_pb = Conversion.conv_pb

Unification constraints

type evar_constraint = conv_pb * Environ.env * econstr * econstr
val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map

The following two functions are for internal use only, see Evarutil.add_unification_pb for a safe interface.

val conv_pbs : evar_map -> evar_constraint list
val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> evar_map * evar_constraint list
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option

The following functions return the set of undefined evars contained in the object.

val evars_of_term : evar_map -> econstr -> Evar.Set.t

including evars in instances of evars

val evars_of_named_context : evar_map -> (econstr, etypes, erelevance) Context.Named.pt -> Evar.Set.t
val evars_of_filtered_evar_info : evar_map -> 'a evar_info -> Evar.Set.t
val meta_list : evar_map -> clbinding Metamap.t

Metas

val meta_value : evar_map -> Constr.metavariable -> econstr

meta_fvalue raises Not_found if meta not in map or Anomaly if meta has no value

val meta_opt_fvalue : evar_map -> Constr.metavariable -> (econstr freelisted * instance_status) option
val meta_declare : Constr.metavariable -> etypes -> ?name:Names.Name.t -> evar_map -> evar_map
val clear_metas : evar_map -> evar_map
val meta_merge : clbinding Metamap.t -> evar_map -> evar_map

meta_merge evd1 evd2 returns evd2 extended with the metas of evd1

val map_metas_fvalue : (econstr -> econstr) -> evar_map -> evar_map
val map_metas : (econstr -> econstr) -> evar_map -> evar_map
val retract_coercible_metas : evar_map -> metabinding list * evar_map
FIXME: Nothing to do here

Rigid or flexible universe variables.

UnivRigid variables are user-provided or come from an explicit Type in the source, we do not minimize them or unify them eagerly.

UnivFlexible alg variables are fresh universe variables of polymorphic constants or generated during refinement, sometimes in algebraic position (i.e. not appearing in the term at the moment of creation). They are the candidates for minimization (if alg, to an algebraic universe) and unified eagerly in the first-order unification heurstic.

type rigid = UState.rigid =
| UnivRigid
| UnivFlexible of bool(*

Is substitution by an algebraic ok?

*)
val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
type 'a in_evar_universe_context = 'a * UState.t
val restrict_universe_context : evar_map -> Univ.Level.Set.t -> evar_map
val universe_of_name : evar_map -> Names.Id.t -> Univ.Level.t

Raises Not_found if not a name for a universe in this map.

val quality_of_name : evar_map -> Names.Id.t -> Sorts.QVar.t
val is_relevance_irrelevant : evar_map -> erelevance -> bool

Whether the relevance is irrelevant modulo qstate

val universe_binders : evar_map -> UnivNames.universe_binders
val new_univ_level_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
val new_quality_variable : ?loc:Loc.t -> ?name:Names.Id.t -> evar_map -> evar_map * Sorts.QVar.t
val new_sort_variable : ?loc:Loc.t -> rigid -> evar_map -> evar_map * esorts
val add_global_univ : evar_map -> Univ.Level.t -> evar_map
val universe_rigidity : evar_map -> Univ.Level.t -> rigid
val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map

See UState.make_nonalgebraic_variable.

val is_flexible_level : evar_map -> Univ.Level.t -> bool
val normalize_universe_instance : evar_map -> UVars.Instance.t -> UVars.Instance.t
val set_leq_sort : Environ.env -> evar_map -> esorts -> esorts -> evar_map
val set_eq_sort : Environ.env -> evar_map -> esorts -> esorts -> evar_map
val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
val set_eq_instances : ?flex:bool -> evar_map -> UVars.Instance.t -> UVars.Instance.t -> evar_map
val check_eq : evar_map -> esorts -> esorts -> bool
val check_leq : evar_map -> esorts -> esorts -> bool
val check_constraints : evar_map -> Univ.Constraints.t -> bool
val check_qconstraints : evar_map -> Sorts.QConstraints.t -> bool
val check_quconstraints : evar_map -> Sorts.QUConstraints.t -> bool
val evar_universe_context : evar_map -> UState.t
val universe_context_set : evar_map -> Univ.ContextSet.t
val sort_context_set : evar_map -> UnivGen.sort_context_set
val universe_subst : evar_map -> UnivFlex.t
val universes : evar_map -> UGraph.t
val to_universe_context : evar_map -> UVars.UContext.t

to_universe_context evm extracts the local universes and constraints of evm and orders the universes the same as Univ.ContextSet.to_context.

val univ_entry : poly:bool -> evar_map -> UState.named_universes_entry
val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> UState.named_universes_entry
val merge_universe_context : evar_map -> UState.t -> evar_map
val set_universe_context : evar_map -> UState.t -> evar_map
val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
val merge_sort_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> UnivGen.sort_context_set -> evar_map
val merge_sort_variables : ?loc:Loc.t -> ?sideff:bool -> evar_map -> Sorts.QVar.Set.t -> evar_map
val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
val with_sort_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a UnivGen.in_sort_context_set -> evar_map * 'a
val nf_univ_variables : evar_map -> evar_map
val collapse_sort_variables : evar_map -> evar_map
val fix_undefined_variables : evar_map -> evar_map
val minimize_universes : evar_map -> evar_map

Universe minimization

val update_sigma_univs : UGraph.t -> evar_map -> evar_map

Lift UState.update_sigma_univs

Polymorphic universes

val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * esorts
val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Names.Constant.t -> evar_map * Constr.pconstant
val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Names.inductive -> evar_map * Constr.pinductive
val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Names.constructor -> evar_map * Constr.pconstructor
val fresh_array_instance : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> evar_map * UVars.Instance.t
val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:UVars.Instance.t -> Environ.env -> evar_map -> Names.GlobRef.t -> evar_map * econstr
type open_constr = evar_map * econstr

Partially constructed constrs.

type unsolvability_explanation =
| SeveralInstancesFound of int(*

Failure explanation.

*)
Summary names
val evar_counter_summary_tag : int Summary.Dyn.tag
val create_evar_defs : evar_map -> evar_map

Deprecated functions

Create an evar_map with empty meta map:

module MiniEConstr : sig ... end

Use this module only to bootstrap EConstr