Add more constant notations

2 files changed, 104 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index f18efd962..5e33f403e 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -150,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [
     67108849,
     67108854,
     67108855,
+    67108858,
     67108859,
     67108861,
     67108862,
@@ -176,6 +177,7 @@ nums = tuple(sorted(set(systematic_nums + [
     268435441,
     268435443,
     268435445,
+    268435451,
     268435452,
     268435453,
     268435454,
@@ -183,6 +185,7 @@ nums = tuple(sorted(set(systematic_nums + [
     536870886,
     536870890,
     536870893,
+    536870902,
     536870906,
     536870907,
     536870908,
@@ -298,22 +301,30 @@ nums = tuple(sorted(set(systematic_nums + [
     2199023255543,
     2199023255550,
     4363955208191,
+    4398046510080,
     4398046511079,
     4398046511086,
+    4398046511095,
     4398046511099,
     4398046511102,
     8727910416382,
+    8791798053935,
     8796090925055,
     8796093021443,
+    8796093022019,
     8796093022158,
     8796093022179,
     8796093022183,
     8796093022189,
+    8796093022190,
     8796093022193,
     8796093022198,
     8796093022205,
     8796093022206,
+    17583596107870,
     17592181850110,
+    17592186042886,
+    17592186044038,
     17592186044358,
     17592186044366,
     17592186044378,
@@ -373,11 +384,13 @@ nums = tuple(sorted(set(systematic_nums + [
     562949953421279,
     562949953421290,
     562949953421293,
+    562949953421294,
     562949953421297,
     562949953421303,
     562949953421310,
     1125899873288191,
     1125899906842558,
+    1125899906842586,
     1125899906842593,
     1125899906842594,
     1125899906842606,
@@ -1232,6 +1245,8 @@ Notation "'0b11111111111111111111110110'" (* 67108854 (0x3fffff6) *)
   := (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~0).
 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 "'0b11111111111111111111111010'" (* 67108858 (0x3fffffa) *)
+  := (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~1~0~1~0).
 Notation "'0b11111111111111111111111011'" (* 67108859 (0x3fffffb) *)
   := (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~1~0~1~1).
 Notation "'0b11111111111111111111111101'" (* 67108861 (0x3fffffd) *)
@@ -1296,6 +1311,8 @@ Notation "'0b1111111111111111111111110011'" (* 268435443 (0xffffff3) *)
   := (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~1~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 "'0b1111111111111111111111111011'" (* 268435451 (0xffffffb) *)
+  := (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~0~1~1).
 Notation "'0b1111111111111111111111111100'" (* 268435452 (0xffffffc) *)
   := (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~0).
 Notation "'0b1111111111111111111111111101'" (* 268435453 (0xffffffd) *)
@@ -1316,6 +1333,8 @@ Notation "'0b11111111111111111111111101010'" (* 536870890 (0x1fffffea) *)
   := (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~0~1~0~1~0).
 Notation "'0b11111111111111111111111101101'" (* 536870893 (0x1fffffed) *)
   := (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~0~1~1~0~1).
+Notation "'0b11111111111111111111111110110'" (* 536870902 (0x1ffffff6) *)
+  := (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~0~1~1~0).
 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) *)
@@ -1622,10 +1641,14 @@ Notation "'0b100000000000000000000000000000000000000001'" (* 2199023255553 (0x20
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
 Notation "'0b111111100000001111111111111111111111111111'" (* 4363955208191 (0x3f80fffffff) *)
   := (Const WO~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~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).
+Notation "'0b111111111111111111111111111111110000000000'" (* 4398046510080 (0x3fffffffc00) *)
+  := (Const WO~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~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b111111111111111111111111111111111111100111'" (* 4398046511079 (0x3ffffffffe7) *)
   := (Const WO~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~0~1~1~1).
 Notation "'0b111111111111111111111111111111111111101110'" (* 4398046511086 (0x3ffffffffee) *)
   := (Const WO~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~0).
+Notation "'0b111111111111111111111111111111111111110111'" (* 4398046511095 (0x3fffffffff7) *)
+  := (Const WO~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~0~1~1~1).
 Notation "'0b111111111111111111111111111111111111111011'" (* 4398046511099 (0x3fffffffffb) *)
   := (Const WO~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~0~1~1).
 Notation "'0b111111111111111111111111111111111111111110'" (* 4398046511102 (0x3fffffffffe) *)
@@ -1638,10 +1661,14 @@ Notation "'0b1000000000000000000000000000000000000000001'" (* 4398046511105 (0x4
   := (Const WO~0~0~0~0~0~0~0~0~0~0~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
 Notation "'0b1111111000000011111111111111111111111111110'" (* 8727910416382 (0x7f01ffffffe) *)
   := (Const WO~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~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~0).
+Notation "'0b1111111111011111111111111111111110000101111'" (* 8791798053935 (0x7fefffffc2f) *)
+  := (Const WO~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~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~0~1~0~1~1~1~1).
 Notation "'0b1111111111111111111110111111111111111111111'" (* 8796090925055 (0x7ffffdfffff) *)
   := (Const WO~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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b1111111111111111111111111111111110100000011'" (* 8796093021443 (0x7fffffffd03) *)
   := (Const WO~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~0~1~0~0~0~0~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111101000011'" (* 8796093022019 (0x7ffffffff43) *)
+  := (Const WO~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~0~1~0~0~0~0~1~1).
 Notation "'0b1111111111111111111111111111111111111001110'" (* 8796093022158 (0x7ffffffffce) *)
   := (Const WO~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~0~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111111100011'" (* 8796093022179 (0x7ffffffffe3) *)
@@ -1650,6 +1677,8 @@ Notation "'0b1111111111111111111111111111111111111100111'" (* 8796093022183 (0x7
   := (Const WO~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~0~0~1~1~1).
 Notation "'0b1111111111111111111111111111111111111101101'" (* 8796093022189 (0x7ffffffffed) *)
   := (Const WO~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~0~1~1~0~1).
+Notation "'0b1111111111111111111111111111111111111101110'" (* 8796093022190 (0x7ffffffffee) *)
+  := (Const WO~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~0~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111111110001'" (* 8796093022193 (0x7fffffffff1) *)
   := (Const WO~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~0~0~0~1).
 Notation "'0b1111111111111111111111111111111111111110110'" (* 8796093022198 (0x7fffffffff6) *)
@@ -1664,8 +1693,14 @@ Notation "'0b10000000000000000000000000000000000000000000'" (* 8796093022208 (0x
   := (Const WO~0~0~0~0~0~0~0~0~0~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b10000000000000000000000000000000000000000001'" (* 8796093022209 (0x80000000001) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b11111111110111111111111111111111100001011110'" (* 17583596107870 (0xffdfffff85e) *)
+  := (Const WO~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~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~0~1~0~1~1~1~1~0).
 Notation "'0b11111111111111111111101111111111111111111110'" (* 17592181850110 (0xfffffbffffe) *)
   := (Const WO~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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111101000000110'" (* 17592186042886 (0xffffffffa06) *)
+  := (Const WO~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~0~1~0~0~0~0~0~0~1~1~0).
+Notation "'0b11111111111111111111111111111111111010000110'" (* 17592186044038 (0xffffffffe86) *)
+  := (Const WO~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~0~1~0~0~0~0~1~1~0).
 Notation "'0b11111111111111111111111111111111111111000110'" (* 17592186044358 (0xfffffffffc6) *)
   := (Const WO~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~0~0~0~1~1~0).
 Notation "'0b11111111111111111111111111111111111111001110'" (* 17592186044366 (0xfffffffffce) *)
@@ -1814,6 +1849,8 @@ Notation "'0b1111111111111111111111111111111111111111111101010'" (* 562949953421
   := (Const WO~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~1~1~1~1~0~1~0~1~0).
 Notation "'0b1111111111111111111111111111111111111111111101101'" (* 562949953421293 (0x1ffffffffffed) *)
   := (Const WO~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~1~1~1~1~0~1~1~0~1).
+Notation "'0b1111111111111111111111111111111111111111111101110'" (* 562949953421294 (0x1ffffffffffee) *)
+  := (Const WO~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~1~1~1~1~0~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111111111111110001'" (* 562949953421297 (0x1fffffffffff1) *)
   := (Const WO~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~1~1~1~1~1~0~0~0~1).
 Notation "'0b1111111111111111111111111111111111111111111110111'" (* 562949953421303 (0x1fffffffffff7) *)
@@ -1830,6 +1867,8 @@ Notation "'0b11111111111111111111111101111111111111111111111111'" (* 11258998732
   := (Const WO~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~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).
 Notation "'0b11111111111111111111111111111111111111111110111110'" (* 1125899906842558 (0x3ffffffffffbe) *)
   := (Const WO~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~1~1~1~0~1~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111111011010'" (* 1125899906842586 (0x3ffffffffffda) *)
+  := (Const WO~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~1~1~1~1~0~1~1~0~1~0).
 Notation "'0b11111111111111111111111111111111111111111111100001'" (* 1125899906842593 (0x3ffffffffffe1) *)
   := (Const WO~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~1~1~1~1~1~0~0~0~0~1).
 Notation "'0b11111111111111111111111111111111111111111111100010'" (* 1125899906842594 (0x3ffffffffffe2) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index a5ab779cd..a1a8c9777 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -150,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [
     67108849,
     67108854,
     67108855,
+    67108858,
     67108859,
     67108861,
     67108862,
@@ -176,6 +177,7 @@ nums = tuple(sorted(set(systematic_nums + [
     268435441,
     268435443,
     268435445,
+    268435451,
     268435452,
     268435453,
     268435454,
@@ -183,6 +185,7 @@ nums = tuple(sorted(set(systematic_nums + [
     536870886,
     536870890,
     536870893,
+    536870902,
     536870906,
     536870907,
     536870908,
@@ -298,22 +301,30 @@ nums = tuple(sorted(set(systematic_nums + [
     2199023255543,
     2199023255550,
     4363955208191,
+    4398046510080,
     4398046511079,
     4398046511086,
+    4398046511095,
     4398046511099,
     4398046511102,
     8727910416382,
+    8791798053935,
     8796090925055,
     8796093021443,
+    8796093022019,
     8796093022158,
     8796093022179,
     8796093022183,
     8796093022189,
+    8796093022190,
     8796093022193,
     8796093022198,
     8796093022205,
     8796093022206,
+    17583596107870,
     17592181850110,
+    17592186042886,
+    17592186044038,
     17592186044358,
     17592186044366,
     17592186044378,
@@ -373,11 +384,13 @@ nums = tuple(sorted(set(systematic_nums + [
     562949953421279,
     562949953421290,
     562949953421293,
+    562949953421294,
     562949953421297,
     562949953421303,
     562949953421310,
     1125899873288191,
     1125899906842558,
+    1125899906842586,
     1125899906842593,
     1125899906842594,
     1125899906842606,
@@ -1870,6 +1883,10 @@ Notation "'0x3fffff7'" (* 67108855 (0x3fffff7) *)
   := (Const 67108855%Z).
 Notation "'0x3fffff7'" (* 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 "'0x3fffffa'" (* 67108858 (0x3fffffa) *)
+  := (Const 67108858%Z).
+Notation "'0x3fffffa'" (* 67108858 (0x3fffffa) *)
+  := (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~1~0~1~0).
 Notation "'0x3fffffb'" (* 67108859 (0x3fffffb) *)
   := (Const 67108859%Z).
 Notation "'0x3fffffb'" (* 67108859 (0x3fffffb) *)
@@ -1998,6 +2015,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 "'0xffffffb'" (* 268435451 (0xffffffb) *)
+  := (Const 268435451%Z).
+Notation "'0xffffffb'" (* 268435451 (0xffffffb) *)
+  := (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~0~1~1).
 Notation "'0xffffffc'" (* 268435452 (0xffffffc) *)
   := (Const 268435452%Z).
 Notation "'0xffffffc'" (* 268435452 (0xffffffc) *)
@@ -2038,6 +2059,10 @@ Notation "'0x1fffffed'" (* 536870893 (0x1fffffed) *)
   := (Const 536870893%Z).
 Notation "'0x1fffffed'" (* 536870893 (0x1fffffed) *)
   := (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~0~1~1~0~1).
+Notation "'0x1ffffff6'" (* 536870902 (0x1ffffff6) *)
+  := (Const 536870902%Z).
+Notation "'0x1ffffff6'" (* 536870902 (0x1ffffff6) *)
+  := (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~0~1~1~0).
 Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *)
   := (Const 536870906%Z).
 Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *)
@@ -2650,6 +2675,10 @@ Notation "'0x3f80fffffff'" (* 4363955208191 (0x3f80fffffff) *)
   := (Const 4363955208191%Z).
 Notation "'0x3f80fffffff'" (* 4363955208191 (0x3f80fffffff) *)
   := (Const WO~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~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).
+Notation "'0x3fffffffc00'" (* 4398046510080 (0x3fffffffc00) *)
+  := (Const 4398046510080%Z).
+Notation "'0x3fffffffc00'" (* 4398046510080 (0x3fffffffc00) *)
+  := (Const WO~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~0~0~0~0~0~0~0~0~0~0).
 Notation "'0x3ffffffffe7'" (* 4398046511079 (0x3ffffffffe7) *)
   := (Const 4398046511079%Z).
 Notation "'0x3ffffffffe7'" (* 4398046511079 (0x3ffffffffe7) *)
@@ -2658,6 +2687,10 @@ Notation "'0x3ffffffffee'" (* 4398046511086 (0x3ffffffffee) *)
   := (Const 4398046511086%Z).
 Notation "'0x3ffffffffee'" (* 4398046511086 (0x3ffffffffee) *)
   := (Const WO~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~0).
+Notation "'0x3fffffffff7'" (* 4398046511095 (0x3fffffffff7) *)
+  := (Const 4398046511095%Z).
+Notation "'0x3fffffffff7'" (* 4398046511095 (0x3fffffffff7) *)
+  := (Const WO~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~0~1~1~1).
 Notation "'0x3fffffffffb'" (* 4398046511099 (0x3fffffffffb) *)
   := (Const 4398046511099%Z).
 Notation "'0x3fffffffffb'" (* 4398046511099 (0x3fffffffffb) *)
@@ -2682,6 +2715,10 @@ Notation "'0x7f01ffffffe'" (* 8727910416382 (0x7f01ffffffe) *)
   := (Const 8727910416382%Z).
 Notation "'0x7f01ffffffe'" (* 8727910416382 (0x7f01ffffffe) *)
   := (Const WO~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~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~0).
+Notation "'0x7fefffffc2f'" (* 8791798053935 (0x7fefffffc2f) *)
+  := (Const 8791798053935%Z).
+Notation "'0x7fefffffc2f'" (* 8791798053935 (0x7fefffffc2f) *)
+  := (Const WO~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~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~0~1~0~1~1~1~1).
 Notation "'0x7ffffdfffff'" (* 8796090925055 (0x7ffffdfffff) *)
   := (Const 8796090925055%Z).
 Notation "'0x7ffffdfffff'" (* 8796090925055 (0x7ffffdfffff) *)
@@ -2690,6 +2727,10 @@ Notation "'0x7fffffffd03'" (* 8796093021443 (0x7fffffffd03) *)
   := (Const 8796093021443%Z).
 Notation "'0x7fffffffd03'" (* 8796093021443 (0x7fffffffd03) *)
   := (Const WO~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~0~1~0~0~0~0~0~0~1~1).
+Notation "'0x7ffffffff43'" (* 8796093022019 (0x7ffffffff43) *)
+  := (Const 8796093022019%Z).
+Notation "'0x7ffffffff43'" (* 8796093022019 (0x7ffffffff43) *)
+  := (Const WO~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~0~1~0~0~0~0~1~1).
 Notation "'0x7ffffffffce'" (* 8796093022158 (0x7ffffffffce) *)
   := (Const 8796093022158%Z).
 Notation "'0x7ffffffffce'" (* 8796093022158 (0x7ffffffffce) *)
@@ -2706,6 +2747,10 @@ Notation "'0x7ffffffffed'" (* 8796093022189 (0x7ffffffffed) *)
   := (Const 8796093022189%Z).
 Notation "'0x7ffffffffed'" (* 8796093022189 (0x7ffffffffed) *)
   := (Const WO~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~0~1~1~0~1).
+Notation "'0x7ffffffffee'" (* 8796093022190 (0x7ffffffffee) *)
+  := (Const 8796093022190%Z).
+Notation "'0x7ffffffffee'" (* 8796093022190 (0x7ffffffffee) *)
+  := (Const WO~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~0~1~1~1~0).
 Notation "'0x7fffffffff1'" (* 8796093022193 (0x7fffffffff1) *)
   := (Const 8796093022193%Z).
 Notation "'0x7fffffffff1'" (* 8796093022193 (0x7fffffffff1) *)
@@ -2734,10 +2779,22 @@ Notation "'0x80000000001'" (* 8796093022209 (0x80000000001) *)
   := (Const 8796093022209%Z).
 Notation "'0x80000000001'" (* 8796093022209 (0x80000000001) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xffdfffff85e'" (* 17583596107870 (0xffdfffff85e) *)
+  := (Const 17583596107870%Z).
+Notation "'0xffdfffff85e'" (* 17583596107870 (0xffdfffff85e) *)
+  := (Const WO~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~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~0~1~0~1~1~1~1~0).
 Notation "'0xfffffbffffe'" (* 17592181850110 (0xfffffbffffe) *)
   := (Const 17592181850110%Z).
 Notation "'0xfffffbffffe'" (* 17592181850110 (0xfffffbffffe) *)
   := (Const WO~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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0xffffffffa06'" (* 17592186042886 (0xffffffffa06) *)
+  := (Const 17592186042886%Z).
+Notation "'0xffffffffa06'" (* 17592186042886 (0xffffffffa06) *)
+  := (Const WO~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~0~1~0~0~0~0~0~0~1~1~0).
+Notation "'0xffffffffe86'" (* 17592186044038 (0xffffffffe86) *)
+  := (Const 17592186044038%Z).
+Notation "'0xffffffffe86'" (* 17592186044038 (0xffffffffe86) *)
+  := (Const WO~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~0~1~0~0~0~0~1~1~0).
 Notation "'0xfffffffffc6'" (* 17592186044358 (0xfffffffffc6) *)
   := (Const 17592186044358%Z).
 Notation "'0xfffffffffc6'" (* 17592186044358 (0xfffffffffc6) *)
@@ -3034,6 +3091,10 @@ Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *)
   := (Const 562949953421293%Z).
 Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *)
   := (Const WO~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~1~1~1~1~0~1~1~0~1).
+Notation "'0x1ffffffffffee'" (* 562949953421294 (0x1ffffffffffee) *)
+  := (Const 562949953421294%Z).
+Notation "'0x1ffffffffffee'" (* 562949953421294 (0x1ffffffffffee) *)
+  := (Const WO~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~1~1~1~1~0~1~1~1~0).
 Notation "'0x1fffffffffff1'" (* 562949953421297 (0x1fffffffffff1) *)
   := (Const 562949953421297%Z).
 Notation "'0x1fffffffffff1'" (* 562949953421297 (0x1fffffffffff1) *)
@@ -3066,6 +3127,10 @@ Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *)
   := (Const 1125899906842558%Z).
 Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *)
   := (Const WO~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~1~1~1~0~1~1~1~1~1~0).
+Notation "'0x3ffffffffffda'" (* 1125899906842586 (0x3ffffffffffda) *)
+  := (Const 1125899906842586%Z).
+Notation "'0x3ffffffffffda'" (* 1125899906842586 (0x3ffffffffffda) *)
+  := (Const WO~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~1~1~1~1~0~1~1~0~1~0).
 Notation "'0x3ffffffffffe1'" (* 1125899906842593 (0x3ffffffffffe1) *)
   := (Const 1125899906842593%Z).
 Notation "'0x3ffffffffffe1'" (* 1125899906842593 (0x3ffffffffffe1) *)