Add support for more constants

2 files changed, 51 insertions, 2 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 1f81baddd..e329b378c 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -7,12 +7,24 @@ Local Notation Const x := (Op (OpConst x) TT).
 (* python:
 <<
 #!/usr/bin/env python
+print(r"""Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Export Bedrock.Word.
+Require Export Crypto.Util.Notations.
+
+Local Notation Const x := (Op (OpConst x) TT).
+(""" + r"""* python:
+<<""")
+print(open(__file__).read())
+print(r""">>
+ *""" + r""")""")
 print('\n'.join('''Notation "'%s'" (* %d (%s) *)\n  := (Const %s).''' % (b, d, h, i)
  for d, h, b, i 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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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
 WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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
+WO~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~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~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~0~1~1~0~1~0
 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~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
@@ -44,9 +56,16 @@ WO~0~1~0~1~0~1~0~1
 WO~0~1~0~1
 WO~1~0~0~1
 WO~1~0
-WO~1~1""".split('\n'))])))
+WO~1~1
+WO~0
+WO~1""".split('\n'))])))
+
 >>
  *)
+Notation "'0b0'" (* 0 (0x0) *)
+  := (Const WO~0).
+Notation "'0b1'" (* 1 (0x1) *)
+  := (Const WO~1).
 Notation "'0b10'" (* 2 (0x2) *)
   := (Const WO~1~0).
 Notation "'0b11'" (* 3 (0x3) *)
@@ -111,6 +130,8 @@ Notation "'0b0000000000001111111111111111111111111111111111111111111111111110'"
   := (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).
 Notation "'0b0000000000001111111111111111111111111111111111111111111111111111'" (* 4503599627370495 (0xfffffffffffff) *)
   := (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~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111111111111111'" (* 18446744073709551615 (0xffffffffffffffffL) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b00000000000000000000000000000000000000000001111111111111111111111111111111111111111111111111111111111111111111111111111111111111'" (* 38685626227668133590597631 (0x1fffffffffffffffffffffL) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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 "'0b00000000000000000000000000000000000000000011111111111111111111111111111111111111111111111111111111111111111111111111111111110110'" (* 77371252455336267181195254 (0x3ffffffffffffffffffff6L) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 399c4a22b..79ec58e62 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -8,12 +8,25 @@ Notation Const x := (Op (OpConst x) TT).
 (* python:
 <<
 #!/usr/bin/env python
+print(r"""Require Import Coq.ZArith.ZArith.
+Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Export Bedrock.Word.
+Require Export Crypto.Util.Notations.
+
+Notation Const x := (Op (OpConst x) TT).
+(""" + r"""* python:
+<<""")
+print(open(__file__).read())
+print(r""">>
+ *""" + r""")""")
 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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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
 WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~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
+WO~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~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~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~0~1~1~0~1~0
 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~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
@@ -45,9 +58,20 @@ WO~0~1~0~1~0~1~0~1
 WO~0~1~0~1
 WO~1~0~0~1
 WO~1~0
-WO~1~1""".split('\n'))])))
+WO~1~1
+WO~0
+WO~1""".split('\n'))])))
+
 >>
  *)
+Notation "'0x0'" (* 0 (0x0) *)
+  := (Const 0%Z).
+Notation "'0x0'" (* 0 (0x0) *)
+  := (Const WO~0).
+Notation "'0x1'" (* 1 (0x1) *)
+  := (Const 1%Z).
+Notation "'0x1'" (* 1 (0x1) *)
+  := (Const WO~1).
 Notation "'0x2'" (* 2 (0x2) *)
   := (Const 2%Z).
 Notation "'0x2'" (* 2 (0x2) *)
@@ -176,6 +200,10 @@ Notation "'0xfffffffffffff'" (* 4503599627370495 (0xfffffffffffff) *)
   := (Const 4503599627370495%Z).
 Notation "'0xfffffffffffff'" (* 4503599627370495 (0xfffffffffffff) *)
   := (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~1).
+Notation "'0xffffffffffffffffL'" (* 18446744073709551615 (0xffffffffffffffffL) *)
+  := (Const 18446744073709551615%Z).
+Notation "'0xffffffffffffffffL'" (* 18446744073709551615 (0xffffffffffffffffL) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0x1fffffffffffffffffffffL'" (* 38685626227668133590597631 (0x1fffffffffffffffffffffL) *)
   := (Const 38685626227668133590597631%Z).
 Notation "'0x1fffffffffffffffffffffL'" (* 38685626227668133590597631 (0x1fffffffffffffffffffffL) *)