package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3
doc/coq-core.engine/Evd/index.html
Module EvdSource
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, Sigma 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_info = {evar_concl : econstr;(*Type of the evar.
*)evar_hyps : Environ.named_context_val;(*Context of the evar.
*)evar_body : evar_body;(*Optional content of the evar.
*)evar_filter : 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 solutionevar_abstract_arguments : 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 (seesecond_order_matching_with_argsfor its use).evar_source : Evar_kinds.t Loc.located;(*Information about the evar.
*)evar_candidates : econstr list option;(*List of possible solutions when known that it is a finite list
*)evar_identity : Identity.t;(*Default evar instance, i.e. a list of Var nodes projected from the filtered environment.
*)
}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).
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.
val new_evar :
evar_map ->
?name:Names.Id.t ->
?typeclass_candidate:bool ->
evar_info ->
evar_map * Evar.tCreates a fresh evar mapping to the given information.
add sigma ev info adds ev with evar info info in sigma. Precondition: ev must not preexist in sigma.
Same as find but restricted to undefined evars. For efficiency reasons.
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.
Add universe constraints in an evar map.
Access the undefined evar mapping directly.
Instantiating partial terms
existential_value sigma ev raises NotInstantiatedEvar if ev has no body and Not_found if it does not exist in sigma
Same as existential_value but returns an option instead of raising an exception.
val evar_instance_array :
(Constr.named_declaration -> 'a -> bool) ->
evar_info ->
'a list ->
(Names.Id.t * 'a) listval evars_reset_evd :
?with_conv_pbs:bool ->
?with_univs:bool ->
evar_map ->
evar_map ->
evar_mapspiwack: this function seems to somewhat break the abstraction.
Misc
val restrict :
Evar.t ->
Filter.t ->
?candidates:econstr list ->
?src:Evar_kinds.t Loc.located ->
evar_map ->
evar_map * Evar.tRestrict 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
The map of aliased evars
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
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
Convenience function. Wrapper around find to recover the source of an evar in a given evar map.
Side-effects
type side_effects = {seff_private : Safe_typing.private_constants;seff_roles : side_effect_role Names.Cmap.t;
}Push a side-effect into the evar map.
Return the effects contained in the evar map.
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.
Add the given universe unification constraints to the evar map.
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.
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.
The state monad with state an 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.
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
Pto?X u v = P u vcan be eta-expanded twice)
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.
Status of an instance together with the status of its type unification
Clausal environments
type clbinding = | Cltyp of Names.Name.t * econstr freelisted| Clval of Names.Name.t * econstr freelisted * instance_status * econstr freelisted
Unification constraints
The following two functions are for internal use only, see Evarutil.add_unification_pb for a safe interface.
val extract_changed_conv_pbs :
evar_map ->
(Evar.Set.t -> evar_constraint -> bool) ->
evar_map * evar_constraint listThe following functions return the set of undefined evars contained in the object.
including evars in instances of evars
same as evars_of_term but also including defined evars. For use in printing dependent evars
Metas
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) optionval meta_declare :
Constr.metavariable ->
etypes ->
?name:Names.Name.t ->
evar_map ->
evar_mapval meta_reassign :
Constr.metavariable ->
(econstr * instance_status) ->
evar_map ->
evar_mapmeta_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.
Raises Not_found if not a name for a universe in this map.
val new_univ_level_variable :
?loc:Loc.t ->
?name:Names.Id.t ->
rigid ->
evar_map ->
evar_map * Univ.Level.tval new_univ_variable :
?loc:Loc.t ->
?name:Names.Id.t ->
rigid ->
evar_map ->
evar_map * Univ.Universe.tSee 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 set_eq_instances :
?flex:bool ->
evar_map ->
Univ.Instance.t ->
Univ.Instance.t ->
evar_mapto_universe_context evm extracts the local universes and constraints of evm and orders the universes the same as Univ.ContextSet.to_context.
val check_univ_decl :
poly:bool ->
evar_map ->
UState.universe_decl ->
UState.named_universes_entryPolymorphic universes
val fresh_constant_instance :
?loc:Loc.t ->
?rigid:rigid ->
Environ.env ->
evar_map ->
Names.Constant.t ->
evar_map * Constr.pconstantval fresh_inductive_instance :
?loc:Loc.t ->
?rigid:rigid ->
Environ.env ->
evar_map ->
Names.inductive ->
evar_map * Constr.pinductiveval fresh_constructor_instance :
?loc:Loc.t ->
?rigid:rigid ->
Environ.env ->
evar_map ->
Names.constructor ->
evar_map * Constr.pconstructorval fresh_array_instance :
?loc:Loc.t ->
?rigid:rigid ->
Environ.env ->
evar_map ->
evar_map * Univ.Instance.tval fresh_global :
?loc:Loc.t ->
?rigid:rigid ->
?names:Univ.Instance.t ->
Environ.env ->
evar_map ->
Names.GlobRef.t ->
evar_map * econstrPartially constructed constrs.
Summary names
Create an evar_map with empty meta map:
Use this module only to bootstrap EConstr