package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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

Module PretypingSource

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

Sourceval search_guard : ?loc:Loc.t -> Environ.env -> int list list -> Constr.rec_declaration -> int array
Sourcetype typing_constraint =
  1. | IsType
    (*

    Necessarily a type

    *)
  2. | OfType of EConstr.types
    (*

    A term of the expected type

    *)
  3. | WithoutTypeConstraint
    (*

    A term of unknown expected type

    *)
Sourcetype use_typeclasses =
  1. | NoUseTC
  2. | UseTCForConv
  3. | 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 = {
  1. use_coercions : bool;
  2. use_typeclasses : use_typeclasses;
  3. solve_unification_constraints : bool;
  4. fail_evar : bool;
  5. expand_evars : bool;
  6. program_mode : bool;
  7. 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.

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.

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

Sourceval 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

Sourceval check_evars_are_solved : program_mode:bool -> Environ.env -> ?initial:Evd.evar_map -> Evd.evar_map -> unit
Sourceval 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)