diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-01 11:12:34 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-01 11:12:34 -0400 |
commit | 8be2d386040833ede5c309b2215e8305c7574a30 (patch) | |
tree | 4953a52b8bd4f2dd56149357418dcdad0de84897 /src/Compilers/Z/HexNotationConstants.v | |
parent | 49f84c562c654b5639b0854186b5a219646ddb81 (diff) |
Add more constant notations
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 98f8efbd1..16e718309 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -38,6 +38,7 @@ nums = tuple(sorted(set(systematic_nums + [ 524269, 524271, 524279, + 679935, 1048471, 1048549, 1048557, @@ -194,6 +195,8 @@ nums = tuple(sorted(set(systematic_nums + [ 1125899906842619, 1125899906842621, 1460151441686527, + 2211942517178367, + 2234929182146559, 2248776156708863, 2251799813160960, 2251799813684483, @@ -202,7 +205,10 @@ nums = tuple(sorted(set(systematic_nums + [ 2251799813685229, 2251799813685239, 4503595332402223, + 4503599627369927, + 4503599627370015, 4503599627370307, + 4503599627370309, 4503599627370458, 4503599627370479, 4503599627370491, @@ -1098,6 +1104,10 @@ Notation "'0x80001'" (* 524289 (0x80001) *) := (Const 524289%Z). Notation "'0x80001'" (* 524289 (0x80001) *) := (Const WO~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~1). +Notation "'0xa5fff'" (* 679935 (0xa5fff) *) + := (Const 679935%Z). +Notation "'0xa5fff'" (* 679935 (0xa5fff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xfff97'" (* 1048471 (0xfff97) *) := (Const 1048471%Z). Notation "'0xfff97'" (* 1048471 (0xfff97) *) @@ -2090,6 +2100,14 @@ Notation "'0x52fffffffffff'" (* 1460151441686527 (0x52fffffffffff) *) := (Const 1460151441686527%Z). Notation "'0x52fffffffffff'" (* 1460151441686527 (0x52fffffffffff) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~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). +Notation "'0x7dbbfffffffff'" (* 2211942517178367 (0x7dbbfffffffff) *) + := (Const 2211942517178367%Z). +Notation "'0x7dbbfffffffff'" (* 2211942517178367 (0x7dbbfffffffff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~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). +Notation "'0x7f0a7ffffffff'" (* 2234929182146559 (0x7f0a7ffffffff) *) + := (Const 2234929182146559%Z). +Notation "'0x7f0a7ffffffff'" (* 2234929182146559 (0x7f0a7ffffffff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~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). Notation "'0x7fd3fffffffff'" (* 2248776156708863 (0x7fd3fffffffff) *) := (Const 2248776156708863%Z). Notation "'0x7fd3fffffffff'" (* 2248776156708863 (0x7fd3fffffffff) *) @@ -2134,10 +2152,22 @@ Notation "'0xffffefffffc2f'" (* 4503595332402223 (0xffffefffffc2f) *) := (Const 4503595332402223%Z). Notation "'0xffffefffffc2f'" (* 4503595332402223 (0xffffefffffc2f) *) := (Const WO~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~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 "'0xffffffffffdc7'" (* 4503599627369927 (0xffffffffffdc7) *) + := (Const 4503599627369927%Z). +Notation "'0xffffffffffdc7'" (* 4503599627369927 (0xffffffffffdc7) *) + := (Const WO~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~0~1~1~1~0~0~0~1~1~1). +Notation "'0xffffffffffe1f'" (* 4503599627370015 (0xffffffffffe1f) *) + := (Const 4503599627370015%Z). +Notation "'0xffffffffffe1f'" (* 4503599627370015 (0xffffffffffe1f) *) + := (Const WO~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~0~0~0~1~1~1~1~1). Notation "'0xfffffffffff43'" (* 4503599627370307 (0xfffffffffff43) *) := (Const 4503599627370307%Z). Notation "'0xfffffffffff43'" (* 4503599627370307 (0xfffffffffff43) *) := (Const WO~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~0~0~0~0~1~1). +Notation "'0xfffffffffff45'" (* 4503599627370309 (0xfffffffffff45) *) + := (Const 4503599627370309%Z). +Notation "'0xfffffffffff45'" (* 4503599627370309 (0xfffffffffff45) *) + := (Const WO~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~0~0~0~1~0~1). Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *) := (Const 4503599627370458%Z). Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *) |