Add more constant notations

2 files changed, 72 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 2600bbff6..11d9973db 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -81,6 +81,7 @@ nums = tuple(sorted(set(systematic_nums + [
     4194275,
     4194279,
     4194285,
+    4194286,
     4194287,
     4194293,
     4194302,
@@ -113,8 +114,11 @@ nums = tuple(sorted(set(systematic_nums + [
     16777212,
     16777213,
     16777214,
+    23199742,
     33423358,
+    33551870,
     33554378,
+    33554382,
     33554398,
     33554399,
     33554413,
@@ -134,6 +138,7 @@ nums = tuple(sorted(set(systematic_nums + [
     67108859,
     67108861,
     67108862,
+    134217666,
     134217690,
     134217694,
     134217697,
@@ -144,6 +149,7 @@ nums = tuple(sorted(set(systematic_nums + [
     134217713,
     134217718,
     134217719,
+    134217724,
     134217726,
     268431360,
     268435398,
@@ -160,6 +166,7 @@ nums = tuple(sorted(set(systematic_nums + [
     536870893,
     536870906,
     536870907,
+    536870908,
     536870909,
     536870910,
     678152731,
@@ -177,6 +184,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2147418110,
     2147483631,
     2147483642,
+    2147483644,
     2147483646,
     2147483647,
     2863311531,
@@ -203,6 +211,7 @@ nums = tuple(sorted(set(systematic_nums + [
     4294967109,
     4294967179,
     4294967191,
+    4294967262,
     4294967263,
     4294967265,
     4294967267,
@@ -993,6 +1002,8 @@ Notation "'0b1111111111111111100111'" (* 4194279 (0x3fffe7) *)
   := (Const WO~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~0~0~1~1~1).
 Notation "'0b1111111111111111101101'" (* 4194285 (0x3fffed) *)
   := (Const WO~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~0~1~1~0~1).
+Notation "'0b1111111111111111101110'" (* 4194286 (0x3fffee) *)
+  := (Const WO~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~0~1~1~1~0).
 Notation "'0b1111111111111111101111'" (* 4194287 (0x3fffef) *)
   := (Const WO~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~0~1~1~1~1).
 Notation "'0b1111111111111111110101'" (* 4194293 (0x3ffff5) *)
@@ -1075,10 +1086,16 @@ Notation "'0b1000000000000000000000000'" (* 16777216 (0x1000000) *)
   := (Const WO~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~0).
 Notation "'0b1000000000000000000000001'" (* 16777217 (0x1000001) *)
   := (Const WO~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~1).
+Notation "'0b1011000011111111111111110'" (* 23199742 (0x161fffe) *)
+  := (Const WO~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~0).
 Notation "'0b1111111011111111111111110'" (* 33423358 (0x1fdfffe) *)
   := (Const WO~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~0).
+Notation "'0b1111111111111010111111110'" (* 33551870 (0x1fff5fe) *)
+  := (Const WO~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~0).
 Notation "'0b1111111111111111111001010'" (* 33554378 (0x1ffffca) *)
   := (Const WO~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~0~0~1~0~1~0).
+Notation "'0b1111111111111111111001110'" (* 33554382 (0x1ffffce) *)
+  := (Const WO~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~0~0~1~1~1~0).
 Notation "'0b1111111111111111111011110'" (* 33554398 (0x1ffffde) *)
   := (Const WO~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~0~1~1~1~1~0).
 Notation "'0b1111111111111111111011111'" (* 33554399 (0x1ffffdf) *)
@@ -1129,6 +1146,8 @@ Notation "'0b100000000000000000000000000'" (* 67108864 (0x4000000) *)
   := (Const WO~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~0~0).
 Notation "'0b100000000000000000000000001'" (* 67108865 (0x4000001) *)
   := (Const WO~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~0~1).
+Notation "'0b111111111111111111111000010'" (* 134217666 (0x7ffffc2) *)
+  := (Const WO~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~0).
 Notation "'0b111111111111111111111011010'" (* 134217690 (0x7ffffda) *)
   := (Const WO~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~1~1~0~1~0).
 Notation "'0b111111111111111111111011110'" (* 134217694 (0x7ffffde) *)
@@ -1149,6 +1168,8 @@ Notation "'0b111111111111111111111110110'" (* 134217718 (0x7fffff6) *)
   := (Const WO~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~0~1~1~0).
 Notation "'0b111111111111111111111110111'" (* 134217719 (0x7fffff7) *)
   := (Const WO~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~0~1~1~1).
+Notation "'0b111111111111111111111111100'" (* 134217724 (0x7fffffc) *)
+  := (Const WO~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~0~0).
 Notation "'0b111111111111111111111111110'" (* 134217726 (0x7fffffe) *)
   := (Const WO~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~0).
 Notation "'0b111111111111111111111111111'" (* 134217727 (0x7ffffff) *)
@@ -1193,6 +1214,8 @@ Notation "'0b11111111111111111111111111010'" (* 536870906 (0x1ffffffa) *)
   := (Const WO~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~0~1~0).
 Notation "'0b11111111111111111111111111011'" (* 536870907 (0x1ffffffb) *)
   := (Const WO~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~0~1~1).
+Notation "'0b11111111111111111111111111100'" (* 536870908 (0x1ffffffc) *)
+  := (Const WO~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~0~0).
 Notation "'0b11111111111111111111111111101'" (* 536870909 (0x1ffffffd) *)
   := (Const WO~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~0~1).
 Notation "'0b11111111111111111111111111110'" (* 536870910 (0x1ffffffe) *)
@@ -1239,6 +1262,8 @@ 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 "'0b1111111111111111111111111111010'" (* 2147483642 (0x7ffffffa) *)
   := (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~0~1~0).
+Notation "'0b1111111111111111111111111111100'" (* 2147483644 (0x7ffffffc) *)
+  := (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~0~0).
 Notation "'0b1111111111111111111111111111110'" (* 2147483646 (0x7ffffffe) *)
   := (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~0).
 Notation "'0b1111111111111111111111111111111'" (* 2147483647 (0x7fffffff) *)
@@ -1295,6 +1320,8 @@ Notation "'0b11111111111111111111111110001011'" (* 4294967179 (0xffffff8b) *)
   := (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~0~0~0~1~0~1~1).
 Notation "'0b11111111111111111111111110010111'" (* 4294967191 (0xffffff97) *)
   := (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~0~0~1~0~1~1~1).
+Notation "'0b11111111111111111111111111011110'" (* 4294967262 (0xffffffde) *)
+  := (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~0~1~1~1~1~0).
 Notation "'0b11111111111111111111111111011111'" (* 4294967263 (0xffffffdf) *)
   := (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~0~1~1~1~1~1).
 Notation "'0b11111111111111111111111111100001'" (* 4294967265 (0xffffffe1) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index c09158bad..6607831d4 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -81,6 +81,7 @@ nums = tuple(sorted(set(systematic_nums + [
     4194275,
     4194279,
     4194285,
+    4194286,
     4194287,
     4194293,
     4194302,
@@ -113,8 +114,11 @@ nums = tuple(sorted(set(systematic_nums + [
     16777212,
     16777213,
     16777214,
+    23199742,
     33423358,
+    33551870,
     33554378,
+    33554382,
     33554398,
     33554399,
     33554413,
@@ -134,6 +138,7 @@ nums = tuple(sorted(set(systematic_nums + [
     67108859,
     67108861,
     67108862,
+    134217666,
     134217690,
     134217694,
     134217697,
@@ -144,6 +149,7 @@ nums = tuple(sorted(set(systematic_nums + [
     134217713,
     134217718,
     134217719,
+    134217724,
     134217726,
     268431360,
     268435398,
@@ -160,6 +166,7 @@ nums = tuple(sorted(set(systematic_nums + [
     536870893,
     536870906,
     536870907,
+    536870908,
     536870909,
     536870910,
     678152731,
@@ -177,6 +184,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2147418110,
     2147483631,
     2147483642,
+    2147483644,
     2147483646,
     2147483647,
     2863311531,
@@ -203,6 +211,7 @@ nums = tuple(sorted(set(systematic_nums + [
     4294967109,
     4294967179,
     4294967191,
+    4294967262,
     4294967263,
     4294967265,
     4294967267,
@@ -1469,6 +1478,10 @@ Notation "'0x3fffed'" (* 4194285 (0x3fffed) *)
   := (Const 4194285%Z).
 Notation "'0x3fffed'" (* 4194285 (0x3fffed) *)
   := (Const WO~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~0~1~1~0~1).
+Notation "'0x3fffee'" (* 4194286 (0x3fffee) *)
+  := (Const 4194286%Z).
+Notation "'0x3fffee'" (* 4194286 (0x3fffee) *)
+  := (Const WO~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~0~1~1~1~0).
 Notation "'0x3fffef'" (* 4194287 (0x3fffef) *)
   := (Const 4194287%Z).
 Notation "'0x3fffef'" (* 4194287 (0x3fffef) *)
@@ -1633,14 +1646,26 @@ Notation "'0x1000001'" (* 16777217 (0x1000001) *)
   := (Const 16777217%Z).
 Notation "'0x1000001'" (* 16777217 (0x1000001) *)
   := (Const WO~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~1).
+Notation "'0x161fffe'" (* 23199742 (0x161fffe) *)
+  := (Const 23199742%Z).
+Notation "'0x161fffe'" (* 23199742 (0x161fffe) *)
+  := (Const WO~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~0).
 Notation "'0x1fdfffe'" (* 33423358 (0x1fdfffe) *)
   := (Const 33423358%Z).
 Notation "'0x1fdfffe'" (* 33423358 (0x1fdfffe) *)
   := (Const WO~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~0).
+Notation "'0x1fff5fe'" (* 33551870 (0x1fff5fe) *)
+  := (Const 33551870%Z).
+Notation "'0x1fff5fe'" (* 33551870 (0x1fff5fe) *)
+  := (Const WO~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~0).
 Notation "'0x1ffffca'" (* 33554378 (0x1ffffca) *)
   := (Const 33554378%Z).
 Notation "'0x1ffffca'" (* 33554378 (0x1ffffca) *)
   := (Const WO~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~0~0~1~0~1~0).
+Notation "'0x1ffffce'" (* 33554382 (0x1ffffce) *)
+  := (Const 33554382%Z).
+Notation "'0x1ffffce'" (* 33554382 (0x1ffffce) *)
+  := (Const WO~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~0~0~1~1~1~0).
 Notation "'0x1ffffde'" (* 33554398 (0x1ffffde) *)
   := (Const 33554398%Z).
 Notation "'0x1ffffde'" (* 33554398 (0x1ffffde) *)
@@ -1741,6 +1766,10 @@ Notation "'0x4000001'" (* 67108865 (0x4000001) *)
   := (Const 67108865%Z).
 Notation "'0x4000001'" (* 67108865 (0x4000001) *)
   := (Const WO~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~0~1).
+Notation "'0x7ffffc2'" (* 134217666 (0x7ffffc2) *)
+  := (Const 134217666%Z).
+Notation "'0x7ffffc2'" (* 134217666 (0x7ffffc2) *)
+  := (Const WO~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~0).
 Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
   := (Const 134217690%Z).
 Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
@@ -1781,6 +1810,10 @@ Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *)
   := (Const 134217719%Z).
 Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *)
   := (Const WO~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~0~1~1~1).
+Notation "'0x7fffffc'" (* 134217724 (0x7fffffc) *)
+  := (Const 134217724%Z).
+Notation "'0x7fffffc'" (* 134217724 (0x7fffffc) *)
+  := (Const WO~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~0~0).
 Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *)
   := (Const 134217726%Z).
 Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *)
@@ -1869,6 +1902,10 @@ Notation "'0x1ffffffb'" (* 536870907 (0x1ffffffb) *)
   := (Const 536870907%Z).
 Notation "'0x1ffffffb'" (* 536870907 (0x1ffffffb) *)
   := (Const WO~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~0~1~1).
+Notation "'0x1ffffffc'" (* 536870908 (0x1ffffffc) *)
+  := (Const 536870908%Z).
+Notation "'0x1ffffffc'" (* 536870908 (0x1ffffffc) *)
+  := (Const WO~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~0~0).
 Notation "'0x1ffffffd'" (* 536870909 (0x1ffffffd) *)
   := (Const 536870909%Z).
 Notation "'0x1ffffffd'" (* 536870909 (0x1ffffffd) *)
@@ -1961,6 +1998,10 @@ Notation "'0x7ffffffa'" (* 2147483642 (0x7ffffffa) *)
   := (Const 2147483642%Z).
 Notation "'0x7ffffffa'" (* 2147483642 (0x7ffffffa) *)
   := (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~0~1~0).
+Notation "'0x7ffffffc'" (* 2147483644 (0x7ffffffc) *)
+  := (Const 2147483644%Z).
+Notation "'0x7ffffffc'" (* 2147483644 (0x7ffffffc) *)
+  := (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~0~0).
 Notation "'0x7ffffffe'" (* 2147483646 (0x7ffffffe) *)
   := (Const 2147483646%Z).
 Notation "'0x7ffffffe'" (* 2147483646 (0x7ffffffe) *)
@@ -2073,6 +2114,10 @@ Notation "'0xffffff97'" (* 4294967191 (0xffffff97) *)
   := (Const 4294967191%Z).
 Notation "'0xffffff97'" (* 4294967191 (0xffffff97) *)
   := (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~0~0~1~0~1~1~1).
+Notation "'0xffffffde'" (* 4294967262 (0xffffffde) *)
+  := (Const 4294967262%Z).
+Notation "'0xffffffde'" (* 4294967262 (0xffffffde) *)
+  := (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~0~1~1~1~1~0).
 Notation "'0xffffffdf'" (* 4294967263 (0xffffffdf) *)
   := (Const 4294967263%Z).
 Notation "'0xffffffdf'" (* 4294967263 (0xffffffdf) *)