Constrintern (coq-core.Constrintern)

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

type var_internalization_type =

| Inductive

| Recursive

| Method

| Variable

type 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

type internalization_env = var_internalization_data Names.Id.Map.t

A map of free variables to their implicit arguments and scopes

val empty_internalization_env : internalization_env

val compute_internalization_data : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.t ->
  var_internalization_type ->
  EConstr.types ->
  Impargs.manual_implicits ->
  var_internalization_data

val compute_internalization_env : 
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  var_internalization_type ->
  Names.Id.t list ->
  EConstr.types list ->
  Impargs.manual_implicits list ->
  internalization_env

val extend_internalization_data : 
  var_internalization_data ->
  Impargs.implicit_status ->
  Notation_term.scope_name list ->
  var_internalization_data

type ltac_sign = {

`ltac_vars : Names.Id.Set.t;`	(* Variables of Ltac which may be bound to a term *)
`ltac_bound : Names.Id.Set.t;`	(* Other variables of Ltac *)
`ltac_extra : Genintern.Store.t;`	(* Arbitrary payload *)

}

val empty_ltac_sign : ltac_sign

Internalization performs interpretation of global names and notations

val intern_constr : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Glob_term.glob_constr

val intern_type : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Glob_term.glob_constr

val intern_gen : 
  Pretyping.typing_constraint ->
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  ?strict_check:bool ->
  ?pattern_mode:bool ->
  ?ltacvars:ltac_sign ->
  Constrexpr.constr_expr ->
  Glob_term.glob_constr

val intern_unknown_if_term_or_type : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Glob_term.glob_constr

val intern_pattern : 
  Environ.env ->
  Constrexpr.cases_pattern_expr ->
  Names.lident list
  * (Names.Id.t Names.Id.Map.t * Glob_term.cases_pattern) list

val intern_context : 
  Environ.env ->
  bound_univs:UnivNames.universe_binders ->
  internalization_env ->
  Constrexpr.local_binder_expr list ->
  internalization_env * Glob_term.glob_decl list

Composing internalization with type inference (pretyping)

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

val interp_constr : 
  ?flags:Pretyping.inference_flags ->
  ?expected_type:Pretyping.typing_constraint ->
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  Constrexpr.constr_expr ->
  EConstr.constr Evd.in_evar_universe_context

val interp_casted_constr : 
  ?flags:Pretyping.inference_flags ->
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  Constrexpr.constr_expr ->
  EConstr.types ->
  EConstr.constr Evd.in_evar_universe_context

val interp_type : 
  ?flags:Pretyping.inference_flags ->
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  Constrexpr.constr_expr ->
  EConstr.types Evd.in_evar_universe_context

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

val interp_open_constr : 
  ?expected_type:Pretyping.typing_constraint ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.constr_expr ->
  Evd.evar_map * EConstr.constr

Accepting unresolved evars

val interp_constr_evars : 
  ?program_mode:bool ->
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  Constrexpr.constr_expr ->
  Evd.evar_map * EConstr.constr

val 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

val 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

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

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

val interp_type_evars_impls : 
  ?flags:Pretyping.inference_flags ->
  Environ.env ->
  Evd.evar_map ->
  ?impls:internalization_env ->
  Constrexpr.constr_expr ->
  Evd.evar_map * (EConstr.types * Impargs.manual_implicits)

Interprets constr patterns

val intern_constr_pattern : 
  Environ.env ->
  Evd.evar_map ->
  ?as_type:bool ->
  ?strict_check:bool ->
  ?ltacvars:ltac_sign ->
  Constrexpr.constr_pattern_expr ->
  Names.Id.Set.t * Pattern.constr_pattern

Without typing

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

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

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

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

val interp_reference : ltac_sign -> Libnames.qualid -> Glob_term.glob_constr

Expands abbreviations; raise an error if not existing

Interpret binders

val interp_binder : 
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  Constrexpr.constr_expr ->
  EConstr.types Evd.in_evar_universe_context

val interp_binder_evars : 
  Environ.env ->
  Evd.evar_map ->
  Names.Name.t ->
  Constrexpr.constr_expr ->
  Evd.evar_map * EConstr.types

Interpret contexts: returns extended env and context

val interp_context_evars : 
  ?program_mode:bool ->
  ?impl_env:internalization_env ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.local_binder_expr list ->
  Evd.evar_map
  * (internalization_env
     * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits))

Interpret named contexts: returns context

val interp_named_context_evars : 
  ?program_mode:bool ->
  ?impl_env:internalization_env ->
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.local_binder_expr list ->
  Evd.evar_map
  * (internalization_env
     * ((Environ.env * EConstr.named_context) * Impargs.manual_implicits))

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

val locate_reference : Libnames.qualid -> Names.GlobRef.t option

val is_global : Names.Id.t -> bool

val interp_notation_constr : 
  Environ.env ->
  ?impls:internalization_env ->
  Notation_term.notation_interp_env ->
  Constrexpr.constr_expr ->
  (bool * Notation_term.subscopes) Names.Id.Map.t
  * Notation_term.notation_constr
  * Notation_term.reversibility_status

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)

val intern_core : 
  Pretyping.typing_constraint ->
  Environ.env ->
  Evd.evar_map ->
  ?strict_check:bool ->
  ?pattern_mode:bool ->
  ?ltacvars:ltac_sign ->
  Genintern.intern_variable_status ->
  Constrexpr.constr_expr ->
  Glob_term.glob_constr

val parsing_explicit : bool Stdlib.ref

Globalization options

val get_asymmetric_patterns : unit -> bool

Placeholder for global option, should be moved to a parameter

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

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

val interp_univ_constraint : 
  Evd.evar_map ->
  (Constrexpr.sort_name_expr * Univ.constraint_type * Constrexpr.sort_name_expr) ->
  Univ.univ_constraint

val interp_univ_decl : 
  Environ.env ->
  Constrexpr.universe_decl_expr ->
  Evd.evar_map * UState.universe_decl

Local universe and constraint declarations.

val interp_univ_decl_opt : 
  Environ.env ->
  Constrexpr.universe_decl_expr option ->
  Evd.evar_map * UState.universe_decl

val interp_cumul_univ_decl_opt : 
  Environ.env ->
  Constrexpr.cumul_univ_decl_expr option ->
  Evd.evar_map * UState.universe_decl * Entries.variance_entry

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