Module CClosure

val stats : bool Stdlib.ref

Flags for profiling reductions.

val with_stats : 'a Stdlib.Lazy.t -> 'a
...
module RedFlags : sig ... end

Sets of reduction kinds.

val all : RedFlags.reds
val allnolet : RedFlags.reds
val beta : RedFlags.reds
val betadeltazeta : RedFlags.reds
val betaiota : RedFlags.reds
val betaiotazeta : RedFlags.reds
val betazeta : RedFlags.reds
val delta : RedFlags.reds
val zeta : RedFlags.reds
val nored : RedFlags.reds
type table_key = Names.Constant.t Univ.puniverses Names.tableKey
module KeyTable : Stdlib.Hashtbl.S with type KeyTable.key = table_key
type fconstr

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

type finvert
type fterm =
| FRel of int
| FAtom of Constr.constr

Metas and Sorts

| FFlex of table_key
| FInd of Names.inductive Univ.puniverses
| FConstruct of Names.constructor Univ.puniverses
| FApp of fconstr * fconstr array
| FProj of Names.Projection.t * fconstr
| FFix of Constr.fixpoint * fconstr Esubst.subs
| FCoFix of Constr.cofixpoint * fconstr Esubst.subs
| FCaseT of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * fconstr * Constr.case_branch array * fconstr Esubst.subs
| FCaseInvert of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * finvert * fconstr * Constr.case_branch array * fconstr Esubst.subs
| FLambda of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * fconstr Esubst.subs
| FProd of Names.Name.t Context.binder_annot * fconstr * Constr.constr * fconstr Esubst.subs
| FLetIn of Names.Name.t Context.binder_annot * fconstr * fconstr * Constr.constr * fconstr Esubst.subs
| FEvar of Constr.existential * fconstr Esubst.subs
| FInt of Uint63.t
| FFloat of Float64.t
| FArray of Univ.Instance.t * fconstr Parray.t * fconstr
| FLIFT of int * fconstr
| FCLOS of Constr.constr * fconstr Esubst.subs
| FIrrelevant
| FLOCKED
type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
type stack_member =
| Zapp of fconstr array
| ZcaseT of Constr.case_info * Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * fconstr Esubst.subs
| Zproj of Names.Projection.Repr.t
| Zfix of fconstr * stack
| Zprimitive of CPrimitives.t * Constr.pconstant * fconstr list * fconstr next_native_args
| Zshift of int
| Zupdate of fconstr
and stack = stack_member list
val empty_stack : stack
val append_stack : fconstr array -> stack -> stack
val check_native_args : CPrimitives.t -> stack -> bool
val get_native_args1 : CPrimitives.t -> Constr.pconstant -> stack -> fconstr list * fconstr * fconstr next_native_args * stack
val stack_args_size : stack -> int
val eta_expand_stack : Names.Name.t Context.binder_annot -> stack -> stack
val skip_irrelevant_stack : stack -> stack
val inductive_subst : Declarations.mutual_inductive_body -> Univ.Instance.t -> fconstr array -> fconstr Esubst.subs
val inject : Constr.constr -> fconstr
val mk_atom : Constr.constr -> fconstr

mk_atom: prevents a term from being evaluated

val mk_red : fterm -> fconstr

mk_red: makes a reducible term (used in ring)

val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> Constr.constr
val destFLambda : (fconstr Esubst.subs -> Constr.constr -> fconstr) -> fconstr -> Names.Name.t Context.binder_annot * fconstr * fconstr
type clos_infos

Global and local constant cache

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

norm_val is for strong normalization

val whd_val : clos_infos -> clos_tab -> fconstr -> Constr.constr

whd_val is for weak head normalization

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

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

val unfold_reference : Environ.env -> TransparentState.t -> clos_tab -> table_key -> (fconstr, Util.Empty.t) Declarations.constant_def

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

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

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

Hook for Reduction

val lift_fconstr : int -> fconstr -> fconstr
val lift_fconstr_vect : int -> fconstr array -> fconstr array
val mk_clos : fconstr Esubst.subs -> Constr.constr -> fconstr
val mk_clos_vect : fconstr Esubst.subs -> Constr.constr array -> fconstr array
val kni : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val knr : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> clos_tab -> fconstr -> Constr.constr
val zip : fconstr -> stack -> fconstr
val term_of_process : fconstr -> stack -> Constr.constr
val to_constr : Esubst.lift -> fconstr -> Constr.constr