Module Vmlambda
type lambda
=
|
Lrel of Names.Name.t * int
|
Lvar of Names.Id.t
|
Levar of Evar.t * lambda array
|
Lprod of lambda * lambda
|
Llam of Names.Name.t Context.binder_annot array * lambda
|
Llet of Names.Name.t Context.binder_annot * lambda * lambda
|
Lapp of lambda * lambda array
|
Lconst of Constr.pconstant
|
Lprim of Constr.pconstant * CPrimitives.t * lambda array
|
Lcase of Constr.case_info * Vmvalues.reloc_table * lambda * lambda * lam_branches
|
Lfix of int array * int * fix_decl
|
Lcofix of int * fix_decl
|
Lint of int
|
Lmakeblock of int * lambda array
|
Luint of Uint63.t
|
Lfloat of Float64.t
|
Lval of Vmvalues.structured_values
|
Lsort of Sorts.t
|
Lind of Constr.pinductive
|
Lproj of Names.Projection.Repr.t * lambda
and lam_branches
=
{
constant_branches : lambda array;
nonconstant_branches : (Names.Name.t Context.binder_annot array * lambda) array;
}
and fix_decl
= Names.Name.t Context.binder_annot array * lambda array * lambda array
exception
TooLargeInductive of Pp.t
val lambda_of_constr : optimize:bool -> Environ.env -> Constr.t -> lambda
val decompose_Llam : lambda -> Names.Name.t Context.binder_annot array * lambda
val get_alias : Environ.env -> Names.Constant.t -> Names.Constant.t
val dump_lambda : bool Stdlib.ref
Dump the VM lambda code after compilation (for debugging purposes)