diff options
Diffstat (limited to 'Dafny/Scanner.cs')
| -rw-r--r-- | Dafny/Scanner.cs | 129 |
1 files changed, 64 insertions, 65 deletions
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index ba5a745d..7d750553 100644 --- a/Dafny/Scanner.cs +++ b/Dafny/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 106;
- const int noSym = 106;
+ const int maxT = 105;
+ const int noSym = 105;
[ContractInvariantMethod]
@@ -515,33 +515,32 @@ public class Scanner { case "reads": t.kind = 41; break;
case "match": t.kind = 44; break;
case "case": t.kind = 45; break;
- case "call": t.kind = 47; break;
- case "label": t.kind = 48; break;
- case "break": t.kind = 49; break;
- case "return": t.kind = 50; break;
- case "new": t.kind = 52; break;
- case "choose": t.kind = 56; break;
- case "havoc": t.kind = 57; break;
- case "if": t.kind = 58; break;
- case "else": t.kind = 59; break;
- case "while": t.kind = 60; break;
- case "invariant": t.kind = 61; break;
- case "foreach": t.kind = 62; break;
- case "in": t.kind = 63; break;
- case "assert": t.kind = 64; break;
- case "assume": t.kind = 65; break;
- case "use": t.kind = 66; break;
- case "print": t.kind = 67; break;
- case "false": t.kind = 91; break;
- case "true": t.kind = 92; break;
- case "null": t.kind = 93; break;
- case "this": t.kind = 94; break;
- case "fresh": t.kind = 95; break;
- case "allocated": t.kind = 96; break;
- case "old": t.kind = 97; break;
- case "then": t.kind = 98; break;
- case "forall": t.kind = 100; break;
- case "exists": t.kind = 102; break;
+ case "label": t.kind = 47; break;
+ case "break": t.kind = 48; break;
+ case "return": t.kind = 49; break;
+ case "new": t.kind = 51; break;
+ case "choose": t.kind = 55; break;
+ case "havoc": t.kind = 56; break;
+ case "if": t.kind = 57; break;
+ case "else": t.kind = 58; break;
+ case "while": t.kind = 59; break;
+ case "invariant": t.kind = 60; break;
+ case "foreach": t.kind = 61; break;
+ case "in": t.kind = 62; break;
+ case "assert": t.kind = 63; break;
+ case "assume": t.kind = 64; break;
+ case "use": t.kind = 65; break;
+ case "print": t.kind = 66; break;
+ case "false": t.kind = 90; break;
+ case "true": t.kind = 91; break;
+ case "null": t.kind = 92; break;
+ case "this": t.kind = 93; break;
+ case "fresh": t.kind = 94; break;
+ case "allocated": t.kind = 95; break;
+ case "old": t.kind = 96; break;
+ case "then": t.kind = 97; break;
+ case "forall": t.kind = 99; break;
+ case "exists": t.kind = 101; break;
default: break;
}
}
@@ -661,70 +660,70 @@ public class Scanner { case 25:
{t.kind = 46; break;}
case 26:
- {t.kind = 51; break;}
+ {t.kind = 50; break;}
case 27:
- {t.kind = 53; break;}
+ {t.kind = 52; break;}
case 28:
- {t.kind = 54; break;}
+ {t.kind = 53; break;}
case 29:
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 68; break;}
+ {t.kind = 67; break;}
case 31:
- {t.kind = 69; break;}
+ {t.kind = 68; break;}
case 32:
- {t.kind = 70; break;}
+ {t.kind = 69; break;}
case 33:
- {t.kind = 71; break;}
+ {t.kind = 70; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 72; break;}
+ {t.kind = 71; break;}
case 36:
- {t.kind = 73; break;}
+ {t.kind = 72; break;}
case 37:
- {t.kind = 74; break;}
+ {t.kind = 73; break;}
case 38:
- {t.kind = 75; break;}
+ {t.kind = 74; break;}
case 39:
- {t.kind = 78; break;}
+ {t.kind = 77; break;}
case 40:
- {t.kind = 79; break;}
+ {t.kind = 78; break;}
case 41:
- {t.kind = 80; break;}
+ {t.kind = 79; break;}
case 42:
if (ch == 'n') {AddCh(); goto case 43;}
else {goto case 0;}
case 43:
- {t.kind = 81; break;}
+ {t.kind = 80; break;}
case 44:
- {t.kind = 82; break;}
+ {t.kind = 81; break;}
case 45:
- {t.kind = 83; break;}
+ {t.kind = 82; break;}
case 46:
- {t.kind = 84; break;}
+ {t.kind = 83; break;}
case 47:
- {t.kind = 85; break;}
+ {t.kind = 84; break;}
case 48:
- {t.kind = 86; break;}
+ {t.kind = 85; break;}
case 49:
- {t.kind = 87; break;}
+ {t.kind = 86; break;}
case 50:
- {t.kind = 88; break;}
+ {t.kind = 87; break;}
case 51:
- {t.kind = 90; break;}
+ {t.kind = 89; break;}
case 52:
- {t.kind = 99; break;}
+ {t.kind = 98; break;}
case 53:
- {t.kind = 101; break;}
+ {t.kind = 100; break;}
case 54:
- {t.kind = 103; break;}
+ {t.kind = 102; break;}
case 55:
- {t.kind = 104; break;}
+ {t.kind = 103; break;}
case 56:
- {t.kind = 105; break;}
+ {t.kind = 104; break;}
case 57:
recEnd = pos; recKind = 16;
if (ch == '>') {AddCh(); goto case 25;}
@@ -748,23 +747,23 @@ public class Scanner { if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
case 62:
- recEnd = pos; recKind = 55;
+ recEnd = pos; recKind = 54;
if (ch == '.') {AddCh(); goto case 52;}
- else {t.kind = 55; break;}
+ else {t.kind = 54; break;}
case 63:
- recEnd = pos; recKind = 89;
+ recEnd = pos; recKind = 88;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
else if (ch == 'i') {AddCh(); goto case 42;}
- else {t.kind = 89; break;}
+ else {t.kind = 88; break;}
case 64:
- recEnd = pos; recKind = 76;
+ recEnd = pos; recKind = 75;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 76; break;}
+ else {t.kind = 75; break;}
case 65:
- recEnd = pos; recKind = 77;
+ recEnd = pos; recKind = 76;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 77; break;}
+ else {t.kind = 76; break;}
}
t.val = new String(tval, 0, tlen);
|