Module `Reductionops`Source

Reduction Functions.

Sourceexception Elimconst

Sourceval 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

Sourcemodule ReductionBehaviour : sig ... end

Machinery to customize the behavior of the reduction

Support for reduction effects

Sourcetype effect_name = string

Source

val declare_reduction_effect : 
  effect_name ->
  (Environ.env -> Evd.evar_map -> Constr.constr -> unit) ->
  unit

Sourceval set_reduction_effect : Names.Constant.t -> effect_name -> unit

Source

val reduction_effect_hook : 
  Environ.env ->
  Evd.evar_map ->
  Names.Constant.t ->
  Constr.constr Lazy.t ->
  unit

Sourcemodule Stack : sig ... end

Source

type reduction_function =
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr

Source

type e_reduction_function =
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Evd.evar_map * EConstr.constr

Source

type stack_reduction_function =
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr * EConstr.constr list

Generic Optimized Reduction Function using Closures

Sourceval clos_norm_flags : CClosure.RedFlags.reds -> reduction_function

Sourceval clos_whd_flags : CClosure.RedFlags.reds -> reduction_function

Sourceval nf_beta : reduction_function

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

Sourceval nf_betaiota : reduction_function

Sourceval nf_betaiotazeta : reduction_function

Sourceval nf_zeta : reduction_function

Sourceval nf_all : reduction_function

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

Lazy strategy, weak head reduction

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

Sourceval whd_nored : reduction_function

Sourceval whd_beta : reduction_function

Sourceval whd_betaiota : reduction_function

Sourceval whd_betaiotazeta : reduction_function

Sourceval whd_all : reduction_function

Sourceval whd_allnolet : reduction_function

Sourceval whd_betalet : reduction_function

Sourceval whd_nored_stack : stack_reduction_function

Removes cast and put into applicative form

Sourceval whd_beta_stack : stack_reduction_function

Sourceval whd_betaiota_stack : stack_reduction_function

Sourceval whd_betaiotazeta_stack : stack_reduction_function

Sourceval whd_all_stack : stack_reduction_function

Sourceval whd_allnolet_stack : stack_reduction_function

Sourceval whd_betalet_stack : stack_reduction_function

Head normal forms

Sourceval whd_const : Names.Constant.t -> reduction_function

Sourceval whd_delta_stack : stack_reduction_function

Sourceval whd_delta : reduction_function

Sourceval whd_betadeltazeta_stack : stack_reduction_function

Sourceval whd_betadeltazeta : reduction_function

Sourceval whd_zeta_stack : stack_reduction_function

Sourceval whd_zeta : reduction_function

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

Various reduction functions

Source

val beta_applist : 
  Evd.evar_map ->
  (EConstr.constr * EConstr.constr list) ->
  EConstr.constr

Source

val hnf_prod_app : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  EConstr.constr

Source

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

Source

val hnf_prod_applist : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr list ->
  EConstr.constr

Source

val hnf_lam_app : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  EConstr.constr

Source

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

Source

val hnf_lam_applist : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr list ->
  EConstr.constr

Source

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

Source

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

Source

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

Source

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

Source

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

Raises Reduction.NotArity

Source

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

Raises Invalid_argument

Source

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

Raises Invalid_argument

Sourceval reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool

Source

val find_conclusion : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  (EConstr.constr, EConstr.constr, EConstr.ESorts.t, EConstr.EInstance.t)
    Constr.kind_of_term

Sourceval is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool

Sourceval is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool

Sourceval contract_fix : Evd.evar_map -> EConstr.fixpoint -> EConstr.constr

Sourceval contract_cofix : Evd.evar_map -> EConstr.cofixpoint -> EConstr.constr

Sourceval is_transparent : Environ.env -> Names.Constant.t Names.tableKey -> bool

Querying the kernel conversion oracle: opaque/transparent constants

Conversion Functions (uses closures, lazy strategy)

Sourcetype conversion_test = Univ.Constraints.t -> Univ.Constraints.t

Sourceval pb_is_equal : Evd.conv_pb -> bool

Sourceval pb_equal : Evd.conv_pb -> Evd.conv_pb

Source

val is_conv : 
  ?reds:TransparentState.t ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Source

val is_conv_leq : 
  ?reds:TransparentState.t ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Source

val is_fconv : 
  ?reds:TransparentState.t ->
  Evd.conv_pb ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

Source

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.

Source

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.

Source

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

Source

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

Source

val native_infer_conv : 
  ?pb:Evd.conv_pb ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  Evd.evar_map option

Source

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

Sourcetype state = EConstr.constr * Stack.t

Sourcetype state_reduction_function = Environ.env -> Evd.evar_map -> state -> state

Sourceval pr_state : Environ.env -> Evd.evar_map -> state -> Pp.t

Sourceval whd_nored_state : state_reduction_function

Source

val whd_betaiota_deltazeta_for_iota_state : 
  TransparentState.t ->
  state_reduction_function

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

Sourcetype meta_instance_subst

Meta-related reduction functions

Sourceval create_meta_instance_subst : Evd.evar_map -> meta_instance_subst

Source

val meta_instance : 
  Environ.env ->
  meta_instance_subst ->
  EConstr.constr Evd.freelisted ->
  EConstr.constr

Sourceval nf_meta : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr

Sourceexception AnomalyInConversion of exn

Source

val inferred_universes : 
  (UGraph.t * Univ.Constraints.t) Reduction.universe_compare

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Reductionops/index.html

Module `Reductionops`Source

Support for reduction effects

Generic Optimized Reduction Function using Closures

Head normal forms

Conversion Functions (uses closures, lazy strategy)

Heuristic for Conversion with Evar

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.pretyping/Reductionops/index.html

Module ReductionopsSource

Support for reduction effects

Generic Optimized Reduction Function using Closures

Head normal forms

Conversion Functions (uses closures, lazy strategy)

Heuristic for Conversion with Evar

Module `Reductionops`Source