Add more notations

2 files changed, 24 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 962c9a3a8..70784511a 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -97,7 +97,9 @@ nums = tuple(list(range(128)) + [
     536870911,
     1073741822,
     1073741823,
+    2147483647,
     4294967107,
+    4294967271,
     4294967294,
     4294967295,
     8589934559,
@@ -130,6 +132,7 @@ nums = tuple(list(range(128)) + [
     549755813887,
     1099511627761,
     1099511627775,
+    1425929142271,
     2199023255543,
     2199023255551,
     4398046511079,
@@ -665,8 +668,12 @@ Notation "'0b111111111111111111111111111110'" (* 1073741822 (0x3ffffffe) *)
   := (Const WO~0~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~0).
 Notation "'0b111111111111111111111111111111'" (* 1073741823 (0x3fffffff) *)
   := (Const WO~0~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).
+Notation "'0b1111111111111111111111111111111'" (* 2147483647 (0x7fffffff) *)
+  := (Const WO~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).
 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) *)
+  := (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~0~0~1~1~1).
 Notation "'0b11111111111111111111111111111110'" (* 4294967294 (0xfffffffe) *)
   := (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).
 Notation "'0b11111111111111111111111111111111'" (* 4294967295 (0xffffffff) *)
@@ -731,6 +738,8 @@ Notation "'0b1111111111111111111111111111111111110001'" (* 1099511627761 (0xffff
   := (Const WO~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~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~0~0~1).
 Notation "'0b1111111111111111111111111111111111111111'" (* 1099511627775 (0xffffffffff) *)
   := (Const WO~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~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).
+Notation "'0b10100101111111111111111111111111111111111'" (* 1425929142271 (0x14bffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~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~1~1).
 Notation "'0b11111111111111111111111111111111111110111'" (* 2199023255543 (0x1fffffffff7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~1~1~1~1~1~0~1~1~1).
 Notation "'0b11111111111111111111111111111111111111111'" (* 2199023255551 (0x1ffffffffff) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index d76adca88..df7e24a01 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -97,7 +97,9 @@ nums = tuple(list(range(128)) + [
     536870911,
     1073741822,
     1073741823,
+    2147483647,
     4294967107,
+    4294967271,
     4294967294,
     4294967295,
     8589934559,
@@ -130,6 +132,7 @@ nums = tuple(list(range(128)) + [
     549755813887,
     1099511627761,
     1099511627775,
+    1425929142271,
     2199023255543,
     2199023255551,
     4398046511079,
@@ -1091,10 +1094,18 @@ Notation "'0x3fffffff'" (* 1073741823 (0x3fffffff) *)
   := (Const 1073741823%Z).
 Notation "'0x3fffffff'" (* 1073741823 (0x3fffffff) *)
   := (Const WO~0~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).
+Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *)
+  := (Const 2147483647%Z).
+Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *)
+  := (Const WO~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).
 Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
   := (Const 4294967107%Z).
 Notation "'0xffffff43'" (* 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 "'0xffffffe7'" (* 4294967271 (0xffffffe7) *)
+  := (Const 4294967271%Z).
+Notation "'0xffffffe7'" (* 4294967271 (0xffffffe7) *)
+  := (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~0~0~1~1~1).
 Notation "'0xfffffffe'" (* 4294967294 (0xfffffffe) *)
   := (Const 4294967294%Z).
 Notation "'0xfffffffe'" (* 4294967294 (0xfffffffe) *)
@@ -1223,6 +1234,10 @@ Notation "'0xffffffffff'" (* 1099511627775 (0xffffffffff) *)
   := (Const 1099511627775%Z).
 Notation "'0xffffffffff'" (* 1099511627775 (0xffffffffff) *)
   := (Const WO~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~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).
+Notation "'0x14bffffffff'" (* 1425929142271 (0x14bffffffff) *)
+  := (Const 1425929142271%Z).
+Notation "'0x14bffffffff'" (* 1425929142271 (0x14bffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~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~1~1).
 Notation "'0x1fffffffff7'" (* 2199023255543 (0x1fffffffff7) *)
   := (Const 2199023255543%Z).
 Notation "'0x1fffffffff7'" (* 2199023255543 (0x1fffffffff7) *)