package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
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.

Sourcetype econstr
Sourcetype etypes = econstr
Existential variables and unification states
Evar filters
Sourcemodule Filter : sig ... end
Sourcemodule Abstraction : sig ... end
Sourcemodule Identity : sig ... end
Evar infos
Sourcetype evar_body =
  1. | Evar_empty
  2. | Evar_defined of econstr
Sourcetype evar_info = {
  1. evar_concl : econstr;
    (*

    Type of the evar.

    *)
  2. evar_hyps : Environ.named_context_val;
    (*

    Context of the evar.

    *)
  3. evar_body : evar_body;
    (*

    Optional content of the evar.

    *)
  4. 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 solution

    *)
  5. evar_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 (see second_order_matching_with_args for its use).

    *)
  6. evar_source : Evar_kinds.t Loc.located;
    (*

    Information about the evar.

    *)
  7. evar_candidates : econstr list option;
    (*

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

    *)
  8. evar_identity : Identity.t;
    (*

    Default evar instance, i.e. a list of Var nodes projected from the filtered environment.

    *)
}
Sourceval evar_concl : evar_info -> econstr
Sourceval evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt
Sourceval evar_filtered_hyps : evar_info -> Environ.named_context_val
Sourceval evar_body : evar_info -> evar_body
Sourceval evar_candidates : evar_info -> Constr.constr list option
Sourceval evar_filter : evar_info -> Filter.t
Sourceval evar_filtered_env : Environ.env -> evar_info -> Environ.env
Sourceval evar_identity_subst : evar_info -> econstr list
Sourceval map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
Sourceval map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
Unification state

*

Sourcetype evar_map

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

Sourceval empty : evar_map

The empty evar map.

Sourceval 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).

Sourceval 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).

Sourceval is_empty : evar_map -> bool

Whether an evarmap is empty.

Sourceval has_undefined : evar_map -> bool

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

Sourceval has_given_up : evar_map -> bool

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

Sourceval has_shelved : evar_map -> bool

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

Sourceval new_evar : evar_map -> ?name:Names.Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t

Creates 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.

Recover the data associated to an evar.

Sourceval find_undefined : evar_map -> Evar.t -> evar_info

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

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

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

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

Whether an evar is present in an evarmap.

Sourceval fold : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

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

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

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

Sourceval raw_map : (Evar.t -> evar_info -> evar_info) -> 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'.

Sourceval raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_map

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

Sourceval 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.
Sourceval 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.

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

Map the function on all terms in the evar map.

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

Alias for mem.

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

Whether an evar is defined in an evarmap.

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

Whether an evar is not defined in an evarmap.

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

Add universe constraints in an evar map.

Sourceval undefined_map : evar_map -> evar_info Evar.Map.t

Access the undefined evar mapping directly.

Sourceval drop_all_defined : evar_map -> evar_map
Sourceval is_maybe_typeclass_hook : (evar_map -> Constr.constr -> bool) Hook.t
Instantiating partial terms
Sourceexception NotInstantiatedEvar
Sourceval 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

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

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

Sourceval existential_opt_value0 : evar_map -> Constr.existential -> Constr.constr option
Sourceval evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> 'a list -> (Names.Id.t * 'a) list
Sourceval instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr
Sourceval evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map

spiwack: this function seems to somewhat break the abstraction.

Misc
Sourceval 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)

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

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

The map of aliased evars

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

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

Sourceval 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.

Sourceval get_typeclass_evars : evar_map -> Evar.Set.t

The set of undefined typeclass evars

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

Is the evar declared resolvable for typeclass resolution

Sourceval get_obligation_evars : evar_map -> Evar.Set.t

The set of obligation evars

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

Declare an evar as an obligation

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

Is the evar declared as an obligation

Sourceval 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

Convenience function. Wrapper around find to recover the source of an evar in a given evar map.

Sourceval evar_ident : Evar.t -> evar_map -> Names.Id.t option
Sourceval evar_key : Names.Id.t -> evar_map -> Evar.t
Sourceval dependent_evar_ident : Evar.t -> evar_map -> Names.Id.t
Side-effects
Sourcetype side_effect_role =
  1. | Schema of Names.inductive * string
Sourcetype side_effects = {
  1. seff_private : Safe_typing.private_constants;
  2. seff_roles : side_effect_role Names.Cmap.t;
}
Sourceval empty_side_effects : side_effects
Sourceval concat_side_effects : side_effects -> side_effects -> side_effects
Sourceval emit_side_effects : side_effects -> evar_map -> evar_map

Push a side-effect into the evar map.

Sourceval eval_side_effects : evar_map -> side_effects

Return the effects contained in the evar map.

Sourceval drop_side_effects : evar_map -> evar_map

This should not be used. For hacking purposes.

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

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

Sourceval 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.

