diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-29 17:42:59 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-29 17:42:59 -0400 |
commit | 4ebf0031d039f3ef68eb1a121b75c044d6ae1206 (patch) | |
tree | 782d86f08e01e0e4ccd0c1b9120d6a65aa3813b1 /src | |
parent | 90192601dbe45c163b4b0ecb14a48ecb0642556a (diff) |
Add more constant notations
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 75 | ||||
-rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 125 |
2 files changed, 200 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index 3edd4cb04..427282d35 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -69,6 +69,7 @@ nums = tuple(sorted(set(systematic_nums + [ 16777201, 16777207, 16777213, + 33554399, 33554413, 33554417, 33554427, @@ -81,9 +82,11 @@ nums = tuple(sorted(set(systematic_nums + [ 67108861, 67108862, 134217690, + 134217699, 134217703, 134217710, 134217713, + 134217719, 134217726, 268431360, 268435441, @@ -91,10 +94,12 @@ nums = tuple(sorted(set(systematic_nums + [ 268435454, 536870893, 536870906, + 536870907, 536870909, 536870910, 678152731, 954437177, + 1065418751, 1073741821, 1073741822, 1332920885, @@ -108,7 +113,10 @@ nums = tuple(sorted(set(systematic_nums + [ 3707621341, 4008636143, 4042322161, + 4289200127, + 4294963199, 4294966319, + 4294966531, 4294967107, 4294967179, 4294967263, @@ -167,6 +175,8 @@ nums = tuple(sorted(set(systematic_nums + [ 140737488355303, 140737488355313, 140737488355319, + 194613558116351, + 281453501874175, 281470681743359, 281474976645119, 281474976710339, @@ -202,7 +212,9 @@ nums = tuple(sorted(set(systematic_nums + [ 18014398509481975, 18014398509481981, 18014398509481982, + 36028797018963937, 36028797018963943, + 36028797018963947, 36028797018963949, 72056494526300160, 72057594037927819, @@ -214,18 +226,24 @@ nums = tuple(sorted(set(systematic_nums + [ 144115188075855857, 144115188075855863, 144115188075855867, + 144115188075855869, + 144115188075855870, 288230376151711717, 288230376151711727, 288230376151711741, 576460752303423467, 576460752303423469, + 576460752303423471, 1117984489315730401, + 1152921504606846974, 3353953467947191203, 3816567739388183093, + 4530058275181297663, 4575938696385134591, 5675921253449092805, 9564978408590137875, 9708812670373448219, + 9963214713607832691, 10248191152060862009, 10330176681277348905, 10365313336655843289, @@ -237,17 +255,24 @@ nums = tuple(sorted(set(systematic_nums + [ 14933078535860113213, 14978125529935106013, 15580212934572586289, + 17050145153302519317, 17216961135462248175, + 17256631552825064415, 17361641481138401521, + 18308539860144619519, 18421974275759013887, 18445336698825998335, + 18446462598732840959, 18446726481523507199, 18446744065119617023, 18446744069414583343, 18446744069414584319, 18446744069414584320, 18446744069414584321, + 18446744073709486079, 18446744073709550851, + 18446744073709551047, + 18446744073709551135, 18446744073709551195, 18446744073709551299, 18446744073709551427, @@ -786,6 +811,8 @@ Notation "'0b1000000000000000000000000'" (* 16777216 (0x1000000) *) := (Const WO~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~0~0~0~0~0~0). Notation "'0b1000000000000000000000001'" (* 16777217 (0x1000001) *) := (Const WO~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~0~0~0~0~0~1). +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) *) := (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~1~0~1~1~0~1). Notation "'0b1111111111111111111110001'" (* 33554417 (0x1fffff1) *) @@ -822,12 +849,16 @@ 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 "'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) *) := (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~1~1~1). Notation "'0b111111111111111111111101110'" (* 134217710 (0x7ffffee) *) := (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~1~1~1~0). Notation "'0b111111111111111111111110001'" (* 134217713 (0x7fffff1) *) := (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~1~0~0~0~1). +Notation "'0b111111111111111111111110111'" (* 134217719 (0x7fffff7) *) + := (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~1~0~1~1~1). Notation "'0b111111111111111111111111110'" (* 134217726 (0x7fffffe) *) := (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~1~1~1~1~0). Notation "'0b111111111111111111111111111'" (* 134217727 (0x7ffffff) *) @@ -854,6 +885,8 @@ Notation "'0b11111111111111111111111101101'" (* 536870893 (0x1fffffed) *) := (Const WO~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~1~1~0~1~1~0~1). Notation "'0b11111111111111111111111111010'" (* 536870906 (0x1ffffffa) *) := (Const WO~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~1~1~1~1~0~1~0). +Notation "'0b11111111111111111111111111011'" (* 536870907 (0x1ffffffb) *) + := (Const WO~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~1~1~1~1~0~1~1). Notation "'0b11111111111111111111111111101'" (* 536870909 (0x1ffffffd) *) := (Const WO~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~1~1~1~1~1~0~1). Notation "'0b11111111111111111111111111110'" (* 536870910 (0x1ffffffe) *) @@ -868,6 +901,8 @@ Notation "'0b101000011010111100101000011011'" (* 678152731 (0x286bca1b) *) := (Const WO~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1). Notation "'0b111000111000111000111000111001'" (* 954437177 (0x38e38e39) *) := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1). +Notation "'0b111111100000001111111111111111'" (* 1065418751 (0x3f80ffff) *) + := (Const WO~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b111111111111111111111111111101'" (* 1073741821 (0x3ffffffd) *) := (Const WO~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1). Notation "'0b111111111111111111111111111110'" (* 1073741822 (0x3ffffffe) *) @@ -904,8 +939,14 @@ Notation "'0b11101110111011101110111011101111'" (* 4008636143 (0xeeeeeeef) *) := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1). Notation "'0b11110000111100001111000011110001'" (* 4042322161 (0xf0f0f0f1) *) := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). +Notation "'0b11111111101001111111111111111111'" (* 4289200127 (0xffa7ffff) *) + := (Const WO~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b11111111111111111110111111111111'" (* 4294963199 (0xffffefff) *) + := (Const WO~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~1~1~1~1~1~1~1). 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 "'0b11111111111111111111111101000011'" (* 4294967107 (0xffffff43) *) := (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~1~0~1~0~0~0~0~1~1). Notation "'0b11111111111111111111111110001011'" (* 4294967179 (0xffffff8b) *) @@ -1118,6 +1159,10 @@ Notation "'0b100000000000000000000000000000000000000000000000'" (* 1407374883553 := (Const WO~0~0~0~0~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~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~0~0~0~0). Notation "'0b100000000000000000000000000000000000000000000001'" (* 140737488355329 (0x800000000001) *) := (Const WO~0~0~0~0~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~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~0~0~0~1). +Notation "'0b101100001111111111111111111111111111111111111111'" (* 194613558116351 (0xb0ffffffffff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b111111111111101011111111111111111111111111111111'" (* 281453501874175 (0xfffaffffffff) *) + := (Const WO~0~0~0~0~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~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b111111111111111011111111111111111111111111111111'" (* 281470681743359 (0xfffeffffffff) *) := (Const WO~0~0~0~0~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~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b111111111111111111111111111111101111111111111111'" (* 281474976645119 (0xfffffffeffff) *) @@ -1230,8 +1275,12 @@ Notation "'0b1000000000000000000000000000000000000000000000000000000'" (* 180143 := (Const WO~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~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~0~0~0~0~0~0~0~0~0~0~0). Notation "'0b1000000000000000000000000000000000000000000000000000001'" (* 18014398509481985 (0x40000000000001) *) := (Const WO~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~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~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0b1111111111111111111111111111111111111111111111111100001'" (* 36028797018963937 (0x7fffffffffffe1) *) + := (Const WO~0~0~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~1~1~1~1~1~1~1~1~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). Notation "'0b1111111111111111111111111111111111111111111111111100111'" (* 36028797018963943 (0x7fffffffffffe7) *) := (Const WO~0~0~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~1~1~1~1~1~1~1~1~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~1~1). +Notation "'0b1111111111111111111111111111111111111111111111111101011'" (* 36028797018963947 (0x7fffffffffffeb) *) + := (Const WO~0~0~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~1~1~1~1~1~1~1~1~1~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~1~1). Notation "'0b1111111111111111111111111111111111111111111111111101101'" (* 36028797018963949 (0x7fffffffffffed) *) := (Const WO~0~0~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~1~1~1~1~1~1~1~1~1~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~0~1). Notation "'0b1111111111111111111111111111111111111111111111111111111'" (* 36028797018963967 (0x7fffffffffffff) *) @@ -1266,6 +1315,10 @@ Notation "'0b111111111111111111111111111111111111111111111111111110111'" (* 1441 := (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~1~1~1~1~1~1~1~1~1~1~1~1~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). Notation "'0b111111111111111111111111111111111111111111111111111111011'" (* 144115188075855867 (0x1fffffffffffffb) *) := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~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). +Notation "'0b111111111111111111111111111111111111111111111111111111101'" (* 144115188075855869 (0x1fffffffffffffd) *) + := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1). +Notation "'0b111111111111111111111111111111111111111111111111111111110'" (* 144115188075855870 (0x1fffffffffffffe) *) + := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). Notation "'0b111111111111111111111111111111111111111111111111111111111'" (* 144115188075855871 (0x1ffffffffffffff) *) := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1000000000000000000000000000000000000000000000000000000000'" (* 144115188075855872 (0x200000000000000) *) @@ -1288,6 +1341,8 @@ Notation "'0b11111111111111111111111111111111111111111111111111111101011'" (* 57 := (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~1~1~1~1~1~1~1~1~1~1~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~1~1). Notation "'0b11111111111111111111111111111111111111111111111111111101101'" (* 576460752303423469 (0x7ffffffffffffed) *) := (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~1~1~1~1~1~1~1~1~1~1~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~0~1). +Notation "'0b11111111111111111111111111111111111111111111111111111101111'" (* 576460752303423471 (0x7ffffffffffffef) *) + := (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~1~1~1~1~1~1~1~1~1~1~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~1). Notation "'0b11111111111111111111111111111111111111111111111111111111111'" (* 576460752303423487 (0x7ffffffffffffff) *) := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b100000000000000000000000000000000000000000000000000000000000'" (* 576460752303423488 (0x800000000000000) *) @@ -1296,6 +1351,8 @@ Notation "'0b100000000000000000000000000000000000000000000000000000000001'" (* 5 := (Const WO~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~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~0~0~0~0~0~0~0~0~1). Notation "'0b111110000011111000001111100000111110000011111000001111100001'" (* 1117984489315730401 (0xf83e0f83e0f83e1) *) := (Const WO~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~1). +Notation "'0b111111111111111111111111111111111111111111111111111111111110'" (* 1152921504606846974 (0xffffffffffffffe) *) + := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). Notation "'0b111111111111111111111111111111111111111111111111111111111111'" (* 1152921504606846975 (0xfffffffffffffff) *) := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1000000000000000000000000000000000000000000000000000000000000'" (* 1152921504606846976 (0x1000000000000000) *) @@ -1312,6 +1369,8 @@ Notation "'0b10111010001011101000101110100010111010001011101000101110100011'" (* := (Const WO~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~0~1~1~1~0~1~0~0~0~1~1). Notation "'0b11010011110111001011000010001101001111011100101100001000110101'" (* 3816567739388183093 (0x34f72c234f72c235) *) := (Const WO~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1). +Notation "'0b11111011011101111111111111111111111111111111111111111111111111'" (* 4530058275181297663 (0x3eddffffffffffff) *) + := (Const WO~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b11111110000000111111111111111111111111111111111111111111111111'" (* 4575938696385134591 (0x3f80ffffffffffff) *) := (Const WO~0~0~1~1~1~1~1~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b11111111111111111111111111111111111111111111111111111111111111'" (* 4611686018427387903 (0x3fffffffffffffff) *) @@ -1332,6 +1391,8 @@ Notation "'0b1000010010111101101000010010111101101000010010111101101000010011'" := (Const WO~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1). Notation "'0b1000011010111100101000011010111100101000011010111100101000011011'" (* 9708812670373448219 (0x86bca1af286bca1bL) *) := (Const WO~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1). +Notation "'0b1000101001000100011100101111111010100001100010100100010001110011'" (* 9963214713607832691 (0x8a4472fea18a4473L) *) + := (Const WO~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~0~1~1~1~1~1~1~1~0~1~0~1~0~0~0~0~1~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~1). Notation "'0b1000111000111000111000111000111000111000111000111000111000111001'" (* 10248191152060862009 (0x8e38e38e38e38e39L) *) := (Const WO~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1). Notation "'0b1000111101011100001010001111010111000010100011110101110000101001'" (* 10330176681277348905 (0x8f5c28f5c28f5c29L) *) @@ -1354,14 +1415,22 @@ Notation "'0b1100111111011100111111011100111111011100111111011100111111011101'" := (Const WO~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~1). Notation "'0b1101100000111000000010010001110111010010001001010011010100110001'" (* 15580212934572586289 (0xd838091dd2253531L) *) := (Const WO~1~1~0~1~1~0~0~0~0~0~1~1~1~0~0~0~0~0~0~0~1~0~0~1~0~0~0~1~1~1~0~1~1~1~0~1~0~0~1~0~0~0~1~0~0~1~0~1~0~0~1~1~0~1~0~1~0~0~1~1~0~0~0~1). +Notation "'0b1110110010011110010010001010111001101111011100011101111000010101'" (* 17050145153302519317 (0xec9e48ae6f71de15L) *) + := (Const WO~1~1~1~0~1~1~0~0~1~0~0~1~1~1~1~0~0~1~0~0~1~0~0~0~1~0~1~0~1~1~1~0~0~1~1~0~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0~1~1~1~1~0~0~0~0~1~0~1~0~1). Notation "'0b1110111011101110111011101110111011101110111011101110111011101111'" (* 17216961135462248175 (0xeeeeeeeeeeeeeeefL) *) := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1). +Notation "'0b1110111101111011110111101111011110111101111011110111101111011111'" (* 17256631552825064415 (0xef7bdef7bdef7bdfL) *) + := (Const WO~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~1). Notation "'0b1111000011110000111100001111000011110000111100001111000011110001'" (* 17361641481138401521 (0xf0f0f0f0f0f0f0f1L) *) := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). +Notation "'0b1111111000010100111111111111111111111111111111111111111111111111'" (* 18308539860144619519 (0xfe14ffffffffffffL) *) + := (Const WO~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1111111110100111111111111111111111111111111111111111111111111111'" (* 18421974275759013887 (0xffa7ffffffffffffL) *) := (Const WO~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1111111111111010111111111111111111111111111111111111111111111111'" (* 18445336698825998335 (0xfffaffffffffffffL) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b1111111111111110111111111111111111111111111111111111111111111111'" (* 18446462598732840959 (0xfffeffffffffffffL) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1111111111111111111011111111111111111111111111111111111111111111'" (* 18446726481523507199 (0xffffefffffffffffL) *) := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1111111111111111111111111111110111111111111111111111111111111111'" (* 18446744065119617023 (0xfffffffdffffffffL) *) @@ -1374,8 +1443,14 @@ Notation "'0b1111111111111111111111111111111100000000000000000000000000000000'" := (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~1~1~1~1~1~1~1~1~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~0~0~0~0~0~0~0). Notation "'0b1111111111111111111111111111111100000000000000000000000000000001'" (* 18446744069414584321 (0xffffffff00000001L) *) := (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~1~1~1~1~1~1~1~1~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~0~0~0~0~0~0~1). +Notation "'0b1111111111111111111111111111111111111111111111101111111111111111'" (* 18446744073709486079 (0xfffffffffffeffffL) *) + := (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~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0b1111111111111111111111111111111111111111111111111111110100000011'" (* 18446744073709550851 (0xfffffffffffffd03L) *) := (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~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111110111000111'" (* 18446744073709551047 (0xfffffffffffffdc7L) *) + := (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~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111000011111'" (* 18446744073709551135 (0xfffffffffffffe1fL) *) + := (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~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111001011011'" (* 18446744073709551195 (0xfffffffffffffe5bL) *) := (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~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111011000011'" (* 18446744073709551299 (0xfffffffffffffec3L) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 822fa7b7b..7c963f0e5 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -69,6 +69,7 @@ nums = tuple(sorted(set(systematic_nums + [ 16777201, 16777207, 16777213, + 33554399, 33554413, 33554417, 33554427, @@ -81,9 +82,11 @@ nums = tuple(sorted(set(systematic_nums + [ 67108861, 67108862, 134217690, + 134217699, 134217703, 134217710, 134217713, + 134217719, 134217726, 268431360, 268435441, @@ -91,10 +94,12 @@ nums = tuple(sorted(set(systematic_nums + [ 268435454, 536870893, 536870906, + 536870907, 536870909, 536870910, 678152731, 954437177, + 1065418751, 1073741821, 1073741822, 1332920885, @@ -108,7 +113,10 @@ nums = tuple(sorted(set(systematic_nums + [ 3707621341, 4008636143, 4042322161, + 4289200127, + 4294963199, 4294966319, + 4294966531, 4294967107, 4294967179, 4294967263, @@ -167,6 +175,8 @@ nums = tuple(sorted(set(systematic_nums + [ 140737488355303, 140737488355313, 140737488355319, + 194613558116351, + 281453501874175, 281470681743359, 281474976645119, 281474976710339, @@ -202,7 +212,9 @@ nums = tuple(sorted(set(systematic_nums + [ 18014398509481975, 18014398509481981, 18014398509481982, + 36028797018963937, 36028797018963943, + 36028797018963947, 36028797018963949, 72056494526300160, 72057594037927819, @@ -214,18 +226,24 @@ nums = tuple(sorted(set(systematic_nums + [ 144115188075855857, 144115188075855863, 144115188075855867, + 144115188075855869, + 144115188075855870, 288230376151711717, 288230376151711727, 288230376151711741, 576460752303423467, 576460752303423469, + 576460752303423471, 1117984489315730401, + 1152921504606846974, 3353953467947191203, 3816567739388183093, + 4530058275181297663, 4575938696385134591, 5675921253449092805, 9564978408590137875, 9708812670373448219, + 9963214713607832691, 10248191152060862009, 10330176681277348905, 10365313336655843289, @@ -237,17 +255,24 @@ nums = tuple(sorted(set(systematic_nums + [ 14933078535860113213, 14978125529935106013, 15580212934572586289, + 17050145153302519317, 17216961135462248175, + 17256631552825064415, 17361641481138401521, + 18308539860144619519, 18421974275759013887, 18445336698825998335, + 18446462598732840959, 18446726481523507199, 18446744065119617023, 18446744069414583343, 18446744069414584319, 18446744069414584320, 18446744069414584321, + 18446744073709486079, 18446744073709550851, + 18446744073709551047, + 18446744073709551135, 18446744073709551195, 18446744073709551299, 18446744073709551427, @@ -1256,6 +1281,10 @@ Notation "'0x1000001'" (* 16777217 (0x1000001) *) := (Const 16777217%Z). Notation "'0x1000001'" (* 16777217 (0x1000001) *) := (Const WO~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~0~0~0~0~0~1). +Notation "'0x1ffffdf'" (* 33554399 (0x1ffffdf) *) + := (Const 33554399%Z). +Notation "'0x1ffffdf'" (* 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 "'0x1ffffed'" (* 33554413 (0x1ffffed) *) := (Const 33554413%Z). Notation "'0x1ffffed'" (* 33554413 (0x1ffffed) *) @@ -1328,6 +1357,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 "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *) + := (Const 134217699%Z). +Notation "'0x7ffffe3'" (* 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 "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *) := (Const 134217703%Z). Notation "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *) @@ -1340,6 +1373,10 @@ Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *) := (Const 134217713%Z). Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *) := (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~1~0~0~0~1). +Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *) + := (Const 134217719%Z). +Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *) + := (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~1~0~1~1~1). Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *) := (Const 134217726%Z). Notation "'0x7fffffe'" (* 134217726 (0x7fffffe) *) @@ -1392,6 +1429,10 @@ Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *) := (Const 536870906%Z). Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *) := (Const WO~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~1~1~1~1~0~1~0). +Notation "'0x1ffffffb'" (* 536870907 (0x1ffffffb) *) + := (Const 536870907%Z). +Notation "'0x1ffffffb'" (* 536870907 (0x1ffffffb) *) + := (Const WO~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~1~1~1~1~0~1~1). Notation "'0x1ffffffd'" (* 536870909 (0x1ffffffd) *) := (Const 536870909%Z). Notation "'0x1ffffffd'" (* 536870909 (0x1ffffffd) *) @@ -1420,6 +1461,10 @@ Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *) := (Const 954437177%Z). Notation "'0x38e38e39'" (* 954437177 (0x38e38e39) *) := (Const WO~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~0~1~1~1~0~0~1). +Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *) + := (Const 1065418751%Z). +Notation "'0x3f80ffff'" (* 1065418751 (0x3f80ffff) *) + := (Const WO~0~0~1~1~1~1~1~1~1~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0x3ffffffd'" (* 1073741821 (0x3ffffffd) *) := (Const 1073741821%Z). Notation "'0x3ffffffd'" (* 1073741821 (0x3ffffffd) *) @@ -1492,10 +1537,22 @@ Notation "'0xf0f0f0f1'" (* 4042322161 (0xf0f0f0f1) *) := (Const 4042322161%Z). Notation "'0xf0f0f0f1'" (* 4042322161 (0xf0f0f0f1) *) := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). +Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *) + := (Const 4289200127%Z). +Notation "'0xffa7ffff'" (* 4289200127 (0xffa7ffff) *) + := (Const WO~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xffffefff'" (* 4294963199 (0xffffefff) *) + := (Const 4294963199%Z). +Notation "'0xffffefff'" (* 4294963199 (0xffffefff) *) + := (Const WO~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~1~1~1~1~1~1~1). Notation "'0xfffffc2f'" (* 4294966319 (0xfffffc2f) *) := (Const 4294966319%Z). Notation "'0xfffffc2f'" (* 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 "'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 "'0xffffff43'" (* 4294967107 (0xffffff43) *) := (Const 4294967107%Z). Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *) @@ -1920,6 +1977,14 @@ Notation "'0x800000000001'" (* 140737488355329 (0x800000000001) *) := (Const 140737488355329%Z). Notation "'0x800000000001'" (* 140737488355329 (0x800000000001) *) := (Const WO~0~0~0~0~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~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~0~0~0~1). +Notation "'0xb0ffffffffff'" (* 194613558116351 (0xb0ffffffffff) *) + := (Const 194613558116351%Z). +Notation "'0xb0ffffffffff'" (* 194613558116351 (0xb0ffffffffff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xfffaffffffff'" (* 281453501874175 (0xfffaffffffff) *) + := (Const 281453501874175%Z). +Notation "'0xfffaffffffff'" (* 281453501874175 (0xfffaffffffff) *) + := (Const WO~0~0~0~0~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~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xfffeffffffff'" (* 281470681743359 (0xfffeffffffff) *) := (Const 281470681743359%Z). Notation "'0xfffeffffffff'" (* 281470681743359 (0xfffeffffffff) *) @@ -2144,10 +2209,18 @@ Notation "'0x40000000000001'" (* 18014398509481985 (0x40000000000001) *) := (Const 18014398509481985%Z). Notation "'0x40000000000001'" (* 18014398509481985 (0x40000000000001) *) := (Const WO~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~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~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0x7fffffffffffe1'" (* 36028797018963937 (0x7fffffffffffe1) *) + := (Const 36028797018963937%Z). +Notation "'0x7fffffffffffe1'" (* 36028797018963937 (0x7fffffffffffe1) *) + := (Const WO~0~0~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~1~1~1~1~1~1~1~1~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). Notation "'0x7fffffffffffe7'" (* 36028797018963943 (0x7fffffffffffe7) *) := (Const 36028797018963943%Z). Notation "'0x7fffffffffffe7'" (* 36028797018963943 (0x7fffffffffffe7) *) := (Const WO~0~0~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~1~1~1~1~1~1~1~1~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~1~1). +Notation "'0x7fffffffffffeb'" (* 36028797018963947 (0x7fffffffffffeb) *) + := (Const 36028797018963947%Z). +Notation "'0x7fffffffffffeb'" (* 36028797018963947 (0x7fffffffffffeb) *) + := (Const WO~0~0~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~1~1~1~1~1~1~1~1~1~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~1~1). Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *) := (Const 36028797018963949%Z). Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *) @@ -2216,6 +2289,14 @@ Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *) := (Const 144115188075855867%Z). Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *) := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~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). +Notation "'0x1fffffffffffffd'" (* 144115188075855869 (0x1fffffffffffffd) *) + := (Const 144115188075855869%Z). +Notation "'0x1fffffffffffffd'" (* 144115188075855869 (0x1fffffffffffffd) *) + := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1). +Notation "'0x1fffffffffffffe'" (* 144115188075855870 (0x1fffffffffffffe) *) + := (Const 144115188075855870%Z). +Notation "'0x1fffffffffffffe'" (* 144115188075855870 (0x1fffffffffffffe) *) + := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). Notation "'0x1ffffffffffffff'" (* 144115188075855871 (0x1ffffffffffffff) *) := (Const 144115188075855871%Z). Notation "'0x1ffffffffffffff'" (* 144115188075855871 (0x1ffffffffffffff) *) @@ -2260,6 +2341,10 @@ Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *) := (Const 576460752303423469%Z). Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *) := (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~1~1~1~1~1~1~1~1~1~1~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~0~1). +Notation "'0x7ffffffffffffef'" (* 576460752303423471 (0x7ffffffffffffef) *) + := (Const 576460752303423471%Z). +Notation "'0x7ffffffffffffef'" (* 576460752303423471 (0x7ffffffffffffef) *) + := (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~1~1~1~1~1~1~1~1~1~1~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~1). Notation "'0x7ffffffffffffff'" (* 576460752303423487 (0x7ffffffffffffff) *) := (Const 576460752303423487%Z). Notation "'0x7ffffffffffffff'" (* 576460752303423487 (0x7ffffffffffffff) *) @@ -2276,6 +2361,10 @@ Notation "'0xf83e0f83e0f83e1'" (* 1117984489315730401 (0xf83e0f83e0f83e1) *) := (Const 1117984489315730401%Z). Notation "'0xf83e0f83e0f83e1'" (* 1117984489315730401 (0xf83e0f83e0f83e1) *) := (Const WO~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~0~1~1~1~1~1~0~0~0~0~1). +Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *) + := (Const 1152921504606846974%Z). +Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *) + := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0). Notation "'0xfffffffffffffff'" (* 1152921504606846975 (0xfffffffffffffff) *) := (Const 1152921504606846975%Z). Notation "'0xfffffffffffffff'" (* 1152921504606846975 (0xfffffffffffffff) *) @@ -2308,6 +2397,10 @@ Notation "'0x34f72c234f72c235'" (* 3816567739388183093 (0x34f72c234f72c235) *) := (Const 3816567739388183093%Z). Notation "'0x34f72c234f72c235'" (* 3816567739388183093 (0x34f72c234f72c235) *) := (Const WO~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1). +Notation "'0x3eddffffffffffff'" (* 4530058275181297663 (0x3eddffffffffffff) *) + := (Const 4530058275181297663%Z). +Notation "'0x3eddffffffffffff'" (* 4530058275181297663 (0x3eddffffffffffff) *) + := (Const WO~0~0~1~1~1~1~1~0~1~1~0~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0x3f80ffffffffffff'" (* 4575938696385134591 (0x3f80ffffffffffff) *) := (Const 4575938696385134591%Z). Notation "'0x3f80ffffffffffff'" (* 4575938696385134591 (0x3f80ffffffffffff) *) @@ -2348,6 +2441,10 @@ Notation "'0x86bca1af286bca1bL'" (* 9708812670373448219 (0x86bca1af286bca1bL) *) := (Const 9708812670373448219%Z). Notation "'0x86bca1af286bca1bL'" (* 9708812670373448219 (0x86bca1af286bca1bL) *) := (Const WO~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~0~1~1~1~1~0~0~1~0~1~0~0~0~0~1~1~0~1~1). +Notation "'0x8a4472fea18a4473L'" (* 9963214713607832691 (0x8a4472fea18a4473L) *) + := (Const 9963214713607832691%Z). +Notation "'0x8a4472fea18a4473L'" (* 9963214713607832691 (0x8a4472fea18a4473L) *) + := (Const WO~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~0~1~1~1~1~1~1~1~0~1~0~1~0~0~0~0~1~1~0~0~0~1~0~1~0~0~1~0~0~0~1~0~0~0~1~1~1~0~0~1~1). Notation "'0x8e38e38e38e38e39L'" (* 10248191152060862009 (0x8e38e38e38e38e39L) *) := (Const 10248191152060862009%Z). Notation "'0x8e38e38e38e38e39L'" (* 10248191152060862009 (0x8e38e38e38e38e39L) *) @@ -2392,14 +2489,26 @@ Notation "'0xd838091dd2253531L'" (* 15580212934572586289 (0xd838091dd2253531L) * := (Const 15580212934572586289%Z). Notation "'0xd838091dd2253531L'" (* 15580212934572586289 (0xd838091dd2253531L) *) := (Const WO~1~1~0~1~1~0~0~0~0~0~1~1~1~0~0~0~0~0~0~0~1~0~0~1~0~0~0~1~1~1~0~1~1~1~0~1~0~0~1~0~0~0~1~0~0~1~0~1~0~0~1~1~0~1~0~1~0~0~1~1~0~0~0~1). +Notation "'0xec9e48ae6f71de15L'" (* 17050145153302519317 (0xec9e48ae6f71de15L) *) + := (Const 17050145153302519317%Z). +Notation "'0xec9e48ae6f71de15L'" (* 17050145153302519317 (0xec9e48ae6f71de15L) *) + := (Const WO~1~1~1~0~1~1~0~0~1~0~0~1~1~1~1~0~0~1~0~0~1~0~0~0~1~0~1~0~1~1~1~0~0~1~1~0~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0~1~1~1~1~0~0~0~0~1~0~1~0~1). Notation "'0xeeeeeeeeeeeeeeefL'" (* 17216961135462248175 (0xeeeeeeeeeeeeeeefL) *) := (Const 17216961135462248175%Z). Notation "'0xeeeeeeeeeeeeeeefL'" (* 17216961135462248175 (0xeeeeeeeeeeeeeeefL) *) := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1). +Notation "'0xef7bdef7bdef7bdfL'" (* 17256631552825064415 (0xef7bdef7bdef7bdfL) *) + := (Const 17256631552825064415%Z). +Notation "'0xef7bdef7bdef7bdfL'" (* 17256631552825064415 (0xef7bdef7bdef7bdfL) *) + := (Const WO~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~0~1~1~1~1~1). Notation "'0xf0f0f0f0f0f0f0f1L'" (* 17361641481138401521 (0xf0f0f0f0f0f0f0f1L) *) := (Const 17361641481138401521%Z). Notation "'0xf0f0f0f0f0f0f0f1L'" (* 17361641481138401521 (0xf0f0f0f0f0f0f0f1L) *) := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). +Notation "'0xfe14ffffffffffffL'" (* 18308539860144619519 (0xfe14ffffffffffffL) *) + := (Const 18308539860144619519%Z). +Notation "'0xfe14ffffffffffffL'" (* 18308539860144619519 (0xfe14ffffffffffffL) *) + := (Const WO~1~1~1~1~1~1~1~0~0~0~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) *) := (Const 18421974275759013887%Z). Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) *) @@ -2408,6 +2517,10 @@ Notation "'0xfffaffffffffffffL'" (* 18445336698825998335 (0xfffaffffffffffffL) * := (Const 18445336698825998335%Z). Notation "'0xfffaffffffffffffL'" (* 18445336698825998335 (0xfffaffffffffffffL) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xfffeffffffffffffL'" (* 18446462598732840959 (0xfffeffffffffffffL) *) + := (Const 18446462598732840959%Z). +Notation "'0xfffeffffffffffffL'" (* 18446462598732840959 (0xfffeffffffffffffL) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *) := (Const 18446726481523507199%Z). Notation "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *) @@ -2432,10 +2545,22 @@ Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) * := (Const 18446744069414584321%Z). Notation "'0xffffffff00000001L'" (* 18446744069414584321 (0xffffffff00000001L) *) := (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~1~1~1~1~1~1~1~1~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~0~0~0~0~0~0~1). +Notation "'0xfffffffffffeffffL'" (* 18446744073709486079 (0xfffffffffffeffffL) *) + := (Const 18446744073709486079%Z). +Notation "'0xfffffffffffeffffL'" (* 18446744073709486079 (0xfffffffffffeffffL) *) + := (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~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xfffffffffffffd03L'" (* 18446744073709550851 (0xfffffffffffffd03L) *) := (Const 18446744073709550851%Z). Notation "'0xfffffffffffffd03L'" (* 18446744073709550851 (0xfffffffffffffd03L) *) := (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~1~1~1~1~1~1~1~1~1~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 "'0xfffffffffffffdc7L'" (* 18446744073709551047 (0xfffffffffffffdc7L) *) + := (Const 18446744073709551047%Z). +Notation "'0xfffffffffffffdc7L'" (* 18446744073709551047 (0xfffffffffffffdc7L) *) + := (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~1~1~1~1~1~1~1~1~1~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 "'0xfffffffffffffe1fL'" (* 18446744073709551135 (0xfffffffffffffe1fL) *) + := (Const 18446744073709551135%Z). +Notation "'0xfffffffffffffe1fL'" (* 18446744073709551135 (0xfffffffffffffe1fL) *) + := (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~1~1~1~1~1~1~1~1~1~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 "'0xfffffffffffffe5bL'" (* 18446744073709551195 (0xfffffffffffffe5bL) *) := (Const 18446744073709551195%Z). Notation "'0xfffffffffffffe5bL'" (* 18446744073709551195 (0xfffffffffffffe5bL) *) |