diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-02 02:20:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-02 02:20:24 -0400 |
| commit | 11144d2e698c4a263e59acb02226d383865f74e0 (patch) | |
| tree | 35a3f211dbf901173ec995d7bbf05e015809b40a /src/Compilers | |
| parent | 54dcfa93f6f214aac69b053c47ab204eb36e596c (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 1c03b5205..50b7b4468 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -111,6 +111,7 @@ nums = tuple(sorted(set(systematic_nums + [ 536870910, 678152731, 954437177, + 1054736383, 1065418751, 1073709055, 1073741821, @@ -957,6 +958,8 @@ Notation "'0b101000011010111100101000011011'" (* 678152731 (0x286bca1b) *) := (Const WO~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1). Notation "'0b111000111000111000111000111001'" (* 954437177 (0x38e38e39) *) := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1). +Notation "'0b111110110111011111111111111111'" (* 1054736383 (0x3eddffff) *) + := (Const WO~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b111111100000001111111111111111'" (* 1065418751 (0x3f80ffff) *) := (Const WO~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b111111111111110111111111111111'" (* 1073709055 (0x3fff7fff) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 7c7554b39..3d952be63 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -111,6 +111,7 @@ nums = tuple(sorted(set(systematic_nums + [ 536870910, 678152731, 954437177, + 1054736383, 1065418751, 1073709055, 1073741821, @@ -1541,6 +1542,10 @@ Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *) := (Const 954437177%Z). Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *) := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1). +Notation "'0x3eddffff'" (* 1054736383 (0x3eddffff) *) + := (Const 1054736383%Z). +Notation "'0x3eddffff'" (* 1054736383 (0x3eddffff) *) + := (Const WO~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *) := (Const 1065418751%Z). Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *) |