diff options
Diffstat (limited to 'Source/Dafny/Scanner.ssc')
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 188 |
1 files changed, 95 insertions, 93 deletions
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index 56c6f0be..cf759f84 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -30,21 +30,21 @@ public class Scanner { [Microsoft.Contracts.Verify(false)]
static Scanner() {
- start[0] = 54;
- start[33] = 32;
+ start[0] = 55;
+ start[33] = 33;
start[34] = 3;
- start[35] = 45;
- start[37] = 43;
- start[38] = 26;
+ start[35] = 46;
+ start[37] = 44;
+ start[38] = 27;
start[39] = 1;
start[40] = 12;
start[41] = 13;
start[42] = 14;
- start[43] = 40;
+ start[43] = 41;
start[44] = 8;
- start[45] = 41;
- start[46] = 46;
- start[47] = 42;
+ start[45] = 42;
+ start[46] = 47;
+ start[47] = 43;
start[48] = 2;
start[49] = 2;
start[50] = 2;
@@ -58,7 +58,7 @@ public class Scanner { start[58] = 9;
start[59] = 7;
start[60] = 10;
- start[61] = 15;
+ start[61] = 16;
start[62] = 11;
start[63] = 1;
start[65] = 1;
@@ -87,11 +87,11 @@ public class Scanner { start[88] = 1;
start[89] = 1;
start[90] = 1;
- start[91] = 47;
+ start[91] = 48;
start[92] = 1;
- start[93] = 48;
+ start[93] = 49;
start[95] = 1;
- start[96] = 1;
+ start[96] = 15;
start[97] = 1;
start[98] = 1;
start[99] = 1;
@@ -119,21 +119,21 @@ public class Scanner { start[121] = 1;
start[122] = 1;
start[123] = 5;
- start[124] = 18;
+ start[124] = 19;
start[125] = 6;
- start[172] = 44;
- start[8226] = 53;
- start[8658] = 25;
- start[8660] = 22;
- start[8704] = 50;
- start[8707] = 51;
- start[8743] = 28;
- start[8744] = 30;
- start[8800] = 37;
- start[8804] = 38;
- start[8805] = 39;
+ start[172] = 45;
+ start[8226] = 54;
+ start[8658] = 26;
+ start[8660] = 23;
+ start[8704] = 51;
+ start[8707] = 52;
+ start[8743] = 29;
+ start[8744] = 31;
+ start[8800] = 38;
+ start[8804] = 39;
+ start[8805] = 40;
}
- const int noSym = 98;
+ const int noSym = 99;
static short[] start = new short[16385];
@@ -297,33 +297,33 @@ public class Scanner { case "object": t.kind = 32; break;
case "function": t.kind = 33; break;
case "reads": t.kind = 34; break;
- case "match": t.kind = 36; break;
- case "case": t.kind = 37; break;
- case "label": t.kind = 39; break;
- case "break": t.kind = 40; break;
- case "return": t.kind = 41; break;
- case "new": t.kind = 43; break;
- case "havoc": t.kind = 44; break;
- case "if": t.kind = 45; break;
- case "else": t.kind = 46; break;
- case "while": t.kind = 47; break;
- case "invariant": t.kind = 48; break;
- case "call": t.kind = 49; break;
- case "foreach": t.kind = 50; break;
- case "in": t.kind = 51; break;
- case "assert": t.kind = 53; break;
- case "assume": t.kind = 54; break;
- case "use": t.kind = 55; break;
- case "print": t.kind = 56; break;
- case "then": t.kind = 57; break;
- case "false": t.kind = 81; break;
- case "true": t.kind = 82; break;
- case "null": t.kind = 83; break;
- case "fresh": t.kind = 86; break;
- case "this": t.kind = 90; break;
- case "old": t.kind = 91; break;
- case "forall": t.kind = 92; break;
- case "exists": t.kind = 94; break;
+ case "match": t.kind = 37; break;
+ case "case": t.kind = 38; break;
+ case "label": t.kind = 40; break;
+ case "break": t.kind = 41; break;
+ case "return": t.kind = 42; break;
+ case "new": t.kind = 44; break;
+ case "havoc": t.kind = 45; break;
+ case "if": t.kind = 46; break;
+ case "else": t.kind = 47; break;
+ case "while": t.kind = 48; break;
+ case "invariant": t.kind = 49; break;
+ case "call": t.kind = 50; break;
+ case "foreach": t.kind = 51; break;
+ case "in": t.kind = 52; break;
+ case "assert": t.kind = 54; break;
+ case "assume": t.kind = 55; break;
+ case "use": t.kind = 56; break;
+ case "print": t.kind = 57; break;
+ case "then": t.kind = 58; break;
+ case "false": t.kind = 82; break;
+ case "true": t.kind = 83; break;
+ case "null": t.kind = 84; break;
+ case "fresh": t.kind = 87; break;
+ case "this": t.kind = 91; break;
+ case "old": t.kind = 92; break;
+ case "forall": t.kind = 93; break;
+ case "exists": t.kind = 95; break;
default: break;
}
@@ -341,7 +341,7 @@ public class Scanner { switch (state) {
case 0: {t.kind = noSym; goto done;} // NextCh already done
case 1:
- if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch >= '_' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}
+ if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}
else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}
case 2:
if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 2;}
@@ -361,14 +361,14 @@ public class Scanner { case 8:
{t.kind = 15; goto done;}
case 9:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 18;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 53;}
else {t.kind = 16; goto done;}
case 10:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
else {t.kind = 17; goto done;}
case 11:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
else {t.kind = 18; goto done;}
case 12:
{t.kind = 26; goto done;}
@@ -377,38 +377,38 @@ public class Scanner { case 14:
{t.kind = 35; goto done;}
case 15:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;}
- else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 36; goto done;}
case 16:
- {t.kind = 38; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 17;}
+ else if (ch == '=') {buf.Append(ch); NextCh(); goto case 24;}
+ else {t.kind = noSym; goto done;}
case 17:
- {t.kind = 42; goto done;}
+ {t.kind = 39; goto done;}
case 18:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}
- else {t.kind = 52; goto done;}
+ {t.kind = 43; goto done;}
case 19:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
- else {t.kind = 67; goto done;}
+ if (ch == '|') {buf.Append(ch); NextCh(); goto case 30;}
+ else {t.kind = 53; goto done;}
case 20:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
- else {t.kind = noSym; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 21;}
+ else {t.kind = 68; goto done;}
case 21:
- {t.kind = 58; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 22;}
+ else {t.kind = noSym; goto done;}
case 22:
{t.kind = 59; goto done;}
case 23:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = 66; goto done;}
- case 24:
{t.kind = 60; goto done;}
+ case 24:
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 25;}
+ else {t.kind = 67; goto done;}
case 25:
{t.kind = 61; goto done;}
case 26:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
- else {t.kind = noSym; goto done;}
- case 27:
{t.kind = 62; goto done;}
+ case 27:
+ if (ch == '&') {buf.Append(ch); NextCh(); goto case 28;}
+ else {t.kind = noSym; goto done;}
case 28:
{t.kind = 63; goto done;}
case 29:
@@ -416,21 +416,21 @@ public class Scanner { case 30:
{t.kind = 65; goto done;}
case 31:
- {t.kind = 68; goto done;}
+ {t.kind = 66; goto done;}
case 32:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
- else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
- else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = 79; goto done;}
- case 33:
{t.kind = 69; goto done;}
+ case 33:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
+ else if (ch == '!') {buf.Append(ch); NextCh(); goto case 35;}
+ else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 36;}
+ else {t.kind = 80; goto done;}
case 34:
{t.kind = 70; goto done;}
case 35:
- if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
- else {t.kind = noSym; goto done;}
- case 36:
{t.kind = 71; goto done;}
+ case 36:
+ if (ch == 'n') {buf.Append(ch); NextCh(); goto case 37;}
+ else {t.kind = noSym; goto done;}
case 37:
{t.kind = 72; goto done;}
case 38:
@@ -446,27 +446,29 @@ public class Scanner { case 43:
{t.kind = 78; goto done;}
case 44:
- {t.kind = 80; goto done;}
+ {t.kind = 79; goto done;}
case 45:
- {t.kind = 84; goto done;}
+ {t.kind = 81; goto done;}
case 46:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
- else {t.kind = 85; goto done;}
+ {t.kind = 85; goto done;}
case 47:
- {t.kind = 87; goto done;}
+ if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
+ else {t.kind = 86; goto done;}
case 48:
{t.kind = 88; goto done;}
case 49:
{t.kind = 89; goto done;}
case 50:
- {t.kind = 93; goto done;}
+ {t.kind = 90; goto done;}
case 51:
- {t.kind = 95; goto done;}
+ {t.kind = 94; goto done;}
case 52:
{t.kind = 96; goto done;}
case 53:
{t.kind = 97; goto done;}
- case 54: {t.kind = 0; goto done;}
+ case 54:
+ {t.kind = 98; goto done;}
+ case 55: {t.kind = 0; goto done;}
}
done:
t.val = buf.ToString();
|