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, 55 insertions, 0 deletions

diff --git a/kernel/uint63.mli b/kernel/uint63.mli
new file mode 100644
index 0000000000..b5f40ca804
--- /dev/null
+++ b/kernel/uint63.mli
@@ -0,0 +1,55 @@
+type t
+
+val uint_size : int
+val maxuint31 : t
+
+      (* conversion to int *)
+val of_int : int -> t
+val to_int2 : t -> int * int (* msb, lsb *)
+val of_int64 : Int64.t -> t
+(*
+val of_uint : int -> t
+*)
+
+val hash : t -> int
+
+     (* convertion to a string *)
+val to_string : t -> string
+val of_string : string -> t
+
+val compile : t -> string
+
+(* constants *)
+val zero    : t
+val one : t
+
+      (* logical operations *)
+val l_sl    : t -> t -> t
+val l_sr    : t -> t -> t
+val l_and   : t -> t -> t
+val l_xor   : t -> t -> t
+val l_or    : t -> t -> t
+
+      (* Arithmetic operations *)
+val add     : t -> t -> t
+val sub     : t -> t -> t
+val mul     : t -> t -> t
+val div     : t -> t -> t
+val rem     : t -> t -> t
+
+      (* Specific arithmetic operations *)
+val mulc    : t -> t -> t * t
+val addmuldiv : t -> t -> t -> t
+val div21   : t -> t -> t -> t * t
+
+      (* comparison *)
+val lt      : t -> t -> bool
+val equal      : t -> t -> bool
+val le      : t -> t -> bool
+val compare : t -> t -> int
+
+      (* head and tail *)
+val head0   : t -> t
+val tail0   : t -> t
+
+val is_uint63 : Obj.t -> bool