package coq-core

  1. Overview
  2. Docs
On This Page
  1. ...
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

doc/coq-core.kernel/CClosure/index.html

Module CClosureSource

...

Delta implies all consts (both global (= by kernel_name) and local (= by Rel or Var)), all evars, and letin's. Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction

Sourcemodule RedFlags : sig ... end

Sets of reduction kinds.

Sourceval allnolet : RedFlags.reds
Sourceval betadeltazeta : RedFlags.reds
Sourceval betaiota : RedFlags.reds
Sourceval betaiotazeta : RedFlags.reds
Sourceval betazeta : RedFlags.reds
Sourcemodule KeyTable : Hashtbl.S with type key = table_key

fconstr is the type of frozen constr

Sourcetype fconstr

fconstr can be accessed by using the function fterm_of and by matching on type fterm

Sourcetype finvert
Sourcetype evar_repack
Sourcetype 'a next_native_args = (CPrimitives.arg_kind * 'a) list
Sourcetype stack_member =
  1. | Zapp of fconstr array
  2. | ZcaseT of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * fconstr usubs
  3. | Zproj of Names.Projection.Repr.t
  4. | Zfix of fconstr * stack
  5. | Zprimitive of CPrimitives.t * Constr.pconstant * fconstr list * fconstr next_native_args
  6. | Zshift of int
  7. | Zupdate of fconstr
Sourceand stack = stack_member list
Sourceval empty_stack : stack
Sourceval append_stack : fconstr array -> stack -> stack
Sourceval check_native_args : CPrimitives.t -> stack -> bool
Sourceval stack_args_size : stack -> int
Sourceval eta_expand_stack : Names.Name.t Context.binder_annot -> stack -> stack
Sourceval skip_irrelevant_stack : stack -> stack
Sourceval usubs_lift : 'a usubs -> 'a usubs
Sourceval usubs_liftn : int -> 'a usubs -> 'a usubs
Sourceval usubs_cons : 'a -> 'a usubs -> 'a usubs

identity if the first instance is empty

To lazy reduce a constr, create a clos_infos with create_clos_infos, inject the term to reduce with inject; then use a reduction function

Sourceval mk_atom : Constr.constr -> fconstr

mk_atom: prevents a term from being evaluated

Sourceval mk_red : fterm -> fconstr

mk_red: makes a reducible term (used in ring)

Sourceval fterm_of : fconstr -> fterm
Sourceval term_of_fconstr : fconstr -> Constr.constr
Sourcetype clos_infos

Global and local constant cache

Sourcetype clos_tab
Sourceval create_conv_infos : ?univs:UGraph.t -> ?evars:Constr.constr Constr.evar_handler -> RedFlags.reds -> Environ.env -> clos_infos
Sourceval create_clos_infos : ?univs:UGraph.t -> ?evars:Constr.constr Constr.evar_handler -> RedFlags.reds -> Environ.env -> clos_infos
Sourceval oracle_of_infos : clos_infos -> Conv_oracle.oracle
Sourceval create_tab : unit -> clos_tab
Sourceval info_env : clos_infos -> Environ.env
Sourceval info_flags : clos_infos -> RedFlags.reds
Sourceval info_univs : clos_infos -> UGraph.t
Sourceval unfold_projection : clos_infos -> Names.Projection.t -> stack_member option
Sourceval push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos
Sourceval push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos
Sourceval set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos
Sourceval info_relevances : clos_infos -> Sorts.relevance Range.t
Sourceval infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos

Reduction function

norm_val is for strong normalization

Same as norm_val but for terms

whd_val is for weak head normalization

Sourceval whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack

whd_stack performs weak head normalization in a given stack. It stops whenever a reduction is blocked.

Sourceval eta_expand_ind_stack : Environ.env -> Names.inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack

eta_expand_ind_stack env ind c s t computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. Assumes t is a rigid term, and not a constructor. ind is the inductive of the constructor term c

  • raises Not_found

    if the inductive is not a primitive record, or if the constructor is partially applied.

Conversion auxiliary functions to do step by step normalisation

unfold_reference unfolds references in a fconstr. Produces a FIrrelevant when the reference is irrelevant.

Sourceval unfold_ref_with_args : clos_infos -> clos_tab -> table_key -> stack -> (fconstr * stack) option

Like unfold_reference, but handles primitives: if there are not enough arguments, return None. Otherwise return Some with ZPrimitive added to the stack. Produces a FIrrelevant when the reference is irrelevant and the infos was created with create_conv_infos.

Sourceval set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit

Hook for Reduction

Sourceval lift_fconstr : int -> fconstr -> fconstr
Sourceval lift_fconstr_vect : int -> fconstr array -> fconstr array
Sourceval mk_clos_vect : fconstr usubs -> Constr.constr array -> fconstr array
Sourceval zip : fconstr -> stack -> fconstr
Sourceval term_of_process : fconstr -> stack -> Constr.constr

End of cbn debug section i