Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

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