diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-01 12:17:48 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-01 12:17:48 -0400 |
| commit | a9a84c9349f40018f0c215fb2035b65da2b2d6cd (patch) | |
| tree | 12a4523cd94f73101b08a6e6aa9af64791162b8b /src/Compilers | |
| parent | e066ca96805c51710873254e780f4b2aa8eebdce (diff) | |
Add more constant notations
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 6 | ||||
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 10 |
2 files changed, 16 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index 5cdcd232b..cff3f5ae1 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -23,6 +23,7 @@ nums = tuple(sorted(set(systematic_nums + [ 765, 977, 5311, + 65531, 114687, 121665, 130307, @@ -55,6 +56,7 @@ nums = tuple(sorted(set(systematic_nums + [ 4194285, 4194287, 4194293, + 8323583, 8388491, 8388577, 8388581, @@ -672,6 +674,8 @@ Notation "'0b1000000000000000'" (* 32768 (0x8000) *) := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0). Notation "'0b1000000000000001'" (* 32769 (0x8001) *) := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0b1111111111111011'" (* 65531 (0xfffb) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1). Notation "'0b1111111111111111'" (* 65535 (0xffff) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b10000000000000000'" (* 65536 (0x10000) *) @@ -778,6 +782,8 @@ Notation "'0b10000000000000000000000'" (* 4194304 (0x400000) *) := (Const WO~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0). Notation "'0b10000000000000000000001'" (* 4194305 (0x400001) *) := (Const WO~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0b11111110000000111111111'" (* 8323583 (0x7f01ff) *) + := (Const WO~0~0~0~0~0~0~0~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). Notation "'0b11111111111111110001011'" (* 8388491 (0x7fff8b) *) := (Const WO~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~0~0~0~1~0~1~1). Notation "'0b11111111111111111100001'" (* 8388577 (0x7fffe1) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 16e718309..7889b2a28 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -23,6 +23,7 @@ nums = tuple(sorted(set(systematic_nums + [ 765, 977, 5311, + 65531, 114687, 121665, 130307, @@ -55,6 +56,7 @@ nums = tuple(sorted(set(systematic_nums + [ 4194285, 4194287, 4194293, + 8323583, 8388491, 8388577, 8388581, @@ -996,6 +998,10 @@ Notation "'0x8001'" (* 32769 (0x8001) *) := (Const 32769%Z). Notation "'0x8001'" (* 32769 (0x8001) *) := (Const WO~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0xfffb'" (* 65531 (0xfffb) *) + := (Const 65531%Z). +Notation "'0xfffb'" (* 65531 (0xfffb) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1). Notation "'0xffff'" (* 65535 (0xffff) *) := (Const 65535%Z). Notation "'0xffff'" (* 65535 (0xffff) *) @@ -1208,6 +1214,10 @@ Notation "'0x400001'" (* 4194305 (0x400001) *) := (Const 4194305%Z). Notation "'0x400001'" (* 4194305 (0x400001) *) := (Const WO~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0x7f01ff'" (* 8323583 (0x7f01ff) *) + := (Const 8323583%Z). +Notation "'0x7f01ff'" (* 8323583 (0x7f01ff) *) + := (Const WO~0~0~0~0~0~0~0~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). Notation "'0x7fff8b'" (* 8388491 (0x7fff8b) *) := (Const 8388491%Z). Notation "'0x7fff8b'" (* 8388491 (0x7fff8b) *) |