package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
doc/coq-core.pretyping/Evarconv/index.html
Module EvarconvSource
Unification for type inference.
The default subterm transparent state is no unfoldings
type unify_fun =
unify_flags ->
Environ.env ->
Evd.evar_map ->
Evd.conv_pb ->
EConstr.constr ->
EConstr.constr ->
Evarsolve.unification_resultMain 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_delay :
?flags:unify_flags ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.constr ->
Evd.evar_mapval unify_leq_delay :
?flags:unify_flags ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
EConstr.constr ->
Evd.evar_mapval unify :
?flags:unify_flags ->
?with_ho:bool ->
Environ.env ->
Evd.evar_map ->
Evd.conv_pb ->
EConstr.constr ->
EConstr.constr ->
Evd.evar_mapThis 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.
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_mapCheck all pending unification problems are solved and raise a PretypeError otherwise
Check if a canonical structure is applicable
val check_conv_record :
Environ.env ->
Evd.evar_map ->
Reductionops.state ->
Reductionops.state ->
Evd.evar_map
* (EConstr.constr * EConstr.constr)
* EConstr.constr
* EConstr.constr list
* (EConstr.t list * EConstr.t list)
* (EConstr.t list * EConstr.t list)
* (Reductionops.Stack.t * Reductionops.Stack.t)
* EConstr.constr
* (int option * EConstr.constr)val compare_heads :
Environ.env ->
Evd.evar_map ->
nargs:int ->
EConstr.t ->
EConstr.t ->
Evarsolve.unification_resultCompares 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 ->
Environ.env ->
Evd.evar_map ->
int ->
EConstr.constr ->
EConstr.constr ->
bool * Evd.evar_mapWhen given the choice of abstracting an occurrence or leaving it, force abstration.
type occurrence_selection = | AtOccurrences of Locus.occurrences| Unspecified of Evd.Abstraction.abstraction
By default, unspecified, not preferring abstraction. This provides the most general solutions.
val default_occurrence_test :
allowed_evars:Evarsolve.AllowedEvars.t ->
TransparentState.t ->
occurrence_match_testval default_occurrences_selection :
?allowed_evars:Evarsolve.AllowedEvars.t ->
TransparentState.t ->
int ->
occurrences_selectiondefault_occurrence_selection n Gives the default test and occurrences for n arguments
val second_order_matching :
unify_flags ->
Environ.env ->
Evd.evar_map ->
EConstr.existential ->
occurrences_selection ->
EConstr.constr ->
Evd.evar_map * boolDeclare 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) ->
unitFunctions to deal with impossible cases