summaryrefslogtreecommitdiff
path: root/Source/Dafny/Scanner.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Scanner.cs')
-rw-r--r--Source/Dafny/Scanner.cs226
1 files changed, 112 insertions, 114 deletions
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 5014ec39..b23cdb25 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
// a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
-[ContractInvariantMethod]
-void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);}
- [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+ [ContractInvariantMethod]
+ void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);
+ }
+
+// [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
}
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 105;
- const int noSym = 105;
-
-
-[ContractInvariantMethod]
-void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
-}
+ const int maxT = 104;
+ const int noSym = 104;
+
+
+ [ContractInvariantMethod]
+ void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+ }
+
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){
Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -256,43 +259,43 @@ void objectInvariant(){
start[97] = 10;
start[123] = 17;
start[125] = 18;
- start[61] = 57;
- start[124] = 58;
+ start[61] = 55;
+ start[124] = 56;
start[59] = 19;
start[44] = 20;
- start[58] = 59;
- start[60] = 60;
- start[62] = 61;
+ start[58] = 57;
+ start[60] = 58;
+ start[62] = 59;
start[40] = 21;
start[41] = 22;
start[42] = 23;
start[96] = 24;
start[91] = 26;
start[93] = 27;
- start[46] = 62;
+ start[46] = 60;
start[8660] = 31;
start[8658] = 33;
start[38] = 34;
start[8743] = 36;
start[8744] = 38;
- start[33] = 63;
- start[8800] = 44;
- start[8804] = 45;
- start[8805] = 46;
- start[43] = 47;
- start[45] = 48;
- start[47] = 49;
- start[37] = 50;
- start[172] = 51;
- start[8704] = 53;
- start[8707] = 54;
- start[8226] = 56;
+ start[33] = 61;
+ start[8800] = 42;
+ start[8804] = 43;
+ start[8805] = 44;
+ start[43] = 45;
+ start[45] = 46;
+ start[47] = 47;
+ start[37] = 48;
+ start[172] = 49;
+ start[8704] = 51;
+ start[8707] = 52;
+ start[8226] = 54;
start[Buffer.EOF] = -1;
}
-
- [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+// [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -302,15 +305,14 @@ void objectInvariant(){
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
-
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
- [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+// [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -319,10 +321,9 @@ void objectInvariant(){
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -343,11 +344,11 @@ void objectInvariant(){
Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +359,7 @@ void objectInvariant(){
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -366,9 +367,9 @@ void objectInvariant(){
// // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +419,7 @@ void objectInvariant(){
return;
}
-
+
}
}
@@ -530,16 +531,16 @@ void objectInvariant(){
case "assert": t.kind = 64; break;
case "assume": 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;
+ case "false": t.kind = 89; break;
+ case "true": t.kind = 90; break;
+ case "null": t.kind = 91; break;
+ case "this": t.kind = 92; break;
+ case "fresh": t.kind = 93; break;
+ case "allocated": t.kind = 94; break;
+ case "old": t.kind = 95; break;
+ case "then": t.kind = 96; break;
+ case "forall": t.kind = 98; break;
+ case "exists": t.kind = 100; break;
default: break;
}
}
@@ -556,10 +557,13 @@ void objectInvariant(){
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -690,73 +694,67 @@ void objectInvariant(){
case 41:
{t.kind = 79; break;}
case 42:
- if (ch == 'n') {AddCh(); goto case 43;}
- else {goto case 0;}
+ {t.kind = 81; break;}
case 43:
- {t.kind = 80; break;}
+ {t.kind = 82; break;}
case 44:
- {t.kind = 81; break;}
+ {t.kind = 83; break;}
case 45:
- {t.kind = 82; break;}
+ {t.kind = 84; break;}
case 46:
- {t.kind = 83; break;}
+ {t.kind = 85; break;}
case 47:
- {t.kind = 84; break;}
+ {t.kind = 86; break;}
case 48:
- {t.kind = 85; break;}
+ {t.kind = 87; break;}
case 49:
- {t.kind = 86; break;}
+ {t.kind = 88; break;}
case 50:
- {t.kind = 87; break;}
+ {t.kind = 97; break;}
case 51:
- {t.kind = 89; break;}
+ {t.kind = 99; break;}
case 52:
- {t.kind = 98; break;}
+ {t.kind = 101; break;}
case 53:
- {t.kind = 100; break;}
- case 54:
{t.kind = 102; break;}
- case 55:
+ case 54:
{t.kind = 103; break;}
- case 56:
- {t.kind = 104; break;}
- case 57:
+ case 55:
recEnd = pos; recKind = 15;
if (ch == '>') {AddCh(); goto case 28;}
- else if (ch == '=') {AddCh(); goto case 64;}
+ else if (ch == '=') {AddCh(); goto case 62;}
else {t.kind = 15; break;}
- case 58:
+ case 56:
recEnd = pos; recKind = 16;
if (ch == '|') {AddCh(); goto case 37;}
else {t.kind = 16; break;}
- case 59:
+ case 57:
recEnd = pos; recKind = 22;
if (ch == '=') {AddCh(); goto case 25;}
- else if (ch == ':') {AddCh(); goto case 55;}
+ else if (ch == ':') {AddCh(); goto case 53;}
else {t.kind = 22; break;}
- case 60:
+ case 58:
recEnd = pos; recKind = 23;
- if (ch == '=') {AddCh(); goto case 65;}
+ if (ch == '=') {AddCh(); goto case 63;}
else {t.kind = 23; break;}
- case 61:
+ case 59:
recEnd = pos; recKind = 24;
if (ch == '=') {AddCh(); goto case 39;}
else {t.kind = 24; break;}
- case 62:
+ case 60:
recEnd = pos; recKind = 53;
- if (ch == '.') {AddCh(); goto case 52;}
+ if (ch == '.') {AddCh(); goto case 50;}
else {t.kind = 53; break;}
- case 63:
- recEnd = pos; recKind = 88;
+ case 61:
+ recEnd = pos; recKind = 80;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
- else if (ch == 'i') {AddCh(); goto case 42;}
- else {t.kind = 88; break;}
- case 64:
+ else {t.kind = 80; break;}
+ case 62:
recEnd = pos; recKind = 75;
if (ch == '>') {AddCh(); goto case 32;}
else {t.kind = 75; break;}
- case 65:
+ case 63:
recEnd = pos; recKind = 76;
if (ch == '=') {AddCh(); goto case 29;}
else {t.kind = 76; break;}
@@ -765,14 +763,14 @@ void objectInvariant(){
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -793,7 +791,7 @@ void objectInvariant(){
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 19:45:06 +0000