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, 10 insertions, 1 deletions

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 46be1bb279..bd04677374 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -10,6 +10,7 @@
 
 open Names
 open Constr
+open Declarations
 open Environ
 open Esubst
 
@@ -117,6 +118,7 @@ type fterm =
   | FProd of Name.t * fconstr * constr * fconstr subs
   | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
   | FEvar of existential * fconstr subs
+  | FInt of Uint63.t
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -124,12 +126,15 @@ type fterm =
 (***********************************************************************
   s A [stack] is a context of arguments, arguments are pushed by
    [append_stack] one array at a time *)
+type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
 
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
   | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
+  | Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args
+       (* operator, constr def, reduced arguments rev, next arguments *)
   | Zshift of int
   | Zupdate of fconstr
 
@@ -138,6 +143,10 @@ and stack = stack_member list
 val empty_stack : stack
 val append_stack : fconstr array -> stack -> stack
 
+val check_native_args : CPrimitives.t -> stack -> bool
+val get_native_args1 : CPrimitives.t -> pconstant -> stack ->
+  fconstr list * fconstr * fconstr next_native_args * stack
+
 val stack_args_size : stack -> int
 val eta_expand_stack : stack -> stack
 
@@ -201,7 +210,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** Conversion auxiliary functions to do step by step normalisation *)
 
 (** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option
+val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr constant_def
 
 (***********************************************************************
   i This is for lazy debug *)