Add back word hex constant notations

1 files changed, 54 insertions, 2 deletions

diff --git a/src/Reflection/Z/HexNotationConstants.v b/src/Reflection/Z/HexNotationConstants.v
index 6df9b9b2b..8c03945cb 100644
--- a/src/Reflection/Z/HexNotationConstants.v
+++ b/src/Reflection/Z/HexNotationConstants.v
@@ -7,8 +7,8 @@ Require Export Crypto.Util.Notations.
 Notation Const x := (Op (OpConst x) TT).
 (* python:
 <<
-print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n  := (Const %s%%Z).''' % (h, d, h, d)
- for d, h, b, i in sorted([(eval(bv), hex(eval(bv)), bv, i)
+print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n  := (Const %s%%Z).\nNotation "'%s'" (* %d (%s) *)\n  := (Const %s).''' % (h, d, h, d, h, d, h, w)
+ for d, h, b, w in sorted([(eval(bv), hex(eval(bv)), bv, i)
  for (bv, i) in (('0b' + i[2:].replace('~', ''), i)
  for i in r"""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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1
 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
@@ -40,53 +40,105 @@ WO~1~1""".split('\n'))])))
  *)
 Notation "'0x2'" (* 2 (0x2) *)
   := (Const 2%Z).
+Notation "'0x2'" (* 2 (0x2) *)
+  := (Const WO~1~0).
 Notation "'0x3'" (* 3 (0x3) *)
   := (Const 3%Z).
+Notation "'0x3'" (* 3 (0x3) *)
+  := (Const WO~1~1).
 Notation "'0x9'" (* 9 (0x9) *)
   := (Const 9%Z).
+Notation "'0x9'" (* 9 (0x9) *)
+  := (Const WO~1~0~0~1).
 Notation "'0x11'" (* 17 (0x11) *)
   := (Const 17%Z).
+Notation "'0x11'" (* 17 (0x11) *)
+  := (Const WO~0~0~0~1~0~0~0~1).
 Notation "'0x13'" (* 19 (0x13) *)
   := (Const 19%Z).
+Notation "'0x13'" (* 19 (0x13) *)
+  := (Const WO~0~0~0~1~0~0~1~1).
 Notation "'0x17'" (* 23 (0x17) *)
   := (Const 23%Z).
+Notation "'0x17'" (* 23 (0x17) *)
+  := (Const WO~0~0~0~1~0~1~1~1).
 Notation "'0x19'" (* 25 (0x19) *)
   := (Const 25%Z).
+Notation "'0x19'" (* 25 (0x19) *)
+  := (Const WO~0~0~0~1~1~0~0~1).
 Notation "'0x1a'" (* 26 (0x1a) *)
   := (Const 26%Z).
+Notation "'0x1a'" (* 26 (0x1a) *)
+  := (Const WO~0~0~0~1~1~0~1~0).
 Notation "'0x1b'" (* 27 (0x1b) *)
   := (Const 27%Z).
+Notation "'0x1b'" (* 27 (0x1b) *)
+  := (Const WO~0~0~0~1~1~0~1~1).
 Notation "'0x1c'" (* 28 (0x1c) *)
   := (Const 28%Z).
+Notation "'0x1c'" (* 28 (0x1c) *)
+  := (Const WO~0~0~0~1~1~1~0~0).
 Notation "'0x33'" (* 51 (0x33) *)
   := (Const 51%Z).
+Notation "'0x33'" (* 51 (0x33) *)
+  := (Const WO~0~0~1~1~0~0~1~1).
 Notation "'0x7fffff'" (* 8388607 (0x7fffff) *)
   := (Const 8388607%Z).
+Notation "'0x7fffff'" (* 8388607 (0x7fffff) *)
+  := (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~1~1~1~1~1~1~1~1~1).
 Notation "'0x1ffffff'" (* 33554431 (0x1ffffff) *)
   := (Const 33554431%Z).
+Notation "'0x1ffffff'" (* 33554431 (0x1ffffff) *)
+  := (Const WO~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).
 Notation "'0x3fffffe'" (* 67108862 (0x3fffffe) *)
   := (Const 67108862%Z).
+Notation "'0x3fffffe'" (* 67108862 (0x3fffffe) *)
+  := (Const WO~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~0).
 Notation "'0x3ffffff'" (* 67108863 (0x3ffffff) *)
   := (Const 67108863%Z).
+Notation "'0x3ffffff'" (* 67108863 (0x3ffffff) *)
+  := (Const WO~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).
 Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
   := (Const 134217690%Z).
+Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
+  := (Const WO~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~1~0~1~0).
 Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *)
   := (Const 134217710%Z).
+Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *)
+  := (Const WO~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~1~1~0).
 Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *)
   := (Const 134217726%Z).
+Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *)
+  := (Const WO~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~0).
 Notation "'0x7ffffff'" (* 134217727 (0x7ffffff) *)
   := (Const 134217727%Z).
+Notation "'0x7ffffff'" (* 134217727 (0x7ffffff) *)
+  := (Const WO~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).
 Notation "'0xffffffe'" (* 268435454 (0xffffffe) *)
   := (Const 268435454%Z).
+Notation "'0xffffffe'" (* 268435454 (0xffffffe) *)
+  := (Const WO~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~0).
 Notation "'0xfffffff'" (* 268435455 (0xfffffff) *)
   := (Const 268435455%Z).
+Notation "'0xfffffff'" (* 268435455 (0xfffffff) *)
+  := (Const WO~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).
 Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *)
   := (Const 536870906%Z).
+Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *)
+  := (Const WO~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~0~1~0).
 Notation "'0x1ffffffe'" (* 536870910 (0x1ffffffe) *)
   := (Const 536870910%Z).
+Notation "'0x1ffffffe'" (* 536870910 (0x1ffffffe) *)
+  := (Const WO~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~0).
 Notation "'0x7ffffffffffff'" (* 2251799813685247 (0x7ffffffffffff) *)
   := (Const 2251799813685247%Z).
+Notation "'0x7ffffffffffff'" (* 2251799813685247 (0x7ffffffffffff) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)
   := (Const 4503599627370458%Z).
+Notation "'0xfffffffffffda'" (* 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 "'0xffffffffffffe'" (* 4503599627370494 (0xffffffffffffe) *)
   := (Const 4503599627370494%Z).
+Notation "'0xffffffffffffe'" (* 4503599627370494 (0xffffffffffffe) *)
+  := (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~1~1~1~1~1~0).