Add more constant notations

2 files changed, 56 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index e79341ff0..6a4d58051 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -44,6 +44,7 @@ nums = tuple(sorted(set(systematic_nums + [
     524267,
     524269,
     524271,
+    524278,
     524279,
     524286,
     679935,
@@ -67,6 +68,8 @@ nums = tuple(sorted(set(systematic_nums + [
     2097135,
     2097143,
     2097150,
+    4188670,
+    4192254,
     4193327,
     4193539,
     4193735,
@@ -79,6 +82,9 @@ nums = tuple(sorted(set(systematic_nums + [
     4194293,
     4194302,
     8323583,
+    8386654,
+    8387078,
+    8388230,
     8388491,
     8388558,
     8388574,
@@ -113,6 +119,7 @@ nums = tuple(sorted(set(systematic_nums + [
     33554429,
     33554430,
     67108798,
+    67108826,
     67108833,
     67108845,
     67108847,
@@ -887,6 +894,8 @@ Notation "'0b1111111111111101101'" (* 524269 (0x7ffed) *)
   := (Const WO~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~0~1~1~0~1).
 Notation "'0b1111111111111101111'" (* 524271 (0x7ffef) *)
   := (Const WO~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~0~1~1~1~1).
+Notation "'0b1111111111111110110'" (* 524278 (0x7fff6) *)
+  := (Const WO~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~0~1~1~0).
 Notation "'0b1111111111111110111'" (* 524279 (0x7fff7) *)
   := (Const WO~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~0~1~1~1).
 Notation "'0b1111111111111111110'" (* 524286 (0x7fffe) *)
@@ -951,6 +960,10 @@ Notation "'0b1000000000000000000000'" (* 2097152 (0x200000) *)
   := (Const WO~0~0~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).
 Notation "'0b1000000000000000000001'" (* 2097153 (0x200001) *)
   := (Const WO~0~0~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~1).
+Notation "'0b1111111110100111111110'" (* 4188670 (0x3fe9fe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~0).
+Notation "'0b1111111111011111111110'" (* 4192254 (0x3ff7fe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111110000101111'" (* 4193327 (0x3ffc2f) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
 Notation "'0b1111111111110100000011'" (* 4193539 (0x3ffd03) *)
@@ -981,6 +994,12 @@ Notation "'0b10000000000000000000001'" (* 4194305 (0x400001) *)
   := (Const WO~0~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~1).
 Notation "'0b11111110000000111111111'" (* 8323583 (0x7f01ff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111100001011110'" (* 8386654 (0x7ff85e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
+Notation "'0b11111111111101000000110'" (* 8387078 (0x7ffa06) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
+Notation "'0b11111111111111010000110'" (* 8388230 (0x7ffe86) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1~0).
 Notation "'0b11111111111111110001011'" (* 8388491 (0x7fff8b) *)
   := (Const WO~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~0~0~0~1~0~1~1).
 Notation "'0b11111111111111111001110'" (* 8388558 (0x7fffce) *)
@@ -1067,6 +1086,8 @@ Notation "'0b10000000000000000000000001'" (* 33554433 (0x2000001) *)
   := (Const WO~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~0~1).
 Notation "'0b11111111111111111110111110'" (* 67108798 (0x3ffffbe) *)
   := (Const WO~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~0~1~1~1~1~1~0).
+Notation "'0b11111111111111111111011010'" (* 67108826 (0x3ffffda) *)
+  := (Const WO~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~0~1~1~0~1~0).
 Notation "'0b11111111111111111111100001'" (* 67108833 (0x3ffffe1) *)
   := (Const WO~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~0~0~0~0~1).
 Notation "'0b11111111111111111111101101'" (* 67108845 (0x3ffffed) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 20d24bb66..16db5d8c7 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -44,6 +44,7 @@ nums = tuple(sorted(set(systematic_nums + [
     524267,
     524269,
     524271,
+    524278,
     524279,
     524286,
     679935,
@@ -67,6 +68,8 @@ nums = tuple(sorted(set(systematic_nums + [
     2097135,
     2097143,
     2097150,
+    4188670,
+    4192254,
     4193327,
     4193539,
     4193735,
@@ -79,6 +82,9 @@ nums = tuple(sorted(set(systematic_nums + [
     4194293,
     4194302,
     8323583,
+    8386654,
+    8387078,
+    8388230,
     8388491,
     8388558,
     8388574,
@@ -113,6 +119,7 @@ nums = tuple(sorted(set(systematic_nums + [
     33554429,
     33554430,
     67108798,
+    67108826,
     67108833,
     67108845,
     67108847,
@@ -1271,6 +1278,10 @@ Notation "'0x7ffef'" (* 524271 (0x7ffef) *)
   := (Const 524271%Z).
 Notation "'0x7ffef'" (* 524271 (0x7ffef) *)
   := (Const WO~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~0~1~1~1~1).
+Notation "'0x7fff6'" (* 524278 (0x7fff6) *)
+  := (Const 524278%Z).
+Notation "'0x7fff6'" (* 524278 (0x7fff6) *)
+  := (Const WO~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~0~1~1~0).
 Notation "'0x7fff7'" (* 524279 (0x7fff7) *)
   := (Const 524279%Z).
 Notation "'0x7fff7'" (* 524279 (0x7fff7) *)
@@ -1399,6 +1410,14 @@ Notation "'0x200001'" (* 2097153 (0x200001) *)
   := (Const 2097153%Z).
 Notation "'0x200001'" (* 2097153 (0x200001) *)
   := (Const WO~0~0~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~1).
+Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *)
+  := (Const 4188670%Z).
+Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~0).
+Notation "'0x3ff7fe'" (* 4192254 (0x3ff7fe) *)
+  := (Const 4192254%Z).
+Notation "'0x3ff7fe'" (* 4192254 (0x3ff7fe) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *)
   := (Const 4193327%Z).
 Notation "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *)
@@ -1459,6 +1478,18 @@ Notation "'0x7f01ff'" (* 8323583 (0x7f01ff) *)
   := (Const 8323583%Z).
 Notation "'0x7f01ff'" (* 8323583 (0x7f01ff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1).
+Notation "'0x7ff85e'" (* 8386654 (0x7ff85e) *)
+  := (Const 8386654%Z).
+Notation "'0x7ff85e'" (* 8386654 (0x7ff85e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
+Notation "'0x7ffa06'" (* 8387078 (0x7ffa06) *)
+  := (Const 8387078%Z).
+Notation "'0x7ffa06'" (* 8387078 (0x7ffa06) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
+Notation "'0x7ffe86'" (* 8388230 (0x7ffe86) *)
+  := (Const 8388230%Z).
+Notation "'0x7ffe86'" (* 8388230 (0x7ffe86) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1~0).
 Notation "'0x7fff8b'" (* 8388491 (0x7fff8b) *)
   := (Const 8388491%Z).
 Notation "'0x7fff8b'" (* 8388491 (0x7fff8b) *)
@@ -1631,6 +1662,10 @@ Notation "'0x3ffffbe'" (* 67108798 (0x3ffffbe) *)
   := (Const 67108798%Z).
 Notation "'0x3ffffbe'" (* 67108798 (0x3ffffbe) *)
   := (Const WO~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~0~1~1~1~1~1~0).
+Notation "'0x3ffffda'" (* 67108826 (0x3ffffda) *)
+  := (Const 67108826%Z).
+Notation "'0x3ffffda'" (* 67108826 (0x3ffffda) *)
+  := (Const WO~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~0~1~1~0~1~0).
 Notation "'0x3ffffe1'" (* 67108833 (0x3ffffe1) *)
   := (Const 67108833%Z).
 Notation "'0x3ffffe1'" (* 67108833 (0x3ffffe1) *)