Module `Genlambda`

Intermediate language used by both the VM and native.

type reloc_table = (int * int) array
type case_annot = Constr.case_info * reloc_table * Declarations.recursivity_kind
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 Context.binder_annot array * 'v lambda | Llet of Names.Name.t Context.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 | Lval of 'v | Lsort of Sorts.t | Lind of Constr.pinductive | Lforce
and 'v lam_branches = { constant_branches : 'v lambda array; nonconstant_branches : (Names.Name.t Context.binder_annot array * 'v lambda) array; }
and 'v fix_decl = Names.Name.t Context.binder_annot array * 'v lambda array * 'v lambda array
type evars = { evars_val : Constr.constr CClosure.evar_handler; }

val mkLapp : 'v lambda -> 'v lambda array -> 'v lambda
val mkLlam : Names.Name.t Context.binder_annot array -> 'v lambda -> 'v lambda
val decompose_Llam : 'v lambda -> Names.Name.t Context.binder_annot array * 'v lambda
val decompose_Llam_Llet : 'v lambda -> (Names.Name.t Context.binder_annot * 'v lambda option) array * 'v lambda
val map_lam_with_binders : (int -> 'a -> 'a) -> ('a -> 'v lambda -> 'v lambda) -> 'a -> 'v lambda -> 'v lambda
val lam_exlift : Esubst.lift -> 'v lambda -> 'v lambda
val lam_lift : int -> 'v lambda -> 'v lambda
val lam_subst_rel : 'v lambda -> Names.Name.t -> int -> 'v lambda Esubst.subs -> 'v lambda
val lam_exsubst : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
val lam_subst_args : 'v lambda Esubst.subs -> 'v lambda array -> 'v lambda array
val simplify : ('v lambda -> bool) -> 'v lambda Esubst.subs -> 'v lambda -> 'v lambda
val remove_let : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda

val get_alias : Environ.env -> Names.Constant.t -> Names.Constant.t
val make_args : int -> int -> 'v lambda array
val makeblock : (int -> 'v lambda array -> 'v option) -> Names.inductive -> int -> int -> int -> 'v lambda array -> 'v lambda
val lambda_of_prim : Environ.env -> Constr.pconstant -> CPrimitives.t -> 'v lambda array -> 'v lambda

module type S = sig ... end

module Make : functor (Val : S) -> sig ... end