Module Reductionops

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 Stdlib.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 : CClosure.RedFlags.reds -> reduction_function
val clos_whd_flags : CClosure.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
val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val whd_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
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_const : Names.Constant.t -> reduction_function
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
val shrink_eta : Evd.evar_map -> EConstr.constr -> EConstr.constr
val beta_applist : Evd.evar_map -> (EConstr.constr * EConstr.constr list) -> EConstr.constr
val hnf_prod_app : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 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_app : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr
val hnf_lam_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr
val hnf_lam_applist : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constr
val splay_prod : Environ.env -> Evd.evar_map -> EConstr.constr -> (Names.Name.t Context.binder_annot * EConstr.constr) list * EConstr.constr
val splay_lam : Environ.env -> Evd.evar_map -> EConstr.constr -> (Names.Name.t Context.binder_annot * EConstr.constr) list * EConstr.constr
val splay_prod_assum : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.rel_context * EConstr.constr
val splay_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> (Names.Name.t Context.binder_annot * EConstr.constr) list * EConstr.ESorts.t

Raises Reduction.NotArity

val sort_of_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.ESorts.t

Raises Reduction.NotArity

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

Raises Invalid_argument

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

Raises Invalid_argument

val reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool
val find_conclusion : Environ.env -> Evd.evar_map -> EConstr.constr -> (EConstr.constr, EConstr.constr, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term
val is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val contract_fix : Evd.evar_map -> EConstr.fixpoint -> EConstr.constr
val contract_cofix : Evd.evar_map -> EConstr.cofixpoint -> EConstr.constr
val is_transparent : Environ.env -> Names.Constant.t Names.tableKey -> 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 pb_is_equal : Evd.conv_pb -> bool
val pb_equal : Evd.conv_pb -> Evd.conv_pb
val is_conv : ?⁠reds:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val is_conv_leq : ?⁠reds:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val is_fconv : ?⁠reds:TransparentState.t -> Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val check_conv : ?⁠pb:Evd.conv_pb -> ?⁠ts: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.

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
val infer_conv_gen : (Evd.conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t -> (Constr.constr, Evd.evar_map) Reduction.generic_conversion_function) -> ?⁠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.

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
val is_head_evar : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
type meta_instance_subst
val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst
val meta_instance : Environ.env -> meta_instance_subst -> EConstr.constr Evd.freelisted -> EConstr.constr
val nf_meta : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
exception AnomalyInConversion of exn
val inferred_universes : (UGraph.t * Univ.Constraints.t) Reduction.universe_compare