diff options
Diffstat (limited to 'Source/Core/Scanner.cs')
-rw-r--r-- | Source/Core/Scanner.cs | 385 |
1 files changed, 202 insertions, 183 deletions
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index e068fc4b..1185963f 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,41 @@ 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 = 48; i <= 57; ++i) start[i] = 19; 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[59] = 24; + start[40] = 25; + start[41] = 26; + start[58] = 60; + start[44] = 27; + start[91] = 28; + start[93] = 29; + start[60] = 61; + start[62] = 62; + start[123] = 30; + start[125] = 63; + start[61] = 64; + start[42] = 65; + start[124] = 66; + start[8660] = 33; + start[8658] = 35; + start[8656] = 36; + start[38] = 37; + start[8743] = 39; + start[8744] = 41; + start[33] = 67; + start[8800] = 45; + start[8804] = 46; + start[8805] = 47; + start[43] = 68; + start[45] = 49; + start[47] = 50; + start[172] = 52; + start[8704] = 55; + start[8707] = 56; + start[955] = 57; + start[8226] = 59; start[Buffer.EOF] = -1; } @@ -503,48 +503,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 +597,201 @@ 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 20;} 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;} - case 10: recEnd = pos; recKind = 5; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;} else {t.kind = 5; break;} - case 11: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} + case 10: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;} else {goto case 0;} - case 12: + case 11: recEnd = pos; recKind = 6; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;} - else if (ch == 'e') {AddCh(); goto case 13;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 11;} + else if (ch == 'e') {AddCh(); goto case 12;} else {t.kind = 6; break;} + case 12: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} + else if (ch == '-') {AddCh(); goto case 13;} + else {goto case 0;} 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 14;} else {goto case 0;} case 14: - if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} - else {goto case 0;} - case 15: recEnd = pos; recKind = 6; - if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;} + if (ch >= '0' && ch <= '9') {AddCh(); goto case 14;} else {t.kind = 6; break;} + case 15: + 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 == 'e') {AddCh(); goto case 17;} + else {goto case 0;} + case 17: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} + else {goto case 0;} + case 18: + recEnd = pos; recKind = 7; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} + else {t.kind = 7; break;} + case 19: + recEnd = pos; recKind = 3; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 19;} else if (ch == 'b') {AddCh(); goto case 3;} - else if (ch == 'e') {AddCh(); goto case 8;} - else if (ch == '.') {AddCh(); goto case 11;} + else if (ch == 'e') {AddCh(); goto case 21;} + else if (ch == '.') {AddCh(); goto case 10;} else {t.kind = 3; break;} - case 17: - if (ch == '"') {AddCh(); goto case 18;} + case 20: + if (ch == '"') {AddCh(); goto case 22;} 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 20;} else {goto case 0;} - case 18: + case 21: + if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;} + else if (ch == '-') {AddCh(); goto case 8;} + else {goto case 0;} + case 22: 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 if (ch == 92) {AddCh(); goto case 20;} else {t.kind = 4; break;} - case 19: - {t.kind = 8; break;} - case 20: - {t.kind = 9; break;} - case 21: - {t.kind = 10; break;} - case 22: - {t.kind = 12; break;} case 23: - {t.kind = 17; break;} + recEnd = pos; recKind = 5; + if (ch >= '0' && ch <= '9') {AddCh(); goto case 23;} + else if (ch == 'f') {AddCh(); goto case 15;} + else {t.kind = 5; break;} case 24: - {t.kind = 18; break;} + {t.kind = 9; break;} case 25: - {t.kind = 27; break;} + {t.kind = 10; break;} case 26: - {t.kind = 50; break;} + {t.kind = 11; break;} case 27: - {t.kind = 55; break;} + {t.kind = 13; break;} case 28: - {t.kind = 56; break;} + {t.kind = 18; break;} case 29: - {t.kind = 57; break;} + {t.kind = 19; break;} case 30: - {t.kind = 58; break;} + {t.kind = 28; break;} case 31: - {t.kind = 60; break;} + {t.kind = 51; break;} case 32: - if (ch == '&') {AddCh(); goto case 33;} - else {goto case 0;} + {t.kind = 56; break;} case 33: - {t.kind = 61; break;} + {t.kind = 57; break;} case 34: - {t.kind = 62; break;} + {t.kind = 58; break;} case 35: - {t.kind = 63; break;} + {t.kind = 59; break;} case 36: - {t.kind = 64; break;} + {t.kind = 61; break;} case 37: - {t.kind = 67; break;} + if (ch == '&') {AddCh(); goto case 38;} + else {goto case 0;} case 38: - {t.kind = 68; break;} + {t.kind = 62; break;} case 39: - {t.kind = 69; break;} + {t.kind = 63; break;} case 40: - {t.kind = 70; break;} + {t.kind = 64; break;} case 41: - {t.kind = 71; break;} + {t.kind = 65; break;} case 42: - {t.kind = 72; break;} + {t.kind = 68; break;} case 43: - {t.kind = 73; break;} + {t.kind = 69; break;} case 44: - {t.kind = 75; break;} + {t.kind = 70; break;} case 45: - {t.kind = 78; break;} + {t.kind = 71; break;} case 46: - {t.kind = 79; break;} + {t.kind = 72; break;} case 47: - {t.kind = 81; break;} + {t.kind = 73; break;} case 48: - {t.kind = 85; break;} + {t.kind = 74; break;} case 49: - {t.kind = 86; break;} + {t.kind = 76; break;} case 50: - {t.kind = 89; break;} + {t.kind = 79; break;} case 51: - {t.kind = 91; break;} + {t.kind = 80; break;} case 52: - {t.kind = 93; break;} + {t.kind = 82; break;} case 53: - {t.kind = 94; break;} + {t.kind = 86; break;} case 54: - {t.kind = 95; break;} + {t.kind = 87; 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 = 90; 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 = 92; break;} case 57: - recEnd = pos; recKind = 20; - if (ch == '=') {AddCh(); goto case 37;} - else {t.kind = 20; break;} + {t.kind = 94; break;} case 58: - recEnd = pos; recKind = 28; - if (ch == '|') {AddCh(); goto case 49;} - else {t.kind = 28; break;} + {t.kind = 95; break;} case 59: - recEnd = pos; recKind = 31; - if (ch == '=') {AddCh(); goto case 65;} - else {t.kind = 31; break;} + {t.kind = 96; break;} case 60: - recEnd = pos; recKind = 44; - if (ch == '*') {AddCh(); goto case 46;} - else {t.kind = 44; break;} + recEnd = pos; recKind = 12; + if (ch == '=') {AddCh(); goto case 31;} + else if (ch == ':') {AddCh(); goto case 58;} + else {t.kind = 12; 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;} + recEnd = pos; recKind = 20; + if (ch == '=') {AddCh(); goto case 69;} + else if (ch == ':') {AddCh(); goto case 44;} + else {t.kind = 20; break;} case 62: - recEnd = pos; recKind = 80; - if (ch == '=') {AddCh(); goto case 38;} - else {t.kind = 80; break;} + recEnd = pos; recKind = 21; + if (ch == '=') {AddCh(); goto case 42;} + else {t.kind = 21; break;} case 63: - recEnd = pos; recKind = 74; - if (ch == '+') {AddCh(); goto case 43;} - else {t.kind = 74; break;} + recEnd = pos; recKind = 29; + if (ch == '|') {AddCh(); goto case 54;} + else {t.kind = 29; break;} case 64: - recEnd = pos; recKind = 66; - if (ch == '=') {AddCh(); goto case 66;} - else {t.kind = 66; break;} + recEnd = pos; recKind = 32; + if (ch == '=') {AddCh(); goto case 70;} + else {t.kind = 32; break;} case 65: - recEnd = pos; recKind = 65; - if (ch == '>') {AddCh(); goto case 29;} - else {t.kind = 65; break;} + recEnd = pos; recKind = 45; + if (ch == '*') {AddCh(); goto case 51;} + else {t.kind = 45; break;} case 66: - recEnd = pos; recKind = 59; - if (ch == '>') {AddCh(); goto case 27;} - else {t.kind = 59; break;} + recEnd = pos; recKind = 55; + if (ch == '|') {AddCh(); goto case 40;} + else if (ch == '{') {AddCh(); goto case 53;} + else {t.kind = 55; break;} + case 67: + recEnd = pos; recKind = 81; + if (ch == '=') {AddCh(); goto case 43;} + else {t.kind = 81; break;} + case 68: + recEnd = pos; recKind = 75; + if (ch == '+') {AddCh(); goto case 48;} + else {t.kind = 75; break;} + case 69: + recEnd = pos; recKind = 67; + if (ch == '=') {AddCh(); goto case 71;} + else {t.kind = 67; break;} + case 70: + recEnd = pos; recKind = 66; + if (ch == '>') {AddCh(); goto case 34;} + else {t.kind = 66; break;} + case 71: + recEnd = pos; recKind = 60; + if (ch == '>') {AddCh(); goto case 32;} + else {t.kind = 60; break;} } t.val = new String(tval, 0, tlen); |