package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.1.tar.gz
sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/coq-core.interp/Constrintern/index.html

Module ConstrinternSource

Translation from front abstract syntax of term to untyped terms (glob_constr)

The translation performs:

  • resolution of names :
  • check all variables are bound
  • make absolute the references to global objets
  • resolution of symbolic notations using scopes
  • insertion of implicit arguments

To interpret implicit arguments and arg scopes of recursive variables while internalizing inductive types and recursive definitions, and also projection while typing records.

the third and fourth arguments associate a list of implicit positions and scopes to identifiers declared in the rel_context of env

Sourcetype var_internalization_type =
  1. | Inductive
  2. | Recursive
  3. | Method
  4. | Variable
Sourcetype var_internalization_data

This collects relevant information for interning local variables:

  • their coqdoc kind (a recursive call in a inductive, fixpoint of class; or a bound variable) e.g. while typing the constructor of JMeq, "JMeq" behaves as a variable of type Inductive
  • their implicit arguments
  • their argument scopes

A map of free variables to their implicit arguments and scopes

Sourceval empty_internalization_env : internalization_env
Sourcetype ltac_sign = {
  1. ltac_vars : Names.Id.Set.t;
    (*

    Variables of Ltac which may be bound to a term

    *)
  2. ltac_bound : Names.Id.Set.t;
    (*

    Other variables of Ltac

    *)
  3. ltac_extra : Genintern.Store.t;
    (*

    Arbitrary payload

    *)
}
Sourceval empty_ltac_sign : ltac_sign
Internalization performs interpretation of global names and notations
Composing internalization with type inference (pretyping)

Main interpretation functions, using type class inference, expecting evars and pending problems to be all resolved

Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars.

Accepting unresolved evars

Sourceval interp_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.constr
Sourceval interp_casted_constr_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * EConstr.constr
Sourceval interp_type_evars : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * EConstr.types

Accepting unresolved evars and giving back the manual implicit arguments

Sourceval interp_constr_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Evd.evar_map * (EConstr.constr * Impargs.manual_implicits)
Sourceval interp_casted_constr_evars_impls : ?program_mode:bool -> Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types -> Evd.evar_map * (EConstr.constr * Impargs.manual_implicits)

Interprets constr patterns

Sourceval intern_constr_pattern : Environ.env -> Evd.evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign -> Constrexpr.constr_pattern_expr -> Pattern.patvar list * Pattern.constr_pattern

Without typing

With typing

Sourceval intern_reference : Libnames.qualid -> Names.GlobRef.t option

Returns None if it's a syndef not bound to a name, raises an error if not existing

Sourceval intern_name_alias : Constrexpr.constr_expr -> (Names.GlobRef.t * Glob_term.glob_level list option) option

Returns None if not a reference or a syndef not bound to a name

Expands abbreviations (syndef); raise an error if not existing

Interpret binders

Interpret contexts: returns extended env and context

Interpret named contexts: returns context

Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file)

Sourceval locate_reference : Libnames.qualid -> Names.GlobRef.t option
Sourceval is_global : Names.Id.t -> bool

Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one.

Idem but to glob_constr (weaker check of binders)

Sourceval parsing_explicit : bool ref

Globalization options

Sourceval for_grammar : ('a -> 'b) -> 'a -> 'b

Globalization leak for Grammar

Sourceval get_asymmetric_patterns : unit -> bool

Placeholder for global option, should be moved to a parameter

Sourceval check_duplicate : ?loc:Loc.t -> (Libnames.qualid * Constrexpr.constr_expr) list -> unit

Check that a list of record field definitions doesn't contain duplicates.

Local universe and constraint declarations.

BEWARE the variance entry needs to be adjusted by ComInductive.variance_of_entry if the instance is extensible.