Reductionops (rocq-runtime.Reductionops)

exception Elimconst

type meta_handler = {

meta_value : Constr.metavariable -> EConstr.t option;

}

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 -> EConstr.constr -> unit) ->
  unit

val set_reduction_effect : 
  Libobject.locality ->
  Names.Constant.t ->
  effect_name ->
  unit

val reduction_effect_hook : 
  Environ.env ->
  Evd.evar_map ->
  Names.Constant.t ->
  EConstr.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 : 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

val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr

Lazy strategy, weak head reduction

val whd_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr

val whd_nored : ?metas:meta_handler -> reduction_function

val whd_beta : reduction_function

val whd_betaiota : ?metas:meta_handler -> reduction_function

val whd_betaiotazeta : ?metas:meta_handler -> reduction_function

val whd_all : ?metas:meta_handler -> reduction_function

val whd_allnolet : reduction_function

val whd_betalet : reduction_function

val whd_nored_stack : ?metas:meta_handler -> stack_reduction_function

Removes cast and put into applicative form

val whd_beta_stack : ?metas:meta_handler -> stack_reduction_function

val whd_betaiota_stack : ?metas:meta_handler -> stack_reduction_function

val whd_betaiotazeta_stack : ?metas:meta_handler -> stack_reduction_function

val whd_all_stack : ?metas:meta_handler -> stack_reduction_function

val whd_allnolet_stack : ?metas:meta_handler -> stack_reduction_function

val whd_betalet_stack : ?metas:meta_handler -> stack_reduction_function

Head normal forms

val whd_const : Names.Constant.t -> reduction_function

val whd_delta_stack : ?metas:meta_handler -> stack_reduction_function

val whd_delta : reduction_function

val whd_betadeltazeta_stack : ?metas:meta_handler -> stack_reduction_function

val whd_betadeltazeta : reduction_function

val whd_zeta_stack : ?metas:meta_handler -> stack_reduction_function

val whd_zeta : reduction_function

val shrink_eta : Evd.evar_map -> EConstr.constr -> EConstr.constr

val whd_stack_gen : 
  RedFlags.reds ->
  ?metas:meta_handler ->
  stack_reduction_function

Various reduction functions

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 whd_decompose_prod : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  (Names.Name.t EConstr.binder_annot * EConstr.constr) list * EConstr.types

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

val whd_decompose_lambda : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (Names.Name.t EConstr.binder_annot * EConstr.constr) list * EConstr.constr

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

val whd_decompose_prod_n : 
  Environ.env ->
  Evd.evar_map ->
  int ->
  EConstr.types ->
  (Names.Name.t EConstr.binder_annot * EConstr.constr) list * EConstr.types

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

val whd_decompose_lambda_n : 
  Environ.env ->
  Evd.evar_map ->
  int ->
  EConstr.constr ->
  (Names.Name.t EConstr.binder_annot * EConstr.constr) list * EConstr.constr

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

val splay_arity : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (Names.Name.t EConstr.binder_annot * EConstr.constr) list * EConstr.ESorts.t

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

val dest_arity : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.rel_context * EConstr.ESorts.t

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

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

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 find_conclusion : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (EConstr.constr,
    EConstr.constr,
    EConstr.ESorts.t,
    EConstr.EInstance.t,
    EConstr.ERelevance.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 -> Evaluable.t -> bool

Querying the kernel conversion oracle: opaque/transparent constants

Conversion Functions (uses closures, lazy strategy)

type conversion_test = Univ.UnivConstraints.t -> Univ.UnivConstraints.t

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 is_conv_nounivs : 
  ?reds:TransparentState.t ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

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 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 = {

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.

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 : ?metas:meta_handler -> state_reduction_function

val whd_betaiota_deltazeta_for_iota_state : 
  TransparentState.t ->
  ?metas:meta_handler ->
  state_reduction_function

exception PatternFailure

val apply_rules : 
  (EConstr.rel_context -> state -> state) ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.EInstance.t ->
  Declarations.machine_rewrite_rule list ->
  Stack.t ->
  Evd.econstr * Stack.t

val is_head_evar : Environ.env -> Evd.evar_map -> EConstr.constr -> bool

exception AnomalyInConversion of exn

val inferred_universes : 
  (UGraph.t * Univ.UnivConstraints.t, Conversion.graph_inconsistency)
    Conversion.universe_compare

val eta_expand : 
  Environ.env ->
  Evd.evar_map ->
  Evd.etypes ->
  Evd.etypes ->
  Evd.etypes

val eta_expand_instantiation : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr array ->
  EConstr.rel_context ->
  EConstr.constr array