diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-03 16:30:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-03 16:30:17 -0400 |
| commit | 720132d552f2978b226c27eff11dfe4903de06b6 (patch) | |
| tree | 96b6433188c0e3c044bfd4d8a20a296ff8e5b96a /src/Compilers | |
| parent | 7f5365299c08bd592176d6e960073069164e56b2 (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 66f429752..a990f2bda 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -50,6 +50,7 @@ nums = tuple(sorted(set(systematic_nums + [ 524279, 524286, 679935, + 1048202, 1048471, 1048526, 1048534, @@ -938,6 +939,8 @@ Notation "'0b10000000000000000001'" (* 524289 (0x80001) *) := (Const WO~0~0~0~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~1). Notation "'0b10100101111111111111'" (* 679935 (0xa5fff) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b11111111111010001010'" (* 1048202 (0xffe8a) *) + := (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~0~1~0~0~0~1~0~1~0). Notation "'0b11111111111110010111'" (* 1048471 (0xfff97) *) := (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~0~0~1~0~1~1~1). Notation "'0b11111111111111001110'" (* 1048526 (0xfffce) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 694ddd44a..98dcc2bd6 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -50,6 +50,7 @@ nums = tuple(sorted(set(systematic_nums + [ 524279, 524286, 679935, + 1048202, 1048471, 1048526, 1048534, @@ -1340,6 +1341,10 @@ Notation "'0xa5fff'" (* 679935 (0xa5fff) *) := (Const 679935%Z). Notation "'0xa5fff'" (* 679935 (0xa5fff) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xffe8a'" (* 1048202 (0xffe8a) *) + := (Const 1048202%Z). +Notation "'0xffe8a'" (* 1048202 (0xffe8a) *) + := (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~0~1~0~0~0~1~0~1~0). Notation "'0xfff97'" (* 1048471 (0xfff97) *) := (Const 1048471%Z). Notation "'0xfff97'" (* 1048471 (0xfff97) *) |