From 47ef3ae951c6e0c994bed467ee52e7c84d15e45a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 18 Oct 2017 23:17:04 -0400 Subject: Add more constant notations --- src/Compilers/Z/BinaryNotationConstants.v | 51 +++++++++++++++++++ src/Compilers/Z/HexNotationConstants.v | 85 +++++++++++++++++++++++++++++++ 2 files changed, 136 insertions(+) (limited to 'src') diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index 868a89eb5..3edd4cb04 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -81,10 +81,13 @@ nums = tuple(sorted(set(systematic_nums + [ 67108861, 67108862, 134217690, + 134217703, 134217710, 134217713, 134217726, 268431360, + 268435441, + 268435445, 268435454, 536870893, 536870906, @@ -94,6 +97,7 @@ nums = tuple(sorted(set(systematic_nums + [ 954437177, 1073741821, 1073741822, + 1332920885, 1749801491, 2147483647, 2863311531, @@ -101,10 +105,14 @@ nums = tuple(sorted(set(systematic_nums + [ 3264175145, 3303820997, 3435973837, + 3707621341, 4008636143, 4042322161, 4294966319, 4294967107, + 4294967179, + 4294967263, + 4294967267, 4294967269, 4294967271, 4294967277, @@ -195,6 +203,7 @@ nums = tuple(sorted(set(systematic_nums + [ 18014398509481981, 18014398509481982, 36028797018963943, + 36028797018963949, 72056494526300160, 72057594037927819, 72057594037927919, @@ -208,6 +217,7 @@ nums = tuple(sorted(set(systematic_nums + [ 288230376151711717, 288230376151711727, 288230376151711741, + 576460752303423467, 576460752303423469, 1117984489315730401, 3353953467947191203, @@ -222,13 +232,17 @@ nums = tuple(sorted(set(systematic_nums + [ 11907422100489763477, 12273715991527008853, 12297829382473034411, + 12754194144713244671, 14757395258967641293, + 14933078535860113213, 14978125529935106013, 15580212934572586289, 17216961135462248175, 17361641481138401521, 18421974275759013887, + 18445336698825998335, 18446726481523507199, + 18446744065119617023, 18446744069414583343, 18446744069414584319, 18446744069414584320, @@ -237,12 +251,15 @@ nums = tuple(sorted(set(systematic_nums + [ 18446744073709551195, 18446744073709551299, 18446744073709551427, + 18446744073709551429, 18446744073709551499, 18446744073709551511, 18446744073709551583, + 18446744073709551585, 18446744073709551587, 18446744073709551589, 18446744073709551591, + 18446744073709551595, 18446744073709551597, 18446744073709551599, 18446744073709551601, @@ -805,6 +822,8 @@ Notation "'0b100000000000000000000000001'" (* 67108865 (0x4000001) *) := (Const WO~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~1). Notation "'0b111111111111111111111011010'" (* 134217690 (0x7ffffda) *) := (Const WO~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~0~1~0). +Notation "'0b111111111111111111111100111'" (* 134217703 (0x7ffffe7) *) + := (Const WO~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~0~1~1~1). Notation "'0b111111111111111111111101110'" (* 134217710 (0x7ffffee) *) := (Const WO~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~0). Notation "'0b111111111111111111111110001'" (* 134217713 (0x7fffff1) *) @@ -819,6 +838,10 @@ 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 "'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) *) + := (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 "'0b1111111111111111111111111110'" (* 268435454 (0xffffffe) *) := (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~1~1~0). Notation "'0b1111111111111111111111111111'" (* 268435455 (0xfffffff) *) @@ -855,6 +878,8 @@ Notation "'0b1000000000000000000000000000000'" (* 1073741824 (0x40000000) *) := (Const WO~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). Notation "'0b1000000000000000000000000000001'" (* 1073741825 (0x40000001) *) := (Const WO~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~1). +Notation "'0b1001111011100101100001000110101'" (* 1332920885 (0x4f72c235) *) + := (Const WO~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1). Notation "'0b1101000010010111101101000010011'" (* 1749801491 (0x684bda13) *) := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1). Notation "'0b1111111111111111111111111111111'" (* 2147483647 (0x7fffffff) *) @@ -873,6 +898,8 @@ Notation "'0b11000100111011000100111011000101'" (* 3303820997 (0xc4ec4ec5) *) := (Const WO~1~1~0~0~0~1~0~0~1~1~1~0~1~1~0~0~0~1~0~0~1~1~1~0~1~1~0~0~0~1~0~1). Notation "'0b11001100110011001100110011001101'" (* 3435973837 (0xcccccccd) *) := (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1). +Notation "'0b11011100111111011100111111011101'" (* 3707621341 (0xdcfdcfdd) *) + := (Const WO~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~1). Notation "'0b11101110111011101110111011101111'" (* 4008636143 (0xeeeeeeef) *) := (Const WO~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~0~1~1~1~1). Notation "'0b11110000111100001111000011110001'" (* 4042322161 (0xf0f0f0f1) *) @@ -881,6 +908,12 @@ Notation "'0b11111111111111111111110000101111'" (* 4294966319 (0xfffffc2f) *) := (Const WO~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 "'0b11111111111111111111111101000011'" (* 4294967107 (0xffffff43) *) := (Const WO~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 "'0b11111111111111111111111110001011'" (* 4294967179 (0xffffff8b) *) + := (Const WO~1~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 "'0b11111111111111111111111111011111'" (* 4294967263 (0xffffffdf) *) + := (Const WO~1~1~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). +Notation "'0b11111111111111111111111111100011'" (* 4294967267 (0xffffffe3) *) + := (Const WO~1~1~1~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~1). Notation "'0b11111111111111111111111111100101'" (* 4294967269 (0xffffffe5) *) := (Const WO~1~1~1~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~0~1). Notation "'0b11111111111111111111111111100111'" (* 4294967271 (0xffffffe7) *) @@ -1199,6 +1232,8 @@ Notation "'0b1000000000000000000000000000000000000000000000000000001'" (* 180143 := (Const WO~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~0~0~0~0~0~0~0~0~1). Notation "'0b1111111111111111111111111111111111111111111111111100111'" (* 36028797018963943 (0x7fffffffffffe7) *) := (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~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111101101'" (* 36028797018963949 (0x7fffffffffffed) *) + := (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~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111'" (* 36028797018963967 (0x7fffffffffffff) *) := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b10000000000000000000000000000000000000000000000000000000'" (* 36028797018963968 (0x80000000000000) *) @@ -1249,6 +1284,8 @@ Notation "'0b10000000000000000000000000000000000000000000000000000000000'" (* 28 := (Const WO~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~0~0~0~0~0~0~0~0~0~0~0~0~0). Notation "'0b10000000000000000000000000000000000000000000000000000000001'" (* 288230376151711745 (0x400000000000001) *) := (Const WO~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~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0b11111111111111111111111111111111111111111111111111111101011'" (* 576460752303423467 (0x7ffffffffffffeb) *) + := (Const WO~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~1~1~1~1~0~1~0~1~1). Notation "'0b11111111111111111111111111111111111111111111111111111101101'" (* 576460752303423469 (0x7ffffffffffffed) *) := (Const WO~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~1~1~1~1~0~1~1~0~1). Notation "'0b11111111111111111111111111111111111111111111111111111111111'" (* 576460752303423487 (0x7ffffffffffffff) *) @@ -1307,8 +1344,12 @@ Notation "'0b1010101001010100111111111010101001010100111111111010101001010101'" := (Const WO~1~0~1~0~1~0~1~0~0~1~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~0~1~0~1~0~1~0~0~1~0~1~0~1~0~0~1~1~1~1~1~1~1~1~1~0~1~0~1~0~1~0~0~1~0~1~0~1~0~1). Notation "'0b1010101010101010101010101010101010101010101010101010101010101011'" (* 12297829382473034411 (0xaaaaaaaaaaaaaaabL) *) := (Const WO~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~1). +Notation "'0b1011000011111111111111111111111111111111111111111111111111111111'" (* 12754194144713244671 (0xb0ffffffffffffffL) *) + := (Const WO~1~0~1~1~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~1~1~1~1~1~1). Notation "'0b1100110011001100110011001100110011001100110011001100110011001101'" (* 14757395258967641293 (0xcccccccccccccccdL) *) := (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1). +Notation "'0b1100111100111100111100111100111100111100111100111100111100111101'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *) + := (Const WO~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~1). Notation "'0b1100111111011100111111011100111111011100111111011100111111011101'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *) := (Const WO~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~1). Notation "'0b1101100000111000000010010001110111010010001001010011010100110001'" (* 15580212934572586289 (0xd838091dd2253531L) *) @@ -1319,8 +1360,12 @@ Notation "'0b1111000011110000111100001111000011110000111100001111000011110001'" := (Const WO~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~0~1~1~1~1~0~0~0~1). Notation "'0b1111111110100111111111111111111111111111111111111111111111111111'" (* 18421974275759013887 (0xffa7ffffffffffffL) *) := (Const WO~1~1~1~1~1~1~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b1111111111111010111111111111111111111111111111111111111111111111'" (* 18445336698825998335 (0xfffaffffffffffffL) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~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~1~1~1~1). Notation "'0b1111111111111111111011111111111111111111111111111111111111111111'" (* 18446726481523507199 (0xffffefffffffffffL) *) := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0b1111111111111111111111111111110111111111111111111111111111111111'" (* 18446744065119617023 (0xfffffffdffffffffL) *) + := (Const WO~1~1~1~1~1~1~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~1~1~1~1~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 "'0b1111111111111111111111111111111011111111111111111111110000101111'" (* 18446744069414583343 (0xfffffffefffffc2fL) *) := (Const WO~1~1~1~1~1~1~1~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~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 "'0b1111111111111111111111111111111011111111111111111111111111111111'" (* 18446744069414584319 (0xfffffffeffffffffL) *) @@ -1337,18 +1382,24 @@ Notation "'0b1111111111111111111111111111111111111111111111111111111011000011'" := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~0~0~0~1~1). Notation "'0b1111111111111111111111111111111111111111111111111111111101000011'" (* 18446744073709551427 (0xffffffffffffff43L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111101000101'" (* 18446744073709551429 (0xffffffffffffff45L) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111110001011'" (* 18446744073709551499 (0xffffffffffffff8bL) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111110010111'" (* 18446744073709551511 (0xffffffffffffff97L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~0~1~1~1). Notation "'0b1111111111111111111111111111111111111111111111111111111111011111'" (* 18446744073709551583 (0xffffffffffffffdfL) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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). +Notation "'0b1111111111111111111111111111111111111111111111111111111111100001'" (* 18446744073709551585 (0xffffffffffffffe1L) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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). Notation "'0b1111111111111111111111111111111111111111111111111111111111100011'" (* 18446744073709551587 (0xffffffffffffffe3L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~1). Notation "'0b1111111111111111111111111111111111111111111111111111111111100101'" (* 18446744073709551589 (0xffffffffffffffe5L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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~0~1). Notation "'0b1111111111111111111111111111111111111111111111111111111111100111'" (* 18446744073709551591 (0xffffffffffffffe7L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111111101011'" (* 18446744073709551595 (0xffffffffffffffebL) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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). Notation "'0b1111111111111111111111111111111111111111111111111111111111101101'" (* 18446744073709551597 (0xffffffffffffffedL) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111111101111'" (* 18446744073709551599 (0xffffffffffffffefL) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index ba7a8c5d8..822fa7b7b 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -81,10 +81,13 @@ nums = tuple(sorted(set(systematic_nums + [ 67108861, 67108862, 134217690, + 134217703, 134217710, 134217713, 134217726, 268431360, + 268435441, + 268435445, 268435454, 536870893, 536870906, @@ -94,6 +97,7 @@ nums = tuple(sorted(set(systematic_nums + [ 954437177, 1073741821, 1073741822, + 1332920885, 1749801491, 2147483647, 2863311531, @@ -101,10 +105,14 @@ nums = tuple(sorted(set(systematic_nums + [ 3264175145, 3303820997, 3435973837, + 3707621341, 4008636143, 4042322161, 4294966319, 4294967107, + 4294967179, + 4294967263, + 4294967267, 4294967269, 4294967271, 4294967277, @@ -195,6 +203,7 @@ nums = tuple(sorted(set(systematic_nums + [ 18014398509481981, 18014398509481982, 36028797018963943, + 36028797018963949, 72056494526300160, 72057594037927819, 72057594037927919, @@ -208,6 +217,7 @@ nums = tuple(sorted(set(systematic_nums + [ 288230376151711717, 288230376151711727, 288230376151711741, + 576460752303423467, 576460752303423469, 1117984489315730401, 3353953467947191203, @@ -222,13 +232,17 @@ nums = tuple(sorted(set(systematic_nums + [ 11907422100489763477, 12273715991527008853, 12297829382473034411, + 12754194144713244671, 14757395258967641293, + 14933078535860113213, 14978125529935106013, 15580212934572586289, 17216961135462248175, 17361641481138401521, 18421974275759013887, + 18445336698825998335, 18446726481523507199, + 18446744065119617023, 18446744069414583343, 18446744069414584319, 18446744069414584320, @@ -237,12 +251,15 @@ nums = tuple(sorted(set(systematic_nums + [ 18446744073709551195, 18446744073709551299, 18446744073709551427, + 18446744073709551429, 18446744073709551499, 18446744073709551511, 18446744073709551583, + 18446744073709551585, 18446744073709551587, 18446744073709551589, 18446744073709551591, + 18446744073709551595, 18446744073709551597, 18446744073709551599, 18446744073709551601, @@ -1311,6 +1328,10 @@ Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *) := (Const 134217690%Z). Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *) := (Const WO~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~0~1~0). +Notation "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *) + := (Const 134217703%Z). +Notation "'0x7ffffe7'" (* 134217703 (0x7ffffe7) *) + := (Const WO~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~0~1~1~1). Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *) := (Const 134217710%Z). Notation "'0x7ffffee'" (* 134217710 (0x7ffffee) *) @@ -1339,6 +1360,14 @@ 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 "'0xffffff1'" (* 268435441 (0xffffff1) *) + := (Const 268435441%Z). +Notation "'0xffffff1'" (* 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 "'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 "'0xffffffe'" (* 268435454 (0xffffffe) *) := (Const 268435454%Z). Notation "'0xffffffe'" (* 268435454 (0xffffffe) *) @@ -1411,6 +1440,10 @@ Notation "'0x40000001'" (* 1073741825 (0x40000001) *) := (Const 1073741825%Z). Notation "'0x40000001'" (* 1073741825 (0x40000001) *) := (Const WO~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~1). +Notation "'0x4f72c235'" (* 1332920885 (0x4f72c235) *) + := (Const 1332920885%Z). +Notation "'0x4f72c235'" (* 1332920885 (0x4f72c235) *) + := (Const WO~0~1~0~0~1~1~1~1~0~1~1~1~0~0~1~0~1~1~0~0~0~0~1~0~0~0~1~1~0~1~0~1). Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *) := (Const 1749801491%Z). Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *) @@ -1447,6 +1480,10 @@ Notation "'0xcccccccd'" (* 3435973837 (0xcccccccd) *) := (Const 3435973837%Z). Notation "'0xcccccccd'" (* 3435973837 (0xcccccccd) *) := (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1). +Notation "'0xdcfdcfdd'" (* 3707621341 (0xdcfdcfdd) *) + := (Const 3707621341%Z). +Notation "'0xdcfdcfdd'" (* 3707621341 (0xdcfdcfdd) *) + := (Const WO~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~0~1~1~1~1~1~1~0~1~1~1~0~1). Notation "'0xeeeeeeef'" (* 4008636143 (0xeeeeeeef) *) := (Const 4008636143%Z). Notation "'0xeeeeeeef'" (* 4008636143 (0xeeeeeeef) *) @@ -1463,6 +1500,18 @@ Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *) := (Const 4294967107%Z). Notation "'0xffffff43'" (* 4294967107 (0xffffff43) *) := (Const WO~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 "'0xffffff8b'" (* 4294967179 (0xffffff8b) *) + := (Const 4294967179%Z). +Notation "'0xffffff8b'" (* 4294967179 (0xffffff8b) *) + := (Const WO~1~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 "'0xffffffdf'" (* 4294967263 (0xffffffdf) *) + := (Const 4294967263%Z). +Notation "'0xffffffdf'" (* 4294967263 (0xffffffdf) *) + := (Const WO~1~1~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). +Notation "'0xffffffe3'" (* 4294967267 (0xffffffe3) *) + := (Const 4294967267%Z). +Notation "'0xffffffe3'" (* 4294967267 (0xffffffe3) *) + := (Const WO~1~1~1~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~1). Notation "'0xffffffe5'" (* 4294967269 (0xffffffe5) *) := (Const 4294967269%Z). Notation "'0xffffffe5'" (* 4294967269 (0xffffffe5) *) @@ -2099,6 +2148,10 @@ Notation "'0x7fffffffffffe7'" (* 36028797018963943 (0x7fffffffffffe7) *) := (Const 36028797018963943%Z). Notation "'0x7fffffffffffe7'" (* 36028797018963943 (0x7fffffffffffe7) *) := (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~1~1~1~1~1~1~1~1~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 "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *) + := (Const 36028797018963949%Z). +Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *) + := (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~1~1~1~1~1~1~1~1~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 "'0x7fffffffffffff'" (* 36028797018963967 (0x7fffffffffffff) *) := (Const 36028797018963967%Z). Notation "'0x7fffffffffffff'" (* 36028797018963967 (0x7fffffffffffff) *) @@ -2199,6 +2252,10 @@ Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *) := (Const 288230376151711745%Z). Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *) := (Const WO~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~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0x7ffffffffffffeb'" (* 576460752303423467 (0x7ffffffffffffeb) *) + := (Const 576460752303423467%Z). +Notation "'0x7ffffffffffffeb'" (* 576460752303423467 (0x7ffffffffffffeb) *) + := (Const WO~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~1~1~1~1~0~1~0~1~1). Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *) := (Const 576460752303423469%Z). Notation "'0x7ffffffffffffed'" (* 576460752303423469 (0x7ffffffffffffed) *) @@ -2315,10 +2372,18 @@ Notation "'0xaaaaaaaaaaaaaaabL'" (* 12297829382473034411 (0xaaaaaaaaaaaaaaabL) * := (Const 12297829382473034411%Z). Notation "'0xaaaaaaaaaaaaaaabL'" (* 12297829382473034411 (0xaaaaaaaaaaaaaaabL) *) := (Const WO~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~0~1~1). +Notation "'0xb0ffffffffffffffL'" (* 12754194144713244671 (0xb0ffffffffffffffL) *) + := (Const 12754194144713244671%Z). +Notation "'0xb0ffffffffffffffL'" (* 12754194144713244671 (0xb0ffffffffffffffL) *) + := (Const WO~1~0~1~1~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~1~1~1~1~1~1). Notation "'0xcccccccccccccccdL'" (* 14757395258967641293 (0xcccccccccccccccdL) *) := (Const 14757395258967641293%Z). Notation "'0xcccccccccccccccdL'" (* 14757395258967641293 (0xcccccccccccccccdL) *) := (Const WO~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~0~1~1~0~1). +Notation "'0xcf3cf3cf3cf3cf3dL'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *) + := (Const 14933078535860113213%Z). +Notation "'0xcf3cf3cf3cf3cf3dL'" (* 14933078535860113213 (0xcf3cf3cf3cf3cf3dL) *) + := (Const WO~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~0~1~1~1~1~0~1). Notation "'0xcfdcfdcfdcfdcfddL'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *) := (Const 14978125529935106013%Z). Notation "'0xcfdcfdcfdcfdcfddL'" (* 14978125529935106013 (0xcfdcfdcfdcfdcfddL) *) @@ -2339,10 +2404,18 @@ Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) * := (Const 18421974275759013887%Z). Notation "'0xffa7ffffffffffffL'" (* 18421974275759013887 (0xffa7ffffffffffffL) *) := (Const WO~1~1~1~1~1~1~1~1~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xfffaffffffffffffL'" (* 18445336698825998335 (0xfffaffffffffffffL) *) + := (Const 18445336698825998335%Z). +Notation "'0xfffaffffffffffffL'" (* 18445336698825998335 (0xfffaffffffffffffL) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~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~1~1~1~1). Notation "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *) := (Const 18446726481523507199%Z). Notation "'0xffffefffffffffffL'" (* 18446726481523507199 (0xffffefffffffffffL) *) := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xfffffffdffffffffL'" (* 18446744065119617023 (0xfffffffdffffffffL) *) + := (Const 18446744065119617023%Z). +Notation "'0xfffffffdffffffffL'" (* 18446744065119617023 (0xfffffffdffffffffL) *) + := (Const WO~1~1~1~1~1~1~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~1~1~1~1~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 "'0xfffffffefffffc2fL'" (* 18446744069414583343 (0xfffffffefffffc2fL) *) := (Const 18446744069414583343%Z). Notation "'0xfffffffefffffc2fL'" (* 18446744069414583343 (0xfffffffefffffc2fL) *) @@ -2375,6 +2448,10 @@ Notation "'0xffffffffffffff43L'" (* 18446744073709551427 (0xffffffffffffff43L) * := (Const 18446744073709551427%Z). Notation "'0xffffffffffffff43L'" (* 18446744073709551427 (0xffffffffffffff43L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0xffffffffffffff45L'" (* 18446744073709551429 (0xffffffffffffff45L) *) + := (Const 18446744073709551429%Z). +Notation "'0xffffffffffffff45L'" (* 18446744073709551429 (0xffffffffffffff45L) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0xffffffffffffff8bL'" (* 18446744073709551499 (0xffffffffffffff8bL) *) := (Const 18446744073709551499%Z). Notation "'0xffffffffffffff8bL'" (* 18446744073709551499 (0xffffffffffffff8bL) *) @@ -2387,6 +2464,10 @@ Notation "'0xffffffffffffffdfL'" (* 18446744073709551583 (0xffffffffffffffdfL) * := (Const 18446744073709551583%Z). Notation "'0xffffffffffffffdfL'" (* 18446744073709551583 (0xffffffffffffffdfL) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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). +Notation "'0xffffffffffffffe1L'" (* 18446744073709551585 (0xffffffffffffffe1L) *) + := (Const 18446744073709551585%Z). +Notation "'0xffffffffffffffe1L'" (* 18446744073709551585 (0xffffffffffffffe1L) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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). Notation "'0xffffffffffffffe3L'" (* 18446744073709551587 (0xffffffffffffffe3L) *) := (Const 18446744073709551587%Z). Notation "'0xffffffffffffffe3L'" (* 18446744073709551587 (0xffffffffffffffe3L) *) @@ -2399,6 +2480,10 @@ Notation "'0xffffffffffffffe7L'" (* 18446744073709551591 (0xffffffffffffffe7L) * := (Const 18446744073709551591%Z). Notation "'0xffffffffffffffe7L'" (* 18446744073709551591 (0xffffffffffffffe7L) *) := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0xffffffffffffffebL'" (* 18446744073709551595 (0xffffffffffffffebL) *) + := (Const 18446744073709551595%Z). +Notation "'0xffffffffffffffebL'" (* 18446744073709551595 (0xffffffffffffffebL) *) + := (Const WO~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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). Notation "'0xffffffffffffffedL'" (* 18446744073709551597 (0xffffffffffffffedL) *) := (Const 18446744073709551597%Z). Notation "'0xffffffffffffffedL'" (* 18446744073709551597 (0xffffffffffffffedL) *) -- cgit v1.2.3