diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-03 07:01:16 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-03 07:01:16 -0400 |
| commit | 1bd2be8679a3244191457b28cb00c04a88aed6e4 (patch) | |
| tree | b30d8fd58afa4c1b83b81710de09b10261351bba /src | |
| parent | bc3d738aa9c66bf09fc5eb9196c2ac103977c164 (diff) | |
Add more constant notations
Diffstat (limited to 'src')
| -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 6a4d58051..4d381cda0 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -132,6 +132,7 @@ nums = tuple(sorted(set(systematic_nums + [ 134217690, 134217694, 134217697, + 134217698, 134217699, 134217703, 134217710, @@ -1118,6 +1119,8 @@ Notation "'0b111111111111111111111011110'" (* 134217694 (0x7ffffde) *) := (Const WO~0~0~0~0~0~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~1~0). Notation "'0b111111111111111111111100001'" (* 134217697 (0x7ffffe1) *) := (Const WO~0~0~0~0~0~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). +Notation "'0b111111111111111111111100010'" (* 134217698 (0x7ffffe2) *) + := (Const WO~0~0~0~0~0~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~1~0). Notation "'0b111111111111111111111100011'" (* 134217699 (0x7ffffe3) *) := (Const WO~0~0~0~0~0~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~1~1). Notation "'0b111111111111111111111100111'" (* 134217703 (0x7ffffe7) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 16db5d8c7..635e3470b 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -132,6 +132,7 @@ nums = tuple(sorted(set(systematic_nums + [ 134217690, 134217694, 134217697, + 134217698, 134217699, 134217703, 134217710, @@ -1726,6 +1727,10 @@ Notation "'0x7ffffe1'" (* 134217697 (0x7ffffe1) *) := (Const 134217697%Z). Notation "'0x7ffffe1'" (* 134217697 (0x7ffffe1) *) := (Const WO~0~0~0~0~0~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). +Notation "'0x7ffffe2'" (* 134217698 (0x7ffffe2) *) + := (Const 134217698%Z). +Notation "'0x7ffffe2'" (* 134217698 (0x7ffffe2) *) + := (Const WO~0~0~0~0~0~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~1~0). Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *) := (Const 134217699%Z). Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *) |