Module `Pretyping`Source

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.

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

Sourceval get_bidirectionality_hint : Names.GlobRef.t -> int option

Sourceval clear_bidirectionality_hint : Names.GlobRef.t -> unit

An auxiliary function for searching for fixpoint guard indexes

Source

val search_guard : 
  ?loc:Loc.t ->
  Environ.env ->
  int list list ->
  Constr.rec_declaration ->
  int array

Sourcetype 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
*)

Sourcetype 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)
*)

Sourcetype inference_flags = {

use_coercions : bool;
use_typeclasses : use_typeclasses;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
polymorphic : bool;

}

Sourceval default_inference_flags : bool -> inference_flags

Sourceval no_classes_no_fail_inference_flags : inference_flags

Sourceval all_no_fail_flags : inference_flags

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

Source

val understand_tcc : 
  ?flags:inference_flags ->
  Environ.env ->
  Evd.evar_map ->
  ?expected_type:typing_constraint ->
  Glob_term.glob_constr ->
  Evd.evar_map * EConstr.constr

Source

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

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

Source

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

Source

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.

Source

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.

Source

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

Source

val check_evars_are_solved : 
  program_mode:bool ->
  Environ.env ->
  ?initial:Evd.evar_map ->
  Evd.evar_map ->
  unit

Source

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)

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Pretyping/index.html

Module `Pretyping`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Pretyping/index.html

Module PretypingSource

Module `Pretyping`Source