From d050cfbe03cc56e6a26d2956a880d07247828555 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 16 Oct 2017 02:44:14 -0400 Subject: Add more notations --- src/Compilers/Z/BinaryNotationConstants.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Compilers/Z/BinaryNotationConstants.v') diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index 962c9a3a8..70784511a 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -97,7 +97,9 @@ nums = tuple(list(range(128)) + [ 536870911, 1073741822, 1073741823, + 2147483647, 4294967107, + 4294967271, 4294967294, 4294967295, 8589934559, @@ -130,6 +132,7 @@ nums = tuple(list(range(128)) + [ 549755813887, 1099511627761, 1099511627775, + 1425929142271, 2199023255543, 2199023255551, 4398046511079, @@ -665,8 +668,12 @@ Notation "'0b111111111111111111111111111110'" (* 1073741822 (0x3ffffffe) *) := (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~1~1~1~0). Notation "'0b111111111111111111111111111111'" (* 1073741823 (0x3fffffff) *) := (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~1~1~1~1). +Notation "'0b1111111111111111111111111111111'" (* 2147483647 (0x7fffffff) *) + := (Const WO~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). 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 "'0b11111111111111111111111111100111'" (* 4294967271 (0xffffffe7) *) + := (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~1~1). Notation "'0b11111111111111111111111111111110'" (* 4294967294 (0xfffffffe) *) := (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). Notation "'0b11111111111111111111111111111111'" (* 4294967295 (0xffffffff) *) @@ -731,6 +738,8 @@ Notation "'0b1111111111111111111111111111111111110001'" (* 1099511627761 (0xffff := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111'" (* 1099511627775 (0xffffffffff) *) := (Const WO~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~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b10100101111111111111111111111111111111111'" (* 1425929142271 (0x14bffffffff) *) + := (Const WO~0~0~0~0~0~0~0~0~0~0~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). Notation "'0b11111111111111111111111111111111111110111'" (* 2199023255543 (0x1fffffffff7) *) := (Const WO~0~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). Notation "'0b11111111111111111111111111111111111111111'" (* 2199023255551 (0x1ffffffffff) *) -- cgit v1.2.3