package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module EvarutilSource

This module provides useful higher-level functions for evar manipulation.

Metas
Sourceval new_meta : unit -> Constr.metavariable

new_meta is a generator of unique meta variables

Creating a fresh evar given their type and context
Sourcetype naming_mode =
  1. | KeepUserNameAndRenameExistingButSectionNames
  2. | KeepUserNameAndRenameExistingEvenSectionNames
  3. | KeepExistingNames
  4. | FailIfConflict
  5. | ProgramNaming
Sourceval new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?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
Sourceval new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?identity:EConstr.t list -> ?abstract_arguments:Evd.Abstraction.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> Evd.evar_map * Evar.t

Low-level interface to create an evar.

  • parameter src

    User-facing source for the evar

  • parameter filter

    See Evd.Filter, must be the same length as named_context_val

  • parameter identity

    See Evd.Identity, must be the name projection of named_context_val

  • parameter naming

    A naming scheme for the evar

  • parameter principal

    Whether the evar is the principal goal

  • parameter named_context_val

    The context of the evar

  • parameter types

    The type of conclusion of the evar

Sourceval 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 * Sorts.t)

Create a new Type existential variable, as we keep track of them during type-checking and unification.

Polymorphic constants

Sourceval make_pure_subst : Evd.evar_info -> 'a list -> (Names.Id.t * 'a) list
Sourceval safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr option
Evars/Metas switching...
Sourceval non_instantiated : Evd.evar_map -> Evd.evar_info Evar.Map.t
Unification utils
Sourceexception NoHeadEvar

head_evar c returns the head evar of c if any

may raise NoHeadEvar

Sourceval has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_ground_term : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_ground_env : Evd.evar_map -> Environ.env -> bool
Sourceval gather_dependent_evars : Evd.evar_map -> Evar.t list -> Evar.Set.t option Evar.Map.t

gather_dependent_evars evm seeds classifies the evars in evm as dependent_evars and goals (these may overlap). A goal is an evar in seeds or an evar appearing in the (partial) definition of a goal. A dependent evar is an evar appearing in the type (hypotheses and conclusion) of a goal, or in the type or (partial) definition of a dependent evar. The value return is a map associating to each dependent evar None if it has no (partial) definition or Some s if s is the list of evars appearing in its (partial) definition.

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

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

Sourceval undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
Sourceval undefined_evars_of_named_context : Evd.evar_map -> Constr.named_context -> Evar.Set.t
Sourceval undefined_evars_of_evar_info : Evd.evar_map -> Evd.evar_info -> Evar.Set.t
Sourcetype undefined_evars_cache
Sourceval create_undefined_evars_cache : unit -> undefined_evars_cache
Sourceval filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> Evd.evar_map -> Evd.evar_info -> Evar.Set.t
Sourceval 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.

Value/Type constraints

flush_and_check_evars raise Uninstantiated_evar if an evar remains uninstantiated; nf_evar leaves uninstantiated evars as is

Sourceval nf_evar_map : Evd.evar_map -> Evd.evar_map
Sourceval nf_evar_map_undefined : Evd.evar_map -> Evd.evar_map

Presenting terms without solved evars

Sourceval nf_evars_universes : Evd.evar_map -> Constr.constr -> Constr.constr
Sourceexception Uninstantiated_evar of Evar.t

Replacing all evars, possibly raising Uninstantiated_evar

Sourceval flush_and_check_evars : Evd.evar_map -> EConstr.constr -> Constr.constr
Sourceval 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.

Term manipulation up to instantiation

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.

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

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.

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

Unification problems

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

Removing hyps in evars'context

raise OccurHypInSimpleClause if the removal breaks dependencies

Sourcetype clear_dependency_error =
  1. | OccurHypInSimpleClause of Names.Id.t option
  2. | EvarTypingBreak of Constr.existential
  3. | NoCandidatesLeft of Evar.t
Sourceexception 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,

Sourceval 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
Sourcetype csubst
Sourceval empty_csubst : csubst
Sourceval csubst_subst : csubst -> EConstr.constr -> EConstr.constr
Sourceval push_rel_decl_to_named_context : ?hypnaming:naming_mode -> Evd.evar_map -> EConstr.rel_declaration -> ext_named_context -> ext_named_context
Sourceval push_rel_context_to_named_context : ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> EConstr.types -> Environ.named_context_val * EConstr.types * EConstr.constr list * csubst
Sourceval generalize_evar_over_rels : Evd.evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
Sourceval meta_counter_summary_tag : int Summary.Dyn.tag
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct