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, 38 insertions, 13 deletions

diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 7b20258929..eb06522a33 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -10,9 +10,45 @@
 open Names
 open Constr
 open Environ
-open Nativeinstr
+open Nativevalues
 
 (** This file defines the lambda code generation phase of the native compiler *)
+type prefix = string
+
+type lambda =
+  | Lrel          of Name.t * int
+  | Lvar          of Id.t
+  | Lmeta         of metavariable * lambda (* type *)
+  | Levar         of Evar.t * lambda array (* arguments *)
+  | Lprod         of lambda * lambda
+  | Llam          of Name.t array * lambda
+  | Lrec          of Name.t * lambda
+  | Llet          of Name.t * lambda * lambda
+  | Lapp          of lambda * lambda array
+  | Lconst        of prefix * pconstant
+  | Lproj         of prefix * inductive * int (* prefix, inductive, index starting from 0 *)
+  | Lprim         of prefix * pconstant * CPrimitives.t * lambda array
+  | Lcase         of annot_sw * lambda * lambda * lam_branches
+                  (* annotations, term being matched, accu, branches *)
+  | Lif           of lambda * lambda * lambda
+  | Lfix          of (int array * (string * inductive) array * int) * fix_decl
+  | Lcofix        of int * fix_decl
+  | Lmakeblock    of prefix * pconstructor * int * lambda array
+                  (* prefix, constructor Name.t, constructor tag, arguments *)
+        (* A fully applied constructor *)
+  | Lconstruct    of prefix * pconstructor (* prefix, constructor Name.t *)
+        (* A partially applied constructor *)
+  | Luint         of Uint63.t
+  | Lval          of Nativevalues.t
+  | Lsort         of Sorts.t
+  | Lind          of prefix * pinductive
+  | Llazy
+  | Lforce
+
+and lam_branches = (constructor * Name.t array * lambda) array
+
+and fix_decl =  Name.t array * lambda array * lambda array
+
 type evars =
     { evars_val : existential -> constr option;
       evars_metas : metavariable -> types }
@@ -22,7 +58,7 @@ val empty_evars : evars
 val decompose_Llam : lambda -> Name.t array * lambda
 val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda
 
-val is_lazy : env -> prefix -> constr -> bool
+val is_lazy : constr -> bool
 val mk_lazy : lambda -> lambda
 
 val get_mind_prefix : env -> MutInd.t -> string
@@ -30,14 +66,3 @@ val get_mind_prefix : env -> MutInd.t -> string
 val get_alias : env -> pconstant -> pconstant
 
 val lambda_of_constr : env -> evars -> Constr.constr -> lambda
-
-val compile_static_int31 : bool -> Constr.constr array -> lambda
-
-val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
-			    lambda
-
-val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda ->
-			 lambda
-
-val compile_prim : CPrimitives.t -> Constant.t -> bool -> prefix -> lambda array ->
-		   lambda