package coq

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

Module EvarconvSource

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

The default subterm transparent state is no unfoldings

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.

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.

  • raises a

    PretypeError if it fails to resolve some problem

Sourceval 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

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

Check if a canonical structure is applicable

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

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

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

Sourcetype occurrence_selection =
  1. | AtOccurrences of Locus.occurrences
  2. | Unspecified of Evd.Abstraction.abstraction
Sourceval default_occurrence_selection : occurrence_selection

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

Sourcetype occurrences_selection = occurrence_match_test * occurrence_selection list
Sourceval default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
Sourceval 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

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

Override default evar_conv_x algorithm.

Sourceval evar_conv_x : unify_fun

The default unification algorithm with evars and universes.

Sourceval evar_unify : Evarsolve.unifier

Functions to deal with impossible cases

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