diff options
author | 2017-05-14 17:28:07 -0400 | |
---|---|---|
committer | 2017-05-14 17:30:40 -0400 | |
commit | e3e3be5b5f9d02059a9dd6f36ea4ddf36395f7e0 (patch) | |
tree | 10c6719e67ec91e18d6576551e95352b4c335228 /src/Compilers/Z/BinaryNotationConstants.v | |
parent | 5aad0d87ee19f69f5e0f413be8ebbe66d33f4d5d (diff) |
Add support for more constants
Diffstat (limited to 'src/Compilers/Z/BinaryNotationConstants.v')
-rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 23 |
1 files changed, 22 insertions, 1 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) *) |