diff options
Diffstat (limited to 'Source/Dafny/Scanner.cs')
| -rw-r--r-- | Source/Dafny/Scanner.cs | 197 |
1 files changed, 99 insertions, 98 deletions
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index a54fe778..df41ffcd 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/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 = 129;
- const int noSym = 129;
+ const int maxT = 130;
+ const int noSym = 130;
[ContractInvariantMethod]
@@ -509,59 +509,60 @@ public class Scanner { case "datatype": t.kind = 33; break;
case "codatatype": t.kind = 34; break;
case "var": t.kind = 36; break;
- case "type": t.kind = 38; break;
- case "new": t.kind = 40; break;
- case "iterator": t.kind = 41; break;
- case "yields": t.kind = 42; break;
- case "returns": t.kind = 43; break;
- case "method": t.kind = 47; break;
- case "lemma": t.kind = 48; break;
- case "colemma": t.kind = 49; break;
- case "comethod": t.kind = 50; break;
- case "constructor": t.kind = 51; break;
- case "modifies": t.kind = 52; break;
- case "free": t.kind = 53; break;
- case "ensures": t.kind = 54; break;
- case "decreases": t.kind = 55; break;
- case "yield": t.kind = 56; break;
- case "bool": t.kind = 57; break;
- case "nat": t.kind = 58; break;
- case "int": t.kind = 59; break;
- case "real": t.kind = 60; break;
- case "set": t.kind = 61; break;
- case "multiset": t.kind = 62; break;
- case "seq": t.kind = 63; break;
- case "map": t.kind = 64; break;
- case "object": t.kind = 65; break;
- case "function": t.kind = 67; break;
- case "predicate": t.kind = 68; break;
- case "copredicate": t.kind = 69; break;
- case "label": t.kind = 71; break;
- case "break": t.kind = 72; break;
- case "where": t.kind = 73; break;
+ case "newtype": t.kind = 38; break;
+ case "where": t.kind = 39; break;
+ case "type": t.kind = 40; break;
+ case "iterator": t.kind = 42; break;
+ case "yields": t.kind = 43; break;
+ case "returns": t.kind = 44; break;
+ case "method": t.kind = 48; break;
+ case "lemma": t.kind = 49; break;
+ case "colemma": t.kind = 50; break;
+ case "comethod": t.kind = 51; break;
+ case "constructor": t.kind = 52; break;
+ case "modifies": t.kind = 53; break;
+ case "free": t.kind = 54; break;
+ case "ensures": t.kind = 55; break;
+ case "decreases": t.kind = 56; break;
+ case "yield": t.kind = 57; break;
+ case "bool": t.kind = 58; break;
+ case "nat": t.kind = 59; break;
+ case "int": t.kind = 60; break;
+ case "real": t.kind = 61; break;
+ case "set": t.kind = 62; break;
+ case "multiset": t.kind = 63; break;
+ case "seq": t.kind = 64; break;
+ case "map": t.kind = 65; break;
+ case "object": t.kind = 66; break;
+ case "function": t.kind = 68; break;
+ case "predicate": t.kind = 69; break;
+ case "copredicate": t.kind = 70; break;
+ case "label": t.kind = 72; break;
+ case "break": t.kind = 73; break;
case "return": t.kind = 75; break;
case "assume": t.kind = 77; break;
- case "if": t.kind = 80; break;
- case "else": t.kind = 81; break;
- case "case": t.kind = 82; break;
- case "while": t.kind = 83; break;
- case "invariant": t.kind = 84; break;
- case "match": t.kind = 85; break;
- case "assert": t.kind = 86; break;
- case "print": t.kind = 87; break;
- case "forall": t.kind = 88; break;
- case "parallel": t.kind = 89; break;
- case "modify": t.kind = 90; break;
- case "calc": t.kind = 91; break;
- case "in": t.kind = 109; break;
- case "false": t.kind = 116; break;
- case "true": t.kind = 117; break;
- case "null": t.kind = 118; break;
- case "this": t.kind = 119; break;
- case "fresh": t.kind = 120; break;
- case "old": t.kind = 121; break;
- case "then": t.kind = 122; break;
- case "exists": t.kind = 125; break;
+ case "new": t.kind = 78; break;
+ case "if": t.kind = 81; break;
+ case "else": t.kind = 82; break;
+ case "case": t.kind = 83; break;
+ case "while": t.kind = 84; break;
+ case "invariant": t.kind = 85; break;
+ case "match": t.kind = 86; break;
+ case "assert": t.kind = 87; break;
+ case "print": t.kind = 88; break;
+ case "forall": t.kind = 89; break;
+ case "parallel": t.kind = 90; break;
+ case "modify": t.kind = 91; break;
+ case "calc": t.kind = 92; break;
+ case "in": t.kind = 110; break;
+ case "false": t.kind = 117; break;
+ case "true": t.kind = 118; break;
+ case "null": t.kind = 119; break;
+ case "this": t.kind = 120; break;
+ case "fresh": t.kind = 121; break;
+ case "old": t.kind = 122; break;
+ case "then": t.kind = 123; break;
+ case "exists": t.kind = 126; break;
default: break;
}
}
@@ -714,66 +715,66 @@ public class Scanner { case 33:
{t.kind = 37; break;}
case 34:
- {t.kind = 44; break;}
+ {t.kind = 45; break;}
case 35:
- {t.kind = 70; break;}
+ {t.kind = 71; break;}
case 36:
{t.kind = 74; break;}
case 37:
{t.kind = 76; break;}
case 38:
- {t.kind = 78; break;}
- case 39:
{t.kind = 79; break;}
+ case 39:
+ {t.kind = 80; break;}
case 40:
- {t.kind = 92; break;}
+ {t.kind = 93; break;}
case 41:
- {t.kind = 94; break;}
- case 42:
{t.kind = 95; break;}
- case 43:
+ case 42:
{t.kind = 96; break;}
- case 44:
+ case 43:
{t.kind = 97; break;}
- case 45:
+ case 44:
{t.kind = 98; break;}
- case 46:
+ case 45:
{t.kind = 99; break;}
- case 47:
+ case 46:
{t.kind = 100; break;}
- case 48:
+ case 47:
{t.kind = 101; break;}
- case 49:
+ case 48:
{t.kind = 102; break;}
+ case 49:
+ {t.kind = 103; break;}
case 50:
- {t.kind = 104; break;}
+ {t.kind = 105; break;}
case 51:
if (ch == '&') {AddCh(); goto case 52;}
else {goto case 0;}
case 52:
- {t.kind = 105; break;}
- case 53:
{t.kind = 106; break;}
- case 54:
+ case 53:
{t.kind = 107; break;}
- case 55:
+ case 54:
{t.kind = 108; break;}
+ case 55:
+ {t.kind = 109; break;}
case 56:
- {t.kind = 111; break;}
+ {t.kind = 112; break;}
case 57:
- {t.kind = 113; break;}
- case 58:
{t.kind = 114; break;}
- case 59:
+ case 58:
{t.kind = 115; break;}
+ case 59:
+ {t.kind = 116; break;}
case 60:
- {t.kind = 124; break;}
+ {t.kind = 125; break;}
case 61:
- {t.kind = 126; break;}
- case 62:
{t.kind = 127; break;}
- case 63:
+ case 62:
{t.kind = 128; break;}
+ case 63:
+ {t.kind = 129; break;}
case 64:
recEnd = pos; recKind = 7;
if (ch == '=') {AddCh(); goto case 36;}
@@ -786,46 +787,46 @@ public class Scanner { else if (ch == '=') {AddCh(); goto case 72;}
else {t.kind = 25; break;}
case 66:
- recEnd = pos; recKind = 112;
+ recEnd = pos; recKind = 113;
if (ch == '>') {AddCh(); goto case 15;}
- else {t.kind = 112; break;}
+ else {t.kind = 113; break;}
case 67:
- recEnd = pos; recKind = 110;
+ recEnd = pos; recKind = 111;
if (ch == 'i') {AddCh(); goto case 21;}
else if (ch == '=') {AddCh(); goto case 42;}
- else {t.kind = 110; break;}
+ else {t.kind = 111; break;}
case 68:
recEnd = pos; recKind = 35;
if (ch == '|') {AddCh(); goto case 54;}
else {t.kind = 35; break;}
case 69:
- recEnd = pos; recKind = 66;
+ recEnd = pos; recKind = 67;
if (ch == '.') {AddCh(); goto case 73;}
- else {t.kind = 66; break;}
+ else {t.kind = 67; break;}
case 70:
- recEnd = pos; recKind = 45;
+ recEnd = pos; recKind = 46;
if (ch == '=') {AddCh(); goto case 74;}
- else {t.kind = 45; break;}
+ else {t.kind = 46; break;}
case 71:
- recEnd = pos; recKind = 46;
+ recEnd = pos; recKind = 47;
if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 46; break;}
+ else {t.kind = 47; break;}
case 72:
- recEnd = pos; recKind = 39;
+ recEnd = pos; recKind = 41;
if (ch == '>') {AddCh(); goto case 48;}
- else {t.kind = 39; break;}
+ else {t.kind = 41; break;}
case 73:
- recEnd = pos; recKind = 123;
+ recEnd = pos; recKind = 124;
if (ch == '.') {AddCh(); goto case 34;}
- else {t.kind = 123; break;}
+ else {t.kind = 124; break;}
case 74:
- recEnd = pos; recKind = 93;
+ recEnd = pos; recKind = 94;
if (ch == '=') {AddCh(); goto case 75;}
- else {t.kind = 93; break;}
+ else {t.kind = 94; break;}
case 75:
- recEnd = pos; recKind = 103;
+ recEnd = pos; recKind = 104;
if (ch == '>') {AddCh(); goto case 46;}
- else {t.kind = 103; break;}
+ else {t.kind = 104; break;}
}
t.val = new String(tval, 0, tlen);
|