package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Reduction Functions.

exception Elimconst
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 -> Constr.constr -> unit) -> unit
val set_reduction_effect : Names.Constant.t -> effect_name -> unit
val reduction_effect_hook : Environ.env -> Evd.evar_map -> Names.Constant.t -> Constr.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 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

Lazy strategy, weak head reduction

val whd_nored : reduction_function
val whd_beta : reduction_function
val whd_betaiota : reduction_function
val whd_betaiotazeta : reduction_function
val whd_all : reduction_function
val whd_allnolet : reduction_function
val whd_betalet : reduction_function
val whd_nored_stack : stack_reduction_function

Removes cast and put into applicative form

val whd_beta_stack : stack_reduction_function
val whd_betaiota_stack : stack_reduction_function
val whd_betaiotazeta_stack : stack_reduction_function
val whd_all_stack : stack_reduction_function
val whd_allnolet_stack : stack_reduction_function
val whd_betalet_stack : stack_reduction_function
Head normal forms
val whd_delta_stack : stack_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : stack_reduction_function
val whd_zeta : reduction_function

Various reduction functions

val beta_applist : Evd.evar_map -> (EConstr.constr * EConstr.constr list) -> 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_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr

Raises Reduction.NotArity

Raises Reduction.NotArity

Raises Invalid_argument

Raises Invalid_argument

val reducible_mind_case : Evd.evar_map -> EConstr.constr -> bool
val is_arity : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_sort : Environ.env -> Evd.evar_map -> EConstr.types -> bool
val is_transparent : Environ.env -> Names.Constant.t Names.tableKey -> bool

Querying the kernel conversion oracle: opaque/transparent constants

Conversion Functions (uses closures, lazy strategy)
type conversion_test = Univ.Constraints.t -> Univ.Constraints.t
val pb_is_equal : Evd.conv_pb -> bool
val pb_equal : Evd.conv_pb -> Evd.conv_pb
val is_conv_leq : ?reds: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.

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

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 : state_reduction_function
val whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> state_reduction_function
val is_head_evar : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
type meta_instance_subst

Meta-related reduction functions

val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst
exception AnomalyInConversion of exn
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