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