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

An auxiliary function for searching for fixpoint guard indexes

val search_guard : ?loc:Loc.t -> Environ.env -> int list list -> Constr.rec_declaration -> int array
type typing_constraint =
| 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_coercions : bool;
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

Generic calls to the interpreter from glob_constr to open_constr; by default, inference_flags tell to use type classes and heuristics (but no external tactic solver hooks), as well as to ensure that conversion problems are all solved and expand evars, but unresolved evars can remain. The difference is in whether the evar_map is modified explicitly or by side-effect.

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

More general entry point with evars from ltac

Generic call to the interpreter from glob_constr to constr

In understand_ltac flags sigma env ltac_env constraint c,

flags: tell how to manage evars sigma: initial set of existential variables (typically current goals) ltac_env: partial substitution of variables (used for the tactic language) constraint: tell if interpreted as a possibly constrained term or a type

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.

Checking evars and pending conversion problems are all solved, reporting an appropriate error message

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)