aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-18 23:17:04 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-10-18 23:17:11 -0400
commit47ef3ae951c6e0c994bed467ee52e7c84d15e45a (patch)
treeb96fe6807d34ef10e83e6bcf35da591ca28e5297 /src
parentec69d329ae2ee0e6a2928ec6e33876a101e922c8 (diff)
Add more constant notations
Diffstat (limited to 'src')
-rw-r--r--src/Compilers/Z/BinaryNotationConstants.v51
-rw-r--r--src/Compilers/Z/HexNotationConstants.v85
2 files changed, 136 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 868a89eb5..3edd4cb04 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -81,10 +81,13 @@ nums = tuple(sorted(set(systematic_nums + [
67108861,
67108862,
134217690,
+ 134217703,
134217710,
134217713,
134217726,
268431360,
+ 268435441,
+ 268435445,
268435454,
536870893,
536870906,
@@ -94,6 +97,7 @@ nums = tuple(sorted(set(systematic_nums + [
954437177,
1073741821,
1073741822,
+ 1332920885,
1749801491,
2147483647,
2863311531,
@@ -101,10 +105,14 @@ nums = tuple(sorted(set(systematic_nums + [
3264175145,
3303820997,
3435973837,
+ 3707621341,
4008636143,
4042322161,
4294966319,
4294967107,
+ 4294967179,
+ 4294967263,
+ 4294967267,
4294967269,
4294967271,
4294967277,
@@ -195,6 +203,7 @@ nums = tuple(sorted(set(systematic_nums + [
18014398509481981,
18014398509481982,
36028797018963943,
+ 36028797018963949,
72056494526300160,
72057594037927819,
72057594037927919,
@@ -208,6 +217,7 @@ nums = tuple(sorted(set(systematic_nums + [
288230376151711717,
288230376151711727,
288230376151711741,
+ 576460752303423467,
576460752303423469,
1117984489315730401,
3353953467947191203,
@@ -222,13 +232,17 @@ nums = tuple(sorted(set(systematic_nums + [
11907422100489763477,
12273715991527008853,
12297829382473034411,
+ 12754194144713244671,
14757395258967641293,
+ 14933078535860113213,
14978125529935106013,
15580212934572586289,
17216961135462248175,
17361641481138401521,
18421974275759013887,
+ 18445336698825998335,
18446726481523507199,
+ 18446744065119617023,
18446744069414583343,
18446744069414584319,
18446744069414584320,
@@ -237,12 +251,15 @@ nums = tuple(sorted(set(systematic_nums + [
18446744073709551195,
18446744073709551299,
18446744073709551427,
+ 18446744073709551429,
18446744073709551499,
18446744073709551511,
18446744073709551583,
+ 18446744073709551585,
18446744073709551587,
18446744073709551589,
18446744073709551591,
+ 18446744073709551595,
18446744073709551597,
18446744073709551599,
18446744073709551601,
@@ -805,6 +822,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 "'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) *)
@@ -819,6 +838,10 @@ Notation "'0b1000000000000000000000000001'" (* 134217729 (0x8000001) *)
:= (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~1).
Notation "'0b1111111111111111000000000000'" (* 268431360 (0xffff000) *)
:= (Const WO~0~0~0~0~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).
+Notation "'0b1111111111111111111111110001'" (* 268435441 (0xffffff1) *)
+ := (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~0~0~0~1).
+Notation "'0b1111111111111111111111110101'" (* 268435445 (0xffffff5) *)
+ := (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~0~1~0~1).
Notation "'0b1111111111111111111111111110'" (* 268435454 (0xffffffe) *)
:= (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~0).
Notation "'0b1111111111111111111111111111'" (* 268435455 (0xfffffff) *)
@@ -855,6 +878,8 @@ Notation "'0b1000000000000000000000000000000'" (* 1073741824 (0x40000000) *)
:= (Const WO~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).
Notation "'0b1000000000000000000000000000001'" (* 1073741825 (0x40000001) *)
:= (Const WO~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~1).
+Notation "'0b1001111011100101100001000110101'" (* 1332920885 (0x4f72c235) *)
+ := (Const WO~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 "'0b1101000010010111101101000010011'" (* 1749801491 (0x684bda13) *)
:= (Const WO~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 "'0b1111111111111111111111111111111'" (* 2147483647 (0x7fffffff) *)
@@ -873,6 +898,8 @@ Notation "'0b11000100111011000100111011000101'" (* 3303820997 (0xc4ec4ec5) *)
:= (Const WO~1~1~0~0~0~1~0~0~1~1~1~0~1~1~0~0~0~1~0~0~1~1~1~0~1~1~0~0~0~1~0~1).
Notation "'0b11001100110011001100110011001101'" (* 3435973837 (0xcccccccd) *)
:= (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1).
+Notation "'0b11011100111111011100111111011101'" (* 3707621341 (0xdcfdcfdd) *)
+ := (Const WO~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 "'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) *)
@@ -881,6 +908,12 @@ 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 "'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) *)
+ := (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~0~0~0~1~0~1~1).
+Notation "'0b11111111111111111111111111011111'" (* 4294967263 (0xffffffdf) *)
+ := (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~0~1~1~1~1~1).
+Notation "'0b11111111111111111111111111100011'" (* 4294967267 (0xffffffe3) *)
+ := (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~0~0~0~1~1).
Notation "'0b11111111111111111111111111100101'" (* 4294967269 (0xffffffe5) *)
:= (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~0~0~1~0~1).
Notation "'0b11111111111111111111111111100111'" (* 4294967271 (0xffffffe7) *)
@@ -1199,6 +1232,8 @@ Notation "'0b1000000000000000000000000000000000000000000000000000001'" (* 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~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 "'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) *)
:= (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~1~1~1~1~1).
Notation "'0b10000000000000000000000000000000000000000000000000000000'" (* 36028797018963968 (0x80000000000000) *)
@@ -1249,6 +1284,8 @@ Notation "'0b10000000000000000000000000000000000000000000000000000000000'" (* 28
:= (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~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 "'0b10000000000000000000000000000000000000000000000000000000001'" (* 288230376151711745 (0x400000000000001) *)
:= (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~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 "'0b11111111111111111111111111111111111111111111111111111101011'" (* 576460752303423467 (0x7ffffffffffffeb) *)
+ := (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 "'0b11111111111111111111111111111111111111111111111111111111111'" (* 576460752303423487 (0x7ffffffffffffff) *)
@@ -1307,8 +1344,12 @@ Notation "'0b1010101001010100111111111010101001010100111111111010101001010101'"
:= (Const WO~1~0~1~0~1~0~1~0~0~1~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~0~1~0~1~0~1~0~0~1~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~0~1~0~1~0~1~0~0~1~0~1~0~1~0~1).
Notation "'0b1010101010101010101010101010101010101010101010101010101010101011'" (* 12297829382473034411 (0xaaaaaaaaaaaaaaabL) *)
:= (Const WO~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~1).
+Notation "'0b1011000011111111111111111111111111111111111111111111111111111111'" (* 12754194144713244671 (0xb0ffffffffffffffL) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b1100110011001100110011001100110011001100110011001100110011001101'" (* 14757395258967641293 (0xcccccccccccccccdL) *)
:= (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1).
+Notation "'0b1100111100111100111100111100111100111100111100111100111100111101'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *)
+ := (Const WO~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~1).
Notation "'0b1100111111011100111111011100111111011100111111011100111111011101'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *)
:= (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) *)
@@ -1319,8 +1360,12 @@ Notation "'0b1111000011110000111100001111000011110000111100001111000011110001'"
:= (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 "'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 "'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) *)
+ := (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~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).
Notation "'0b1111111111111111111111111111111011111111111111111111110000101111'" (* 18446744069414583343 (0xfffffffefffffc2fL) *)
:= (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~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~0~1~1~1~1).
Notation "'0b1111111111111111111111111111111011111111111111111111111111111111'" (* 18446744069414584319 (0xfffffffeffffffffL) *)
@@ -1337,18 +1382,24 @@ Notation "'0b1111111111111111111111111111111111111111111111111111111011000011'"
:= (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~1~1~0~0~0~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111101000011'" (* 18446744073709551427 (0xffffffffffffff43L) *)
:= (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~1~0~1~0~0~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111111101000101'" (* 18446744073709551429 (0xffffffffffffff45L) *)
+ := (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~1~0~1~0~0~0~1~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111110001011'" (* 18446744073709551499 (0xffffffffffffff8bL) *)
:= (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~1~1~0~0~0~1~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111110010111'" (* 18446744073709551511 (0xffffffffffffff97L) *)
:= (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~1~1~0~0~1~0~1~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111111011111'" (* 18446744073709551583 (0xffffffffffffffdfL) *)
:= (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~1~1~1~0~1~1~1~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111111111100001'" (* 18446744073709551585 (0xffffffffffffffe1L) *)
+ := (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~1~1~1~1~0~0~0~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111111100011'" (* 18446744073709551587 (0xffffffffffffffe3L) *)
:= (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~1~1~1~1~0~0~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111111100101'" (* 18446744073709551589 (0xffffffffffffffe5L) *)
:= (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~1~1~1~1~0~0~1~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111111100111'" (* 18446744073709551591 (0xffffffffffffffe7L) *)
:= (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~1~1~1~1~0~0~1~1~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111111111101011'" (* 18446744073709551595 (0xffffffffffffffebL) *)
+ := (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~1~1~1~1~0~1~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111111101101'" (* 18446744073709551597 (0xffffffffffffffedL) *)
:= (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~1~1~1~1~0~1~1~0~1).
Notation "'0b1111111111111111111111111111111111111111111111111111111111101111'" (* 18446744073709551599 (0xffffffffffffffefL) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index ba7a8c5d8..822fa7b7b 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -81,10 +81,13 @@ nums = tuple(sorted(set(systematic_nums + [
67108861,
67108862,
134217690,
+ 134217703,
134217710,
134217713,
134217726,
268431360,
+ 268435441,
+ 268435445,
268435454,
536870893,
536870906,
@@ -94,6 +97,7 @@ nums = tuple(sorted(set(systematic_nums + [
954437177,
1073741821,
1073741822,
+ 1332920885,
1749801491,
2147483647,
2863311531,
@@ -101,10 +105,14 @@ nums = tuple(sorted(set(systematic_nums + [
3264175145,
3303820997,
3435973837,
+ 3707621341,
4008636143,
4042322161,
4294966319,
4294967107,
+ 4294967179,
+ 4294967263,
+ 4294967267,
4294967269,
4294967271,
4294967277,
@@ -195,6 +203,7 @@ nums = tuple(sorted(set(systematic_nums + [
18014398509481981,
18014398509481982,
36028797018963943,
+ 36028797018963949,
72056494526300160,
72057594037927819,
72057594037927919,
@@ -208,6 +217,7 @@ nums = tuple(sorted(set(systematic_nums + [
288230376151711717,
288230376151711727,
288230376151711741,
+ 576460752303423467,
576460752303423469,
1117984489315730401,
3353953467947191203,
@@ -222,13 +232,17 @@ nums = tuple(sorted(set(systematic_nums + [
11907422100489763477,
12273715991527008853,
12297829382473034411,
+ 12754194144713244671,
14757395258967641293,
+ 14933078535860113213,
14978125529935106013,
15580212934572586289,
17216961135462248175,
17361641481138401521,
18421974275759013887,
+ 18445336698825998335,
18446726481523507199,
+ 18446744065119617023,
18446744069414583343,
18446744069414584319,
18446744069414584320,
@@ -237,12 +251,15 @@ nums = tuple(sorted(set(systematic_nums + [
18446744073709551195,
18446744073709551299,
18446744073709551427,
+ 18446744073709551429,
18446744073709551499,
18446744073709551511,
18446744073709551583,
+ 18446744073709551585,
18446744073709551587,
18446744073709551589,
18446744073709551591,
+ 18446744073709551595,
18446744073709551597,
18446744073709551599,
18446744073709551601,
@@ -1311,6 +1328,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 "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *)
+ := (Const 134217703%Z).
+Notation "'0x7ffffe7'" (* 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 "'0x7ffffee'" (* 134217710 (0x7ffffee) *)
:= (Const 134217710%Z).
Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *)
@@ -1339,6 +1360,14 @@ Notation "'0xffff000'" (* 268431360 (0xffff000) *)
:= (Const 268431360%Z).
Notation "'0xffff000'" (* 268431360 (0xffff000) *)
:= (Const WO~0~0~0~0~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).
+Notation "'0xffffff1'" (* 268435441 (0xffffff1) *)
+ := (Const 268435441%Z).
+Notation "'0xffffff1'" (* 268435441 (0xffffff1) *)
+ := (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~0~0~0~1).
+Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
+ := (Const 268435445%Z).
+Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
+ := (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~0~1~0~1).
Notation "'0xffffffe'" (* 268435454 (0xffffffe) *)
:= (Const 268435454%Z).
Notation "'0xffffffe'" (* 268435454 (0xffffffe) *)
@@ -1411,6 +1440,10 @@ Notation "'0x40000001'" (* 1073741825 (0x40000001) *)
:= (Const 1073741825%Z).
Notation "'0x40000001'" (* 1073741825 (0x40000001) *)
:= (Const WO~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~1).
+Notation "'0x4f72c235'" (* 1332920885 (0x4f72c235) *)
+ := (Const 1332920885%Z).
+Notation "'0x4f72c235'" (* 1332920885 (0x4f72c235) *)
+ := (Const WO~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 "'0x684bda13'" (* 1749801491 (0x684bda13) *)
:= (Const 1749801491%Z).
Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *)
@@ -1447,6 +1480,10 @@ Notation "'0xcccccccd'" (* 3435973837 (0xcccccccd) *)
:= (Const 3435973837%Z).
Notation "'0xcccccccd'" (* 3435973837 (0xcccccccd) *)
:= (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1).
+Notation "'0xdcfdcfdd'" (* 3707621341 (0xdcfdcfdd) *)
+ := (Const 3707621341%Z).
+Notation "'0xdcfdcfdd'" (* 3707621341 (0xdcfdcfdd) *)
+ := (Const WO~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 "'0xeeeeeeef'" (* 4008636143 (0xeeeeeeef) *)
:= (Const 4008636143%Z).
Notation "'0xeeeeeeef'" (* 4008636143 (0xeeeeeeef) *)
@@ -1463,6 +1500,18 @@ Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *)
:= (Const 4294967107%Z).
Notation "'0xffffff43'" (* 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 "'0xffffff8b'" (* 4294967179 (0xffffff8b) *)
+ := (Const 4294967179%Z).
+Notation "'0xffffff8b'" (* 4294967179 (0xffffff8b) *)
+ := (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~0~0~0~1~0~1~1).
+Notation "'0xffffffdf'" (* 4294967263 (0xffffffdf) *)
+ := (Const 4294967263%Z).
+Notation "'0xffffffdf'" (* 4294967263 (0xffffffdf) *)
+ := (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~0~1~1~1~1~1).
+Notation "'0xffffffe3'" (* 4294967267 (0xffffffe3) *)
+ := (Const 4294967267%Z).
+Notation "'0xffffffe3'" (* 4294967267 (0xffffffe3) *)
+ := (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~0~0~0~1~1).
Notation "'0xffffffe5'" (* 4294967269 (0xffffffe5) *)
:= (Const 4294967269%Z).
Notation "'0xffffffe5'" (* 4294967269 (0xffffffe5) *)
@@ -2099,6 +2148,10 @@ 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 "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *)
+ := (Const 36028797018963949%Z).
+Notation "'0x7fffffffffffed'" (* 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 "'0x7fffffffffffff'" (* 36028797018963967 (0x7fffffffffffff) *)
:= (Const 36028797018963967%Z).
Notation "'0x7fffffffffffff'" (* 36028797018963967 (0x7fffffffffffff) *)
@@ -2199,6 +2252,10 @@ Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *)
:= (Const 288230376151711745%Z).
Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *)
:= (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~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 "'0x7ffffffffffffeb'" (* 576460752303423467 (0x7ffffffffffffeb) *)
+ := (Const 576460752303423467%Z).
+Notation "'0x7ffffffffffffeb'" (* 576460752303423467 (0x7ffffffffffffeb) *)
+ := (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 "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *)
:= (Const 576460752303423469%Z).
Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *)
@@ -2315,10 +2372,18 @@ Notation "'0xaaaaaaaaaaaaaaabL'" (* 12297829382473034411 (0xaaaaaaaaaaaaaaabL) *
:= (Const 12297829382473034411%Z).
Notation "'0xaaaaaaaaaaaaaaabL'" (* 12297829382473034411 (0xaaaaaaaaaaaaaaabL) *)
:= (Const WO~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~1).
+Notation "'0xb0ffffffffffffffL'" (* 12754194144713244671 (0xb0ffffffffffffffL) *)
+ := (Const 12754194144713244671%Z).
+Notation "'0xb0ffffffffffffffL'" (* 12754194144713244671 (0xb0ffffffffffffffL) *)
+ := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0xcccccccccccccccdL'" (* 14757395258967641293 (0xcccccccccccccccdL) *)
:= (Const 14757395258967641293%Z).
Notation "'0xcccccccccccccccdL'" (* 14757395258967641293 (0xcccccccccccccccdL) *)
:= (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1).
+Notation "'0xcf3cf3cf3cf3cf3dL'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *)
+ := (Const 14933078535860113213%Z).
+Notation "'0xcf3cf3cf3cf3cf3dL'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *)
+ := (Const WO~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~1).
Notation "'0xcfdcfdcfdcfdcfddL'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *)
:= (Const 14978125529935106013%Z).
Notation "'0xcfdcfdcfdcfdcfddL'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *)
@@ -2339,10 +2404,18 @@ Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) *
:= (Const 18421974275759013887%Z).
Notation "'0xffa7ffffffffffffL'" (* 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 "'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 "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *)
:= (Const 18446726481523507199%Z).
Notation "'0xffffefffffffffffL'" (* 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 "'0xfffffffdffffffffL'" (* 18446744065119617023 (0xfffffffdffffffffL) *)
+ := (Const 18446744065119617023%Z).
+Notation "'0xfffffffdffffffffL'" (* 18446744065119617023 (0xfffffffdffffffffL) *)
+ := (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~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).
Notation "'0xfffffffefffffc2fL'" (* 18446744069414583343 (0xfffffffefffffc2fL) *)
:= (Const 18446744069414583343%Z).
Notation "'0xfffffffefffffc2fL'" (* 18446744069414583343 (0xfffffffefffffc2fL) *)
@@ -2375,6 +2448,10 @@ Notation "'0xffffffffffffff43L'" (* 18446744073709551427 (0xffffffffffffff43L) *
:= (Const 18446744073709551427%Z).
Notation "'0xffffffffffffff43L'" (* 18446744073709551427 (0xffffffffffffff43L) *)
:= (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~1~0~1~0~0~0~0~1~1).
+Notation "'0xffffffffffffff45L'" (* 18446744073709551429 (0xffffffffffffff45L) *)
+ := (Const 18446744073709551429%Z).
+Notation "'0xffffffffffffff45L'" (* 18446744073709551429 (0xffffffffffffff45L) *)
+ := (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~1~0~1~0~0~0~1~0~1).
Notation "'0xffffffffffffff8bL'" (* 18446744073709551499 (0xffffffffffffff8bL) *)
:= (Const 18446744073709551499%Z).
Notation "'0xffffffffffffff8bL'" (* 18446744073709551499 (0xffffffffffffff8bL) *)
@@ -2387,6 +2464,10 @@ Notation "'0xffffffffffffffdfL'" (* 18446744073709551583 (0xffffffffffffffdfL) *
:= (Const 18446744073709551583%Z).
Notation "'0xffffffffffffffdfL'" (* 18446744073709551583 (0xffffffffffffffdfL) *)
:= (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~1~1~1~0~1~1~1~1~1).
+Notation "'0xffffffffffffffe1L'" (* 18446744073709551585 (0xffffffffffffffe1L) *)
+ := (Const 18446744073709551585%Z).
+Notation "'0xffffffffffffffe1L'" (* 18446744073709551585 (0xffffffffffffffe1L) *)
+ := (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~1~1~1~1~0~0~0~0~1).
Notation "'0xffffffffffffffe3L'" (* 18446744073709551587 (0xffffffffffffffe3L) *)
:= (Const 18446744073709551587%Z).
Notation "'0xffffffffffffffe3L'" (* 18446744073709551587 (0xffffffffffffffe3L) *)
@@ -2399,6 +2480,10 @@ Notation "'0xffffffffffffffe7L'" (* 18446744073709551591 (0xffffffffffffffe7L) *
:= (Const 18446744073709551591%Z).
Notation "'0xffffffffffffffe7L'" (* 18446744073709551591 (0xffffffffffffffe7L) *)
:= (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~1~1~1~1~0~0~1~1~1).
+Notation "'0xffffffffffffffebL'" (* 18446744073709551595 (0xffffffffffffffebL) *)
+ := (Const 18446744073709551595%Z).
+Notation "'0xffffffffffffffebL'" (* 18446744073709551595 (0xffffffffffffffebL) *)
+ := (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~1~1~1~1~0~1~0~1~1).
Notation "'0xffffffffffffffedL'" (* 18446744073709551597 (0xffffffffffffffedL) *)
:= (Const 18446744073709551597%Z).
Notation "'0xffffffffffffffedL'" (* 18446744073709551597 (0xffffffffffffffedL) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 05:18:44 +0000