diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-02 01:22:13 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-02 01:22:13 -0400 |
| commit | 7a5265682957414a49e3e650c5c56bf5482f2fd0 (patch) | |
| tree | 78aa5332ba97a62fbe954a9a565b5fd4cab1a755 /src/Compilers | |
| parent | 743f894f247b56f39e16324f480d6307b3db3842 (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 cf188caaf..739c17146 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -131,6 +131,8 @@ nums = tuple(sorted(set(systematic_nums + [ 4294963199, 4294966319, 4294966531, + 4294966727, + 4294966815, 4294966875, 4294966979, 4294967107, @@ -1001,6 +1003,10 @@ Notation "'0b11111111111111111111110000101111'" (* 4294966319 (0xfffffc2f) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1). Notation "'0b11111111111111111111110100000011'" (* 4294966531 (0xfffffd03) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1). +Notation "'0b11111111111111111111110111000111'" (* 4294966727 (0xfffffdc7) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1). +Notation "'0b11111111111111111111111000011111'" (* 4294966815 (0xfffffe1f) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1). Notation "'0b11111111111111111111111001011011'" (* 4294966875 (0xfffffe5b) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1). Notation "'0b11111111111111111111111011000011'" (* 4294966979 (0xfffffec3) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index f1c7d111b..e0670fa26 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -131,6 +131,8 @@ nums = tuple(sorted(set(systematic_nums + [ 4294963199, 4294966319, 4294966531, + 4294966727, + 4294966815, 4294966875, 4294966979, 4294967107, @@ -1635,6 +1637,14 @@ Notation "'0xfffffd03'" (* 4294966531 (0xfffffd03) *) := (Const 4294966531%Z). Notation "'0xfffffd03'" (* 4294966531 (0xfffffd03) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1). +Notation "'0xfffffdc7'" (* 4294966727 (0xfffffdc7) *) + := (Const 4294966727%Z). +Notation "'0xfffffdc7'" (* 4294966727 (0xfffffdc7) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1). +Notation "'0xfffffe1f'" (* 4294966815 (0xfffffe1f) *) + := (Const 4294966815%Z). +Notation "'0xfffffe1f'" (* 4294966815 (0xfffffe1f) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1). Notation "'0xfffffe5b'" (* 4294966875 (0xfffffe5b) *) := (Const 4294966875%Z). Notation "'0xfffffe5b'" (* 4294966875 (0xfffffe5b) *) |