diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-02 02:07:32 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-02 02:07:32 -0400 |
| commit | 2e50ee8e8abfcdbaae8ac70c62436b75f0598fb9 (patch) | |
| tree | 040f54e567a64c5621b7956fdce66fb1c611e9ef /src/Compilers | |
| parent | 4786b83d53c76d802c7dced2e05977f945e026f4 (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 2d17668c6..1c03b5205 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -128,6 +128,7 @@ nums = tuple(sorted(set(systematic_nums + [ 3707621341, 4008636143, 4042322161, + 4262789119, 4289200127, 4294639615, 4294901759, @@ -1000,6 +1001,8 @@ Notation "'0b11101110111011101110111011101111'" (* 4008636143 (0xeeeeeeef) *) := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1). Notation "'0b11110000111100001111000011110001'" (* 4042322161 (0xf0f0f0f1) *) := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). +Notation "'0b11111110000101001111111111111111'" (* 4262789119 (0xfe14ffff) *) + := (Const WO~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b11111111101001111111111111111111'" (* 4289200127 (0xffa7ffff) *) := (Const WO~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b11111111111110101111111111111111'" (* 4294639615 (0xfffaffff) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 27a235d35..7c7554b39 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -128,6 +128,7 @@ nums = tuple(sorted(set(systematic_nums + [ 3707621341, 4008636143, 4042322161, + 4262789119, 4289200127, 4294639615, 4294901759, @@ -1628,6 +1629,10 @@ Notation "'0xf0f0f0f1'" (* 4042322161 (0xf0f0f0f1) *) := (Const 4042322161%Z). Notation "'0xf0f0f0f1'" (* 4042322161 (0xf0f0f0f1) *) := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). +Notation "'0xfe14ffff'" (* 4262789119 (0xfe14ffff) *) + := (Const 4262789119%Z). +Notation "'0xfe14ffff'" (* 4262789119 (0xfe14ffff) *) + := (Const WO~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *) := (Const 4289200127%Z). Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *) |