Sourcemodule FutureGoals : sig ... end
Sourceval push_future_goals : evar_map -> evar_map
Sourceval pop_future_goals : evar_map -> FutureGoals.t * evar_map
Sourceval fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
Sourceval remove_future_goal : evar_map -> Evar.t -> evar_map
Sourceval pr_future_goals_stack : evar_map -> Pp.t
Sourceval push_shelf : evar_map -> evar_map
Sourceval pop_shelf : evar_map -> Evar.t list * evar_map
Sourceval filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map
Sourceval give_up : Evar.t -> evar_map -> evar_map
Sourceval shelve : evar_map -> Evar.t list -> evar_map
Sourceval unshelve : evar_map -> Evar.t list -> evar_map
Sourceval given_up : evar_map -> Evar.Set.t
Sourceval shelf : evar_map -> Evar.t list
Sourceval 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.

Sourceexception UniversesDiffer
Sourceval add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map

Add the given universe unification constraints to the evar map.

  • 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.

Datatype used to store additional information in evar maps.

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

    The base object.

    *)
  2. sigma : evar_map;
    (*

    The added unification state.

    *)
}

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

Sourceval sig_it : 'a sigma -> 'a
Sourceval sig_sig : 'a sigma -> evar_map
Sourceval on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b
The state monad with state an evar map
Sourcemodule MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
Sourcemodule 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.

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

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)
Sourcetype instance_constraint =
  1. | IsSuperType
  2. | IsSubType
  3. | Conv
Sourceval 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:

  • 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.
Sourcetype instance_typing_status =
  1. | CoerceToType
  2. | TypeNotProcessed
  3. | TypeProcessed

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

Clausal environments

Unification constraints

Sourcetype evar_constraint = conv_pb * Environ.env * econstr * econstr
Sourceval 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.

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

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

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

including evars in instances of evars

Sourceval evar_nodes_of_term : econstr -> Evar.Set.t

same as evars_of_term but also including defined evars. For use in printing dependent evars

Sourceval evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t
Sourceval evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t
Sourceval meta_list : evar_map -> (Constr.metavariable * clbinding) list

Metas

Sourceval meta_defined : evar_map -> Constr.metavariable -> bool

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

Sourceval meta_declare : Constr.metavariable -> etypes -> ?name:Names.Name.t -> evar_map -> evar_map
Sourceval clear_metas : evar_map -> evar_map
Sourceval meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map

meta_merge evd1 evd2 returns evd2 extended with the metas of evd1

Sourceval undefined_metas : evar_map -> Constr.metavariable list
Sourceval map_metas_fvalue : (econstr -> econstr) -> evar_map -> evar_map
Sourceval map_metas : (econstr -> econstr) -> evar_map -> evar_map
Sourceval 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.

Sourcetype rigid = UState.rigid =
  1. | UnivRigid
  2. | UnivFlexible of bool
    (*

    Is substitution by an algebraic ok?

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

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

Sourceval universe_binders : evar_map -> UnivNames.universe_binders
Sourceval new_univ_level_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
Sourceval new_univ_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
Sourceval new_sort_variable : ?loc:Loc.t -> ?name:Names.Id.t -> rigid -> evar_map -> evar_map * Sorts.t
Sourceval add_global_univ : evar_map -> Univ.Level.t -> evar_map
Sourceval universe_rigidity : evar_map -> Univ.Level.t -> rigid
Sourceval make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map

See UState.make_flexible_variable

Sourceval make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map

See UState.make_nonalgebraic_variable.

Sourceval is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option

is_sort_variable evm s returns Some u or None if s is not a local sort variable declared in evm

Sourceval is_flexible_level : evar_map -> Univ.Level.t -> bool
Sourceval normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t
Sourceval normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
Sourceval set_leq_sort : Environ.env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
Sourceval set_eq_sort : Environ.env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
Sourceval set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
Sourceval set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
Sourceval set_eq_instances : ?flex:bool -> evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
Sourceval check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
Sourceval check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
Sourceval check_constraints : evar_map -> Univ.Constraints.t -> bool
Sourceval evar_universe_context : evar_map -> UState.t
Sourceval universe_context_set : evar_map -> Univ.ContextSet.t
Sourceval universes : evar_map -> UGraph.t
Sourceval to_universe_context : evar_map -> Univ.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.

Sourceval univ_entry : poly:bool -> evar_map -> UState.named_universes_entry
Sourceval check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> UState.named_universes_entry
Sourceval merge_universe_context : evar_map -> UState.t -> evar_map
Sourceval set_universe_context : evar_map -> UState.t -> evar_map
Sourceval merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map
Sourceval with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a
Sourceval nf_univ_variables : evar_map -> evar_map
Sourceval fix_undefined_variables : evar_map -> evar_map
Sourceval minimize_universes : evar_map -> evar_map

Universe minimization

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

Lift UState.update_sigma_univs

Polymorphic universes

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

Partially constructed constrs.

Sourcetype unsolvability_explanation =
  1. | SeveralInstancesFound of int
    (*

    Failure explanation.

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

Deprecated functions

Create an evar_map with empty meta map:

Sourcemodule MiniEConstr : sig ... end

Use this module only to bootstrap EConstr