Module Reductionops
Reduction Functions.
module ReductionBehaviour : sig ... endMachinery to customize the behavior of the reduction
Support for reduction effects
val declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unitval set_reduction_effect : Names.Constant.t -> effect_name -> unitval reduction_effect_hook : Environ.env -> Evd.evar_map -> Names.Constant.t -> Constr.constr Stdlib.Lazy.t -> unit
module Cst_stack : sig ... end
module Stack : sig ... endtype state= EConstr.constr * EConstr.constr Stack.ttype contextual_reduction_function= Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constrtype reduction_function= contextual_reduction_functiontype local_reduction_function= Evd.evar_map -> EConstr.constr -> EConstr.constrtype e_reduction_function= Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constrtype contextual_stack_reduction_function= Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr listtype stack_reduction_function= contextual_stack_reduction_functiontype local_stack_reduction_function= Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr listtype contextual_state_reduction_function= Environ.env -> Evd.evar_map -> state -> statetype state_reduction_function= contextual_state_reduction_functiontype local_state_reduction_function= Evd.evar_map -> state -> state
val pr_state : Environ.env -> Evd.evar_map -> state -> Pp.t
Reduction Function Operators
val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) -> CClosure.RedFlags.reds -> reduction_functionval strong : reduction_function -> reduction_functionval local_strong : local_reduction_function -> local_reduction_functionval strong_prodspine : local_reduction_function -> local_reduction_functionval stacklam : (state -> 'a) -> EConstr.constr list -> Evd.evar_map -> EConstr.constr -> EConstr.constr Stack.t -> 'aval whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.tval iterate_whd_gen : bool -> CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
Generic Optimized Reduction Function using Closures
val clos_norm_flags : CClosure.RedFlags.reds -> reduction_functionval clos_whd_flags : CClosure.RedFlags.reds -> reduction_functionval nf_beta : reduction_functionSame as
(strong whd_beta[delta][iota]), but much faster on big terms
val nf_betaiota : reduction_functionval nf_betaiotazeta : reduction_functionval nf_zeta : reduction_functionval nf_all : reduction_functionval nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val whd_evar : Evd.evar_map -> EConstr.constr -> EConstr.constrval whd_nored : local_reduction_functionval whd_beta : local_reduction_functionval whd_betaiota : local_reduction_functionval whd_betaiotazeta : local_reduction_functionval whd_all : contextual_reduction_functionval whd_allnolet : contextual_reduction_functionval whd_betalet : local_reduction_functionval whd_nored_stack : local_stack_reduction_functionRemoves cast and put into applicative form
val whd_beta_stack : local_stack_reduction_functionval whd_betaiota_stack : local_stack_reduction_functionval whd_betaiotazeta_stack : local_stack_reduction_functionval whd_all_stack : contextual_stack_reduction_functionval whd_allnolet_stack : contextual_stack_reduction_functionval whd_betalet_stack : local_stack_reduction_functionval whd_nored_state : local_state_reduction_functionval whd_beta_state : local_state_reduction_functionval whd_betaiota_state : local_state_reduction_functionval whd_betaiotazeta_state : local_state_reduction_functionval whd_all_state : contextual_state_reduction_functionval whd_allnolet_state : contextual_state_reduction_functionval whd_betalet_state : local_state_reduction_function
Head normal forms
val whd_delta_stack : stack_reduction_functionval whd_delta_state : state_reduction_functionval whd_delta : reduction_functionval whd_betadeltazeta_stack : stack_reduction_functionval whd_betadeltazeta_state : state_reduction_functionval whd_betadeltazeta : reduction_functionval whd_zeta_stack : local_stack_reduction_functionval whd_zeta_state : local_state_reduction_functionval whd_zeta : local_reduction_functionval shrink_eta : EConstr.constr -> EConstr.constr
val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr optionval beta_applist : Evd.evar_map -> (EConstr.constr * EConstr.constr list) -> EConstr.constrval hnf_prod_app : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constrval hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constrval hnf_prod_applist : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constrval hnf_lam_app : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constrval hnf_lam_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constrval hnf_lam_applist : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> EConstr.constrval splay_prod : Environ.env -> Evd.evar_map -> EConstr.constr -> (Names.Name.t Context.binder_annot * EConstr.constr) list * EConstr.constrval splay_lam : Environ.env -> Evd.evar_map -> EConstr.constr -> (Names.Name.t Context.binder_annot * EConstr.constr) list * EConstr.constrval splay_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> (Names.Name.t Context.binder_annot * EConstr.constr) list * EConstr.ESorts.tval sort_of_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.ESorts.tval splay_prod_n : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constrval splay_lam_n : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constrval splay_prod_assum : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.rel_context * EConstr.constr
type 'a miota_args={mP : EConstr.constr;the result type
mconstr : EConstr.constr;the constructor
mci : Constr.case_info;special info to re-build pattern
mcargs : 'a list;the constructor's arguments
mlf : 'a array;}the branch code vector
val reducible_mind_case : Evd.evar_map -> EConstr.constr -> boolval reduce_mind_case : Evd.evar_map -> EConstr.constr miota_args -> EConstr.constrval find_conclusion : Environ.env -> Evd.evar_map -> EConstr.constr -> (EConstr.constr, EConstr.constr, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_termval is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> boolval is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> boolval contract_fix : ?env:Environ.env -> Evd.evar_map -> ?reference:Names.Constant.t -> EConstr.fixpoint -> EConstr.constrval fix_recarg : ('a, 'a) Constr.pfixpoint -> 'b Stack.t -> (int * 'b) optionval is_transparent : Environ.env -> Names.Constant.t Names.tableKey -> boolQuerying the kernel conversion oracle: opaque/transparent constants
Conversion Functions (uses closures, lazy strategy)
type conversion_test= Univ.Constraint.t -> Univ.Constraint.t
val pb_is_equal : Evd.conv_pb -> boolval pb_equal : Evd.conv_pb -> Evd.conv_pbval is_conv : ?reds:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> boolval is_conv_leq : ?reds:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> boolval is_fconv : ?reds:TransparentState.t -> Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> boolval check_conv : ?pb:Evd.conv_pb -> ?ts:TransparentState.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> boolcheck_convChecks 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 optioninfer_convAdds 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 set_vm_infer_conv : (?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map option) -> unitConversion with inference of universe constraints
val vm_infer_conv : ?pb:Evd.conv_pb -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> Evd.evar_map optionval 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 optioninfer_conv_genbehaves likeinfer_convbut is parametrized by a conversion function. Used to pretype vm and native casts.
Special-Purpose Reduction Functions
val whd_meta : local_reduction_functionval plain_instance : Evd.evar_map -> EConstr.constr Evd.Metamap.t -> EConstr.constr -> EConstr.constrval instance : Evd.evar_map -> EConstr.constr Evd.Metamap.t -> EConstr.constr -> EConstr.constrval betazetaevar_applist : Evd.evar_map -> int -> EConstr.constr -> EConstr.constr list -> EConstr.constr
Heuristic for Conversion with Evar
val whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> state * Cst_stack.tval meta_instance : Evd.evar_map -> EConstr.constr Evd.freelisted -> EConstr.constrMeta-related reduction functions
val nf_meta : Evd.evar_map -> EConstr.constr -> EConstr.constrval meta_reducible_instance : Evd.evar_map -> EConstr.constr Evd.freelisted -> EConstr.constr