Module Pretyping

This file implements type inference. It maps glob_constr (i.e. untyped terms whose names are located) to constr. In particular, it drives complex pattern-matching problems ("match") into elementary ones, insertion of coercions and resolution of implicit arguments.

val add_bidirectionality_hint : Names.GlobRef.t -> int -> unit

A bidirectionality hint `n` for a global `g` tells the pretyper to use typing information from the context after typing the `n` for arguments of an application of `g`.

val get_bidirectionality_hint : Names.GlobRef.t -> int option
val clear_bidirectionality_hint : Names.GlobRef.t -> unit
val known_glob_level : Evd.evar_map -> Glob_term.glob_sort_name -> Univ.Level.t
val search_guard : ?⁠loc:Loc.t -> Environ.env -> int list list -> Constr.rec_declaration -> int array
type typing_constraint =
| UnknownIfTermOrType

E.g., unknown if manual implicit arguments allowed

| IsType

Necessarily a type

| OfType of EConstr.types

A term of the expected type

| WithoutTypeConstraint

A term of unknown expected type

type use_typeclasses =
| NoUseTC
| UseTCForConv
| UseTC

Typeclasses are used in 2 ways:

  • through the "Typeclass Resolution For Conversion" option, if a conversion problem fails we try again after resolving typeclasses (UseTCForConv and UseTC)
  • after pretyping we resolve typeclasses (UseTC) (in solve_remaining_evars)
type inference_flags = {
use_typeclasses : use_typeclasses;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
polymorphic : bool;
}
val default_inference_flags : bool -> inference_flags
val no_classes_no_fail_inference_flags : inference_flags
val all_no_fail_flags : inference_flags
val all_and_fail_flags : inference_flags
val understand_tcc : ?⁠flags:inference_flags -> Environ.env -> Evd.evar_map -> ?⁠expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr
val understand_tcc_ty : ?⁠flags:inference_flags -> Environ.env -> Evd.evar_map -> ?⁠expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr * EConstr.types

As understand_tcc but also returns the type of the elaborated term. The expand_evars flag is not applied to the type (only to the term).

val understand_ltac : inference_flags -> Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t
val understand : ?⁠flags:inference_flags -> ?⁠expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> EConstr.constr Evd.in_evar_universe_context

Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; the default inference_flags tells to use type classes and heuristics (but no external tactic solver hook), as well as to ensure that conversion problems are all solved and that no unresolved evar remains, expanding evars.

type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> (Evd.evar_map * EConstr.constr) option

hook env sigma ev returns Some (sigma', term) if ev can be instantiated with a solution, None otherwise. Used to extend solve_remaining_evars below.

val solve_remaining_evars : ?⁠hook:inference_hook -> inference_flags -> Environ.env -> ?⁠initial:Evd.evar_map -> Evd.evar_map -> Evd.evar_map

Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags.

val check_evars_are_solved : program_mode:bool -> Environ.env -> ?⁠initial:Evd.evar_map -> Evd.evar_map -> unit
val check_evars : Environ.env -> ?⁠initial:Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit

check_evars env ?initial sigma c fails if some unresolved evar remains in c which isn't in initial (any unresolved evar if initial not provided)