diff options
Diffstat (limited to 'Source/Dafny')
-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 |
4 files changed, 230 insertions, 193 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.
|