Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

1 files changed, 31 insertions, 18 deletions

diff --git a/kernel/clambda.mli b/kernel/clambda.mli
index 8ff10b4549..4d921fd45e 100644
--- a/kernel/clambda.mli
+++ b/kernel/clambda.mli
@@ -1,7 +1,37 @@
 open Names
-open Cinstr
+open Constr
+open Vmvalues
 open Environ
 
+type lambda =
+  | Lrel          of Name.t * int
+  | Lvar          of Id.t
+  | Levar         of Evar.t * lambda array
+  | Lprod         of lambda * lambda
+  | Llam          of Name.t array * lambda
+  | Llet          of Name.t * lambda * lambda
+  | Lapp          of lambda * lambda array
+  | Lconst        of pconstant
+  | Lprim         of pconstant option * CPrimitives.t * lambda array
+        (* No check if None *)
+  | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
+  | Lif           of lambda * lambda * lambda
+  | Lfix          of (int array * int) * fix_decl
+  | Lcofix        of int * fix_decl
+  | Lint          of int
+  | Lmakeblock    of int * lambda array
+  | Luint         of Uint63.t
+  | Lval          of structured_values
+  | Lsort         of Sorts.t
+  | Lind          of pinductive
+  | Lproj         of Projection.Repr.t * lambda
+
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t array * lambda) array }
+
+and fix_decl =  Name.t array * lambda array * lambda array
+
 exception TooLargeInductive of Pp.t
 
 val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda
@@ -10,22 +40,5 @@ val decompose_Llam : lambda -> Name.t array * lambda
 
 val get_alias : 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
-
 (** Dump the VM lambda code after compilation (for debugging purposes) *)
 val dump_lambda : bool ref