From e5d16e788da463ab19a92a1c2c040e0c861b229b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 3 Nov 2017 14:42:15 -0400
Subject: Add more constant notations

---
 src/Compilers/Z/BinaryNotationConstants.v |  6 ++++++
 src/Compilers/Z/HexNotationConstants.v    | 10 ++++++++++
 2 files changed, 16 insertions(+)

(limited to 'src/Compilers')

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index eb05ffaba..0f918aca4 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -72,6 +72,8 @@ nums = tuple(sorted(set(systematic_nums + [
     2097135,
     2097143,
     2097150,
+    4120062,
+    4162878,
     4188670,
     4192254,
     4193327,
@@ -991,6 +993,10 @@ Notation "'0b1000000000000000000000'" (* 2097152 (0x200000) *)
   := (Const WO~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).
 Notation "'0b1000000000000000000001'" (* 2097153 (0x200001) *)
   := (Const WO~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~1).
+Notation "'0b1111101101110111111110'" (* 4120062 (0x3eddfe) *)
+  := (Const WO~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~0).
+Notation "'0b1111111000010100111110'" (* 4162878 (0x3f853e) *)
+  := (Const WO~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~0).
 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) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 4958fe902..3a76165f5 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -72,6 +72,8 @@ nums = tuple(sorted(set(systematic_nums + [
     2097135,
     2097143,
     2097150,
+    4120062,
+    4162878,
     4188670,
     4192254,
     4193327,
@@ -1449,6 +1451,14 @@ Notation "'0x200001'" (* 2097153 (0x200001) *)
   := (Const 2097153%Z).
 Notation "'0x200001'" (* 2097153 (0x200001) *)
   := (Const WO~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~1).
+Notation "'0x3eddfe'" (* 4120062 (0x3eddfe) *)
+  := (Const 4120062%Z).
+Notation "'0x3eddfe'" (* 4120062 (0x3eddfe) *)
+  := (Const WO~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~0).
+Notation "'0x3f853e'" (* 4162878 (0x3f853e) *)
+  := (Const 4162878%Z).
+Notation "'0x3f853e'" (* 4162878 (0x3f853e) *)
+  := (Const WO~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~0).
 Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *)
   := (Const 4188670%Z).
 Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *)
-- 
cgit v1.2.3