Module `Constrintern`Source

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 =

| Inductive
| Recursive
| Method
| 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

Sourcetype internalization_env = var_internalization_data Names.Id.Map.t

A map of free variables to their implicit arguments and scopes

Sourceval empty_internalization_env : internalization_env

Source

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

Source

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

Source

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

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

}

Sourceval empty_ltac_sign : ltac_sign

Internalization performs interpretation of global names and notations

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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

Source

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.

Source

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

Source

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

Source

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

Source

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

Source

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)

Source

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)

Source

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

Source

val 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

Source

val interp_constr_pattern : 
  Environ.env ->
  Evd.evar_map ->
  ?expected_type:Pretyping.typing_constraint ->
  Constrexpr.constr_pattern_expr ->
  Pattern.constr_pattern

With typing

Sourceval 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

Source

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

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

Expands abbreviations; raise an error if not existing

Interpret binders

Source

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

Source

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

Source

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

Source

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)

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

Sourceval is_global : Names.Id.t -> bool

Source

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)

Source

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

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

Source

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.

Source

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

Source

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

Local universe and constraint declarations.

Source

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

Source

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.

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Constrintern`Source

Internalization performs interpretation of global names and notations

Composing internalization with type inference (pretyping)

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module ConstrinternSource

Internalization performs interpretation of global names and notations

Composing internalization with type inference (pretyping)

Module `Constrintern`Source