From d9288564309f93c8963e90aed0efbde9901f5be3 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 2 Nov 2017 04:53:53 -0400
Subject: Add more constant notations

---
 src/Compilers/Z/BinaryNotationConstants.v | 12 ++++++++++++
 src/Compilers/Z/HexNotationConstants.v    | 20 ++++++++++++++++++++
 2 files changed, 32 insertions(+)

(limited to 'src/Compilers/Z')

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 90c488549..67fb1a260 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -37,6 +37,7 @@ nums = tuple(sorted(set(systematic_nums + [
     523807,
     524101,
     524263,
+    524267,
     524269,
     524271,
     524279,
@@ -46,6 +47,8 @@ nums = tuple(sorted(set(systematic_nums + [
     1048557,
     1048559,
     1048573,
+    2060031,
+    2081439,
     2094335,
     2096127,
     2096128,
@@ -54,6 +57,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2097143,
     4193327,
     4193539,
+    4193735,
     4193987,
     4194115,
     4194275,
@@ -745,6 +749,8 @@ Notation "'0b1111111111101000101'" (* 524101 (0x7ff45) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1).
 Notation "'0b1111111111111100111'" (* 524263 (0x7ffe7) *)
   := (Const WO~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~0~0~1~1~1).
+Notation "'0b1111111111111101011'" (* 524267 (0x7ffeb) *)
+  := (Const WO~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~0~1~0~1~1).
 Notation "'0b1111111111111101101'" (* 524269 (0x7ffed) *)
   := (Const WO~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~0~1~1~0~1).
 Notation "'0b1111111111111101111'" (* 524271 (0x7ffef) *)
@@ -775,6 +781,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 "'0b111110110111011111111'" (* 2060031 (0x1f6eff) *)
+  := (Const WO~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).
+Notation "'0b111111100001010011111'" (* 2081439 (0x1fc29f) *)
+  := (Const WO~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).
 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) *)
@@ -797,6 +807,8 @@ 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 "'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) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 0ba5a8f40..05898aa28 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -37,6 +37,7 @@ nums = tuple(sorted(set(systematic_nums + [
     523807,
     524101,
     524263,
+    524267,
     524269,
     524271,
     524279,
@@ -46,6 +47,8 @@ nums = tuple(sorted(set(systematic_nums + [
     1048557,
     1048559,
     1048573,
+    2060031,
+    2081439,
     2094335,
     2096127,
     2096128,
@@ -54,6 +57,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2097143,
     4193327,
     4193539,
+    4193735,
     4193987,
     4194115,
     4194275,
@@ -1115,6 +1119,10 @@ Notation "'0x7ffe7'" (* 524263 (0x7ffe7) *)
   := (Const 524263%Z).
 Notation "'0x7ffe7'" (* 524263 (0x7ffe7) *)
   := (Const WO~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~0~0~1~1~1).
+Notation "'0x7ffeb'" (* 524267 (0x7ffeb) *)
+  := (Const 524267%Z).
+Notation "'0x7ffeb'" (* 524267 (0x7ffeb) *)
+  := (Const WO~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~0~1~0~1~1).
 Notation "'0x7ffed'" (* 524269 (0x7ffed) *)
   := (Const 524269%Z).
 Notation "'0x7ffed'" (* 524269 (0x7ffed) *)
@@ -1175,6 +1183,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 "'0x1f6eff'" (* 2060031 (0x1f6eff) *)
+  := (Const 2060031%Z).
+Notation "'0x1f6eff'" (* 2060031 (0x1f6eff) *)
+  := (Const WO~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).
+Notation "'0x1fc29f'" (* 2081439 (0x1fc29f) *)
+  := (Const 2081439%Z).
+Notation "'0x1fc29f'" (* 2081439 (0x1fc29f) *)
+  := (Const WO~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).
 Notation "'0x1ff4ff'" (* 2094335 (0x1ff4ff) *)
   := (Const 2094335%Z).
 Notation "'0x1ff4ff'" (* 2094335 (0x1ff4ff) *)
@@ -1219,6 +1235,10 @@ 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 "'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 "'0x3ffec3'" (* 4193987 (0x3ffec3) *)
   := (Const 4193987%Z).
 Notation "'0x3ffec3'" (* 4193987 (0x3ffec3) *)
-- 
cgit v1.2.3