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.
Existential variables and unification states
Evar filters
Evar infos
type evar_body = | Evar_empty| Evar_defined of econstr
Projections from evar infos
List of possible solutions when known that it is a finite list
Boolean mask over evar_hyps. Should have the same length. When filtered out, the corresponding variable is not allowed to occur in the solution
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).
Relevance of the conclusion of the evar.
Derived projections
Unification state
*
Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction.
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).
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).
Whether an evarmap is empty.
has_undefined sigma is true if and only if there are uninstantiated evars in sigma.
has_given_up sigma is true if and only if there are given up evars in sigma.
has_shelved sigma is true if and only if there are shelved evars in sigma.
Low-level interface to create an evar.
add sigma ev info adds ev with evar info info in sigma. Precondition: ev must not preexist in sigma.
Recover the data associated to an evar.
Same as find but restricted to undefined evars. For efficiency reasons.
Remove an evar from an evar map. Use with caution.
Remove the body of an evar. Only there for backward compat, do not use.
Whether an evar is present in an evarmap.
Apply a function to all evars and their associated info in an evarmap.
Same as fold, but restricted to undefined evars. For efficiency reasons.
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'.
Same as raw_map, but restricted to undefined evars. For efficiency reasons.
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.
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.
Map the function on all terms in the evar map.
Whether an evar is defined in an evarmap.
Whether an evar is not defined in an evarmap.
Add universe constraints in an evar map.
Access the undefined evar mapping directly.
Instantiating partial terms
exception NotInstantiatedEvarexistential_value sigma ev raises NotInstantiatedEvar if ev has no body and Not_found if it does not exist in sigma
Returns the full evar instance with implicit default variables turned into explicit Var nodes.
Misc
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)
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
Tell if an evar has been aliased to another evar, and if yes, which
Mark the given set of evars as available for resolution.
Precondition: they should indeed refer to undefined typeclass evars.
The set of undefined typeclass evars
Is the evar declared resolvable for typeclass resolution
The set of obligation evars
Declare an evar as an obligation
Is the evar declared as an obligation
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
Side-effects
Push a side-effect into the evar map.
Return the effects contained in the evar map.
This should not be used. For hacking purposes.
Future goals
Adds an existential variable to the list of future goals. For internal uses only.
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.
Sort variables
Evar maps also keep track of the universe constraints defined at a given point. This section defines the relevant manipulation functions.
exception UniversesDifferAdd the given universe unification constraints to the evar map.
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.
Datatype used to store additional information in evar maps.
Enriching with evar maps
type 'a sigma = {it : 'a;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 -> 'aThe state monad with state an evar map
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.
type 'a freelisted = {rebus : 'a;freemetas : Metaset.t;
}Status of an instance found by unification wrt to the meta it solves:
- a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
- a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
- a term that can be eta-expanded n times while still being a solution (e.g. the solution
P to ?X u v = P u v can be eta-expanded twice)
type instance_constraint = | IsSuperType| IsSubType| Conv
Status of the unification of the type of an instance against the type of the meta it instantiates:
- CoerceToType means that the unification of types has not been done and that a coercion can still be inserted: the meta should not be substituted freely (this happens for instance given via the "with" binding clause).
- TypeProcessed means that the information obtainable from the unification of types has been extracted.
- TypeNotProcessed means that the unification of types has not been done but it is known that no coercion may be inserted: the meta can be substituted freely.
type instance_typing_status = | CoerceToType| TypeNotProcessed| TypeProcessed
Status of an instance together with the status of its type unification
Clausal environments
The following two functions are for internal use only, see Evarutil.add_unification_pb for a safe interface.
The following functions return the set of undefined evars contained in the object.
including evars in instances of evars
meta_fvalue raises Not_found if meta not in map or Anomaly if meta has no value
meta_merge evd1 evd2 returns evd2 extended with the metas of evd1
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 boolIs substitution by an algebraic ok?
val univ_flexible : rigidval univ_flexible_alg : rigidtype 'a in_evar_universe_context = 'a * UState.tRaises Not_found if not a name for a universe in this map.
See UState.make_flexible_variable
See UState.make_nonalgebraic_variable.
is_sort_variable evm s returns Some u or None if s is not a local sort variable declared in evm
val to_universe_context : evar_map -> Univ.UContext.tto_universe_context evm extracts the local universes and constraints of evm and orders the universes the same as Univ.ContextSet.to_context.
Lift UState.update_sigma_univs
Polymorphic universes
Partially constructed constrs.
type unsolvability_explanation = | SeveralInstancesFound of int
Summary names
Create an evar_map with empty meta map:
Use this module only to bootstrap EConstr