From c21d39f35ed774dc7f2405d79acbc21086ee2ef1 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 14 Nov 2017 15:54:13 -0500
Subject: Add more constant notations

---
 src/Compilers/Z/BinaryNotationConstants.v | 18 ++++++++++++++++++
 src/Compilers/Z/HexNotationConstants.v    | 30 ++++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)

(limited to 'src/Compilers')

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 7c73cd8d2..375265c9c 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -79,6 +79,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2095622,
     2096127,
     2096128,
+    2096583,
     2096942,
     2097098,
     2097114,
@@ -91,9 +92,11 @@ nums = tuple(sorted(set(systematic_nums + [
     4162878,
     4188670,
     4192254,
+    4193166,
     4193327,
     4193539,
     4193735,
+    4193823,
     4193883,
     4193987,
     4194115,
@@ -116,8 +119,10 @@ nums = tuple(sorted(set(systematic_nums + [
     8386654,
     8387078,
     8387470,
+    8387646,
     8387766,
     8387974,
+    8388127,
     8388187,
     8388230,
     8388291,
@@ -145,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16647166,
     16711679,
     16775935,
+    16776254,
     16776374,
     16776582,
     16776842,
@@ -1217,6 +1223,8 @@ 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 "'0b111111111110111000111'" (* 2096583 (0x1ffdc7) *)
+  := (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~1~1~1~0~0~0~1~1~1).
 Notation "'0b111111111111100101110'" (* 2096942 (0x1fff2e) *)
   := (Const WO~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~0).
 Notation "'0b111111111111111001010'" (* 2097098 (0x1fffca) *)
@@ -1247,12 +1255,16 @@ Notation "'0b1111111110100111111110'" (* 4188670 (0x3fe9fe) *)
   := (Const WO~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~0).
 Notation "'0b1111111111011111111110'" (* 4192254 (0x3ff7fe) *)
   := (Const WO~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~0).
+Notation "'0b1111111111101110001110'" (* 4193166 (0x3ffb8e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
 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 "'0b1111111111110111000111'" (* 4193735 (0x3ffdc7) *)
   := (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~1~1~0~0~0~1~1~1).
+Notation "'0b1111111111111000011111'" (* 4193823 (0x3ffe1f) *)
+  := (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~0~0~0~1~1~1~1~1).
 Notation "'0b1111111111111001011011'" (* 4193883 (0x3ffe5b) *)
   := (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~0~1~0~1~1~0~1~1).
 Notation "'0b1111111111111011000011'" (* 4193987 (0x3ffec3) *)
@@ -1303,10 +1315,14 @@ Notation "'0b11111111111101000000110'" (* 8387078 (0x7ffa06) *)
   := (Const WO~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~0).
 Notation "'0b11111111111101110001110'" (* 8387470 (0x7ffb8e) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0b11111111111110000111110'" (* 8387646 (0x7ffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0b11111111111110010110110'" (* 8387766 (0x7ffcb6) *)
   := (Const WO~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~0~1~1~0).
 Notation "'0b11111111111110110000110'" (* 8387974 (0x7ffd86) *)
   := (Const WO~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~0).
+Notation "'0b11111111111111000011111'" (* 8388127 (0x7ffe1f) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1).
 Notation "'0b11111111111111001011011'" (* 8388187 (0x7ffe5b) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1).
 Notation "'0b11111111111111010000110'" (* 8388230 (0x7ffe86) *)
@@ -1367,6 +1383,8 @@ Notation "'0b111111101111111111111111'" (* 16711679 (0xfeffff) *)
   := (Const WO~0~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).
 Notation "'0b111111111111101011111111'" (* 16775935 (0xfffaff) *)
   := (Const WO~0~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).
+Notation "'0b111111111111110000111110'" (* 16776254 (0xfffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0b111111111111110010110110'" (* 16776374 (0xfffcb6) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1~0).
 Notation "'0b111111111111110110000110'" (* 16776582 (0xfffd86) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 3727cd1d8..fe08c9d1f 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -79,6 +79,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2095622,
     2096127,
     2096128,
+    2096583,
     2096942,
     2097098,
     2097114,
@@ -91,9 +92,11 @@ nums = tuple(sorted(set(systematic_nums + [
     4162878,
     4188670,
     4192254,
+    4193166,
     4193327,
     4193539,
     4193735,
+    4193823,
     4193883,
     4193987,
     4194115,
@@ -116,8 +119,10 @@ nums = tuple(sorted(set(systematic_nums + [
     8386654,
     8387078,
     8387470,
+    8387646,
     8387766,
     8387974,
+    8388127,
     8388187,
     8388230,
     8388291,
@@ -145,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16647166,
     16711679,
     16775935,
+    16776254,
     16776374,
     16776582,
     16776842,
@@ -1683,6 +1689,10 @@ Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
   := (Const 2096128%Z).
 Notation "'0x1ffc00'" (* 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 "'0x1ffdc7'" (* 2096583 (0x1ffdc7) *)
+  := (Const 2096583%Z).
+Notation "'0x1ffdc7'" (* 2096583 (0x1ffdc7) *)
+  := (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~1~1~1~0~0~0~1~1~1).
 Notation "'0x1fff2e'" (* 2096942 (0x1fff2e) *)
   := (Const 2096942%Z).
 Notation "'0x1fff2e'" (* 2096942 (0x1fff2e) *)
@@ -1743,6 +1753,10 @@ Notation "'0x3ff7fe'" (* 4192254 (0x3ff7fe) *)
   := (Const 4192254%Z).
 Notation "'0x3ff7fe'" (* 4192254 (0x3ff7fe) *)
   := (Const WO~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~0).
+Notation "'0x3ffb8e'" (* 4193166 (0x3ffb8e) *)
+  := (Const 4193166%Z).
+Notation "'0x3ffb8e'" (* 4193166 (0x3ffb8e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
 Notation "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *)
   := (Const 4193327%Z).
 Notation "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *)
@@ -1755,6 +1769,10 @@ Notation "'0x3ffdc7'" (* 4193735 (0x3ffdc7) *)
   := (Const 4193735%Z).
 Notation "'0x3ffdc7'" (* 4193735 (0x3ffdc7) *)
   := (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~1~1~0~0~0~1~1~1).
+Notation "'0x3ffe1f'" (* 4193823 (0x3ffe1f) *)
+  := (Const 4193823%Z).
+Notation "'0x3ffe1f'" (* 4193823 (0x3ffe1f) *)
+  := (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~0~0~0~1~1~1~1~1).
 Notation "'0x3ffe5b'" (* 4193883 (0x3ffe5b) *)
   := (Const 4193883%Z).
 Notation "'0x3ffe5b'" (* 4193883 (0x3ffe5b) *)
@@ -1855,6 +1873,10 @@ Notation "'0x7ffb8e'" (* 8387470 (0x7ffb8e) *)
   := (Const 8387470%Z).
 Notation "'0x7ffb8e'" (* 8387470 (0x7ffb8e) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0x7ffc3e'" (* 8387646 (0x7ffc3e) *)
+  := (Const 8387646%Z).
+Notation "'0x7ffc3e'" (* 8387646 (0x7ffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0x7ffcb6'" (* 8387766 (0x7ffcb6) *)
   := (Const 8387766%Z).
 Notation "'0x7ffcb6'" (* 8387766 (0x7ffcb6) *)
@@ -1863,6 +1885,10 @@ Notation "'0x7ffd86'" (* 8387974 (0x7ffd86) *)
   := (Const 8387974%Z).
 Notation "'0x7ffd86'" (* 8387974 (0x7ffd86) *)
   := (Const WO~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~0).
+Notation "'0x7ffe1f'" (* 8388127 (0x7ffe1f) *)
+  := (Const 8388127%Z).
+Notation "'0x7ffe1f'" (* 8388127 (0x7ffe1f) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1).
 Notation "'0x7ffe5b'" (* 8388187 (0x7ffe5b) *)
   := (Const 8388187%Z).
 Notation "'0x7ffe5b'" (* 8388187 (0x7ffe5b) *)
@@ -1983,6 +2009,10 @@ Notation "'0xfffaff'" (* 16775935 (0xfffaff) *)
   := (Const 16775935%Z).
 Notation "'0xfffaff'" (* 16775935 (0xfffaff) *)
   := (Const WO~0~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).
+Notation "'0xfffc3e'" (* 16776254 (0xfffc3e) *)
+  := (Const 16776254%Z).
+Notation "'0xfffc3e'" (* 16776254 (0xfffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0xfffcb6'" (* 16776374 (0xfffcb6) *)
   := (Const 16776374%Z).
 Notation "'0xfffcb6'" (* 16776374 (0xfffcb6) *)
-- 
cgit v1.2.3