diff options
| author |  leino <unknown> | 2014-10-23 21:52:12 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-23 21:52:12 -0700 |
| commit | 40f36d68b8cb9489d052ababada29539c7d8de92 (patch) | |
| tree | 46b3b65776325e0bb78b5a5bfae1d483fec0485a | |
| parent | 07ac1e4cfe6cdaf73a5bfa8b863728beae2a4c86 (diff) | |
Allow underscores in numeric literals (and in field/destructor names that are written as numeric strings). The
underscores have no semantic meaning, but can help a human parse the numbers.
| -rw-r--r-- | Source/Dafny/Dafny.atg | 35 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 361 | ||||
| -rw-r--r-- | Source/Dafny/Util.cs | 14 | ||||
| -rw-r--r-- | Test/dafny0/Basics.dfy | 28 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 17 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/RealTypes.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny4/BinarySearch.dfy | 6 |
9 files changed, 269 insertions, 215 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2903d471..20765b74 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -181,7 +181,7 @@ CHARACTERS idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
- ischarMinusTick = idchar - '\''.
+ idcharMinusTick = idchar - '\''.
/* string literals */
charChar = ANY - '\'' - '\\' - cr - lf.
stringChar = ANY - '"' - '\\' - cr - lf.
@@ -197,12 +197,12 @@ TOKENS | 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
| 'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}
| "'" [ idchar ] /* if char 0 is a '\'' and length is 1 or 2, then it is an identifier */
- | "'" idchar ischarMinusTick /* if char 0 is '\'' and length is 3, then it is an identifier provided char 2 is not '\'' */
+ | "'" idchar idcharMinusTick /* if char 0 is '\'' and length is 3, then it is an identifier provided char 2 is not '\'' */
| "'" idchar idchar idchar { idchar } /* if char 0 is '\'' and length exceeds 3, then it is an identifier */
.
- digits = digit {digit}.
- hexdigits = "0x" hexdigit {hexdigit}.
- decimaldigits = digit {digit} '.' digit {digit}.
+ digits = digit {['_'] digit}.
+ hexdigits = "0x" hexdigit {['_'] hexdigit}.
+ decimaldigits = digit {['_'] digit} '.' digit {['_'] digit}.
arrayToken = "array" [posDigit {digit}].
charToken =
"'"
@@ -2659,31 +2659,36 @@ WildIdent<out IToken/*!*/ x, bool allowWildcardId> .
Nat<out BigInteger n>
-= (. n = BigInteger.Zero; .)
- (digits
- (. try {
- n = BigInteger.Parse(t.val);
+= (. n = BigInteger.Zero;
+ string S;
+ .)
+ ( digits
+ (. S = Util.RemoveUnderscores(t.val);
+ try {
+ n = BigInteger.Parse(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
}
.)
- |hexdigits
- (. try {
+ | hexdigits
+ (. S = Util.RemoveUnderscores(t.val.Substring(2));
+ try {
// note: leading 0 required when parsing positive hex numbers
- n = BigInteger.Parse("0" + t.val.Substring(2), System.Globalization.NumberStyles.HexNumber);
+ n = BigInteger.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
}
.)
- )
+ )
.
Dec<out Basetypes.BigDec d>
= (. d = Basetypes.BigDec.ZERO; .)
(decimaldigits
- (. try {
- d = Basetypes.BigDec.FromString(t.val);
+ (. var S = Util.RemoveUnderscores(t.val);
+ try {
+ d = Basetypes.BigDec.FromString(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
d = Basetypes.BigDec.ZERO;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 8755d275..6ce29b9c 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -3632,11 +3632,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void Nat(out BigInteger n) {
- n = BigInteger.Zero;
+ n = BigInteger.Zero;
+ string S;
+
if (la.kind == 2) {
Get();
+ S = Util.RemoveUnderscores(t.val);
try {
- n = BigInteger.Parse(t.val);
+ n = BigInteger.Parse(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -3644,9 +3647,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 3) {
Get();
+ S = Util.RemoveUnderscores(t.val.Substring(2));
try {
// note: leading 0 required when parsing positive hex numbers
- n = BigInteger.Parse("0" + t.val.Substring(2), System.Globalization.NumberStyles.HexNumber);
+ n = BigInteger.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -3658,8 +3662,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Dec(out Basetypes.BigDec d) {
d = Basetypes.BigDec.ZERO;
Expect(4);
+ var S = Util.RemoveUnderscores(t.val);
try {
- d = Basetypes.BigDec.FromString(t.val);
+ d = Basetypes.BigDec.FromString(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
d = Basetypes.BigDec.ZERO;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 1eb22802..06493434 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -253,47 +253,47 @@ public class Scanner { for (int i = 65; i <= 90; ++i) start[i] = 1;
for (int i = 95; i <= 95; ++i) start[i] = 1;
for (int i = 98; i <= 122; ++i) start[i] = 1;
- for (int i = 49; i <= 57; ++i) start[i] = 38;
- start[97] = 39;
- start[39] = 40;
- start[48] = 41;
- start[34] = 19;
- start[64] = 24;
- start[58] = 86;
- start[124] = 87;
- start[59] = 27;
- start[61] = 88;
- start[45] = 89;
- start[123] = 30;
- start[125] = 31;
- start[40] = 32;
- start[41] = 33;
- start[42] = 34;
- start[33] = 90;
- start[44] = 55;
- start[46] = 91;
- start[60] = 92;
- start[62] = 93;
- start[96] = 57;
- start[91] = 60;
- start[93] = 61;
- start[35] = 62;
- start[8800] = 65;
- start[8804] = 66;
- start[8805] = 67;
- start[8660] = 69;
- start[8658] = 71;
- start[8656] = 72;
- start[38] = 73;
- start[8743] = 75;
- start[8744] = 77;
- start[43] = 78;
- start[47] = 79;
- start[37] = 80;
- start[172] = 81;
- start[8704] = 82;
- start[8707] = 83;
- start[8226] = 85;
+ for (int i = 49; i <= 57; ++i) start[i] = 40;
+ start[97] = 41;
+ start[39] = 42;
+ start[48] = 43;
+ start[34] = 21;
+ start[64] = 26;
+ start[58] = 89;
+ start[124] = 90;
+ start[59] = 29;
+ start[61] = 91;
+ start[45] = 92;
+ start[123] = 32;
+ start[125] = 33;
+ start[40] = 34;
+ start[41] = 35;
+ start[42] = 36;
+ start[33] = 93;
+ start[44] = 58;
+ start[46] = 94;
+ start[60] = 95;
+ start[62] = 96;
+ start[96] = 60;
+ start[91] = 63;
+ start[93] = 64;
+ start[35] = 65;
+ start[8800] = 68;
+ start[8804] = 69;
+ start[8805] = 70;
+ start[8660] = 72;
+ start[8658] = 74;
+ start[8656] = 75;
+ start[38] = 76;
+ start[8743] = 78;
+ start[8744] = 80;
+ start[43] = 81;
+ start[47] = 82;
+ start[37] = 83;
+ start[172] = 84;
+ start[8704] = 85;
+ start[8707] = 86;
+ start[8226] = 88;
start[Buffer.EOF] = -1;
}
@@ -639,280 +639,293 @@ public class Scanner { case 10:
recEnd = pos; recKind = 3;
if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 10;}
+ else if (ch == '_') {AddCh(); goto case 11;}
else {t.kind = 3; break;}
case 11:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 10;}
else {goto case 0;}
case 12:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+ else {goto case 0;}
+ case 13:
recEnd = pos; recKind = 4;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+ else if (ch == '_') {AddCh(); goto case 14;}
else {t.kind = 4; break;}
- case 13:
- if (ch == 39) {AddCh(); goto case 18;}
- else {goto case 0;}
case 14:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 15;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
else {goto case 0;}
case 15:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 16;}
+ if (ch == 39) {AddCh(); goto case 20;}
else {goto case 0;}
case 16:
if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 17;}
else {goto case 0;}
case 17:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 13;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 18;}
else {goto case 0;}
case 18:
- {t.kind = 6; break;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 19;}
+ else {goto case 0;}
case 19:
- if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 19;}
- else if (ch == '"') {AddCh(); goto case 26;}
- else if (ch == 92) {AddCh(); goto case 44;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 15;}
else {goto case 0;}
case 20:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 21;}
- else {goto case 0;}
+ {t.kind = 6; break;}
case 21:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 22;}
+ if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 21;}
+ else if (ch == '"') {AddCh(); goto case 28;}
+ else if (ch == 92) {AddCh(); goto case 46;}
else {goto case 0;}
case 22:
if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 23;}
else {goto case 0;}
case 23:
- if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 19;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 24;}
else {goto case 0;}
case 24:
- if (ch == '"') {AddCh(); goto case 25;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 25;}
else {goto case 0;}
case 25:
- if (ch <= '!' || ch >= '#' && ch <= 65535) {AddCh(); goto case 25;}
- else if (ch == '"') {AddCh(); goto case 45;}
+ if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 21;}
else {goto case 0;}
case 26:
- {t.kind = 7; break;}
+ if (ch == '"') {AddCh(); goto case 27;}
+ else {goto case 0;}
case 27:
- {t.kind = 10; break;}
+ if (ch <= '!' || ch >= '#' && ch <= 65535) {AddCh(); goto case 27;}
+ else if (ch == '"') {AddCh(); goto case 47;}
+ else {goto case 0;}
case 28:
- {t.kind = 11; break;}
+ {t.kind = 7; break;}
case 29:
- {t.kind = 12; break;}
+ {t.kind = 10; break;}
case 30:
- {t.kind = 15; break;}
+ {t.kind = 11; break;}
case 31:
- {t.kind = 16; break;}
+ {t.kind = 12; break;}
case 32:
- {t.kind = 17; break;}
+ {t.kind = 15; break;}
case 33:
- {t.kind = 18; break;}
+ {t.kind = 16; break;}
case 34:
- {t.kind = 19; break;}
+ {t.kind = 17; break;}
case 35:
- if (ch == 'n') {AddCh(); goto case 36;}
- else {goto case 0;}
+ {t.kind = 18; break;}
case 36:
- if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch >= '[' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 37;}
- else {goto case 0;}
+ {t.kind = 19; break;}
case 37:
+ if (ch == 'n') {AddCh(); goto case 38;}
+ else {goto case 0;}
+ case 38:
+ if (ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch >= '[' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {apx++; AddCh(); goto case 39;}
+ else {goto case 0;}
+ case 39:
{
tlen -= apx;
SetScannerBehindT();
t.kind = 20; break;}
- case 38:
+ case 40:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
- else if (ch == '.') {AddCh(); goto case 11;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 40;}
+ else if (ch == '_') {AddCh(); goto case 48;}
+ else if (ch == '.') {AddCh(); goto case 12;}
else {t.kind = 2; break;}
- case 39:
+ case 41:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 2;}
- else if (ch == 'r') {AddCh(); goto case 46;}
+ else if (ch == 'r') {AddCh(); goto case 49;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 40:
+ case 42:
recEnd = pos; recKind = 1;
- if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 47;}
- else if (ch == 39) {AddCh(); goto case 48;}
- else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {AddCh(); goto case 13;}
- else if (ch == 92) {AddCh(); goto case 43;}
+ if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 50;}
+ else if (ch == 39) {AddCh(); goto case 51;}
+ else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {AddCh(); goto case 15;}
+ else if (ch == 92) {AddCh(); goto case 45;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 41:
+ case 43:
recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 40;}
+ else if (ch == '_') {AddCh(); goto case 48;}
else if (ch == 'x') {AddCh(); goto case 9;}
- else if (ch == '.') {AddCh(); goto case 11;}
+ else if (ch == '.') {AddCh(); goto case 12;}
else {t.kind = 2; break;}
- case 42:
+ case 44:
recEnd = pos; recKind = 1;
- if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 42;}
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 44;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 43:
- if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 13;}
- else if (ch == 'u') {AddCh(); goto case 14;}
+ case 45:
+ if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 15;}
+ else if (ch == 'u') {AddCh(); goto case 16;}
else {goto case 0;}
- case 44:
- if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 19;}
- else if (ch == 'u') {AddCh(); goto case 20;}
+ case 46:
+ if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 21;}
+ else if (ch == 'u') {AddCh(); goto case 22;}
else {goto case 0;}
- case 45:
+ case 47:
recEnd = pos; recKind = 7;
- if (ch == '"') {AddCh(); goto case 25;}
+ if (ch == '"') {AddCh(); goto case 27;}
else {t.kind = 7; break;}
- case 46:
+ case 48:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 40;}
+ else {goto case 0;}
+ case 49:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 3;}
- else if (ch == 'r') {AddCh(); goto case 49;}
+ else if (ch == 'r') {AddCh(); goto case 52;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 47:
+ case 50:
recEnd = pos; recKind = 1;
- if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 50;}
- else if (ch == 39) {AddCh(); goto case 51;}
+ if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 53;}
+ else if (ch == 39) {AddCh(); goto case 54;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 48:
+ case 51:
recEnd = pos; recKind = 1;
- if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 50;}
+ if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 53;}
else if (ch == 39) {AddCh(); goto case 7;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 49:
+ case 52:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'b' && ch <= 'z') {AddCh(); goto case 4;}
- else if (ch == 'a') {AddCh(); goto case 52;}
+ else if (ch == 'a') {AddCh(); goto case 55;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 50:
+ case 53:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 8;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 51:
+ case 54:
recEnd = pos; recKind = 6;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 8;}
else {t.kind = 6; break;}
- case 52:
+ case 55:
recEnd = pos; recKind = 1;
if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'x' || ch == 'z') {AddCh(); goto case 5;}
- else if (ch == 'y') {AddCh(); goto case 53;}
+ else if (ch == 'y') {AddCh(); goto case 56;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
- case 53:
+ case 56:
recEnd = pos; recKind = 5;
if (ch == 39 || ch == '0' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
- else if (ch >= '1' && ch <= '9') {AddCh(); goto case 54;}
+ else if (ch >= '1' && ch <= '9') {AddCh(); goto case 57;}
else {t.kind = 5; break;}
- case 54:
+ case 57:
recEnd = pos; recKind = 5;
- if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 42;}
- else if (ch >= '0' && ch <= '9') {AddCh(); goto case 54;}
+ if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 44;}
+ else if (ch >= '0' && ch <= '9') {AddCh(); goto case 57;}
else {t.kind = 5; break;}
- case 55:
+ case 58:
{t.kind = 38; break;}
- case 56:
+ case 59:
{t.kind = 45; break;}
- case 57:
+ case 60:
{t.kind = 73; break;}
- case 58:
+ case 61:
{t.kind = 77; break;}
- case 59:
+ case 62:
{t.kind = 79; break;}
- case 60:
+ case 63:
{t.kind = 82; break;}
- case 61:
+ case 64:
{t.kind = 83; break;}
- case 62:
+ case 65:
{t.kind = 96; break;}
- case 63:
+ case 66:
{t.kind = 98; break;}
- case 64:
+ case 67:
{t.kind = 99; break;}
- case 65:
+ case 68:
{t.kind = 100; break;}
- case 66:
+ case 69:
{t.kind = 101; break;}
- case 67:
+ case 70:
{t.kind = 102; break;}
- case 68:
+ case 71:
{t.kind = 103; break;}
- case 69:
+ case 72:
{t.kind = 104; break;}
- case 70:
+ case 73:
{t.kind = 105; break;}
- case 71:
+ case 74:
{t.kind = 106; break;}
- case 72:
+ case 75:
{t.kind = 108; break;}
- case 73:
- if (ch == '&') {AddCh(); goto case 74;}
+ case 76:
+ if (ch == '&') {AddCh(); goto case 77;}
else {goto case 0;}
- case 74:
+ case 77:
{t.kind = 109; break;}
- case 75:
+ case 78:
{t.kind = 110; break;}
- case 76:
+ case 79:
{t.kind = 111; break;}
- case 77:
+ case 80:
{t.kind = 112; break;}
- case 78:
+ case 81:
{t.kind = 115; break;}
- case 79:
+ case 82:
{t.kind = 117; break;}
- case 80:
+ case 83:
{t.kind = 118; break;}
- case 81:
+ case 84:
{t.kind = 119; break;}
- case 82:
+ case 85:
{t.kind = 128; break;}
- case 83:
+ case 86:
{t.kind = 130; break;}
- case 84:
+ case 87:
{t.kind = 131; break;}
- case 85:
+ case 88:
{t.kind = 132; break;}
- case 86:
+ case 89:
recEnd = pos; recKind = 8;
- if (ch == '=') {AddCh(); goto case 58;}
- else if (ch == '|') {AddCh(); goto case 59;}
- else if (ch == ':') {AddCh(); goto case 84;}
+ if (ch == '=') {AddCh(); goto case 61;}
+ else if (ch == '|') {AddCh(); goto case 62;}
+ else if (ch == ':') {AddCh(); goto case 87;}
else {t.kind = 8; break;}
- case 87:
+ case 90:
recEnd = pos; recKind = 9;
- if (ch == '|') {AddCh(); goto case 76;}
+ if (ch == '|') {AddCh(); goto case 79;}
else {t.kind = 9; break;}
- case 88:
+ case 91:
recEnd = pos; recKind = 27;
- if (ch == '>') {AddCh(); goto case 28;}
- else if (ch == '=') {AddCh(); goto case 94;}
+ if (ch == '>') {AddCh(); goto case 30;}
+ else if (ch == '=') {AddCh(); goto case 97;}
else {t.kind = 27; break;}
- case 89:
+ case 92:
recEnd = pos; recKind = 116;
- if (ch == '>') {AddCh(); goto case 29;}
+ if (ch == '>') {AddCh(); goto case 31;}
else {t.kind = 116; break;}
- case 90:
+ case 93:
recEnd = pos; recKind = 114;
- if (ch == 'i') {AddCh(); goto case 35;}
- else if (ch == '=') {AddCh(); goto case 64;}
+ if (ch == 'i') {AddCh(); goto case 37;}
+ else if (ch == '=') {AddCh(); goto case 67;}
else {t.kind = 114; break;}
- case 91:
+ case 94:
recEnd = pos; recKind = 69;
- if (ch == '.') {AddCh(); goto case 95;}
+ if (ch == '.') {AddCh(); goto case 98;}
else {t.kind = 69; break;}
- case 92:
+ case 95:
recEnd = pos; recKind = 46;
- if (ch == '=') {AddCh(); goto case 96;}
+ if (ch == '=') {AddCh(); goto case 99;}
else {t.kind = 46; break;}
- case 93:
+ case 96:
recEnd = pos; recKind = 47;
- if (ch == '=') {AddCh(); goto case 63;}
+ if (ch == '=') {AddCh(); goto case 66;}
else {t.kind = 47; break;}
- case 94:
+ case 97:
recEnd = pos; recKind = 41;
- if (ch == '>') {AddCh(); goto case 70;}
+ if (ch == '>') {AddCh(); goto case 73;}
else {t.kind = 41; break;}
- case 95:
+ case 98:
recEnd = pos; recKind = 127;
- if (ch == '.') {AddCh(); goto case 56;}
+ if (ch == '.') {AddCh(); goto case 59;}
else {t.kind = 127; break;}
- case 96:
+ case 99:
recEnd = pos; recKind = 97;
- if (ch == '=') {AddCh(); goto case 97;}
+ if (ch == '=') {AddCh(); goto case 100;}
else {t.kind = 97; break;}
- case 97:
+ case 100:
recEnd = pos; recKind = 107;
- if (ch == '>') {AddCh(); goto case 68;}
+ if (ch == '>') {AddCh(); goto case 71;}
else {t.kind = 107; break;}
}
diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index bc4017c0..f9421659 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -68,6 +68,20 @@ namespace Microsoft.Dafny { }
/// <summary>
+ /// Returns s but with all occurrences of '_' removed.
+ /// </summary>
+ public static string RemoveUnderscores(string s) {
+ Contract.Requires(s != null);
+ while (true) {
+ var j = s.IndexOf('_');
+ if (j == -1) {
+ return s;
+ }
+ s = s.Substring(0, j) + s.Substring(j + 1);
+ }
+ }
+
+ /// <summary>
/// For "S" returns S and false.
/// For @"S" return S and true.
/// Assumes that s has one of these forms.
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 6e71e5b2..26baa35f 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -427,23 +427,23 @@ method HexTest() assert forall i :: 0 <= i < |first16upper| ==> first16upper[i] == i;
var randomHex := [ 0xCF4458F2, 0x9A5C5BAF, 0x26A6ABD6, 0x00EB3933, 0x9123D2CF, 0xBE040001, 0x5AD038FA, 0xC75597A6, 0x7CF821A7, 0xCDEFB617, 0x4889D968, 0xB05F896A,
- 0x75B18DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46,
- 0x610D0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D,
- 0x02FBF254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D,
- 0x730D85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190,
- 0xc95f056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143,
- 0x1520b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e,
- 0xbfcd3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30,
- 0xcd85f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd8C6FAF7 ];
+ 0x75B1_8DB2, 0xCAD773B0, 0xD8845EF8, 0x8EFA513D, 0x8EBAD321, 0x9C405DDE, 0x0EA9DF16, 0xCD48236A, 0x8A6892CF, 0x99BF0779, 0xEA52E108, 0x0379BF46,
+ 0x610D_0339, 0xDB433BC7, 0xE94C026E, 0xFC18735C, 0x6A5FBDB3, 0xFDA622F9, 0x6204DB79, 0x52050F94, 0x5ABDD3FD, 0x7F1CFCDF, 0xEC7C907F, 0xFA41A43D,
+ 0x02FB_F254, 0x9E76751A, 0xF753002C, 0x9635D361, 0xBA2C14E6, 0x415CA2FB, 0xA478EF6C, 0x7F80D7EC, 0xB4DD8598, 0x06C4ED20, 0xBFC9F800, 0x69F9675D,
+ 0x730D_85E7, 0x30152491, 0x0226b79d, 0x6c7f895c, 0x4f466fa2, 0x2e470749, 0xacacf22e, 0x455ab875, 0xa0927dc7, 0xe27c93d7, 0x4f134daf, 0xd2c6c190,
+ 0xc95f_056e, 0x45547ddf, 0x6a5c2767, 0xadc55905, 0xc5d6217d, 0x4ae4453e, 0xbe11d3d9, 0x339b8b14, 0xe68f7571, 0xf528199d, 0x0e640ee0, 0x9f716143,
+ 0x1520_b76f, 0x7bfe38e9, 0x8c289b71, 0x677ff535, 0x0bb94f4e, 0xfb417c00, 0xa1cac03a, 0x5e3cdaf2, 0x7616f734, 0xb55744fb, 0x27642f2b, 0xa161c47e,
+ 0xbfcd_3fff, 0xa62df579, 0x3ea317b0, 0xc87063bf, 0x0038c98d, 0x95a5e874, 0x76d824f6, 0x18687e3e, 0x4be6d02a, 0x2c2cc14c, 0x6e91d56b, 0x76e2bb30,
+ 0xcd85_f1cc, 0x6219d3ae, 0xbe59d8d4, 0xd_8_C_6_F_A_F_7 ];
var randomDec := [ 3477362930, 2589744047, 648457174, 15415603, 2435044047, 3187933185, 1523595514, 3344275366, 2096636327, 3455038999, 1216993640, 2959051114,
- 1974570418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470,
- 1628242745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885,
- 50066004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605,
- 1930266087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040,
- 3378447726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811,
+ 1_974_570_418, 3403117488, 3632553720, 2398769469, 2394608417, 2621464030, 246013718, 3444056938, 2322109135, 2579433337, 3931300104, 58310470,
+ 1_628_242_745, 3678616519, 3914072686, 4229460828, 1784659379, 4255523577, 1644485497, 1376063380, 1522390013, 2132606175, 3967586431, 4198605885,
+ 50_066_004, 2658563354, 4149411884, 2520109921, 3123451110, 1096590075, 2759389036, 2139150316, 3034416536, 113569056, 3217684480, 1777952605,
+ 1_930_266_087, 806691985, 36091805, 1820297564, 1330016162, 776406857, 2897015342, 1163573365, 2693955015, 3799815127, 1326665135, 3536241040,
+ 3_378_447_726, 1163165151, 1784424295, 2915391749, 3319144829, 1256473918, 3188839385, 865831700, 3868161393, 4113045917, 241438432, 2675007811,
354465647, 2080258281, 2351471473, 1736439093, 196693838, 4215372800, 2714419258, 1581046514, 1981216564, 3042395387, 660877099, 2707539070,
3217899519, 2788029817, 1050875824, 3362808767, 3721613, 2510678132, 1993876726, 409501246, 1273417770, 741130572, 1855051115, 1994570544,
- 3448107468, 1645859758, 3193559252, 3636919031 ];
+ 3448107468, 1645859758, 3_1_9_3_5_5_9_2_5_2, 3636919031 ];
assert forall i :: 0 <= i < |randomHex| ==> randomHex[i] == randomDec[i];
}
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 2bff422f..d8ff3989 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -210,3 +210,20 @@ module GhostLetExpr { G(5, xyz)
}
}
+
+class DigitUnderscore_Names {
+ // the following would be the same integers, but they are different fields
+ var 0_1_0: int;
+ var 010: int;
+ var 10: int;
+ // ... as we see here:
+ method M()
+ modifies this;
+ {
+ this.0_1_0 := 007;
+ this.010 := 000_008;
+ this.10 := 0x0000_0009;
+ assert this.0_1_0 == int(00_07.0_0) && this.010 == 8 && this.10 == 9;
+ this.10 := 20;
+ }
+}
diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect index af8ed2fc..0a1938ae 100644 --- a/Test/dafny0/Compilation.dfy.expect +++ b/Test/dafny0/Compilation.dfy.expect @@ -1,3 +1,3 @@ -Dafny program verifier finished with 44 verified, 0 errors
+Dafny program verifier finished with 46 verified, 0 errors
Compiled assembly into Compilation.exe
diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy index 76ac9d93..1004a015 100644 --- a/Test/dafny0/RealTypes.dfy +++ b/Test/dafny0/RealTypes.dfy @@ -23,10 +23,10 @@ method R2(ghost x: real, ghost y: real) { // Check that literals are handled properly
method R3() {
- ghost var x := 1.5;
- ghost var y := real(3);
- assert x == y / 2.0000000;
- assert x == y / 2.000000000000000000000000001; // error
+ ghost var x := 000_00_0_1.5_0_0_00_000_0; // 1.5
+ ghost var y := real(000_000_003); // 3
+ assert x == y / 2.000_000_0;
+ assert x == y / 2.000_000_000_000_000_000_000_000_001; // error
}
// Check that real value in decreases clause doesn't scare Dafny
diff --git a/Test/dafny4/BinarySearch.dfy b/Test/dafny4/BinarySearch.dfy index a06f6c4a..1c1d7299 100644 --- a/Test/dafny4/BinarySearch.dfy +++ b/Test/dafny4/BinarySearch.dfy @@ -28,10 +28,10 @@ method BinarySearch(a: array<int>, key: int) returns (r: int) // Binary search using bounded integers
-newtype int32 = x | -0x80000000 <= x < 0x80000000
+newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000
method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32)
- requires a != null && a.Length < 0x80000000;
+ requires a != null && a.Length < 0x8000_0000;
requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];
ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;
ensures r < 0 ==> key !in a[..];
@@ -54,7 +54,7 @@ method BinarySearchInt32_bad(a: array<int>, key: int) returns (r: int32) }
method BinarySearchInt32_good(a: array<int>, key: int) returns (r: int32)
- requires a != null && a.Length < 0x80000000;
+ requires a != null && a.Length < 0x8000_0000;
requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];
ensures 0 <= r ==> r < int32(a.Length) && a[r] == key;
ensures r < 0 ==> key !in a[..];
|