Module Genlambda

Intermediate language used by both the VM and native.

type reloc_table = (int * int) array
type 'v lambda =
| Lrel of Names.Name.t * int
| Lvar of Names.Id.t
| Levar of Evar.t * 'v lambda array
| Lprod of 'v lambda * 'v lambda
| Llam of Names.Name.t Constr.binder_annot array * 'v lambda
| Llet of Names.Name.t Constr.binder_annot * 'v lambda * 'v lambda
| Lapp of 'v lambda * 'v lambda array
| Lconst of Constr.pconstant
| Lproj of Names.Projection.Repr.t * 'v lambda
| Lprim of Constr.pconstant * CPrimitives.t * 'v lambda array
| Lcase of case_annot * 'v lambda * 'v lambda * 'v lam_branches
| Lfix of int array * Names.inductive array * int * 'v fix_decl
| Lcofix of int * 'v fix_decl
| Lint of int
| Lparray of 'v lambda array * 'v lambda
| Lmakeblock of Names.inductive * int * 'v lambda array
| Luint of Uint63.t
| Lfloat of Float64.t
| Lstring of Pstring.t
| Lval of 'v
| Lsort of Sorts.t
| Lind of Constr.pinductive
and 'v lam_branches = {
constant_branches : 'v lambda array;
nonconstant_branches : (Names.Name.t Constr.binder_annot array * 'v lambda) array;
}
and 'v fix_decl = Names.Name.t Constr.binder_annot array * 'v lambda array * 'v lambda array
type evars = {
evars_val : CClosure.evar_handler;
}
val empty_evars : Environ.env -> evars
Manipulation functions
val mkLapp : 'v lambda -> 'v lambda array -> 'v lambda
val mkLlam : Names.Name.t Constr.binder_annot array -> 'v lambda -> 'v lambda
val decompose_Llam : 'v lambda -> Names.Name.t Constr.binder_annot array * 'v lambda
val decompose_Llam_Llet : 'v lambda -> (Names.Name.t Constr.binder_annot * 'v lambda option) array * 'v lambda
val free_rels : 'v lambda -> Int.Set.t
val optimize : 'v lambda -> 'v lambda
Translation functions
val get_alias : Environ.env -> Names.Constant.t -> Names.Constant.t * bool array
module type S = sig ... end
module Make (Val : S) : sig ... end
Printing
val pp_lam : 'v lambda -> Pp.t