package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type var_internalization_type =
  1. | Inductive
  2. | Recursive
  3. | Method
  4. | 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_env : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> ?force:Names.Id.Set.t list -> var_internalization_type -> Names.Id.t list -> EConstr.types list -> Impargs.manual_implicits list -> internalization_env
val set_obligation_internalization_data : Names.Id.t -> var_internalization_data -> var_internalization_data
val implicits_of_decl_in_internalization_env : Names.Id.t -> internalization_env -> Impargs.implicit_status list
type 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

    *)
}
val empty_ltac_sign : ltac_sign
Internalization performs interpretation of global names and notations
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
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

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)

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_uninstantiated_constr_pattern : Environ.env -> Evd.evar_map -> ?as_type:bool -> ?strict_check:bool -> ?ltacvars:ltac_sign -> Constrexpr.constr_pattern_expr -> Names.Id.Set.t * [ `uninstantiated ] Pattern.constr_pattern_r
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_instance 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

Interpret contexts: returns extended env and context; share:true means that the interpretation of t in binders of the form (x y z : t) is shared

val interp_context_evars : ?program_mode:bool -> ?unconstrained_sorts:bool -> ?impl_env:internalization_env -> ?share:bool -> 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

val interp_named_context_evars : ?program_mode:bool -> ?unconstrained_sorts:bool -> ?impl_env:internalization_env -> ?share:bool -> ?autoimp_enable:bool -> 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

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.

Local universe and constraint declarations.

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

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

Check that all defined udecls of a list of udecls associated to a mutual definition are the same and interpret this common udecl

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct