diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-03 14:42:15 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-03 14:42:15 -0400 |
| commit | e5d16e788da463ab19a92a1c2c040e0c861b229b (patch) | |
| tree | 64c935ff0f0b9c3282f145260efb75c537ef75bf /src/Compilers | |
| parent | 99376c66e4ff240915455d75cf5901f2d38d8ef6 (diff) | |
Add more constant notations
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/BinaryNotationConstants.v | 6 | ||||
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 10 |
2 files changed, 16 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v index eb05ffaba..0f918aca4 100644 --- a/src/Compilers/Z/BinaryNotationConstants.v +++ b/src/Compilers/Z/BinaryNotationConstants.v @@ -72,6 +72,8 @@ nums = tuple(sorted(set(systematic_nums + [ 2097135, 2097143, 2097150, + 4120062, + 4162878, 4188670, 4192254, 4193327, @@ -991,6 +993,10 @@ Notation "'0b1000000000000000000000'" (* 2097152 (0x200000) *) := (Const WO~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). Notation "'0b1000000000000000000001'" (* 2097153 (0x200001) *) := (Const WO~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~1). +Notation "'0b1111101101110111111110'" (* 4120062 (0x3eddfe) *) + := (Const WO~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~0). +Notation "'0b1111111000010100111110'" (* 4162878 (0x3f853e) *) + := (Const WO~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~0). Notation "'0b1111111110100111111110'" (* 4188670 (0x3fe9fe) *) := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~0). Notation "'0b1111111111011111111110'" (* 4192254 (0x3ff7fe) *) diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index 4958fe902..3a76165f5 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -72,6 +72,8 @@ nums = tuple(sorted(set(systematic_nums + [ 2097135, 2097143, 2097150, + 4120062, + 4162878, 4188670, 4192254, 4193327, @@ -1449,6 +1451,14 @@ Notation "'0x200001'" (* 2097153 (0x200001) *) := (Const 2097153%Z). Notation "'0x200001'" (* 2097153 (0x200001) *) := (Const WO~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~1). +Notation "'0x3eddfe'" (* 4120062 (0x3eddfe) *) + := (Const 4120062%Z). +Notation "'0x3eddfe'" (* 4120062 (0x3eddfe) *) + := (Const WO~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~0). +Notation "'0x3f853e'" (* 4162878 (0x3f853e) *) + := (Const 4162878%Z). +Notation "'0x3f853e'" (* 4162878 (0x3f853e) *) + := (Const WO~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~0). Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *) := (Const 4188670%Z). Notation "'0x3fe9fe'" (* 4188670 (0x3fe9fe) *) |