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

Source

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

Raises Reduction.NotArity

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-project
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-core

Install

dune-project 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

dune-project
Dependency

Module `Reductionops`Source