Add more constants

2 files changed, 40 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index b4ec2ce7e..fd0fd1d0e 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -21,6 +21,7 @@ nums = tuple(sorted(set(systematic_nums + [
     481,
     569,
     765,
+    977,
     114687,
     121665,
     130307,
@@ -82,6 +83,7 @@ nums = tuple(sorted(set(systematic_nums + [
     536870906,
     536870910,
     1073741822,
+    4294966319,
     4294967107,
     4294967271,
     4294967294,
@@ -143,7 +145,10 @@ nums = tuple(sorted(set(systematic_nums + [
     4503599627370494,
     9007199187632127,
     72057594037927934,
+    18446744069414584319,
+    18446744069414584320,
     18446744069414584321,
+    18446744073709551299,
     18446744073709551614,
     77371252455336267181195254,
     77371252455336267181195262,
@@ -476,6 +481,8 @@ Notation "'0b1000111001'" (* 569 (0x239) *)
   := (Const WO~0~0~0~0~0~0~1~0~0~0~1~1~1~0~0~1).
 Notation "'0b1011111101'" (* 765 (0x2fd) *)
   := (Const WO~0~0~0~0~0~0~1~0~1~1~1~1~1~1~0~1).
+Notation "'0b1111010001'" (* 977 (0x3d1) *)
+  := (Const WO~0~0~0~0~0~0~1~1~1~1~0~1~0~0~0~1).
 Notation "'0b1111111111'" (* 1023 (0x3ff) *)
   := (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b10000000000'" (* 1024 (0x400) *)
@@ -730,6 +737,8 @@ Notation "'0b10000000000000000000000000000000'" (* 2147483648 (0x80000000) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b10000000000000000000000000000001'" (* 2147483649 (0x80000001) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b11111111111111111111110000101111'" (* 4294966319 (0xfffffc2f) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
 Notation "'0b11111111111111111111111101000011'" (* 4294967107 (0xffffff43) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1).
 Notation "'0b11111111111111111111111111100111'" (* 4294967271 (0xffffffe7) *)
@@ -1044,8 +1053,14 @@ Notation "'0b1000000000000000000000000000000000000000000000000000000000000000'"
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b1000000000000000000000000000000000000000000000000000000000000001'" (* 9223372036854775809 (0x8000000000000001L) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111111111111111111111111111011111111111111111111111111111111'" (* 18446744069414584319 (0xfffffffeffffffffL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b1111111111111111111111111111111100000000000000000000000000000000'" (* 18446744069414584320 (0xffffffff00000000L) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b1111111111111111111111111111111100000000000000000000000000000001'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111111011000011'" (* 18446744073709551299 (0xfffffffffffffec3L) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1).
 Notation "'0b1111111111111111111111111111111111111111111111111111111111111110'" (* 18446744073709551614 (0xfffffffffffffffeL) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111111111111111111111111111111111'" (* 18446744073709551615 (0xffffffffffffffffL) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 74162d5d8..ee0de1903 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -21,6 +21,7 @@ nums = tuple(sorted(set(systematic_nums + [
     481,
     569,
     765,
+    977,
     114687,
     121665,
     130307,
@@ -82,6 +83,7 @@ nums = tuple(sorted(set(systematic_nums + [
     536870906,
     536870910,
     1073741822,
+    4294966319,
     4294967107,
     4294967271,
     4294967294,
@@ -143,7 +145,10 @@ nums = tuple(sorted(set(systematic_nums + [
     4503599627370494,
     9007199187632127,
     72057594037927934,
+    18446744069414584319,
+    18446744069414584320,
     18446744069414584321,
+    18446744073709551299,
     18446744073709551614,
     77371252455336267181195254,
     77371252455336267181195262,
@@ -760,6 +765,10 @@ Notation "'0x2fd'" (* 765 (0x2fd) *)
   := (Const 765%Z).
 Notation "'0x2fd'" (* 765 (0x2fd) *)
   := (Const WO~0~0~0~0~0~0~1~0~1~1~1~1~1~1~0~1).
+Notation "'0x3d1'" (* 977 (0x3d1) *)
+  := (Const 977%Z).
+Notation "'0x3d1'" (* 977 (0x3d1) *)
+  := (Const WO~0~0~0~0~0~0~1~1~1~1~0~1~0~0~0~1).
 Notation "'0x3ff'" (* 1023 (0x3ff) *)
   := (Const 1023%Z).
 Notation "'0x3ff'" (* 1023 (0x3ff) *)
@@ -1268,6 +1277,10 @@ Notation "'0x80000001'" (* 2147483649 (0x80000001) *)
   := (Const 2147483649%Z).
 Notation "'0x80000001'" (* 2147483649 (0x80000001) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xfffffc2f'" (* 4294966319 (0xfffffc2f) *)
+  := (Const 4294966319%Z).
+Notation "'0xfffffc2f'" (* 4294966319 (0xfffffc2f) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
 Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
   := (Const 4294967107%Z).
 Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
@@ -1896,10 +1909,22 @@ Notation "'0x8000000000000001L'" (* 9223372036854775809 (0x8000000000000001L) *)
   := (Const 9223372036854775809%Z).
 Notation "'0x8000000000000001L'" (* 9223372036854775809 (0x8000000000000001L) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xfffffffeffffffffL'" (* 18446744069414584319 (0xfffffffeffffffffL) *)
+  := (Const 18446744069414584319%Z).
+Notation "'0xfffffffeffffffffL'" (* 18446744069414584319 (0xfffffffeffffffffL) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xffffffff00000000L'" (* 18446744069414584320 (0xffffffff00000000L) *)
+  := (Const 18446744069414584320%Z).
+Notation "'0xffffffff00000000L'" (* 18446744069414584320 (0xffffffff00000000L) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const 18446744069414584321%Z).
 Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xfffffffffffffec3L'" (* 18446744073709551299 (0xfffffffffffffec3L) *)
+  := (Const 18446744073709551299%Z).
+Notation "'0xfffffffffffffec3L'" (* 18446744073709551299 (0xfffffffffffffec3L) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1).
 Notation "'0xfffffffffffffffeL'" (* 18446744073709551614 (0xfffffffffffffffeL) *)
   := (Const 18446744073709551614%Z).
 Notation "'0xfffffffffffffffeL'" (* 18446744073709551614 (0xfffffffffffffffeL) *)