Cbv (coq-core.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.pconstant * cbv_value array

| ARRAY of Univ.Instance.t * cbv_value Parray.t * cbv_value

and cbv_stack =

| TOP

| APP of cbv_value list * cbv_stack

| CASE of Univ.Instance.t * Constr.constr array * Constr.case_return * Constr.case_branch array * Constr.case_invert * 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 list -> 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

End of cbv debug section i