Module Cbv

type cbv_infos

Entry point for cbv normalization of a constr

val create_cbv_infos : CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> cbv_infos
val cbv_norm : cbv_infos -> EConstr.constr -> EConstr.constr
type cbv_value =
| VAL of int * Constr.constr
| STACK of int * cbv_value * cbv_stack
| CBN of Constr.constr * cbv_value Esubst.subs
| LAM of int * (Names.Name.t Context.binder_annot * Constr.constr) list * Constr.constr * cbv_value Esubst.subs
| FIXP of Constr.fixpoint * cbv_value Esubst.subs * cbv_value array
| COFIXP of Constr.cofixpoint * cbv_value Esubst.subs * cbv_value array
| CONSTR of Names.constructor Univ.puniverses * cbv_value array
| PRIMITIVE of CPrimitives.t * Constr.t * cbv_value array
and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
| CASE of Constr.constr * Constr.constr array * Constr.case_info * cbv_value Esubst.subs * cbv_stack
| PROJ of Names.Projection.t * cbv_stack
val shift_value : int -> cbv_value -> cbv_value
val stack_app : cbv_value array -> cbv_stack -> cbv_stack
val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
val cbv_stack_term : cbv_infos -> cbv_stack -> cbv_value Esubst.subs -> Constr.constr -> cbv_value

recursive functions...

val cbv_norm_term : cbv_infos -> cbv_value Esubst.subs -> Constr.constr -> Constr.constr
val norm_head : cbv_infos -> cbv_value Esubst.subs -> Constr.constr -> cbv_stack -> cbv_value * cbv_stack
val apply_stack : cbv_infos -> Constr.constr -> cbv_stack -> Constr.constr
val cbv_norm_value : cbv_infos -> cbv_value -> Constr.constr