CClosure
Lazy reduction.
fconstr
is the type of frozen constr
type usubs = fconstr Esubst.subs UVars.puniverses
type table_key = Names.Constant.t UVars.puniverses Names.tableKey
type fterm =
Relevances (eg in binder_annot or case_info) have NOT been substituted when there is a usubs field
type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
type stack_member =
| Zapp of fconstr array |
| ZcaseT of Constr.case_info * UVars.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * usubs |
| Zproj of Names.Projection.Repr.t * Sorts.relevance |
| 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 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 inductive_subst : Declarations.mutual_inductive_body -> UVars.Instance.t -> fconstr array -> usubs
val usubst_instance : 'a UVars.puniverses -> UVars.Instance.t -> UVars.Instance.t
identity if the first instance is empty
val usubst_binder : _ UVars.puniverses -> 'a Constr.binder_annot -> 'a Constr.binder_annot
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
val inject : Constr.constr -> fconstr
val mk_clos : usubs -> Constr.constr -> fconstr
val mk_clos_vect : usubs -> Constr.constr array -> fconstr array
val term_of_fconstr : fconstr -> Constr.constr
val term_of_process : fconstr -> stack -> Constr.constr
val destFLambda : (usubs -> Constr.constr -> fconstr) -> fconstr -> Names.Name.t Constr.binder_annot * fconstr * fconstr
type evar_handler = {
evar_expand : Constr.constr Constr.pexistential -> Constr.constr evar_expansion; |
evar_repack : (Evar.t * Constr.constr list) -> Constr.constr; |
evar_irrelevant : Constr.constr Constr.pexistential -> bool; |
qvar_irrelevant : Sorts.QVar.t -> bool; |
}
val default_evar_handler : Environ.env -> evar_handler
val create_conv_infos : ?univs:UGraph.t -> ?evars:evar_handler -> RedFlags.reds -> Environ.env -> clos_infos
val create_clos_infos : ?univs:UGraph.t -> ?evars:evar_handler -> 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 -> Sorts.relevance -> stack_member option
val push_relevance : clos_infos -> 'b Constr.binder_annot -> clos_infos
val push_relevances : clos_infos -> 'b Constr.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 is_irrelevant : clos_infos -> Sorts.relevance -> bool
val infos_with_reds : clos_infos -> RedFlags.reds -> clos_infos
Reduction function
val norm_val : clos_infos -> clos_tab -> fconstr -> Constr.constr
norm_val
is for strong normalization
val norm_term : clos_infos -> clos_tab -> usubs -> Constr.constr -> Constr.constr
Same as norm_val
but for terms
val whd_val : clos_infos -> clos_tab -> fconstr -> Constr.constr
whd_val
is for weak head normalization
whd_stack
performs weak head normalization in a given stack. It stops whenever a reduction is blocked.
val skip_irrelevant_stack : clos_infos -> stack -> stack
val eta_expand_stack : clos_infos -> Names.Name.t Constr.binder_annot -> stack -> stack
val eta_expand_ind_stack : Environ.env -> Constr.pinductive -> 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
Conversion auxiliary functions to do step by step normalisation
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 get_ref_mask : clos_infos -> clos_tab -> table_key -> bool array
val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit
Hook for Reduction