diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-17 16:34:42 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-17 16:34:42 -0400 |
| commit | cbaeb861dda777cfb035593bb625b4397d6e5ef3 (patch) | |
| tree | a72b7bd87638f81ba0dd7cb7669b51a04b162d7d /src/Compilers/Z | |
| parent | 599922047d89a89afe6fca798cb52d5f6adc7615 (diff) | |
Add more constants
Diffstat (limited to 'src/Compilers/Z')
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 9 | ||||
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 15 |
2 files changed, 24 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index e2adc7573..6e240ff87 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -58,6 +58,9 @@ WO~0~0~0~1~1~0~1~1 WO~0~0~0~1~1~1~0~0 WO~0~0~1~1~0~0~1~1 WO~0~1~0~1~0~1~0~1 +WO~1~0~0~0~0~0~0~0 +WO~1~0~0~0~0~0~0 +WO~1~0~0~0~0~0 WO~1~1~1~0~0~0 WO~0~1~0~1 WO~1~0~0~1 @@ -94,12 +97,18 @@ Notation "'0b00011011'" (* 27 (0x1b) *) := (Const WO~0~0~0~1~1~0~1~1). Notation "'0b00011100'" (* 28 (0x1c) *) := (Const WO~0~0~0~1~1~1~0~0). +Notation "'0b100000'" (* 32 (0x20) *) + := (Const WO~1~0~0~0~0~0). Notation "'0b00110011'" (* 51 (0x33) *) := (Const WO~0~0~1~1~0~0~1~1). Notation "'0b111000'" (* 56 (0x38) *) := (Const WO~1~1~1~0~0~0). +Notation "'0b1000000'" (* 64 (0x40) *) + := (Const WO~1~0~0~0~0~0~0). Notation "'0b01010101'" (* 85 (0x55) *) := (Const WO~0~1~0~1~0~1~0~1). +Notation "'0b10000000'" (* 128 (0x80) *) + := (Const WO~1~0~0~0~0~0~0~0). Notation "'0b00000000000000011101101101000001'" (* 121665 (0x1db41) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~0~1~1~0~1~1~0~1~0~0~0~0~0~1). Notation "'0b00000000011111111111111111111111'" (* 8388607 (0x7fffff) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 9d6abe422..b818b97d7 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -60,6 +60,9 @@ WO~0~0~0~1~1~0~1~1 WO~0~0~0~1~1~1~0~0 WO~0~0~1~1~0~0~1~1 WO~0~1~0~1~0~1~0~1 +WO~1~0~0~0~0~0~0~0 +WO~1~0~0~0~0~0~0 +WO~1~0~0~0~0~0 WO~1~1~1~0~0~0 WO~0~1~0~1 WO~1~0~0~1 @@ -122,6 +125,10 @@ Notation "'0x1c'" (* 28 (0x1c) *) := (Const 28%Z). Notation "'0x1c'" (* 28 (0x1c) *) := (Const WO~0~0~0~1~1~1~0~0). +Notation "'0x20'" (* 32 (0x20) *) + := (Const 32%Z). +Notation "'0x20'" (* 32 (0x20) *) + := (Const WO~1~0~0~0~0~0). Notation "'0x33'" (* 51 (0x33) *) := (Const 51%Z). Notation "'0x33'" (* 51 (0x33) *) @@ -130,10 +137,18 @@ Notation "'0x38'" (* 56 (0x38) *) := (Const 56%Z). Notation "'0x38'" (* 56 (0x38) *) := (Const WO~1~1~1~0~0~0). +Notation "'0x40'" (* 64 (0x40) *) + := (Const 64%Z). +Notation "'0x40'" (* 64 (0x40) *) + := (Const WO~1~0~0~0~0~0~0). Notation "'0x55'" (* 85 (0x55) *) := (Const 85%Z). Notation "'0x55'" (* 85 (0x55) *) := (Const WO~0~1~0~1~0~1~0~1). +Notation "'0x80'" (* 128 (0x80) *) + := (Const 128%Z). +Notation "'0x80'" (* 128 (0x80) *) + := (Const WO~1~0~0~0~0~0~0~0). Notation "'0x1db41'" (* 121665 (0x1db41) *) := (Const 121665%Z). Notation "'0x1db41'" (* 121665 (0x1db41) *) |