diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-31 00:33:57 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-31 00:33:57 -0400 |
| commit | bffba898afa15aceb97459df5a0c9b4d75c1a7f1 (patch) | |
| tree | 5ce67c1ff1a8a06f399dd9d5f64b74e3f6b3a071 /src/Compilers | |
| parent | 7b9ab040811ce6035d0d0adc082aad592223a127 (diff) | |
Add more constant notations
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 3 | ||||
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 5 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index 427282d35..5684885d3 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -252,6 +252,7 @@ nums = tuple(sorted(set(systematic_nums + [ 12297829382473034411, 12754194144713244671, 14757395258967641293, + 14897608040525528621, 14933078535860113213, 14978125529935106013, 15580212934572586289, @@ -1409,6 +1410,8 @@ Notation "'0b1011000011111111111111111111111111111111111111111111111111111111'" := (Const WO~1~0~1~1~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). Notation "'0b1100110011001100110011001100110011001100110011001100110011001101'" (* 14757395258967641293 (0xcccccccccccccccdL) *) := (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1). +Notation "'0b1100111010111110111011111001010011111010100001101111111000101101'" (* 14897608040525528621 (0xcebeef94fa86fe2dL) *) + := (Const WO~1~1~0~0~1~1~1~0~1~0~1~1~1~1~1~0~1~1~1~0~1~1~1~1~1~0~0~1~0~1~0~0~1~1~1~1~1~0~1~0~1~0~0~0~0~1~1~0~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0~1). Notation "'0b1100111100111100111100111100111100111100111100111100111100111101'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *) := (Const WO~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~1). Notation "'0b1100111111011100111111011100111111011100111111011100111111011101'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 7c963f0e5..98f8efbd1 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -252,6 +252,7 @@ nums = tuple(sorted(set(systematic_nums + [ 12297829382473034411, 12754194144713244671, 14757395258967641293, + 14897608040525528621, 14933078535860113213, 14978125529935106013, 15580212934572586289, @@ -2477,6 +2478,10 @@ Notation "'0xcccccccccccccccdL'" (* 14757395258967641293 (0xcccccccccccccccdL) * := (Const 14757395258967641293%Z). Notation "'0xcccccccccccccccdL'" (* 14757395258967641293 (0xcccccccccccccccdL) *) := (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1). +Notation "'0xcebeef94fa86fe2dL'" (* 14897608040525528621 (0xcebeef94fa86fe2dL) *) + := (Const 14897608040525528621%Z). +Notation "'0xcebeef94fa86fe2dL'" (* 14897608040525528621 (0xcebeef94fa86fe2dL) *) + := (Const WO~1~1~0~0~1~1~1~0~1~0~1~1~1~1~1~0~1~1~1~0~1~1~1~1~1~0~0~1~0~1~0~0~1~1~1~1~1~0~1~0~1~0~0~0~0~1~1~0~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0~1). Notation "'0xcf3cf3cf3cf3cf3dL'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *) := (Const 14933078535860113213%Z). Notation "'0xcf3cf3cf3cf3cf3dL'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *) |