Evarutil
This module provides useful higher-level functions for evar manipulation.
val new_meta : unit -> Constr.metavariable
new_meta
is a generator of unique meta variables
val next_evar_name :
Evd.evar_map ->
Namegen.intro_pattern_naming_expr ->
Names.Id.t option
module VarSet : sig ... end
val new_evar :
?src:Evar_kinds.t Loc.located ->
?filter:Evd.Filter.t ->
?relevance:Sorts.relevance ->
?abstract_arguments:Evd.Abstraction.t ->
?candidates:EConstr.constr list ->
?naming:Namegen.intro_pattern_naming_expr ->
?typeclass_candidate:bool ->
?principal:bool ->
?hypnaming:naming_mode ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
Evd.evar_map * EConstr.t
val new_pure_evar :
?src:Evar_kinds.t Loc.located ->
?filter:Evd.Filter.t ->
?relevance:Sorts.relevance ->
?abstract_arguments:Evd.Abstraction.t ->
?candidates:EConstr.constr list ->
?name:Names.Id.t ->
?typeclass_candidate:bool ->
?principal:bool ->
Environ.named_context_val ->
Evd.evar_map ->
EConstr.types ->
Evd.evar_map * Evar.t
Alias of Evd.new_pure_evar
val new_type_evar :
?src:Evar_kinds.t Loc.located ->
?filter:Evd.Filter.t ->
?naming:Namegen.intro_pattern_naming_expr ->
?principal:bool ->
?hypnaming:naming_mode ->
Environ.env ->
Evd.evar_map ->
Evd.rigid ->
Evd.evar_map * (EConstr.constr * EConstr.ESorts.t)
Create a new Type existential variable, as we keep track of them during type-checking and unification.
val new_Type :
?rigid:Evd.rigid ->
Evd.evar_map ->
Evd.evar_map * EConstr.constr
val head_evar : Evd.evar_map -> EConstr.constr -> Evar.t
may raise NoHeadEvar
val whd_head_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
val is_ground_term : Evd.evar_map -> EConstr.constr -> bool
val is_ground_env : Evd.evar_map -> Environ.env -> bool
val advance : Evd.evar_map -> Evar.t -> Evar.t option
advance sigma g
returns Some g'
if g'
is undefined and is the current avatar of g
(for instance g
was changed by clear
into g'
). It returns None
if g
has been (partially) solved.
val reachable_from_evars : Evd.evar_map -> Evar.Set.t -> Evar.Set.t
reachable_from_evars sigma seeds
computes the descendents of evars in seeds
by restriction or evar-evar unifications in sigma
.
The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and nf_evar
.
val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
val undefined_evars_of_named_context :
Evd.evar_map ->
Constr.named_context ->
Evar.Set.t
val create_undefined_evars_cache : unit -> undefined_evars_cache
val filtered_undefined_evars_of_evar_info :
?cache:undefined_evars_cache ->
Evd.evar_map ->
'a Evd.evar_info ->
Evar.Set.t
val occur_evar_upto : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
occur_evar_upto sigma k c
returns true
if k
appears in c
. It looks up recursively in sigma
for the value of existential variables.
val judge_of_new_Type : Evd.evar_map -> Evd.evar_map * EConstr.unsafe_judgment
val create_clos_infos :
Environ.env ->
Evd.evar_map ->
CClosure.RedFlags.reds ->
CClosure.clos_infos
flush_and_check_evars
raise Uninstantiated_evar
if an evar remains uninstantiated; nf_evar
leaves uninstantiated evars as is
val whd_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val j_nf_evar :
Evd.evar_map ->
EConstr.unsafe_judgment ->
EConstr.unsafe_judgment
val jl_nf_evar :
Evd.evar_map ->
EConstr.unsafe_judgment list ->
EConstr.unsafe_judgment list
val jv_nf_evar :
Evd.evar_map ->
EConstr.unsafe_judgment array ->
EConstr.unsafe_judgment array
val tj_nf_evar :
Evd.evar_map ->
EConstr.unsafe_type_judgment ->
EConstr.unsafe_type_judgment
val nf_named_context_evar :
Evd.evar_map ->
Constr.named_context ->
Constr.named_context
val nf_rel_context_evar :
Evd.evar_map ->
EConstr.rel_context ->
EConstr.rel_context
val nf_env_evar : Evd.evar_map -> Environ.env -> Environ.env
val nf_evar_info : Evd.evar_map -> 'a Evd.evar_info -> 'a Evd.evar_info
val nf_evar_map : Evd.evar_map -> Evd.evar_map
val nf_evar_map_undefined : Evd.evar_map -> Evd.evar_map
val nf_relevance : Evd.evar_map -> Sorts.relevance -> Sorts.relevance
Presenting terms without solved evars
val nf_evars_universes : Evd.evar_map -> Constr.constr -> Constr.constr
exception Uninstantiated_evar of Evar.t
Replacing all evars, possibly raising Uninstantiated_evar
val flush_and_check_evars : Evd.evar_map -> EConstr.constr -> Constr.constr
val finalize :
?abort_on_undefined_evars:bool ->
Evd.evar_map ->
( ( EConstr.t -> Constr.t ) -> 'a ) ->
Evd.evar_map * 'a
finalize env sigma f
combines universe minimisation, evar-and-universe normalisation and universe restriction.
It minimizes universes in sigma
, calls f
a normalisation function with respect to the updated sigma
and restricts the local universes of sigma
to those encountered while running f
.
Note that the normalizer passed to f
holds some imperative state in its closure.
val kind_of_term_upto :
Evd.evar_map ->
Constr.constr ->
( Constr.constr, Constr.types, Sorts.t, Univ.Instance.t ) Constr.kind_of_term
Like Constr.kind
except that kind_of_term sigma t
exposes t
as an evar e
only if e
is uninstantiated in sigma
. Otherwise the value of e
in sigma
is (recursively) used.
val eq_constr_univs_test :
evd:Evd.evar_map ->
extended_evd:Evd.evar_map ->
EConstr.constr ->
EConstr.constr ->
bool
eq_constr_univs_test ~evd ~extended_evd t u
tests equality of t
and u
up to existential variable instantiation and equalisable universes. The term t
is interpreted in evd
while u
is interpreted in extended_evd
. The universe constraints in extended_evd
are assumed to be an extension of those in evd
.
val compare_cumulative_instances :
Conversion.conv_pb ->
Univ.Variance.t array ->
Univ.Instance.t ->
Univ.Instance.t ->
Evd.evar_map ->
( Evd.evar_map, UGraph.univ_inconsistency ) Util.union
compare_cumulative_instances cv_pb variance u1 u2 sigma
Returns Inl sigma'
where sigma'
is sigma
augmented with universe constraints such that u1 cv_pb? u2
according to variance
. Additionally flexible universes in irrelevant positions are unified if possible. Returns Inr p
when the former is impossible.
val compare_constructor_instances :
Evd.evar_map ->
Univ.Instance.t ->
Univ.Instance.t ->
Evd.evar_map
We should only compare constructors at convertible types, so this is only an opportunity to unify universes.
type unification_pb =
Evd.conv_pb * Environ.env * EConstr.constr * EConstr.constr
Unification problems
val add_unification_pb :
?tail:bool ->
unification_pb ->
Evd.evar_map ->
Evd.evar_map
add_unification_pb ?tail pb sigma
Add a unification problem pb
to sigma
, if not already present. Put it at the end of the list if tail
is true, by default it is false.
raise OccurHypInSimpleClause if the removal breaks dependencies
type clear_dependency_error =
| OccurHypInSimpleClause of Names.Id.t option |
| EvarTypingBreak of Constr.existential |
| NoCandidatesLeft of Evar.t |
exception ClearDependencyError of Names.Id.t
* clear_dependency_error
* Names.GlobRef.t option
Restrict an undefined evar according to a (sub)filter and candidates. The evar will be defined if there is only one candidate left,
val restrict_evar :
Evd.evar_map ->
Evar.t ->
Evd.Filter.t ->
?src:Evar_kinds.t Loc.located ->
EConstr.constr list option ->
Evd.evar_map * Evar.t
val clear_hyps_in_evi :
Environ.env ->
Evd.evar_map ->
Environ.named_context_val ->
EConstr.types ->
Names.Id.Set.t ->
Evd.evar_map * Environ.named_context_val * EConstr.types
val clear_hyps2_in_evi :
Environ.env ->
Evd.evar_map ->
Environ.named_context_val ->
EConstr.types ->
EConstr.types ->
Names.Id.Set.t ->
Evd.evar_map * Environ.named_context_val * EConstr.types * EConstr.types
val check_and_clear_in_constr :
Environ.env ->
Evd.evar_map ->
clear_dependency_error ->
Names.Id.Set.t ->
EConstr.constr ->
Evd.evar_map
val empty_csubst : csubst
val csubst_subst : Evd.evar_map -> csubst -> EConstr.constr -> EConstr.constr
type ext_named_context = csubst * Names.Id.Set.t * Environ.named_context_val
val default_ext_instance : ext_named_context -> EConstr.constr SList.t
val push_rel_decl_to_named_context :
hypnaming:naming_mode ->
Evd.evar_map ->
EConstr.rel_declaration ->
ext_named_context ->
ext_named_context
val push_rel_context_to_named_context :
hypnaming:naming_mode ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
Environ.named_context_val * EConstr.types * EConstr.constr SList.t * csubst
val generalize_evar_over_rels :
Evd.evar_map ->
EConstr.existential ->
EConstr.types * EConstr.constr list
val subterm_source :
Evar.t ->
?where:Evar_kinds.subevar_kind ->
Evar_kinds.t Loc.located ->
Evar_kinds.t Loc.located
val meta_counter_summary_tag : int Summary.Dyn.tag