package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.pretyping/Reductionops/index.html

Module ReductionopsSource

Reduction Functions.

Sourceexception Elimconst
Sourcetype meta_handler = {
  1. meta_value : Constr.metavariable -> EConstr.t option;
}
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 : Libobject.locality -> 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
Sourceval clos_norm_flags : RedFlags.reds -> reduction_function
Sourceval clos_whd_flags : RedFlags.reds -> 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

Lazy strategy, weak head reduction

Sourceval whd_nored : ?metas:meta_handler -> reduction_function
Sourceval whd_betaiota : ?metas:meta_handler -> reduction_function
Sourceval whd_betaiotazeta : ?metas:meta_handler -> reduction_function
Sourceval whd_all : ?metas:meta_handler -> reduction_function
Sourceval whd_allnolet : reduction_function
Sourceval whd_betalet : reduction_function
Sourceval whd_nored_stack : ?metas:meta_handler -> stack_reduction_function

Removes cast and put into applicative form

Sourceval whd_beta_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_betaiota_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_betaiotazeta_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_all_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_allnolet_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_betalet_stack : ?metas:meta_handler -> stack_reduction_function
Head normal forms
Sourceval whd_delta_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_delta : reduction_function
Sourceval whd_betadeltazeta_stack : ?metas:meta_handler -> stack_reduction_function
Sourceval whd_betadeltazeta : reduction_function
Sourceval whd_zeta_stack : ?metas:meta_handler -> stack_reduction_function

Various reduction functions

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

Decompose a term into a sequence of lambdas and a non-lambda conclusion in head normal form, using head-reduction to expose the lambdas

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

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

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

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

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

Raises Reduction.NotArity

Sourceval 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

Sourceval 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

Sourceval 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

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 -> Evaluable.t -> 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 (8.18) 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
Sourcetype genconv = {
  1. genconv : 'a 'err. Evd.conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t -> Environ.env -> ('a, 'err) Conversion.generic_conversion_function;
}
Sourceval 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.

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 : ?metas:meta_handler -> state_reduction_function
Sourceval whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> ?metas:meta_handler -> state_reduction_function
Sourceexception PatternFailure
Sourceval is_head_evar : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
Sourceexception AnomalyInConversion of exn

Deprecated

  • deprecated (8.18) Use [whd_decompose_prod] instead.
  • deprecated (8.18) Use [whd_decompose_lambda] instead.
  • deprecated (8.18) Use [whd_decompose_prod_decls] instead.
  • deprecated (8.18) This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, then returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)
  • deprecated (8.18) This function contracts let-ins. Replace either with whd_decompose_lambda_n (if only lambdas are expected, then returning only a list of assumptions) or whd_decompose_lambda_n_assum (if let-ins are expected to be preserved, returning a rel_context)

Re-deprecated in 8.19

  • deprecated (8.19) Use [whd_decompose_prod] instead.
  • deprecated (8.19) Use [whd_decompose_lambda] instead.
  • deprecated (8.19) Use [whd_decompose_prod_decls] instead.
Sourceval hnf_decompose_prod_n_decls : Environ.env -> Evd.evar_map -> int -> EConstr.types -> EConstr.rel_context * EConstr.types
  • deprecated (8.19) This function contracts let-ins. Replace either with whd_decompose_prod_n (if only products are expected, then returning only a list of assumptions), whd_decompose_prod_n_assum (if let-ins are expected to be preserved, returning a rel_context), or whd_decompose_prod_n_decls (if let-ins are expected to be preserved and counted, returning also a rel_context)
Sourceval hnf_decompose_lambda_n_assum : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.rel_context * EConstr.constr
  • deprecated (8.19) This function contracts let-ins. Replace either with whd_decompose_lambda_n (if only lambdas are expected, then returning only a list of assumptions) or whd_decompose_lambda_n_assum (if let-ins are expected to be preserved, returning a rel_context)