package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ReductionopsSource

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
Sourceval declare_reduction_effect : effect_name -> (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
Sourceval set_reduction_effect : Names.Constant.t -> effect_name -> unit
Sourceval reduction_effect_hook : Environ.env -> Evd.evar_map -> Names.Constant.t -> Constr.constr Lazy.t -> unit
Sourcemodule Stack : sig ... end
Sourcetype reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
Sourcetype stack_reduction_function = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr list
Generic Optimized Reduction Function using Closures

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

Sourceval nf_betaiota : reduction_function
Sourceval nf_betaiotazeta : reduction_function

Lazy strategy, weak head reduction

Sourceval whd_nored : reduction_function
Sourceval whd_betaiota : reduction_function
Sourceval whd_betaiotazeta : 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_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

Various reduction functions

Raises Reduction.NotArity

Raises Reduction.NotArity

Sourceval hnf_decompose_prod_n_decls : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr

Raises Invalid_argument

Sourceval hnf_decompose_lambda_n_assum : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr

Raises Invalid_argument

Raises Reduction.NotArity

Sourceval reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool
Sourceval is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
Sourceval is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool
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)

check_conv Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state.

  • deprecated Use Reductionops.is_fconv instead
Sourceval 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.

Sourceval 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

Conversion with inference of universe constraints

Sourceval native_infer_conv : ?pb:Evd.conv_pb -> 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.

Sourceval check_hyps_inclusion : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Constr.named_context -> unit

Typeops.check_hyps_inclusion but handles evars in the environment.

Heuristic for Conversion with Evar
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
Sourceval whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> state_reduction_function
Sourceval is_head_evar : Environ.env -> Evd.evar_map -> EConstr.constr -> bool

Meta-related reduction functions

Deprecated

  • deprecated Use [hnf_decompose_prod] instead.
  • deprecated Use [hnf_decompose_lambda] instead.
  • deprecated Use [hnf_decompose_prod_decls] instead.
  • deprecated Use [hnf_decompose_prod_n_decls] instead.
  • deprecated Use [hnf_decompose_lambda_n_assum] instead.
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct