Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

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.