New IR in VM: Clambda.

This intermediate representation serves two purposes:
1- It is a preliminary step for primitive machine integers, as iterators
will be compiled to Clambda.
2- It makes the VM compilation passes closer to the ones of
native_compute. Once we unifiy the representation of values, we should
be able to factorize the lambda-code generation between the two
compilers, as well as the reification code.

This code was written by Benjamin Grégoire and myself.

1 files changed, 27 insertions, 0 deletions

diff --git a/kernel/clambda.mli b/kernel/clambda.mli
new file mode 100644
index 000000000..89b7fd8e3
--- /dev/null
+++ b/kernel/clambda.mli
@@ -0,0 +1,27 @@
+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