Add more constant notations

2 files changed, 40 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 79ee3eb78..2600bbff6 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -24,6 +24,8 @@ nums = tuple(sorted(set(systematic_nums + [
     977,
     5311,
     32765,
+    32766,
+    65530,
     65531,
     65534,
     114687,
@@ -53,6 +55,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1048538,
     1048549,
     1048557,
+    1048558,
     1048559,
     1048573,
     1048574,
@@ -107,6 +110,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16777201,
     16777207,
     16777210,
+    16777212,
     16777213,
     16777214,
     33423358,
@@ -170,6 +174,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1073741822,
     1332920885,
     1749801491,
+    2147418110,
     2147483631,
     2147483642,
     2147483646,
@@ -832,12 +837,16 @@ 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 "'0b111111111111110'" (* 32766 (0x7ffe) *)
+  := (Const WO~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 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) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
 Notation "'0b1000000000000001'" (* 32769 (0x8001) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111111111010'" (* 65530 (0xfffa) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
 Notation "'0b1111111111111011'" (* 65531 (0xfffb) *)
   := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
 Notation "'0b1111111111111110'" (* 65534 (0xfffe) *)
@@ -920,6 +929,8 @@ Notation "'0b11111111111111100101'" (* 1048549 (0xfffe5) *)
   := (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~0~0~1~0~1).
 Notation "'0b11111111111111101101'" (* 1048557 (0xfffed) *)
   := (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~0~1~1~0~1).
+Notation "'0b11111111111111101110'" (* 1048558 (0xfffee) *)
+  := (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~0~1~1~1~0).
 Notation "'0b11111111111111101111'" (* 1048559 (0xfffef) *)
   := (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~0~1~1~1~1).
 Notation "'0b11111111111111111101'" (* 1048573 (0xffffd) *)
@@ -1052,6 +1063,8 @@ Notation "'0b111111111111111111110111'" (* 16777207 (0xfffff7) *)
   := (Const WO~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~0~1~1~1).
 Notation "'0b111111111111111111111010'" (* 16777210 (0xfffffa) *)
   := (Const WO~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~0).
+Notation "'0b111111111111111111111100'" (* 16777212 (0xfffffc) *)
+  := (Const WO~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~0~0).
 Notation "'0b111111111111111111111101'" (* 16777213 (0xfffffd) *)
   := (Const WO~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~0~1).
 Notation "'0b111111111111111111111110'" (* 16777214 (0xfffffe) *)
@@ -1220,6 +1233,8 @@ Notation "'0b1001111011100101100001000110101'" (* 1332920885 (0x4f72c235) *)
   := (Const WO~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1).
 Notation "'0b1101000010010111101101000010011'" (* 1749801491 (0x684bda13) *)
   := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1).
+Notation "'0b1111111111111101111111111111110'" (* 2147418110 (0x7ffefffe) *)
+  := (Const WO~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~0).
 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) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index eb3cee549..c09158bad 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -24,6 +24,8 @@ nums = tuple(sorted(set(systematic_nums + [
     977,
     5311,
     32765,
+    32766,
+    65530,
     65531,
     65534,
     114687,
@@ -53,6 +55,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1048538,
     1048549,
     1048557,
+    1048558,
     1048559,
     1048573,
     1048574,
@@ -107,6 +110,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16777201,
     16777207,
     16777210,
+    16777212,
     16777213,
     16777214,
     33423358,
@@ -170,6 +174,7 @@ nums = tuple(sorted(set(systematic_nums + [
     1073741822,
     1332920885,
     1749801491,
+    2147418110,
     2147483631,
     2147483642,
     2147483646,
@@ -1152,6 +1157,10 @@ 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 "'0x7ffe'" (* 32766 (0x7ffe) *)
+  := (Const 32766%Z).
+Notation "'0x7ffe'" (* 32766 (0x7ffe) *)
+  := (Const WO~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0x7fff'" (* 32767 (0x7fff) *)
   := (Const 32767%Z).
 Notation "'0x7fff'" (* 32767 (0x7fff) *)
@@ -1164,6 +1173,10 @@ Notation "'0x8001'" (* 32769 (0x8001) *)
   := (Const 32769%Z).
 Notation "'0x8001'" (* 32769 (0x8001) *)
   := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xfffa'" (* 65530 (0xfffa) *)
+  := (Const 65530%Z).
+Notation "'0xfffa'" (* 65530 (0xfffa) *)
+  := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
 Notation "'0xfffb'" (* 65531 (0xfffb) *)
   := (Const 65531%Z).
 Notation "'0xfffb'" (* 65531 (0xfffb) *)
@@ -1328,6 +1341,10 @@ Notation "'0xfffed'" (* 1048557 (0xfffed) *)
   := (Const 1048557%Z).
 Notation "'0xfffed'" (* 1048557 (0xfffed) *)
   := (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~0~1~1~0~1).
+Notation "'0xfffee'" (* 1048558 (0xfffee) *)
+  := (Const 1048558%Z).
+Notation "'0xfffee'" (* 1048558 (0xfffee) *)
+  := (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~0~1~1~1~0).
 Notation "'0xfffef'" (* 1048559 (0xfffef) *)
   := (Const 1048559%Z).
 Notation "'0xfffef'" (* 1048559 (0xfffef) *)
@@ -1592,6 +1609,10 @@ Notation "'0xfffffa'" (* 16777210 (0xfffffa) *)
   := (Const 16777210%Z).
 Notation "'0xfffffa'" (* 16777210 (0xfffffa) *)
   := (Const WO~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~0).
+Notation "'0xfffffc'" (* 16777212 (0xfffffc) *)
+  := (Const 16777212%Z).
+Notation "'0xfffffc'" (* 16777212 (0xfffffc) *)
+  := (Const WO~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~0~0).
 Notation "'0xfffffd'" (* 16777213 (0xfffffd) *)
   := (Const 16777213%Z).
 Notation "'0xfffffd'" (* 16777213 (0xfffffd) *)
@@ -1928,6 +1949,10 @@ Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *)
   := (Const 1749801491%Z).
 Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *)
   := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1).
+Notation "'0x7ffefffe'" (* 2147418110 (0x7ffefffe) *)
+  := (Const 2147418110%Z).
+Notation "'0x7ffefffe'" (* 2147418110 (0x7ffefffe) *)
+  := (Const WO~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~0).
 Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *)
   := (Const 2147483631%Z).
 Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *)