aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Compilers/Z/BinaryNotationConstants.v21
-rw-r--r--src/Compilers/Z/HexNotationConstants.v35
2 files changed, 56 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 11d9973db..eb05ffaba 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -65,6 +65,7 @@ nums = tuple(sorted(set(systematic_nums + [
2094335,
2096127,
2096128,
+ 2096942,
2097114,
2097118,
2097127,
@@ -78,6 +79,7 @@ nums = tuple(sorted(set(systematic_nums + [
4193735,
4193987,
4194115,
+ 4194270,
4194275,
4194279,
4194285,
@@ -88,9 +90,12 @@ nums = tuple(sorted(set(systematic_nums + [
8323583,
8386654,
8387078,
+ 8387470,
+ 8387974,
8388230,
8388491,
8388558,
+ 8388570,
8388574,
8388577,
8388581,
@@ -105,6 +110,7 @@ nums = tuple(sorted(set(systematic_nums + [
16776959,
16776982,
16777162,
+ 16777182,
16777189,
16777191,
16777199,
@@ -152,6 +158,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217724,
134217726,
268431360,
+ 268435394,
268435398,
268435406,
268435426,
@@ -964,6 +971,8 @@ Notation "'0b111111111101111111111'" (* 2096127 (0x1ffbff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1).
Notation "'0b111111111110000000000'" (* 2096128 (0x1ffc00) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0b111111111111100101110'" (* 2096942 (0x1fff2e) *)
+ := (Const WO~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~0~1~0~1~1~1~0).
Notation "'0b111111111111111011010'" (* 2097114 (0x1fffda) *)
:= (Const WO~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~0~1~0).
Notation "'0b111111111111111011110'" (* 2097118 (0x1fffde) *)
@@ -996,6 +1005,8 @@ Notation "'0b1111111111111011000011'" (* 4193987 (0x3ffec3) *)
:= (Const WO~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~1~0~0~0~0~1~1).
Notation "'0b1111111111111101000011'" (* 4194115 (0x3fff43) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1).
+Notation "'0b1111111111111111011110'" (* 4194270 (0x3fffde) *)
+ := (Const WO~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~1~0~1~1~1~1~0).
Notation "'0b1111111111111111100011'" (* 4194275 (0x3fffe3) *)
:= (Const WO~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~1~1~0~0~0~1~1).
Notation "'0b1111111111111111100111'" (* 4194279 (0x3fffe7) *)
@@ -1022,12 +1033,18 @@ Notation "'0b11111111111100001011110'" (* 8386654 (0x7ff85e) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1~0).
Notation "'0b11111111111101000000110'" (* 8387078 (0x7ffa06) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
+Notation "'0b11111111111101110001110'" (* 8387470 (0x7ffb8e) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0b11111111111110110000110'" (* 8387974 (0x7ffd86) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
Notation "'0b11111111111111010000110'" (* 8388230 (0x7ffe86) *)
:= (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~0~1~0~0~0~0~1~1~0).
Notation "'0b11111111111111110001011'" (* 8388491 (0x7fff8b) *)
:= (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~0~0~0~1~0~1~1).
Notation "'0b11111111111111111001110'" (* 8388558 (0x7fffce) *)
:= (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~0~0~1~1~1~0).
+Notation "'0b11111111111111111011010'" (* 8388570 (0x7fffda) *)
+ := (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~0~1~1~0~1~0).
Notation "'0b11111111111111111011110'" (* 8388574 (0x7fffde) *)
:= (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~0~1~1~1~1~0).
Notation "'0b11111111111111111100001'" (* 8388577 (0x7fffe1) *)
@@ -1062,6 +1079,8 @@ Notation "'0b111111111111111100010110'" (* 16776982 (0xffff16) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0).
Notation "'0b111111111111111111001010'" (* 16777162 (0xffffca) *)
:= (Const WO~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~0~0~1~0~1~0).
+Notation "'0b111111111111111111011110'" (* 16777182 (0xffffde) *)
+ := (Const WO~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~0~1~1~1~1~0).
Notation "'0b111111111111111111100101'" (* 16777189 (0xffffe5) *)
:= (Const WO~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~0~0~1~0~1).
Notation "'0b111111111111111111100111'" (* 16777191 (0xffffe7) *)
@@ -1180,6 +1199,8 @@ 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 "'0b1111111111111111111111000010'" (* 268435394 (0xfffffc2) *)
+ := (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~0~0~0~0~1~0).
Notation "'0b1111111111111111111111000110'" (* 268435398 (0xfffffc6) *)
:= (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~0~0~0~1~1~0).
Notation "'0b1111111111111111111111001110'" (* 268435406 (0xfffffce) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 6607831d4..4958fe902 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -65,6 +65,7 @@ nums = tuple(sorted(set(systematic_nums + [
2094335,
2096127,
2096128,
+ 2096942,
2097114,
2097118,
2097127,
@@ -78,6 +79,7 @@ nums = tuple(sorted(set(systematic_nums + [
4193735,
4193987,
4194115,
+ 4194270,
4194275,
4194279,
4194285,
@@ -88,9 +90,12 @@ nums = tuple(sorted(set(systematic_nums + [
8323583,
8386654,
8387078,
+ 8387470,
+ 8387974,
8388230,
8388491,
8388558,
+ 8388570,
8388574,
8388577,
8388581,
@@ -105,6 +110,7 @@ nums = tuple(sorted(set(systematic_nums + [
16776959,
16776982,
16777162,
+ 16777182,
16777189,
16777191,
16777199,
@@ -152,6 +158,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217724,
134217726,
268431360,
+ 268435394,
268435398,
268435406,
268435426,
@@ -1402,6 +1409,10 @@ Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
:= (Const 2096128%Z).
Notation "'0x1ffc00'" (* 2096128 (0x1ffc00) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0x1fff2e'" (* 2096942 (0x1fff2e) *)
+ := (Const 2096942%Z).
+Notation "'0x1fff2e'" (* 2096942 (0x1fff2e) *)
+ := (Const WO~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~0~1~0~1~1~1~0).
Notation "'0x1fffda'" (* 2097114 (0x1fffda) *)
:= (Const 2097114%Z).
Notation "'0x1fffda'" (* 2097114 (0x1fffda) *)
@@ -1466,6 +1477,10 @@ Notation "'0x3fff43'" (* 4194115 (0x3fff43) *)
:= (Const 4194115%Z).
Notation "'0x3fff43'" (* 4194115 (0x3fff43) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~1~1).
+Notation "'0x3fffde'" (* 4194270 (0x3fffde) *)
+ := (Const 4194270%Z).
+Notation "'0x3fffde'" (* 4194270 (0x3fffde) *)
+ := (Const WO~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~1~0~1~1~1~1~0).
Notation "'0x3fffe3'" (* 4194275 (0x3fffe3) *)
:= (Const 4194275%Z).
Notation "'0x3fffe3'" (* 4194275 (0x3fffe3) *)
@@ -1518,6 +1533,14 @@ Notation "'0x7ffa06'" (* 8387078 (0x7ffa06) *)
:= (Const 8387078%Z).
Notation "'0x7ffa06'" (* 8387078 (0x7ffa06) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
+Notation "'0x7ffb8e'" (* 8387470 (0x7ffb8e) *)
+ := (Const 8387470%Z).
+Notation "'0x7ffb8e'" (* 8387470 (0x7ffb8e) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0x7ffd86'" (* 8387974 (0x7ffd86) *)
+ := (Const 8387974%Z).
+Notation "'0x7ffd86'" (* 8387974 (0x7ffd86) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
Notation "'0x7ffe86'" (* 8388230 (0x7ffe86) *)
:= (Const 8388230%Z).
Notation "'0x7ffe86'" (* 8388230 (0x7ffe86) *)
@@ -1530,6 +1553,10 @@ Notation "'0x7fffce'" (* 8388558 (0x7fffce) *)
:= (Const 8388558%Z).
Notation "'0x7fffce'" (* 8388558 (0x7fffce) *)
:= (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~0~0~1~1~1~0).
+Notation "'0x7fffda'" (* 8388570 (0x7fffda) *)
+ := (Const 8388570%Z).
+Notation "'0x7fffda'" (* 8388570 (0x7fffda) *)
+ := (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~0~1~1~0~1~0).
Notation "'0x7fffde'" (* 8388574 (0x7fffde) *)
:= (Const 8388574%Z).
Notation "'0x7fffde'" (* 8388574 (0x7fffde) *)
@@ -1598,6 +1625,10 @@ Notation "'0xffffca'" (* 16777162 (0xffffca) *)
:= (Const 16777162%Z).
Notation "'0xffffca'" (* 16777162 (0xffffca) *)
:= (Const WO~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~0~0~1~0~1~0).
+Notation "'0xffffde'" (* 16777182 (0xffffde) *)
+ := (Const 16777182%Z).
+Notation "'0xffffde'" (* 16777182 (0xffffde) *)
+ := (Const WO~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~0~1~1~1~1~0).
Notation "'0xffffe5'" (* 16777189 (0xffffe5) *)
:= (Const 16777189%Z).
Notation "'0xffffe5'" (* 16777189 (0xffffe5) *)
@@ -1834,6 +1865,10 @@ 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 "'0xfffffc2'" (* 268435394 (0xfffffc2) *)
+ := (Const 268435394%Z).
+Notation "'0xfffffc2'" (* 268435394 (0xfffffc2) *)
+ := (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~0~0~0~0~1~0).
Notation "'0xfffffc6'" (* 268435398 (0xfffffc6) *)
:= (Const 268435398%Z).
Notation "'0xfffffc6'" (* 268435398 (0xfffffc6) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 09:04:16 +0000