diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-02 03:38:37 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-02 03:38:37 -0400 |
| commit | ba89ee9983ca991ab1f077cf6d19172ca448e5fc (patch) | |
| tree | 8190c506c715fe566856406419c1b2927e179ac4 /src/Compilers | |
| parent | 4b3a79558c25a806ee658290a0cef2156eab616d (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 50b7b4468..90c488549 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -93,6 +93,7 @@ nums = tuple(sorted(set(systematic_nums + [ 67108861, 67108862, 134217690, + 134217697, 134217699, 134217703, 134217710, @@ -904,6 +905,8 @@ Notation "'0b100000000000000000000000001'" (* 67108865 (0x4000001) *) := (Const WO~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~0~0~0~1). Notation "'0b111111111111111111111011010'" (* 134217690 (0x7ffffda) *) := (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~0~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 "'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 3d952be63..0ba5a8f40 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -93,6 +93,7 @@ nums = tuple(sorted(set(systematic_nums + [ 67108861, 67108862, 134217690, + 134217697, 134217699, 134217703, 134217710, @@ -1434,6 +1435,10 @@ Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *) := (Const 134217690%Z). Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *) := (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~0~1~0). +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 "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *) := (Const 134217699%Z). Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *) |