Add more constant notations

2 files changed, 48 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 5684885d3..5cdcd232b 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -38,6 +38,7 @@ nums = tuple(sorted(set(systematic_nums + [
     524269,
     524271,
     524279,
+    679935,
     1048471,
     1048549,
     1048557,
@@ -194,6 +195,8 @@ nums = tuple(sorted(set(systematic_nums + [
     1125899906842619,
     1125899906842621,
     1460151441686527,
+    2211942517178367,
+    2234929182146559,
     2248776156708863,
     2251799813160960,
     2251799813684483,
@@ -202,7 +205,10 @@ nums = tuple(sorted(set(systematic_nums + [
     2251799813685229,
     2251799813685239,
     4503595332402223,
+    4503599627369927,
+    4503599627370015,
     4503599627370307,
+    4503599627370309,
     4503599627370458,
     4503599627370479,
     4503599627370491,
@@ -720,6 +726,8 @@ Notation "'0b10000000000000000000'" (* 524288 (0x80000) *)
   := (Const WO~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).
 Notation "'0b10000000000000000001'" (* 524289 (0x80001) *)
   := (Const WO~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~1).
+Notation "'0b10100101111111111111'" (* 679935 (0xa5fff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b11111111111110010111'" (* 1048471 (0xfff97) *)
   := (Const WO~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~0~0~1~0~1~1~1).
 Notation "'0b11111111111111100101'" (* 1048549 (0xfffe5) *)
@@ -1216,6 +1224,10 @@ Notation "'0b100000000000000000000000000000000000000000000000001'" (* 1125899906
   := (Const WO~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~0~0~0~0~0~0~1).
 Notation "'0b101001011111111111111111111111111111111111111111111'" (* 1460151441686527 (0x52fffffffffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b111110110111011111111111111111111111111111111111111'" (* 2211942517178367 (0x7dbbfffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b111111100001010011111111111111111111111111111111111'" (* 2234929182146559 (0x7f0a7ffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~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).
 Notation "'0b111111111010011111111111111111111111111111111111111'" (* 2248776156708863 (0x7fd3fffffffff) *)
   := (Const WO~0~0~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~1~1~1~1~1~1~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 "'0b111111111111111111111111111111110000000000000000000'" (* 2251799813160960 (0x7fffffff80000) *)
@@ -1238,8 +1250,14 @@ Notation "'0b1000000000000000000000000000000000000000000000000001'" (* 225179981
   := (Const WO~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~0~0~0~0~0~0~0~1).
 Notation "'0b1111111111111111111011111111111111111111110000101111'" (* 4503595332402223 (0xffffefffffc2f) *)
   := (Const WO~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~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 "'0b1111111111111111111111111111111111111111110111000111'" (* 4503599627369927 (0xffffffffffdc7) *)
+  := (Const WO~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~0~1~1~1~0~0~0~1~1~1).
+Notation "'0b1111111111111111111111111111111111111111111000011111'" (* 4503599627370015 (0xffffffffffe1f) *)
+  := (Const WO~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~0~0~0~1~1~1~1~1).
 Notation "'0b1111111111111111111111111111111111111111111101000011'" (* 4503599627370307 (0xfffffffffff43) *)
   := (Const WO~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~0~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111101000101'" (* 4503599627370309 (0xfffffffffff45) *)
+  := (Const WO~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~0~0~1~0~1).
 Notation "'0b1111111111111111111111111111111111111111111111011010'" (* 4503599627370458 (0xfffffffffffda) *)
   := (Const WO~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~1~0~1~1~0~1~0).
 Notation "'0b1111111111111111111111111111111111111111111111101111'" (* 4503599627370479 (0xfffffffffffef) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 98f8efbd1..16e718309 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -38,6 +38,7 @@ nums = tuple(sorted(set(systematic_nums + [
     524269,
     524271,
     524279,
+    679935,
     1048471,
     1048549,
     1048557,
@@ -194,6 +195,8 @@ nums = tuple(sorted(set(systematic_nums + [
     1125899906842619,
     1125899906842621,
     1460151441686527,
+    2211942517178367,
+    2234929182146559,
     2248776156708863,
     2251799813160960,
     2251799813684483,
@@ -202,7 +205,10 @@ nums = tuple(sorted(set(systematic_nums + [
     2251799813685229,
     2251799813685239,
     4503595332402223,
+    4503599627369927,
+    4503599627370015,
     4503599627370307,
+    4503599627370309,
     4503599627370458,
     4503599627370479,
     4503599627370491,
@@ -1098,6 +1104,10 @@ Notation "'0x80001'" (* 524289 (0x80001) *)
   := (Const 524289%Z).
 Notation "'0x80001'" (* 524289 (0x80001) *)
   := (Const WO~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~1).
+Notation "'0xa5fff'" (* 679935 (0xa5fff) *)
+  := (Const 679935%Z).
+Notation "'0xa5fff'" (* 679935 (0xa5fff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0xfff97'" (* 1048471 (0xfff97) *)
   := (Const 1048471%Z).
 Notation "'0xfff97'" (* 1048471 (0xfff97) *)
@@ -2090,6 +2100,14 @@ Notation "'0x52fffffffffff'" (* 1460151441686527 (0x52fffffffffff) *)
   := (Const 1460151441686527%Z).
 Notation "'0x52fffffffffff'" (* 1460151441686527 (0x52fffffffffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x7dbbfffffffff'" (* 2211942517178367 (0x7dbbfffffffff) *)
+  := (Const 2211942517178367%Z).
+Notation "'0x7dbbfffffffff'" (* 2211942517178367 (0x7dbbfffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~0~1~1~0~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x7f0a7ffffffff'" (* 2234929182146559 (0x7f0a7ffffffff) *)
+  := (Const 2234929182146559%Z).
+Notation "'0x7f0a7ffffffff'" (* 2234929182146559 (0x7f0a7ffffffff) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~0~0~0~1~0~1~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).
 Notation "'0x7fd3fffffffff'" (* 2248776156708863 (0x7fd3fffffffff) *)
   := (Const 2248776156708863%Z).
 Notation "'0x7fd3fffffffff'" (* 2248776156708863 (0x7fd3fffffffff) *)
@@ -2134,10 +2152,22 @@ Notation "'0xffffefffffc2f'" (* 4503595332402223 (0xffffefffffc2f) *)
   := (Const 4503595332402223%Z).
 Notation "'0xffffefffffc2f'" (* 4503595332402223 (0xffffefffffc2f) *)
   := (Const WO~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~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 "'0xffffffffffdc7'" (* 4503599627369927 (0xffffffffffdc7) *)
+  := (Const 4503599627369927%Z).
+Notation "'0xffffffffffdc7'" (* 4503599627369927 (0xffffffffffdc7) *)
+  := (Const WO~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~0~1~1~1~0~0~0~1~1~1).
+Notation "'0xffffffffffe1f'" (* 4503599627370015 (0xffffffffffe1f) *)
+  := (Const 4503599627370015%Z).
+Notation "'0xffffffffffe1f'" (* 4503599627370015 (0xffffffffffe1f) *)
+  := (Const WO~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~0~0~0~1~1~1~1~1).
 Notation "'0xfffffffffff43'" (* 4503599627370307 (0xfffffffffff43) *)
   := (Const 4503599627370307%Z).
 Notation "'0xfffffffffff43'" (* 4503599627370307 (0xfffffffffff43) *)
   := (Const WO~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~0~0~0~1~1).
+Notation "'0xfffffffffff45'" (* 4503599627370309 (0xfffffffffff45) *)
+  := (Const 4503599627370309%Z).
+Notation "'0xfffffffffff45'" (* 4503599627370309 (0xfffffffffff45) *)
+  := (Const WO~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~0~0~1~0~1).
 Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)
   := (Const 4503599627370458%Z).
 Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)