summaryrefslogtreecommitdiff
path: root/Source/Core/Scanner.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/Scanner.cs')
-rw-r--r--Source/Core/Scanner.cs486
1 files changed, 305 insertions, 181 deletions
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index e068fc4b..46a3c419 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/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 = 96;
- const int noSym = 96;
+ const int maxT = 97;
+ const int noSym = 97;
[ContractInvariantMethod]
@@ -267,41 +267,42 @@ public class Scanner {
for (int i = 65; i <= 90; ++i) start[i] = 2;
for (int i = 94; i <= 122; ++i) start[i] = 2;
for (int i = 126; i <= 126; ++i) start[i] = 2;
- for (int i = 48; i <= 57; ++i) start[i] = 16;
+ for (int i = 49; i <= 57; ++i) start[i] = 45;
for (int i = 34; i <= 34; ++i) start[i] = 6;
start[92] = 1;
- start[59] = 19;
- start[40] = 20;
- start[41] = 21;
- start[58] = 55;
- start[44] = 22;
- start[91] = 23;
- start[93] = 24;
- start[60] = 56;
- start[62] = 57;
- start[123] = 25;
- start[125] = 58;
- start[61] = 59;
- start[42] = 60;
- start[124] = 61;
- start[8660] = 28;
- start[8658] = 30;
- start[8656] = 31;
- start[38] = 32;
- start[8743] = 34;
- start[8744] = 36;
- start[33] = 62;
- start[8800] = 40;
- start[8804] = 41;
- start[8805] = 42;
- start[43] = 63;
- start[45] = 44;
- start[47] = 45;
- start[172] = 47;
- start[8704] = 50;
- start[8707] = 51;
- start[955] = 52;
- start[8226] = 54;
+ start[45] = 87;
+ start[48] = 46;
+ start[59] = 52;
+ start[40] = 53;
+ start[41] = 54;
+ start[58] = 88;
+ start[44] = 55;
+ start[91] = 56;
+ start[93] = 57;
+ start[60] = 89;
+ start[62] = 90;
+ start[123] = 58;
+ start[125] = 91;
+ start[61] = 92;
+ start[42] = 93;
+ start[124] = 94;
+ start[8660] = 61;
+ start[8658] = 63;
+ start[8656] = 64;
+ start[38] = 65;
+ start[8743] = 67;
+ start[8744] = 69;
+ start[33] = 95;
+ start[8800] = 73;
+ start[8804] = 74;
+ start[8805] = 75;
+ start[43] = 96;
+ start[47] = 77;
+ start[172] = 79;
+ start[8704] = 82;
+ start[8707] = 83;
+ start[955] = 84;
+ start[8226] = 86;
start[Buffer.EOF] = -1;
}
@@ -503,48 +504,48 @@ public class Scanner {
void CheckLiteral() {
switch (t.val) {
- case "var": t.kind = 7; break;
- case "where": t.kind = 13; break;
- case "int": t.kind = 14; break;
- case "real": t.kind = 15; break;
- case "bool": t.kind = 16; break;
- case "const": t.kind = 21; break;
- case "unique": t.kind = 22; break;
- case "extends": t.kind = 23; break;
- case "complete": t.kind = 24; break;
- case "function": t.kind = 25; break;
- case "returns": t.kind = 26; break;
- case "axiom": t.kind = 29; break;
- case "type": t.kind = 30; break;
- case "procedure": t.kind = 32; break;
- case "implementation": t.kind = 33; break;
- case "modifies": t.kind = 34; break;
- case "free": t.kind = 35; break;
- case "requires": t.kind = 36; break;
- case "ensures": t.kind = 37; break;
- case "goto": t.kind = 38; break;
- case "return": t.kind = 39; break;
- case "if": t.kind = 40; break;
- case "else": t.kind = 41; break;
- case "while": t.kind = 42; break;
- case "invariant": t.kind = 43; break;
- case "break": t.kind = 45; break;
- case "assert": t.kind = 46; break;
- case "assume": t.kind = 47; break;
- case "havoc": t.kind = 48; break;
- case "yield": t.kind = 49; break;
- case "async": t.kind = 51; break;
- case "call": t.kind = 52; break;
- case "par": t.kind = 53; break;
- case "div": t.kind = 76; break;
- case "mod": t.kind = 77; break;
- case "false": t.kind = 82; break;
- case "true": t.kind = 83; break;
- case "old": t.kind = 84; break;
- case "then": t.kind = 87; break;
- case "forall": t.kind = 88; break;
- case "exists": t.kind = 90; break;
- case "lambda": t.kind = 92; break;
+ case "var": t.kind = 8; break;
+ case "where": t.kind = 14; break;
+ case "int": t.kind = 15; break;
+ case "real": t.kind = 16; break;
+ case "bool": t.kind = 17; break;
+ case "const": t.kind = 22; break;
+ case "unique": t.kind = 23; break;
+ case "extends": t.kind = 24; break;
+ case "complete": t.kind = 25; break;
+ case "function": t.kind = 26; break;
+ case "returns": t.kind = 27; break;
+ case "axiom": t.kind = 30; break;
+ case "type": t.kind = 31; break;
+ case "procedure": t.kind = 33; break;
+ case "implementation": t.kind = 34; break;
+ case "modifies": t.kind = 35; break;
+ case "free": t.kind = 36; break;
+ case "requires": t.kind = 37; break;
+ case "ensures": t.kind = 38; break;
+ case "goto": t.kind = 39; break;
+ case "return": t.kind = 40; break;
+ case "if": t.kind = 41; break;
+ case "else": t.kind = 42; break;
+ case "while": t.kind = 43; break;
+ case "invariant": t.kind = 44; break;
+ case "break": t.kind = 46; break;
+ case "assert": t.kind = 47; break;
+ case "assume": t.kind = 48; break;
+ case "havoc": t.kind = 49; break;
+ case "yield": t.kind = 50; break;
+ case "async": t.kind = 52; break;
+ case "call": t.kind = 53; break;
+ case "par": t.kind = 54; break;
+ case "div": t.kind = 77; break;
+ case "mod": t.kind = 78; break;
+ case "false": t.kind = 83; break;
+ case "true": t.kind = 84; break;
+ case "old": t.kind = 85; break;
+ case "then": t.kind = 88; break;
+ case "forall": t.kind = 89; break;
+ case "exists": t.kind = 91; break;
+ case "lambda": t.kind = 93; break;
default: break;
}
}
@@ -597,182 +598,305 @@ public class Scanner {
case 6:
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ else if (ch == 92) {AddCh(); goto case 47;}
else {goto case 0;}
case 7:
{t.kind = 4; break;}
case 8:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else if (ch == '-') {AddCh(); goto case 9;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
else {goto case 0;}
case 9:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else {goto case 0;}
+ recEnd = pos; recKind = 6;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
+ else if (ch == 'e') {AddCh(); goto case 10;}
+ else {t.kind = 6; break;}
case 10:
- recEnd = pos; recKind = 5;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
- else {t.kind = 5; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ else if (ch == '-') {AddCh(); goto case 11;}
+ else {goto case 0;}
case 11:
if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
else {goto case 0;}
case 12:
recEnd = pos; recKind = 6;
if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
- else if (ch == 'e') {AddCh(); goto case 13;}
else {t.kind = 6; break;}
case 13:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else if (ch == '-') {AddCh(); goto case 14;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+ else if (ch == 'e') {AddCh(); goto case 14;}
else {goto case 0;}
case 14:
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else if (ch == '-') {AddCh(); goto case 15;}
else {goto case 0;}
case 15:
- recEnd = pos; recKind = 6;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
- else {t.kind = 6; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else {goto case 0;}
case 16:
- recEnd = pos; recKind = 3;
if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
- else if (ch == 'b') {AddCh(); goto case 3;}
- else if (ch == 'e') {AddCh(); goto case 8;}
- else if (ch == '.') {AddCh(); goto case 11;}
- else {t.kind = 3; break;}
+ else if (ch == 'f') {AddCh(); goto case 17;}
+ else {goto case 0;}
case 17:
- if (ch == '"') {AddCh(); goto case 18;}
- else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
else {goto case 0;}
case 18:
- recEnd = pos; recKind = 4;
- if (ch == '"') {AddCh(); goto case 7;}
- else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 17;}
- else {t.kind = 4; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;}
+ else if (ch == 'e') {AddCh(); goto case 19;}
+ else {goto case 0;}
case 19:
- {t.kind = 8; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+ else {goto case 0;}
case 20:
- {t.kind = 9; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 20;}
+ else {t.kind = 7; break;}
case 21:
- {t.kind = 10; break;}
+ if (ch == 'a') {AddCh(); goto case 22;}
+ else {goto case 0;}
case 22:
- {t.kind = 12; break;}
+ if (ch == 'N') {AddCh(); goto case 23;}
+ else {goto case 0;}
case 23:
- {t.kind = 17; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+ else {goto case 0;}
case 24:
- {t.kind = 18; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 24;}
+ else if (ch == 'e') {AddCh(); goto case 25;}
+ else {goto case 0;}
case 25:
- {t.kind = 27; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;}
+ else {goto case 0;}
case 26:
- {t.kind = 50; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 26;}
+ else {t.kind = 7; break;}
case 27:
- {t.kind = 55; break;}
+ if (ch == 'a') {AddCh(); goto case 28;}
+ else {goto case 0;}
case 28:
- {t.kind = 56; break;}
+ if (ch == 'n') {AddCh(); goto case 29;}
+ else {goto case 0;}
case 29:
- {t.kind = 57; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
+ else {goto case 0;}
case 30:
- {t.kind = 58; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 30;}
+ else if (ch == 'e') {AddCh(); goto case 31;}
+ else {goto case 0;}
case 31:
- {t.kind = 60; break;}
- case 32:
- if (ch == '&') {AddCh(); goto case 33;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
else {goto case 0;}
+ case 32:
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 32;}
+ else {t.kind = 7; break;}
case 33:
- {t.kind = 61; break;}
+ if (ch == 'o') {AddCh(); goto case 34;}
+ else {goto case 0;}
case 34:
- {t.kind = 62; break;}
+ if (ch == 'o') {AddCh(); goto case 35;}
+ else {goto case 0;}
case 35:
- {t.kind = 63; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+ else {goto case 0;}
case 36:
- {t.kind = 64; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 36;}
+ else if (ch == 'e') {AddCh(); goto case 37;}
+ else {goto case 0;}
case 37:
- {t.kind = 67; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+ else {goto case 0;}
case 38:
- {t.kind = 68; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 38;}
+ else {t.kind = 7; break;}
case 39:
- {t.kind = 69; break;}
+ if (ch == 'o') {AddCh(); goto case 40;}
+ else {goto case 0;}
case 40:
- {t.kind = 70; break;}
+ if (ch == 'o') {AddCh(); goto case 41;}
+ else {goto case 0;}
case 41:
- {t.kind = 71; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
+ else {goto case 0;}
case 42:
- {t.kind = 72; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 42;}
+ else if (ch == 'e') {AddCh(); goto case 43;}
+ else {goto case 0;}
case 43:
- {t.kind = 73; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+ else {goto case 0;}
case 44:
- {t.kind = 75; break;}
+ recEnd = pos; recKind = 7;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 44;}
+ else {t.kind = 7; break;}
case 45:
- {t.kind = 78; break;}
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;}
+ else if (ch == 'b') {AddCh(); goto case 3;}
+ else if (ch == 'e') {AddCh(); goto case 48;}
+ else if (ch == '.') {AddCh(); goto case 8;}
+ else {t.kind = 3; break;}
case 46:
- {t.kind = 79; break;}
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 45;}
+ else if (ch == 'b') {AddCh(); goto case 3;}
+ else if (ch == 'e') {AddCh(); goto case 48;}
+ else if (ch == '.') {AddCh(); goto case 8;}
+ else if (ch == 'N') {AddCh(); goto case 21;}
+ else if (ch == 'n') {AddCh(); goto case 27;}
+ else if (ch == '+') {AddCh(); goto case 33;}
+ else if (ch == '-') {AddCh(); goto case 39;}
+ else {t.kind = 3; break;}
case 47:
- {t.kind = 81; break;}
+ if (ch == '"') {AddCh(); goto case 49;}
+ else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
+ else if (ch == 92) {AddCh(); goto case 47;}
+ else {goto case 0;}
case 48:
- {t.kind = 85; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+ else if (ch == '-') {AddCh(); goto case 51;}
+ else {goto case 0;}
case 49:
- {t.kind = 86; break;}
+ recEnd = pos; recKind = 4;
+ if (ch == '"') {AddCh(); goto case 7;}
+ else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
+ else if (ch == 92) {AddCh(); goto case 47;}
+ else {t.kind = 4; break;}
case 50:
- {t.kind = 89; break;}
+ recEnd = pos; recKind = 5;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+ else if (ch == 'f') {AddCh(); goto case 17;}
+ else {t.kind = 5; break;}
case 51:
- {t.kind = 91; break;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 50;}
+ else {goto case 0;}
case 52:
- {t.kind = 93; break;}
+ {t.kind = 9; break;}
case 53:
- {t.kind = 94; break;}
+ {t.kind = 10; break;}
case 54:
- {t.kind = 95; break;}
+ {t.kind = 11; break;}
case 55:
- recEnd = pos; recKind = 11;
- if (ch == '=') {AddCh(); goto case 26;}
- else if (ch == ':') {AddCh(); goto case 53;}
- else {t.kind = 11; break;}
+ {t.kind = 13; break;}
case 56:
- recEnd = pos; recKind = 19;
- if (ch == '=') {AddCh(); goto case 64;}
- else if (ch == ':') {AddCh(); goto case 39;}
- else {t.kind = 19; break;}
+ {t.kind = 18; break;}
case 57:
- recEnd = pos; recKind = 20;
- if (ch == '=') {AddCh(); goto case 37;}
- else {t.kind = 20; break;}
+ {t.kind = 19; break;}
case 58:
- recEnd = pos; recKind = 28;
- if (ch == '|') {AddCh(); goto case 49;}
- else {t.kind = 28; break;}
+ {t.kind = 28; break;}
case 59:
- recEnd = pos; recKind = 31;
- if (ch == '=') {AddCh(); goto case 65;}
- else {t.kind = 31; break;}
+ {t.kind = 51; break;}
case 60:
- recEnd = pos; recKind = 44;
- if (ch == '*') {AddCh(); goto case 46;}
- else {t.kind = 44; break;}
+ {t.kind = 56; break;}
case 61:
- recEnd = pos; recKind = 54;
- if (ch == '|') {AddCh(); goto case 35;}
- else if (ch == '{') {AddCh(); goto case 48;}
- else {t.kind = 54; break;}
+ {t.kind = 57; break;}
case 62:
- recEnd = pos; recKind = 80;
- if (ch == '=') {AddCh(); goto case 38;}
- else {t.kind = 80; break;}
+ {t.kind = 58; break;}
case 63:
- recEnd = pos; recKind = 74;
- if (ch == '+') {AddCh(); goto case 43;}
- else {t.kind = 74; break;}
+ {t.kind = 59; break;}
case 64:
- recEnd = pos; recKind = 66;
- if (ch == '=') {AddCh(); goto case 66;}
- else {t.kind = 66; break;}
+ {t.kind = 61; break;}
case 65:
- recEnd = pos; recKind = 65;
- if (ch == '>') {AddCh(); goto case 29;}
- else {t.kind = 65; break;}
+ if (ch == '&') {AddCh(); goto case 66;}
+ else {goto case 0;}
case 66:
- recEnd = pos; recKind = 59;
- if (ch == '>') {AddCh(); goto case 27;}
- else {t.kind = 59; break;}
+ {t.kind = 62; break;}
+ case 67:
+ {t.kind = 63; break;}
+ case 68:
+ {t.kind = 64; break;}
+ case 69:
+ {t.kind = 65; break;}
+ case 70:
+ {t.kind = 68; break;}
+ case 71:
+ {t.kind = 69; break;}
+ case 72:
+ {t.kind = 70; break;}
+ case 73:
+ {t.kind = 71; break;}
+ case 74:
+ {t.kind = 72; break;}
+ case 75:
+ {t.kind = 73; break;}
+ case 76:
+ {t.kind = 74; break;}
+ case 77:
+ {t.kind = 79; break;}
+ case 78:
+ {t.kind = 80; break;}
+ case 79:
+ {t.kind = 82; break;}
+ case 80:
+ {t.kind = 86; break;}
+ case 81:
+ {t.kind = 87; break;}
+ case 82:
+ {t.kind = 90; break;}
+ case 83:
+ {t.kind = 92; break;}
+ case 84:
+ {t.kind = 94; break;}
+ case 85:
+ {t.kind = 95; break;}
+ case 86:
+ {t.kind = 96; break;}
+ case 87:
+ recEnd = pos; recKind = 76;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 13;}
+ else {t.kind = 76; break;}
+ case 88:
+ recEnd = pos; recKind = 12;
+ if (ch == '=') {AddCh(); goto case 59;}
+ else if (ch == ':') {AddCh(); goto case 85;}
+ else {t.kind = 12; break;}
+ case 89:
+ recEnd = pos; recKind = 20;
+ if (ch == '=') {AddCh(); goto case 97;}
+ else if (ch == ':') {AddCh(); goto case 72;}
+ else {t.kind = 20; break;}
+ case 90:
+ recEnd = pos; recKind = 21;
+ if (ch == '=') {AddCh(); goto case 70;}
+ else {t.kind = 21; break;}
+ case 91:
+ recEnd = pos; recKind = 29;
+ if (ch == '|') {AddCh(); goto case 81;}
+ else {t.kind = 29; break;}
+ case 92:
+ recEnd = pos; recKind = 32;
+ if (ch == '=') {AddCh(); goto case 98;}
+ else {t.kind = 32; break;}
+ case 93:
+ recEnd = pos; recKind = 45;
+ if (ch == '*') {AddCh(); goto case 78;}
+ else {t.kind = 45; break;}
+ case 94:
+ recEnd = pos; recKind = 55;
+ if (ch == '|') {AddCh(); goto case 68;}
+ else if (ch == '{') {AddCh(); goto case 80;}
+ else {t.kind = 55; break;}
+ case 95:
+ recEnd = pos; recKind = 81;
+ if (ch == '=') {AddCh(); goto case 71;}
+ else {t.kind = 81; break;}
+ case 96:
+ recEnd = pos; recKind = 75;
+ if (ch == '+') {AddCh(); goto case 76;}
+ else {t.kind = 75; break;}
+ case 97:
+ recEnd = pos; recKind = 67;
+ if (ch == '=') {AddCh(); goto case 99;}
+ else {t.kind = 67; break;}
+ case 98:
+ recEnd = pos; recKind = 66;
+ if (ch == '>') {AddCh(); goto case 62;}
+ else {t.kind = 66; break;}
+ case 99:
+ recEnd = pos; recKind = 60;
+ if (ch == '>') {AddCh(); goto case 60;}
+ else {t.kind = 60; break;}
}
t.val = new String(tval, 0, tlen);
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 19:11:18 +0000