diff options
Diffstat (limited to 'kernel/clambda.mli')
| -rw-r--r-- | kernel/clambda.mli | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/kernel/clambda.mli b/kernel/clambda.mli new file mode 100644 index 00000000..827eb550 --- /dev/null +++ b/kernel/clambda.mli @@ -0,0 +1,30 @@ +open Names +open Cinstr + +exception TooLargeInductive of Pp.t + +val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda + +val decompose_Llam : lambda -> Name.t array * lambda + +val get_alias : Pre_env.env -> Constant.t -> Constant.t + +val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda + +(** spiwack: this function contains the information needed to perform + the static compilation of int31 (trying and obtaining + a 31-bit integer in processor representation at compile time) *) +val compile_structured_int31 : bool -> Constr.t array -> lambda + +(** this function contains the information needed to perform + the dynamic compilation of int31 (trying and obtaining a + 31-bit integer in processor representation at runtime when + it failed at compile time *) +val dynamic_int31_compilation : bool -> lambda array -> lambda + +(*spiwack: compiling function to insert dynamic decompilation before + matching integers (in case they are in processor representation) *) +val int31_escape_before_match : bool -> lambda -> lambda + +val eta_expand : (Pre_env.env -> Constr.t -> Constr.types -> Constr.t) Hook.value +val eta_expand_hook : (Pre_env.env -> Constr.t -> Constr.types -> Constr.t) Hook.t |