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>

8 files changed, 108 insertions, 1 deletions

diff --git a/test-suite/output/Int31Syntax.out b/test-suite/output/Int31Syntax.out
index 4e8796c14b..0d6504f5f8 100644
--- a/test-suite/output/Int31Syntax.out
+++ b/test-suite/output/Int31Syntax.out
@@ -12,3 +12,5 @@ I31
      : int31
      = 710436486
      : int31
+The command has indeed failed with message:
+Cannot interpret this number as a value of type int31
diff --git a/test-suite/output/Int31Syntax.v b/test-suite/output/Int31Syntax.v
index 83be3b976b..48889a26ef 100644
--- a/test-suite/output/Int31Syntax.v
+++ b/test-suite/output/Int31Syntax.v
@@ -3,11 +3,12 @@ Require Import Int31 Cyclic31.
 Open Scope int31_scope.
 Check I31. (* Would be nice to have I31 : digits->digits->...->int31
               For the moment, I31 : digits31 int31, which is better
-	      than (fix nfun .....) size int31 *)
+              than (fix nfun .....) size int31 *)
 Check 2.
 Check 1000000000000000000. (* = 660865024, after modulo 2^31 *)
 Check (add31 2 2).
 Check (2+2).
 Eval vm_compute in 2+2.
 Eval vm_compute in 65675757 * 565675998.
+Fail Check -1.
 Close Scope int31_scope.
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
new file mode 100644
index 0000000000..fdd5599565
--- /dev/null
+++ b/test-suite/output/Int63Syntax.out
@@ -0,0 +1,16 @@
+2
+     : int
+9223372036854775807
+     : int
+2 + 2
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
+The command has indeed failed with message:
+int63 are only non-negative numbers.
+The command has indeed failed with message:
+overflow in int63 literal: 9223372036854775808
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
new file mode 100644
index 0000000000..3dc364eddb
--- /dev/null
+++ b/test-suite/output/Int63Syntax.v
@@ -0,0 +1,12 @@
+Require Import Int63 Cyclic63.
+
+Open Scope int63_scope.
+Check 2.
+Check 9223372036854775807.
+Check (Int63.add 2 2).
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
+Fail Check -1.
+Fail Check 9223372036854775808.
+Close Scope int63_scope.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 7a64b7eb45..efa895d709 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -51,3 +51,5 @@ r 2 3
      : Prop
 Notation Cn := Foo.FooCn
 Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
+let v := 0%test17 in v : myint63
+     : myint63
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 90babf9c55..b4c65ce196 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -197,3 +197,16 @@ End Mfoo.
 About Cn.
 
 End J.
+
+Require Import Coq.Numbers.Cyclic.Int63.Int63.
+Module NumeralNotations.
+  Module Test17.
+    (** Test int63 *)
+    Declare Scope test17_scope.
+    Delimit Scope test17_scope with test17.
+    Local Set Primitive Projections.
+    Record myint63 := of_int { to_int : int }.
+    Numeral Notation myint63 of_int to_int : test17_scope.
+    Check let v := 0%test17 in v : myint63.
+  End Test17.
+End NumeralNotations.
diff --git a/test-suite/output/sint63Notation.out b/test-suite/output/sint63Notation.out
new file mode 100644
index 0000000000..9d325b38c7
--- /dev/null
+++ b/test-suite/output/sint63Notation.out
@@ -0,0 +1,24 @@
+     = 0
+     : uint
+     = 1
+     : uint
+     = 9223372036854775807
+     : uint
+let v := 0 in v : uint
+     : uint
+let v := 1 in v : uint
+     : uint
+let v := 9223372036854775807 in v : uint
+     : uint
+     = 0
+     : sint
+     = 1
+     : sint
+     = -1
+     : sint
+let v := 0 in v : sint
+     : sint
+let v := 1 in v : sint
+     : sint
+let v := -1 in v : sint
+     : sint
diff --git a/test-suite/output/sint63Notation.v b/test-suite/output/sint63Notation.v
new file mode 100644
index 0000000000..331d74ed3d
--- /dev/null
+++ b/test-suite/output/sint63Notation.v
@@ -0,0 +1,37 @@
+From Coq
+Require Import Int63.
+Import ZArith.
+
+Declare Scope uint_scope.
+Declare Scope sint_scope.
+Delimit Scope uint_scope with uint.
+Delimit Scope sint_scope with sint.
+
+Record uint := wrapu { unwrapu : int }.
+Record sint := wraps { unwraps : int }.
+
+Definition uof_Z (v : Z) := wrapu (of_Z v).
+Definition uto_Z (v : uint) := to_Z (unwrapu v).
+
+Definition sof_Z (v : Z) := wraps (of_Z (v mod (2 ^ 31))).
+Definition as_signed (bw : Z) (v : Z) :=
+  (((2 ^ (bw - 1) + v) mod (2 ^ bw)) - 2 ^ (bw - 1))%Z.
+
+Definition sto_Z (v : sint) := as_signed 31 (to_Z (unwraps v)).
+Numeral Notation uint uof_Z uto_Z : uint_scope.
+Numeral Notation sint sof_Z sto_Z : sint_scope.
+Open Scope uint_scope.
+Compute uof_Z 0.
+Compute uof_Z 1.
+Compute uof_Z (-1).
+Check let v := 0 in v : uint.
+Check let v := 1 in v : uint.
+Check let v := -1 in v : uint.
+Close Scope uint_scope.
+Open Scope sint_scope.
+Compute sof_Z 0.
+Compute sof_Z 1.
+Compute sof_Z (-1).
+Check let v := 0 in v : sint.
+Check let v := 1 in v : sint.
+Check let v := -1 in v : sint.