Add more constant notations

2 files changed, 136 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index cff3f5ae1..cf188caaf 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -23,6 +23,7 @@ nums = tuple(sorted(set(systematic_nums + [
     765,
     977,
     5311,
+    32765,
     65531,
     114687,
     121665,
@@ -45,10 +46,14 @@ nums = tuple(sorted(set(systematic_nums + [
     1048557,
     1048559,
     1048573,
+    2094335,
+    2096127,
     2096128,
     2097127,
     2097135,
     2097143,
+    4193327,
+    4193539,
     4193987,
     4194115,
     4194275,
@@ -80,6 +85,7 @@ nums = tuple(sorted(set(systematic_nums + [
     67108833,
     67108845,
     67108847,
+    67108849,
     67108855,
     67108859,
     67108861,
@@ -94,6 +100,7 @@ nums = tuple(sorted(set(systematic_nums + [
     268431360,
     268435441,
     268435445,
+    268435453,
     268435454,
     536870893,
     536870906,
@@ -103,12 +110,14 @@ nums = tuple(sorted(set(systematic_nums + [
     678152731,
     954437177,
     1065418751,
+    1073709055,
     1073741821,
     1073741822,
     1332920885,
     1749801491,
     2147483647,
     2863311531,
+    2969567231,
     3123612579,
     3264175145,
     3303820997,
@@ -117,15 +126,23 @@ nums = tuple(sorted(set(systematic_nums + [
     4008636143,
     4042322161,
     4289200127,
+    4294639615,
+    4294901759,
     4294963199,
     4294966319,
     4294966531,
+    4294966875,
+    4294966979,
     4294967107,
+    4294967109,
     4294967179,
+    4294967191,
     4294967263,
+    4294967265,
     4294967267,
     4294967269,
     4294967271,
+    4294967275,
     4294967277,
     4294967279,
     4294967281,
@@ -668,6 +685,8 @@ Notation "'0b100000000000000'" (* 16384 (0x4000) *)
   := (Const WO~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b100000000000001'" (* 16385 (0x4001) *)
   := (Const WO~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b111111111111101'" (* 32765 (0x7ffd) *)
+  := (Const WO~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
 Notation "'0b111111111111111'" (* 32767 (0x7fff) *)
   := (Const WO~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1000000000000000'" (* 32768 (0x8000) *)
@@ -748,6 +767,10 @@ Notation "'0b100000000000000000000'" (* 1048576 (0x100000) *)
   := (Const WO~0~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).
 Notation "'0b100000000000000000001'" (* 1048577 (0x100001) *)
   := (Const WO~0~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~1).
+Notation "'0b111111111010011111111'" (* 2094335 (0x1ff4ff) *)
+  := (Const WO~0~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).
+Notation "'0b111111111101111111111'" (* 2096127 (0x1ffbff) *)
+  := (Const WO~0~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).
 Notation "'0b111111111110000000000'" (* 2096128 (0x1ffc00) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b111111111111111100111'" (* 2097127 (0x1fffe7) *)
@@ -762,6 +785,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 "'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) *)
+  := (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~1~0~0~0~0~0~0~1~1).
 Notation "'0b1111111111111011000011'" (* 4193987 (0x3ffec3) *)
   := (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~0~1~1~0~0~0~0~1~1).
 Notation "'0b1111111111111101000011'" (* 4194115 (0x3fff43) *)
@@ -848,6 +875,8 @@ Notation "'0b11111111111111111111101101'" (* 67108845 (0x3ffffed) *)
   := (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~1~1~0~1).
 Notation "'0b11111111111111111111101111'" (* 67108847 (0x3ffffef) *)
   := (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~1~1~1~1).
+Notation "'0b11111111111111111111110001'" (* 67108849 (0x3fffff1) *)
+  := (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~1~0~0~0~1).
 Notation "'0b11111111111111111111110111'" (* 67108855 (0x3fffff7) *)
   := (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~1~0~1~1~1).
 Notation "'0b11111111111111111111111011'" (* 67108859 (0x3fffffb) *)
@@ -888,6 +917,8 @@ Notation "'0b1111111111111111111111110001'" (* 268435441 (0xffffff1) *)
   := (Const WO~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~0~0~0~1).
 Notation "'0b1111111111111111111111110101'" (* 268435445 (0xffffff5) *)
   := (Const WO~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~0~1~0~1).
+Notation "'0b1111111111111111111111111101'" (* 268435453 (0xffffffd) *)
+  := (Const WO~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~1).
 Notation "'0b1111111111111111111111111110'" (* 268435454 (0xffffffe) *)
   := (Const WO~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~0).
 Notation "'0b1111111111111111111111111111'" (* 268435455 (0xfffffff) *)
@@ -918,6 +949,8 @@ Notation "'0b111000111000111000111000111001'" (* 954437177 (0x38e38e39) *)
   := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1).
 Notation "'0b111111100000001111111111111111'" (* 1065418751 (0x3f80ffff) *)
   := (Const WO~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~1~1~1~1~1~1~1).
+Notation "'0b111111111111110111111111111111'" (* 1073709055 (0x3fff7fff) *)
+  := (Const WO~0~0~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).
 Notation "'0b111111111111111111111111111101'" (* 1073741821 (0x3ffffffd) *)
   := (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~0~1).
 Notation "'0b111111111111111111111111111110'" (* 1073741822 (0x3ffffffe) *)
@@ -940,6 +973,8 @@ 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 "'0b10101010101010101010101010101011'" (* 2863311531 (0xaaaaaaab) *)
   := (Const WO~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~1).
+Notation "'0b10110000111111111111111111111111'" (* 2969567231 (0xb0ffffff) *)
+  := (Const WO~1~0~1~1~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).
 Notation "'0b10111010001011101000101110100011'" (* 3123612579 (0xba2e8ba3) *)
   := (Const WO~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~1).
 Notation "'0b11000010100011110101110000101001'" (* 3264175145 (0xc28f5c29) *)
@@ -956,24 +991,40 @@ Notation "'0b11110000111100001111000011110001'" (* 4042322161 (0xf0f0f0f1) *)
   := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1).
 Notation "'0b11111111101001111111111111111111'" (* 4289200127 (0xffa7ffff) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111110101111111111111111'" (* 4294639615 (0xfffaffff) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111111101111111111111111'" (* 4294901759 (0xfffeffff) *)
+  := (Const WO~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).
 Notation "'0b11111111111111111110111111111111'" (* 4294963199 (0xffffefff) *)
   := (Const WO~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).
 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 "'0b11111111111111111111110100000011'" (* 4294966531 (0xfffffd03) *)
   := (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~1~0~0~0~0~0~0~1~1).
+Notation "'0b11111111111111111111111001011011'" (* 4294966875 (0xfffffe5b) *)
+  := (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~0~0~1~0~1~1~0~1~1).
+Notation "'0b11111111111111111111111011000011'" (* 4294966979 (0xfffffec3) *)
+  := (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~0~1~1~0~0~0~0~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 "'0b11111111111111111111111101000101'" (* 4294967109 (0xffffff45) *)
+  := (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~1~0~1).
 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 "'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) *)
+  := (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~0~0~1).
 Notation "'0b11111111111111111111111111100011'" (* 4294967267 (0xffffffe3) *)
   := (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~0~1~1).
 Notation "'0b11111111111111111111111111100101'" (* 4294967269 (0xffffffe5) *)
   := (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~0~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 "'0b11111111111111111111111111101011'" (* 4294967275 (0xffffffeb) *)
+  := (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~1~0~1~1).
 Notation "'0b11111111111111111111111111101101'" (* 4294967277 (0xffffffed) *)
   := (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~1~1~0~1).
 Notation "'0b11111111111111111111111111101111'" (* 4294967279 (0xffffffef) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 7889b2a28..f1c7d111b 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -23,6 +23,7 @@ nums = tuple(sorted(set(systematic_nums + [
     765,
     977,
     5311,
+    32765,
     65531,
     114687,
     121665,
@@ -45,10 +46,14 @@ nums = tuple(sorted(set(systematic_nums + [
     1048557,
     1048559,
     1048573,
+    2094335,
+    2096127,
     2096128,
     2097127,
     2097135,
     2097143,
+    4193327,
+    4193539,
     4193987,
     4194115,
     4194275,
@@ -80,6 +85,7 @@ nums = tuple(sorted(set(systematic_nums + [
     67108833,
     67108845,
     67108847,
+    67108849,
     67108855,
     67108859,
     67108861,
@@ -94,6 +100,7 @@ nums = tuple(sorted(set(systematic_nums + [
     268431360,
     268435441,
     268435445,
+    268435453,
     268435454,
     536870893,
     536870906,
@@ -103,12 +110,14 @@ nums = tuple(sorted(set(systematic_nums + [
     678152731,
     954437177,
     1065418751,
+    1073709055,
     1073741821,
     1073741822,
     1332920885,
     1749801491,
     2147483647,
     2863311531,
+    2969567231,
     3123612579,
     3264175145,
     3303820997,
@@ -117,15 +126,23 @@ nums = tuple(sorted(set(systematic_nums + [
     4008636143,
     4042322161,
     4289200127,
+    4294639615,
+    4294901759,
     4294963199,
     4294966319,
     4294966531,
+    4294966875,
+    4294966979,
     4294967107,
+    4294967109,
     4294967179,
+    4294967191,
     4294967263,
+    4294967265,
     4294967267,
     4294967269,
     4294967271,
+    4294967275,
     4294967277,
     4294967279,
     4294967281,
@@ -986,6 +1003,10 @@ Notation "'0x4001'" (* 16385 (0x4001) *)
   := (Const 16385%Z).
 Notation "'0x4001'" (* 16385 (0x4001) *)
   := (Const WO~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x7ffd'" (* 32765 (0x7ffd) *)
+  := (Const 32765%Z).
+Notation "'0x7ffd'" (* 32765 (0x7ffd) *)
+  := (Const WO~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
 Notation "'0x7fff'" (* 32767 (0x7fff) *)
   := (Const 32767%Z).
 Notation "'0x7fff'" (* 32767 (0x7fff) *)
@@ -1146,6 +1167,14 @@ Notation "'0x100001'" (* 1048577 (0x100001) *)
   := (Const 1048577%Z).
 Notation "'0x100001'" (* 1048577 (0x100001) *)
   := (Const WO~0~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~1).
+Notation "'0x1ff4ff'" (* 2094335 (0x1ff4ff) *)
+  := (Const 2094335%Z).
+Notation "'0x1ff4ff'" (* 2094335 (0x1ff4ff) *)
+  := (Const WO~0~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).
+Notation "'0x1ffbff'" (* 2096127 (0x1ffbff) *)
+  := (Const 2096127%Z).
+Notation "'0x1ffbff'" (* 2096127 (0x1ffbff) *)
+  := (Const WO~0~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).
 Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
   := (Const 2096128%Z).
 Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
@@ -1174,6 +1203,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 "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *)
+  := (Const 4193327%Z).
+Notation "'0x3ffc2f'" (* 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 "'0x3ffd03'" (* 4193539 (0x3ffd03) *)
+  := (Const 4193539%Z).
+Notation "'0x3ffd03'" (* 4193539 (0x3ffd03) *)
+  := (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~1~0~0~0~0~0~0~1~1).
 Notation "'0x3ffec3'" (* 4193987 (0x3ffec3) *)
   := (Const 4193987%Z).
 Notation "'0x3ffec3'" (* 4193987 (0x3ffec3) *)
@@ -1346,6 +1383,10 @@ Notation "'0x3ffffef'" (* 67108847 (0x3ffffef) *)
   := (Const 67108847%Z).
 Notation "'0x3ffffef'" (* 67108847 (0x3ffffef) *)
   := (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~1~1~1~1).
+Notation "'0x3fffff1'" (* 67108849 (0x3fffff1) *)
+  := (Const 67108849%Z).
+Notation "'0x3fffff1'" (* 67108849 (0x3fffff1) *)
+  := (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~1~0~0~0~1).
 Notation "'0x3fffff7'" (* 67108855 (0x3fffff7) *)
   := (Const 67108855%Z).
 Notation "'0x3fffff7'" (* 67108855 (0x3fffff7) *)
@@ -1426,6 +1467,10 @@ Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
   := (Const 268435445%Z).
 Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
   := (Const WO~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~0~1~0~1).
+Notation "'0xffffffd'" (* 268435453 (0xffffffd) *)
+  := (Const 268435453%Z).
+Notation "'0xffffffd'" (* 268435453 (0xffffffd) *)
+  := (Const WO~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~1).
 Notation "'0xffffffe'" (* 268435454 (0xffffffe) *)
   := (Const 268435454%Z).
 Notation "'0xffffffe'" (* 268435454 (0xffffffe) *)
@@ -1486,6 +1531,10 @@ Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *)
   := (Const 1065418751%Z).
 Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *)
   := (Const WO~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~1~1~1~1~1~1~1).
+Notation "'0x3fff7fff'" (* 1073709055 (0x3fff7fff) *)
+  := (Const 1073709055%Z).
+Notation "'0x3fff7fff'" (* 1073709055 (0x3fff7fff) *)
+  := (Const WO~0~0~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).
 Notation "'0x3ffffffd'" (* 1073741821 (0x3ffffffd) *)
   := (Const 1073741821%Z).
 Notation "'0x3ffffffd'" (* 1073741821 (0x3ffffffd) *)
@@ -1530,6 +1579,10 @@ Notation "'0xaaaaaaab'" (* 2863311531 (0xaaaaaaab) *)
   := (Const 2863311531%Z).
 Notation "'0xaaaaaaab'" (* 2863311531 (0xaaaaaaab) *)
   := (Const WO~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~1).
+Notation "'0xb0ffffff'" (* 2969567231 (0xb0ffffff) *)
+  := (Const 2969567231%Z).
+Notation "'0xb0ffffff'" (* 2969567231 (0xb0ffffff) *)
+  := (Const WO~1~0~1~1~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).
 Notation "'0xba2e8ba3'" (* 3123612579 (0xba2e8ba3) *)
   := (Const 3123612579%Z).
 Notation "'0xba2e8ba3'" (* 3123612579 (0xba2e8ba3) *)
@@ -1562,6 +1615,14 @@ Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *)
   := (Const 4289200127%Z).
 Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xfffaffff'" (* 4294639615 (0xfffaffff) *)
+  := (Const 4294639615%Z).
+Notation "'0xfffaffff'" (* 4294639615 (0xfffaffff) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0xfffeffff'" (* 4294901759 (0xfffeffff) *)
+  := (Const 4294901759%Z).
+Notation "'0xfffeffff'" (* 4294901759 (0xfffeffff) *)
+  := (Const WO~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).
 Notation "'0xffffefff'" (* 4294963199 (0xffffefff) *)
   := (Const 4294963199%Z).
 Notation "'0xffffefff'" (* 4294963199 (0xffffefff) *)
@@ -1574,18 +1635,38 @@ Notation "'0xfffffd03'" (* 4294966531 (0xfffffd03) *)
   := (Const 4294966531%Z).
 Notation "'0xfffffd03'" (* 4294966531 (0xfffffd03) *)
   := (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~1~0~0~0~0~0~0~1~1).
+Notation "'0xfffffe5b'" (* 4294966875 (0xfffffe5b) *)
+  := (Const 4294966875%Z).
+Notation "'0xfffffe5b'" (* 4294966875 (0xfffffe5b) *)
+  := (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~0~0~1~0~1~1~0~1~1).
+Notation "'0xfffffec3'" (* 4294966979 (0xfffffec3) *)
+  := (Const 4294966979%Z).
+Notation "'0xfffffec3'" (* 4294966979 (0xfffffec3) *)
+  := (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~0~1~1~0~0~0~0~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 "'0xffffff45'" (* 4294967109 (0xffffff45) *)
+  := (Const 4294967109%Z).
+Notation "'0xffffff45'" (* 4294967109 (0xffffff45) *)
+  := (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~1~0~1).
 Notation "'0xffffff8b'" (* 4294967179 (0xffffff8b) *)
   := (Const 4294967179%Z).
 Notation "'0xffffff8b'" (* 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 "'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 "'0xffffffdf'" (* 4294967263 (0xffffffdf) *)
   := (Const 4294967263%Z).
 Notation "'0xffffffdf'" (* 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 "'0xffffffe1'" (* 4294967265 (0xffffffe1) *)
+  := (Const 4294967265%Z).
+Notation "'0xffffffe1'" (* 4294967265 (0xffffffe1) *)
+  := (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~0~0~1).
 Notation "'0xffffffe3'" (* 4294967267 (0xffffffe3) *)
   := (Const 4294967267%Z).
 Notation "'0xffffffe3'" (* 4294967267 (0xffffffe3) *)
@@ -1598,6 +1679,10 @@ 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 "'0xffffffeb'" (* 4294967275 (0xffffffeb) *)
+  := (Const 4294967275%Z).
+Notation "'0xffffffeb'" (* 4294967275 (0xffffffeb) *)
+  := (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~1~0~1~1).
 Notation "'0xffffffed'" (* 4294967277 (0xffffffed) *)
   := (Const 4294967277%Z).
 Notation "'0xffffffed'" (* 4294967277 (0xffffffed) *)