diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-03 08:13:40 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-03 08:13:40 -0400 |
| commit | 9b415fbaf8902eeae9d04bcc983ee1e4da9936e0 (patch) | |
| tree | 4e9d0bad69b5f5a950e9881ce5a1eae9a74affbd /src/Compilers | |
| parent | accfea7c7a65d5a95fa1d7bb0783a4bd39ec107b (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 4d381cda0..79ee3eb78 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -111,6 +111,7 @@ nums = tuple(sorted(set(systematic_nums + [ 16777214, 33423358, 33554378, + 33554398, 33554399, 33554413, 33554414, @@ -1065,6 +1066,8 @@ Notation "'0b1111111011111111111111110'" (* 33423358 (0x1fdfffe) *) := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). Notation "'0b1111111111111111111001010'" (* 33554378 (0x1ffffca) *) := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0). +Notation "'0b1111111111111111111011110'" (* 33554398 (0x1ffffde) *) + := (Const WO~0~0~0~0~0~0~0~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 "'0b1111111111111111111011111'" (* 33554399 (0x1ffffdf) *) := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1). Notation "'0b1111111111111111111101101'" (* 33554413 (0x1ffffed) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 635e3470b..eb3cee549 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -111,6 +111,7 @@ nums = tuple(sorted(set(systematic_nums + [ 16777214, 33423358, 33554378, + 33554398, 33554399, 33554413, 33554414, @@ -1619,6 +1620,10 @@ Notation "'0x1ffffca'" (* 33554378 (0x1ffffca) *) := (Const 33554378%Z). Notation "'0x1ffffca'" (* 33554378 (0x1ffffca) *) := (Const WO~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0). +Notation "'0x1ffffde'" (* 33554398 (0x1ffffde) *) + := (Const 33554398%Z). +Notation "'0x1ffffde'" (* 33554398 (0x1ffffde) *) + := (Const WO~0~0~0~0~0~0~0~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 "'0x1ffffdf'" (* 33554399 (0x1ffffdf) *) := (Const 33554399%Z). Notation "'0x1ffffdf'" (* 33554399 (0x1ffffdf) *) |