diff options
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
-rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 3727cd1d8..fe08c9d1f 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -79,6 +79,7 @@ nums = tuple(sorted(set(systematic_nums + [ 2095622, 2096127, 2096128, + 2096583, 2096942, 2097098, 2097114, @@ -91,9 +92,11 @@ nums = tuple(sorted(set(systematic_nums + [ 4162878, 4188670, 4192254, + 4193166, 4193327, 4193539, 4193735, + 4193823, 4193883, 4193987, 4194115, @@ -116,8 +119,10 @@ nums = tuple(sorted(set(systematic_nums + [ 8386654, 8387078, 8387470, + 8387646, 8387766, 8387974, + 8388127, 8388187, 8388230, 8388291, @@ -145,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [ 16647166, 16711679, 16775935, + 16776254, 16776374, 16776582, 16776842, @@ -1683,6 +1689,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 "'0x1ffdc7'" (* 2096583 (0x1ffdc7) *) + := (Const 2096583%Z). +Notation "'0x1ffdc7'" (* 2096583 (0x1ffdc7) *) + := (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~1~1~1~0~0~0~1~1~1). Notation "'0x1fff2e'" (* 2096942 (0x1fff2e) *) := (Const 2096942%Z). Notation "'0x1fff2e'" (* 2096942 (0x1fff2e) *) @@ -1743,6 +1753,10 @@ Notation "'0x3ff7fe'" (* 4192254 (0x3ff7fe) *) := (Const 4192254%Z). Notation "'0x3ff7fe'" (* 4192254 (0x3ff7fe) *) := (Const WO~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~0). +Notation "'0x3ffb8e'" (* 4193166 (0x3ffb8e) *) + := (Const 4193166%Z). +Notation "'0x3ffb8e'" (* 4193166 (0x3ffb8e) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0). Notation "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *) := (Const 4193327%Z). Notation "'0x3ffc2f'" (* 4193327 (0x3ffc2f) *) @@ -1755,6 +1769,10 @@ Notation "'0x3ffdc7'" (* 4193735 (0x3ffdc7) *) := (Const 4193735%Z). Notation "'0x3ffdc7'" (* 4193735 (0x3ffdc7) *) := (Const WO~0~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). +Notation "'0x3ffe1f'" (* 4193823 (0x3ffe1f) *) + := (Const 4193823%Z). +Notation "'0x3ffe1f'" (* 4193823 (0x3ffe1f) *) + := (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~0~0~0~1~1~1~1~1). Notation "'0x3ffe5b'" (* 4193883 (0x3ffe5b) *) := (Const 4193883%Z). Notation "'0x3ffe5b'" (* 4193883 (0x3ffe5b) *) @@ -1855,6 +1873,10 @@ 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 "'0x7ffc3e'" (* 8387646 (0x7ffc3e) *) + := (Const 8387646%Z). +Notation "'0x7ffc3e'" (* 8387646 (0x7ffc3e) *) + := (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~0~0~0~1~1~1~1~1~0). Notation "'0x7ffcb6'" (* 8387766 (0x7ffcb6) *) := (Const 8387766%Z). Notation "'0x7ffcb6'" (* 8387766 (0x7ffcb6) *) @@ -1863,6 +1885,10 @@ 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 "'0x7ffe1f'" (* 8388127 (0x7ffe1f) *) + := (Const 8388127%Z). +Notation "'0x7ffe1f'" (* 8388127 (0x7ffe1f) *) + := (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~0~0~0~1~1~1~1~1). Notation "'0x7ffe5b'" (* 8388187 (0x7ffe5b) *) := (Const 8388187%Z). Notation "'0x7ffe5b'" (* 8388187 (0x7ffe5b) *) @@ -1983,6 +2009,10 @@ Notation "'0xfffaff'" (* 16775935 (0xfffaff) *) := (Const 16775935%Z). Notation "'0xfffaff'" (* 16775935 (0xfffaff) *) := (Const WO~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). +Notation "'0xfffc3e'" (* 16776254 (0xfffc3e) *) + := (Const 16776254%Z). +Notation "'0xfffc3e'" (* 16776254 (0xfffc3e) *) + := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0). Notation "'0xfffcb6'" (* 16776374 (0xfffcb6) *) := (Const 16776374%Z). Notation "'0xfffcb6'" (* 16776374 (0xfffcb6) *) |