From 4160ba9f0eb6c0f216f398edff006f6959fd26e3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 2 Nov 2017 23:16:25 -0400 Subject: Add more constant notations --- src/Compilers/Z/BinaryNotationConstants.v | 36 +++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) (limited to 'src/Compilers/Z/BinaryNotationConstants.v') diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index 82f6b76a3..7113173f6 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -43,20 +43,26 @@ nums = tuple(sorted(set(systematic_nums + [ 524269, 524271, 524279, + 524286, 679935, 1048471, + 1048526, + 1048538, 1048549, 1048557, 1048559, 1048573, + 1048574, 2060031, 2081439, 2094335, 2096127, 2096128, + 2097118, 2097127, 2097135, 2097143, + 2097150, 4193327, 4193539, 4193735, @@ -71,6 +77,7 @@ nums = tuple(sorted(set(systematic_nums + [ 8323583, 8388491, 8388558, + 8388574, 8388577, 8388581, 8388591, @@ -121,6 +128,7 @@ nums = tuple(sorted(set(systematic_nums + [ 268435398, 268435406, 268435426, + 268435438, 268435441, 268435445, 268435452, @@ -138,6 +146,7 @@ nums = tuple(sorted(set(systematic_nums + [ 1054736383, 1065418751, 1073709055, + 1073741786, 1073741814, 1073741818, 1073741821, @@ -245,6 +254,7 @@ nums = tuple(sorted(set(systematic_nums + [ 70368744177659, 70368744177661, 140737471578110, + 140737488355294, 140737488355303, 140737488355313, 140737488355319, @@ -330,7 +340,9 @@ nums = tuple(sorted(set(systematic_nums + [ 36028797018963966, 72056494526300160, 72057594037927819, + 72057594037927874, 72057594037927886, + 72057594037927894, 72057594037927898, 72057594037927919, 72057594037927931, @@ -859,6 +871,8 @@ Notation "'0b1111111111111101111'" (* 524271 (0x7ffef) *) := (Const WO~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~0~1~1~1~1). Notation "'0b1111111111111110111'" (* 524279 (0x7fff7) *) := (Const WO~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~0~1~1~1). +Notation "'0b1111111111111111110'" (* 524286 (0x7fffe) *) + := (Const WO~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~0). Notation "'0b1111111111111111111'" (* 524287 (0x7ffff) *) := (Const WO~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). Notation "'0b10000000000000000000'" (* 524288 (0x80000) *) @@ -869,6 +883,10 @@ Notation "'0b10100101111111111111'" (* 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 "'0b11111111111110010111'" (* 1048471 (0xfff97) *) := (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~0~0~1~0~1~1~1). +Notation "'0b11111111111111001110'" (* 1048526 (0xfffce) *) + := (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~0~0~1~1~1~0). +Notation "'0b11111111111111011010'" (* 1048538 (0xfffda) *) + := (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~0~1~1~0~1~0). Notation "'0b11111111111111100101'" (* 1048549 (0xfffe5) *) := (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~0~0~1~0~1). Notation "'0b11111111111111101101'" (* 1048557 (0xfffed) *) @@ -877,6 +895,8 @@ Notation "'0b11111111111111101111'" (* 1048559 (0xfffef) *) := (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~0~1~1~1~1). Notation "'0b11111111111111111101'" (* 1048573 (0xffffd) *) := (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~0~1). +Notation "'0b11111111111111111110'" (* 1048574 (0xffffe) *) + := (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). Notation "'0b11111111111111111111'" (* 1048575 (0xfffff) *) := (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). Notation "'0b100000000000000000000'" (* 1048576 (0x100000) *) @@ -893,12 +913,16 @@ 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 "'0b111111111111111011110'" (* 2097118 (0x1fffde) *) + := (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~1~1~0). Notation "'0b111111111111111100111'" (* 2097127 (0x1fffe7) *) := (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~1~0~0~1~1~1). Notation "'0b111111111111111101111'" (* 2097135 (0x1fffef) *) := (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~1~0~1~1~1~1). Notation "'0b111111111111111110111'" (* 2097143 (0x1ffff7) *) := (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~1~1~0~1~1~1). +Notation "'0b111111111111111111110'" (* 2097150 (0x1ffffe) *) + := (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~1~1~1~1~1~0). Notation "'0b111111111111111111111'" (* 2097151 (0x1fffff) *) := (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~1~1~1~1~1~1). Notation "'0b1000000000000000000000'" (* 2097152 (0x200000) *) @@ -939,6 +963,8 @@ 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 "'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) *) := (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~0~0~0~0~1). Notation "'0b11111111111111111100101'" (* 8388581 (0x7fffe5) *) @@ -1069,6 +1095,8 @@ Notation "'0b1111111111111111111111001110'" (* 268435406 (0xfffffce) *) := (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~1~1~1~0). Notation "'0b1111111111111111111111100010'" (* 268435426 (0xfffffe2) *) := (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~0~0~0~1~0). +Notation "'0b1111111111111111111111101110'" (* 268435438 (0xfffffee) *) + := (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~0~1~1~1~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) *) @@ -1115,6 +1143,8 @@ Notation "'0b111111100000001111111111111111'" (* 1065418751 (0x3f80ffff) *) := (Const WO~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). Notation "'0b111111111111110111111111111111'" (* 1073709055 (0x3fff7fff) *) := (Const WO~0~0~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). +Notation "'0b111111111111111111111111011010'" (* 1073741786 (0x3fffffda) *) + := (Const WO~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~0). Notation "'0b111111111111111111111111110110'" (* 1073741814 (0x3ffffff6) *) := (Const WO~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~0~1~1~0). Notation "'0b111111111111111111111111111010'" (* 1073741818 (0x3ffffffa) *) @@ -1429,6 +1459,8 @@ Notation "'0b10000000000000000000000000000000000000000000001'" (* 70368744177665 := (Const WO~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~0~0~0~1). Notation "'0b11111111111111111111110111111111111111111111110'" (* 140737471578110 (0x7ffffefffffe) *) := (Const WO~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~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). +Notation "'0b11111111111111111111111111111111111111111011110'" (* 140737488355294 (0x7fffffffffde) *) + := (Const WO~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~1~1~1~0~1~1~1~1~0). Notation "'0b11111111111111111111111111111111111111111100111'" (* 140737488355303 (0x7fffffffffe7) *) := (Const WO~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~1~1~1~1~0~0~1~1~1). Notation "'0b11111111111111111111111111111111111111111110001'" (* 140737488355313 (0x7ffffffffff1) *) @@ -1653,8 +1685,12 @@ Notation "'0b11111111111111110000000000000000000000000000000000000000'" (* 72056 := (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~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 "'0b11111111111111111111111111111111111111111111111110001011'" (* 72057594037927819 (0xffffffffffff8b) *) := (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~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111000010'" (* 72057594037927874 (0xffffffffffffc2) *) + := (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~1~1~1~1~1~1~1~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~0). Notation "'0b11111111111111111111111111111111111111111111111111001110'" (* 72057594037927886 (0xffffffffffffce) *) := (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~1~1~1~1~1~1~1~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~0). +Notation "'0b11111111111111111111111111111111111111111111111111010110'" (* 72057594037927894 (0xffffffffffffd6) *) + := (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~1~1~1~1~1~1~1~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~0). Notation "'0b11111111111111111111111111111111111111111111111111011010'" (* 72057594037927898 (0xffffffffffffda) *) := (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~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111101111'" (* 72057594037927919 (0xffffffffffffef) *) -- cgit v1.2.3