diff options
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
-rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index a5ab779cd..a1a8c9777 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -150,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [ 67108849, 67108854, 67108855, + 67108858, 67108859, 67108861, 67108862, @@ -176,6 +177,7 @@ nums = tuple(sorted(set(systematic_nums + [ 268435441, 268435443, 268435445, + 268435451, 268435452, 268435453, 268435454, @@ -183,6 +185,7 @@ nums = tuple(sorted(set(systematic_nums + [ 536870886, 536870890, 536870893, + 536870902, 536870906, 536870907, 536870908, @@ -298,22 +301,30 @@ nums = tuple(sorted(set(systematic_nums + [ 2199023255543, 2199023255550, 4363955208191, + 4398046510080, 4398046511079, 4398046511086, + 4398046511095, 4398046511099, 4398046511102, 8727910416382, + 8791798053935, 8796090925055, 8796093021443, + 8796093022019, 8796093022158, 8796093022179, 8796093022183, 8796093022189, + 8796093022190, 8796093022193, 8796093022198, 8796093022205, 8796093022206, + 17583596107870, 17592181850110, + 17592186042886, + 17592186044038, 17592186044358, 17592186044366, 17592186044378, @@ -373,11 +384,13 @@ nums = tuple(sorted(set(systematic_nums + [ 562949953421279, 562949953421290, 562949953421293, + 562949953421294, 562949953421297, 562949953421303, 562949953421310, 1125899873288191, 1125899906842558, + 1125899906842586, 1125899906842593, 1125899906842594, 1125899906842606, @@ -1870,6 +1883,10 @@ Notation "'0x3fffff7'" (* 67108855 (0x3fffff7) *) := (Const 67108855%Z). Notation "'0x3fffff7'" (* 67108855 (0x3fffff7) *) := (Const WO~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~0~1~1~1). +Notation "'0x3fffffa'" (* 67108858 (0x3fffffa) *) + := (Const 67108858%Z). +Notation "'0x3fffffa'" (* 67108858 (0x3fffffa) *) + := (Const WO~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~0~1~0). Notation "'0x3fffffb'" (* 67108859 (0x3fffffb) *) := (Const 67108859%Z). Notation "'0x3fffffb'" (* 67108859 (0x3fffffb) *) @@ -1998,6 +2015,10 @@ 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 "'0xffffffb'" (* 268435451 (0xffffffb) *) + := (Const 268435451%Z). +Notation "'0xffffffb'" (* 268435451 (0xffffffb) *) + := (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~0~1~1). Notation "'0xffffffc'" (* 268435452 (0xffffffc) *) := (Const 268435452%Z). Notation "'0xffffffc'" (* 268435452 (0xffffffc) *) @@ -2038,6 +2059,10 @@ Notation "'0x1fffffed'" (* 536870893 (0x1fffffed) *) := (Const 536870893%Z). Notation "'0x1fffffed'" (* 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 "'0x1ffffff6'" (* 536870902 (0x1ffffff6) *) + := (Const 536870902%Z). +Notation "'0x1ffffff6'" (* 536870902 (0x1ffffff6) *) + := (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~0~1~1~0). Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *) := (Const 536870906%Z). Notation "'0x1ffffffa'" (* 536870906 (0x1ffffffa) *) @@ -2650,6 +2675,10 @@ Notation "'0x3f80fffffff'" (* 4363955208191 (0x3f80fffffff) *) := (Const 4363955208191%Z). Notation "'0x3f80fffffff'" (* 4363955208191 (0x3f80fffffff) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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). +Notation "'0x3fffffffc00'" (* 4398046510080 (0x3fffffffc00) *) + := (Const 4398046510080%Z). +Notation "'0x3fffffffc00'" (* 4398046510080 (0x3fffffffc00) *) + := (Const WO~0~0~0~0~0~0~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~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). Notation "'0x3ffffffffe7'" (* 4398046511079 (0x3ffffffffe7) *) := (Const 4398046511079%Z). Notation "'0x3ffffffffe7'" (* 4398046511079 (0x3ffffffffe7) *) @@ -2658,6 +2687,10 @@ Notation "'0x3ffffffffee'" (* 4398046511086 (0x3ffffffffee) *) := (Const 4398046511086%Z). Notation "'0x3ffffffffee'" (* 4398046511086 (0x3ffffffffee) *) := (Const WO~0~0~0~0~0~0~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~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 "'0x3fffffffff7'" (* 4398046511095 (0x3fffffffff7) *) + := (Const 4398046511095%Z). +Notation "'0x3fffffffff7'" (* 4398046511095 (0x3fffffffff7) *) + := (Const WO~0~0~0~0~0~0~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~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 "'0x3fffffffffb'" (* 4398046511099 (0x3fffffffffb) *) := (Const 4398046511099%Z). Notation "'0x3fffffffffb'" (* 4398046511099 (0x3fffffffffb) *) @@ -2682,6 +2715,10 @@ Notation "'0x7f01ffffffe'" (* 8727910416382 (0x7f01ffffffe) *) := (Const 8727910416382%Z). Notation "'0x7f01ffffffe'" (* 8727910416382 (0x7f01ffffffe) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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~0). +Notation "'0x7fefffffc2f'" (* 8791798053935 (0x7fefffffc2f) *) + := (Const 8791798053935%Z). +Notation "'0x7fefffffc2f'" (* 8791798053935 (0x7fefffffc2f) *) + := (Const WO~0~0~0~0~0~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~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 "'0x7ffffdfffff'" (* 8796090925055 (0x7ffffdfffff) *) := (Const 8796090925055%Z). Notation "'0x7ffffdfffff'" (* 8796090925055 (0x7ffffdfffff) *) @@ -2690,6 +2727,10 @@ Notation "'0x7fffffffd03'" (* 8796093021443 (0x7fffffffd03) *) := (Const 8796093021443%Z). Notation "'0x7fffffffd03'" (* 8796093021443 (0x7fffffffd03) *) := (Const WO~0~0~0~0~0~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~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 "'0x7ffffffff43'" (* 8796093022019 (0x7ffffffff43) *) + := (Const 8796093022019%Z). +Notation "'0x7ffffffff43'" (* 8796093022019 (0x7ffffffff43) *) + := (Const WO~0~0~0~0~0~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~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 "'0x7ffffffffce'" (* 8796093022158 (0x7ffffffffce) *) := (Const 8796093022158%Z). Notation "'0x7ffffffffce'" (* 8796093022158 (0x7ffffffffce) *) @@ -2706,6 +2747,10 @@ Notation "'0x7ffffffffed'" (* 8796093022189 (0x7ffffffffed) *) := (Const 8796093022189%Z). Notation "'0x7ffffffffed'" (* 8796093022189 (0x7ffffffffed) *) := (Const WO~0~0~0~0~0~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~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 "'0x7ffffffffee'" (* 8796093022190 (0x7ffffffffee) *) + := (Const 8796093022190%Z). +Notation "'0x7ffffffffee'" (* 8796093022190 (0x7ffffffffee) *) + := (Const WO~0~0~0~0~0~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~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). Notation "'0x7fffffffff1'" (* 8796093022193 (0x7fffffffff1) *) := (Const 8796093022193%Z). Notation "'0x7fffffffff1'" (* 8796093022193 (0x7fffffffff1) *) @@ -2734,10 +2779,22 @@ Notation "'0x80000000001'" (* 8796093022209 (0x80000000001) *) := (Const 8796093022209%Z). Notation "'0x80000000001'" (* 8796093022209 (0x80000000001) *) := (Const WO~0~0~0~0~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~1). +Notation "'0xffdfffff85e'" (* 17583596107870 (0xffdfffff85e) *) + := (Const 17583596107870%Z). +Notation "'0xffdfffff85e'" (* 17583596107870 (0xffdfffff85e) *) + := (Const WO~0~0~0~0~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~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~0). Notation "'0xfffffbffffe'" (* 17592181850110 (0xfffffbffffe) *) := (Const 17592181850110%Z). Notation "'0xfffffbffffe'" (* 17592181850110 (0xfffffbffffe) *) := (Const WO~0~0~0~0~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~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~0). +Notation "'0xffffffffa06'" (* 17592186042886 (0xffffffffa06) *) + := (Const 17592186042886%Z). +Notation "'0xffffffffa06'" (* 17592186042886 (0xffffffffa06) *) + := (Const WO~0~0~0~0~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~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~0). +Notation "'0xffffffffe86'" (* 17592186044038 (0xffffffffe86) *) + := (Const 17592186044038%Z). +Notation "'0xffffffffe86'" (* 17592186044038 (0xffffffffe86) *) + := (Const WO~0~0~0~0~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~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~0). Notation "'0xfffffffffc6'" (* 17592186044358 (0xfffffffffc6) *) := (Const 17592186044358%Z). Notation "'0xfffffffffc6'" (* 17592186044358 (0xfffffffffc6) *) @@ -3034,6 +3091,10 @@ Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *) := (Const 562949953421293%Z). Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *) := (Const WO~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~1~1~1~1~1~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 "'0x1ffffffffffee'" (* 562949953421294 (0x1ffffffffffee) *) + := (Const 562949953421294%Z). +Notation "'0x1ffffffffffee'" (* 562949953421294 (0x1ffffffffffee) *) + := (Const WO~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~1~1~1~1~1~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). Notation "'0x1fffffffffff1'" (* 562949953421297 (0x1fffffffffff1) *) := (Const 562949953421297%Z). Notation "'0x1fffffffffff1'" (* 562949953421297 (0x1fffffffffff1) *) @@ -3066,6 +3127,10 @@ Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *) := (Const 1125899906842558%Z). Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *) := (Const WO~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~1~1~1~1~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~0). +Notation "'0x3ffffffffffda'" (* 1125899906842586 (0x3ffffffffffda) *) + := (Const 1125899906842586%Z). +Notation "'0x3ffffffffffda'" (* 1125899906842586 (0x3ffffffffffda) *) + := (Const WO~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~1~1~1~1~1~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~0). Notation "'0x3ffffffffffe1'" (* 1125899906842593 (0x3ffffffffffe1) *) := (Const 1125899906842593%Z). Notation "'0x3ffffffffffe1'" (* 1125899906842593 (0x3ffffffffffe1) *) |