Module Evarconv

Unification for type inference.
type unify_flags = Evarsolve.unify_flags
val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags

The default subterm transparent state is no unfoldings

val conv_fun : unify_fun -> Evarsolve.unifier
exception UnableToUnify of Evd.evar_map * Pretype_errors.unification_error
Main unification algorithm for type inference.

There are two variants for unification: one that delays constraints outside its capabilities (unify_delay) and another that tries to solve such remaining constraints using heuristics (unify).

These functions allow to pass arbitrary flags to the unifier and can delay constraints. In case the flags are not specified, they default to default_flags_of TransparentState.full currently.

In case of success, the two terms are hence unifiable only if the remaining constraints can be solved or check_problems_are_solved is true.

val unify : ?flags:unify_flags -> ?with_ho:bool -> Environ.env -> Evd.evar_map -> Evd.conv_pb -> EConstr.constr -> EConstr.constr -> Evd.evar_map

This function also calls solve_unif_constraints_with_heuristics to resolve any remaining constraints. In case of success the two terms are unified without condition.

The with_ho option tells if higher-order unification should be tried to resolve the constraints.

  • raises a

    PretypeError if it cannot unify

Unification heuristics.

Try heuristics to solve pending unification problems and to solve evars with candidates.

The with_ho option tells if higher-order unification should be tried to resolve the constraints.

val solve_unif_constraints_with_heuristics : Environ.env -> ?flags:unify_flags -> ?with_ho:bool -> Evd.evar_map -> Evd.evar_map

Check all pending unification problems are solved and raise a PretypeError otherwise

val check_problems_are_solved : Environ.env -> Evd.evar_map -> unit

Check if a canonical structure is applicable

val compare_heads : Environ.env -> Evd.evar_map -> nargs:int -> EConstr.t -> EConstr.t -> Evarsolve.unification_result

Compares two constants/inductives/constructors unifying their universes. It required the number of arguments applied to the c/i/c in order to decided the kind of check it must perform.

Try to solve problems of the form ?xargs = c by second-order matching, using typing to select occurrences

type occurrence_match_test = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool * Evd.evar_map

When given the choice of abstracting an occurrence or leaving it, force abstration.

type occurrence_selection =
| AtOccurrences of Locus.occurrences
| Unspecified of Evd.Abstraction.abstraction
val default_occurrence_selection : occurrence_selection

By default, unspecified, not preferring abstraction. This provides the most general solutions.

type occurrences_selection = occurrence_match_test * occurrence_selection list
val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> int -> occurrences_selection

default_occurrence_selection n Gives the default test and occurrences for n arguments

Declare function to enforce evars resolution by using typing constraints

val set_solve_evars : (Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr) -> unit
val set_evar_conv : unify_fun -> unit

Override default evar_conv_x algorithm.

val evar_conv_x : unify_fun

The default unification algorithm with evars and universes.

val evar_unify : Evarsolve.unifier

Functions to deal with impossible cases