Add more constant notations

2 files changed, 24 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 739c17146..2d17668c6 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -69,7 +69,9 @@ nums = tuple(sorted(set(systematic_nums + [
     8388599,
     8388605,
     8388606,
+    11599871,
     16711679,
+    16775935,
     16776959,
     16777189,
     16777191,
@@ -115,6 +117,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1073741822,
     1332920885,
     1749801491,
+    2147483631,
     2147483647,
     2863311531,
     2969567231,
@@ -833,8 +836,12 @@ Notation "'0b100000000000000000000000'" (* 8388608 (0x800000) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b100000000000000000000001'" (* 8388609 (0x800001) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b101100001111111111111111'" (* 11599871 (0xb0ffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111101111111111111111'" (* 16711679 (0xfeffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b111111111111101011111111'" (* 16775935 (0xfffaff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111111011111111'" (* 16776959 (0xfffeff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111111111100101'" (* 16777189 (0xffffe5) *)
@@ -967,6 +974,8 @@ Notation "'0b1001111011100101100001000110101'" (* 1332920885 (0x4f72c235) *)
   := (Const WO~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1).
 Notation "'0b1101000010010111101101000010011'" (* 1749801491 (0x684bda13) *)
   := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1).
+Notation "'0b1111111111111111111111111101111'" (* 2147483631 (0x7fffffef) *)
+  := (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~0~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 "'0b10000000000000000000000000000000'" (* 2147483648 (0x80000000) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index e0670fa26..27a235d35 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -69,7 +69,9 @@ nums = tuple(sorted(set(systematic_nums + [
     8388599,
     8388605,
     8388606,
+    11599871,
     16711679,
+    16775935,
     16776959,
     16777189,
     16777191,
@@ -115,6 +117,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1073741822,
     1332920885,
     1749801491,
+    2147483631,
     2147483647,
     2863311531,
     2969567231,
@@ -1297,10 +1300,18 @@ Notation "'0x800001'" (* 8388609 (0x800001) *)
   := (Const 8388609%Z).
 Notation "'0x800001'" (* 8388609 (0x800001) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xb0ffff'" (* 11599871 (0xb0ffff) *)
+  := (Const 11599871%Z).
+Notation "'0xb0ffff'" (* 11599871 (0xb0ffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0xfeffff'" (* 16711679 (0xfeffff) *)
   := (Const 16711679%Z).
 Notation "'0xfeffff'" (* 16711679 (0xfeffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xfffaff'" (* 16775935 (0xfffaff) *)
+  := (Const 16775935%Z).
+Notation "'0xfffaff'" (* 16775935 (0xfffaff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1).
 Notation "'0xfffeff'" (* 16776959 (0xfffeff) *)
   := (Const 16776959%Z).
 Notation "'0xfffeff'" (* 16776959 (0xfffeff) *)
@@ -1565,6 +1576,10 @@ Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *)
   := (Const 1749801491%Z).
 Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *)
   := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1).
+Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *)
+  := (Const 2147483631%Z).
+Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *)
+  := (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~0~1~1~1~1).
 Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *)
   := (Const 2147483647%Z).
 Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *)