package coq-core

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

Reduction Functions.

exception Elimconst
val debug_RAKAM : CDebug.t
module CredNative : Primred.RedNative with type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map and type uinstance = EConstr.EInstance.t
module ReductionBehaviour : sig ... end

Machinery to customize the behavior of the reduction

Support for reduction effects
type effect_name = string
val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
val set_reduction_effect : Names.Constant.t -> effect_name -> unit
val reduction_effect_hook : Environ.env -> Evd.evar_map -> Names.Constant.t -> Constr.constr Lazy.t -> unit
module Stack : sig ... end
type reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
type e_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
type stack_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
Generic Optimized Reduction Function using Closures
val clos_norm_flags : RedFlags.reds -> reduction_function
val clos_whd_flags : RedFlags.reds -> reduction_function
val nf_beta : reduction_function

Same as (strong whd_beta[delta][iota]), but much faster on big terms

val nf_betaiota : reduction_function
val nf_betaiotazeta : reduction_function
val nf_zeta : reduction_function
val nf_all : reduction_function

Lazy strategy, weak head reduction

val whd_nored : reduction_function
val whd_beta : reduction_function
val whd_betaiota : reduction_function
val whd_betaiotazeta : reduction_function
val whd_all : reduction_function
val whd_allnolet : reduction_function
val whd_betalet : reduction_function
val whd_nored_stack : stack_reduction_function

Removes cast and put into applicative form

val whd_beta_stack : stack_reduction_function
val whd_betaiota_stack : stack_reduction_function
val whd_betaiotazeta_stack : stack_reduction_function
val whd_all_stack : stack_reduction_function
val whd_allnolet_stack : stack_reduction_function
val whd_betalet_stack : stack_reduction_function
Head normal forms
val whd_delta_stack : stack_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : stack_reduction_function
val whd_zeta : reduction_function

Various reduction functions

val beta_applist : Evd.evar_map -> (EConstr.constr * EConstr.constr list) -> EConstr.constr
val hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
val hnf_prod_applist : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val hnf_lam_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr

Decompose a type into a sequence of products and a non-product conclusion in head normal form, using head-reduction to expose the products

Decompose a term into a sequence of lambdas and a non-lambda conclusion in head normal form, using head-reduction to expose the lambdas

val whd_decompose_prod_decls : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.rel_context * EConstr.types

Decompose a type into a context and a conclusion not starting with a product or let-in, using head-reduction without zeta to expose the products and let-ins

Like whd_decompose_prod but limited at n products; raises Invalid_argument if not enough products

Like whd_decompose_lambda but limited at n lambdas; raises Invalid_argument if not enough lambdas

Decompose an arity reducing let-ins; Raises Reduction.NotArity

Decompose an arity preserving let-ins; Raises Reduction.NotArity

Raises Reduction.NotArity

val whd_decompose_prod_n_assum : Environ.env -> Evd.evar_map -> int -> EConstr.types -> EConstr.rel_context * EConstr.types

Extract the n first products of a type, preserving let-ins (but not counting them); Raises Invalid_argument if not enough products

val whd_decompose_prod_n_decls : Environ.env -> Evd.evar_map -> int -> EConstr.types -> EConstr.rel_context * EConstr.types

Extract the n first products of a type, counting and preserving let-ins; Raises Invalid_argument if not enough products or let-ins

val whd_decompose_lambda_n_assum : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr

Extract the n first lambdas of a term, preserving let-ins (but not counting them); Raises Invalid_argument if not enough lambdas

val reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool
val is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val is_transparent : Environ.env -> Evaluable.t -> bool

Querying the kernel conversion oracle: opaque/transparent constants

Conversion Functions (uses closures, lazy strategy)
type conversion_test = Univ.Constraints.t -> Univ.Constraints.t
val is_conv_leq : ?reds:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool

check_conv Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state.

  • deprecated Use Reductionops.is_fconv instead
val infer_conv : ?catch_incon:bool -> ?pb:Evd.conv_pb -> ?ts:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option

infer_conv Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state.

  • raises UniverseInconsistency

    iff catch_incon is set to false, otherwise returns false in that case.

val infer_conv_ustate : ?catch_incon:bool -> ?pb:Evd.conv_pb -> ?ts:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> UnivProblem.Set.t option
val vm_infer_conv : ?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option

Conversion with inference of universe constraints

val native_infer_conv : ?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option
type genconv = {
  1. genconv : 'a 'err. Evd.conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t -> Environ.env -> ('a, 'err) Conversion.generic_conversion_function;
}
val infer_conv_gen : genconv -> ?catch_incon:bool -> ?pb:Evd.conv_pb -> ?ts:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option

infer_conv_gen behaves like infer_conv but is parametrized by a conversion function. Used to pretype vm and native casts.

val check_hyps_inclusion : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Constr.named_context -> unit

Typeops.check_hyps_inclusion but handles evars in the environment.

Heuristic for Conversion with Evar
type state = EConstr.constr * Stack.t
type state_reduction_function = Environ.env -> Evd.evar_map -> state -> state
val pr_state : Environ.env -> Evd.evar_map -> state -> Pp.t
val whd_nored_state : state_reduction_function
val whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> state_reduction_function
exception PatternFailure
val is_head_evar : Environ.env -> Evd.evar_map -> EConstr.constr -> bool

Meta-related reduction functions

exception AnomalyInConversion of exn

Deprecated

  • deprecated Use [whd_decompose_prod] instead.
  • deprecated Use [whd_decompose_lambda] instead.
  • deprecated Use [whd_decompose_prod_decls] instead.
  • deprecated This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, then returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)
  • deprecated This function contracts let-ins. Replace either with whd_decompose_lambda_n (if only lambdas are expected, then returning only a list of assumptions) or whd_decompose_lambda_n_assum (if let-ins are expected to be preserved, returning a rel_context)

Re-deprecated in 8.19

  • deprecated Use [whd_decompose_prod] instead.
  • deprecated Use [whd_decompose_lambda] instead.
val hnf_decompose_prod_decls : Environ.env -> Evd.evar_map -> EConstr.types -> EConstr.rel_context * EConstr.types
  • deprecated Use [whd_decompose_prod_decls] instead.
val hnf_decompose_prod_n_decls : Environ.env -> Evd.evar_map -> int -> EConstr.types -> EConstr.rel_context * EConstr.types
  • deprecated This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, then returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)
val hnf_decompose_lambda_n_assum : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr
  • deprecated This function contracts let-ins. Replace either with whd_decompose_lambda_n (if only lambdas are expected, then returning only a list of assumptions) or whd_decompose_lambda_n_assum (if let-ins are expected to be preserved, returning a rel_context)
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