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

diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml
new file mode 100644
index 0000000000..0fcaf4f10a
--- /dev/null
+++ b/kernel/write_uint63.ml
@@ -0,0 +1,30 @@
+(** Equivalent of rm -f *)
+
+let safe_remove f =
+  try Unix.chmod f 0o644; Sys.remove f with _ -> ()
+
+(** * Generate an implementation of 63-bit arithmetic *)
+
+let ml_file_copy input output =
+  safe_remove output;
+  let i = open_in input in
+  let o = open_out output in
+  let pr s = Printf.fprintf o s in
+  pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n";
+  pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n";
+  try
+    while true do
+      output_string o (input_line i); output_char o '\n'
+    done
+  with End_of_file ->
+    close_in i;
+    close_out o;
+    Unix.chmod output 0o444
+
+let write_uint63 () =
+  ml_file_copy
+    (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml"
+     else (* 64 bits *) "uint63_amd64.ml")
+    "uint63.ml"
+
+let () = write_uint63 ()