diff options
| author |  mikebarnett <unknown> | 2010-06-22 17:58:58 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2010-06-22 17:58:58 +0000 |
| commit | 67c07706d2b4ee941954301a0c18abfcf253384c (patch) | |
| tree | 994d3e772c2fce65605bd28b947ed7f2ede9d00a /Source/Core/Scanner.ssc | |
| parent | 98ee7b446b22df255ecf914d68f1997ea987877e (diff) | |
Updated the frame files to work with the latest Coco/R. This entails *not* having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.
Lots of code changes to compensate for the new frame files.
Diffstat (limited to 'Source/Core/Scanner.ssc')
| -rw-r--r-- | Source/Core/Scanner.ssc | 1095 |
1 files changed, 584 insertions, 511 deletions
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index a6f2c0a4..3765574e 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -1,3 +1,4 @@ +
using System;
using System.IO;
using System.Collections;
@@ -5,7 +6,6 @@ using System.Collections.Generic; using System.Text;
using Microsoft.Contracts;
-
namespace Microsoft.Boogie {
[Immutable]
@@ -19,26 +19,30 @@ namespace Microsoft.Boogie { bool IsValid { get; }
}
-
+
[Immutable]
public class Token : IToken {
- int _kind; // token kind
+ public int _kind; // token kind
string _filename; // token file
- int _pos; // token position in the source text (starting at 0)
- int _col; // token column (starting at 0)
- int _line; // token line (starting at 1)
- string/*!*/ _val = "foo"; // token value
-
+ public int _pos; // token position in the source text (starting at 0)
+ public int _col; // token column (starting at 1)
+ public int _line; // token line (starting at 1)
+ public string/*!*/ _val; // token value
+ public Token next; // ML 2005-03-11 Tokens are kept in linked list
+
public static IToken! NoToken = new Token();
- public Token();
+ public Token() {
+ this._val = "anything so that it is nonnull";
+ }
public Token(int linenum, int colnum) {
this._line = linenum;
this._col = colnum;
+ this._val = "anything so that it is nonnull";
base();
}
- public int kind {
+ public int kind {
get { return this._kind; }
set { this._kind = value; }
}
@@ -47,7 +51,7 @@ namespace Microsoft.Boogie { get { return this._filename; }
set { this._filename = value; }
}
-
+
public int pos{
get { return this._pos; }
set { this._pos = value; }
@@ -67,394 +71,435 @@ namespace Microsoft.Boogie { get { return this._val; }
set { this._val = value; }
}
-
+
public bool IsValid { get { return this._filename != null; } }
- }
+
}
-namespace BoogiePL {
-
-using Microsoft.Boogie;
-
+//-----------------------------------------------------------------------------------
+// Buffer
+//-----------------------------------------------------------------------------------
public class Buffer {
- static string/*!*/ buf;
- static int bufLen;
- static int pos;
- public const int eof = '\uffff';
+ // This Buffer supports the following cases:
+ // 1) seekable stream (file)
+ // a) whole stream in buffer
+ // b) part of stream in buffer
+ // 2) non seekable stream (network, console)
- public static void Fill(TextReader! reader) {
- List<string!> defines = new List<string!>();
- Fill(reader, defines);
- }
-
- struct ReadState {
- public bool hasSeenElse;
- public bool mayStillIncludeAnotherAlternative;
- public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {
- this.hasSeenElse = hasSeenElse;
- this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;
- }
- }
-
- public static void Fill(TextReader! reader, List<string!>! defines) {
- StringBuilder sb = new StringBuilder();
- List<ReadState>! readState = new List<ReadState>(); // readState.Count is the current nesting level of #if's
- int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n
- while (true)
- invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count;
- {
- string s = reader.ReadLine();
- if (s == null) {
- if (readState.Count != 0) {
- sb.AppendLine("#MalformedInput: missing #endif");
- }
- break;
- }
- string t = s.Trim();
- if (t.StartsWith("#if")) {
- ReadState rs = new ReadState(false, false);
- if (ignoreCutoff != -1) {
- // we're already in a state of ignoring, so continue to ignore
- } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) {
- // include this branch
- } else {
- ignoreCutoff = readState.Count; // start ignoring
- rs.mayStillIncludeAnotherAlternative = true; // allow some later "elsif" or "else" branch to be included
- }
- readState.Add(rs);
- sb.AppendLine(); // ignore the #if line
-
- } else if (t.StartsWith("#elsif")) {
- ReadState rs;
- if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {
- sb.AppendLine("#MalformedInput: misplaced #elsif"); // malformed input
- break;
- }
- if (ignoreCutoff == -1) {
- // we had included the previous branch
- assert !rs.mayStillIncludeAnotherAlternative;
- ignoreCutoff = readState.Count-1; // start ignoring
- } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) {
- // include this branch, but no subsequent branch at this level
- ignoreCutoff = -1;
- rs.mayStillIncludeAnotherAlternative = false;
- readState[readState.Count-1] = rs;
- }
- sb.AppendLine(); // ignore the #elsif line
-
- } else if (t == "#else") {
- ReadState rs;
- if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {
- sb.AppendLine("#MalformedInput: misplaced #else"); // malformed input
- break;
- }
- rs.hasSeenElse = true;
- if (ignoreCutoff == -1) {
- // we had included the previous branch
- assert !rs.mayStillIncludeAnotherAlternative;
- ignoreCutoff = readState.Count-1; // start ignoring
- } else if (rs.mayStillIncludeAnotherAlternative) {
- // include this branch
- ignoreCutoff = -1;
- rs.mayStillIncludeAnotherAlternative = false;
- }
- readState[readState.Count-1] = rs;
- sb.AppendLine(); // ignore the #else line
-
- } else if (t == "#endif") {
- if (readState.Count == 0) {
- sb.AppendLine("#MalformedInput: misplaced #endif"); // malformed input
- break;
- }
- readState.RemoveAt(readState.Count-1); // pop
- if (ignoreCutoff == readState.Count) {
- // we had ignored the branch that ends here; so, now we start including again
- ignoreCutoff = -1;
- }
- sb.AppendLine(); // ignore the #endif line
-
- } else if (ignoreCutoff == -1) {
- sb.AppendLine(s); // included line
-
- } else {
- sb.AppendLine(); // ignore the line
- }
- }
-
- Fill(sb.ToString());
- }
+ 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
+ byte[]! buf; // input buffer
+ int bufStart; // position of first byte in buffer relative to input stream
+ int bufLen; // length of buffer
+ int fileLen; // length of input stream (may change if the stream is no file)
+ int bufPos; // current position in buffer
+ Stream! stream; // input stream (seekable)
+ bool isUserStream; // was the stream opened by the user?
+
+ [NotDelayed]
+ public Buffer (Stream! s, bool isUserStream) {
+ stream = s; this.isUserStream = isUserStream;
+
+ int fl, bl;
+ if (s.CanSeek) {
+ fl = (int) s.Length;
+ bl = fl < MAX_BUFFER_LENGTH ? fl : MAX_BUFFER_LENGTH; // Math.Min(fileLen, MAX_BUFFER_LENGTH);
+ bufStart = Int32.MaxValue; // nothing in the buffer so far
+ } else {
+ fl = bl = bufStart = 0;
+ }
- // "arg" is assumed to be trimmed
- private static bool IfdefConditionSaysToInclude(string! arg, List<string!>! defines) {
- bool sense = true;
- while (arg.StartsWith("!")) {
- sense = !sense;
- arg = arg.Substring(1).TrimStart();
- }
- return defines.Contains(arg) == sense;
- }
-
- public static void Fill(string! text) {
- buf = text;
- bufLen = buf.Length;
- pos = 0;
- }
-
- public static int Read() {
- if (pos < bufLen) {
- return buf[pos++];
- } else {
- return eof;
- }
- }
+ buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
+ fileLen = fl; bufLen = bl;
+ base();
+ 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
+ buf = b.buf;
+ bufStart = b.bufStart;
+ bufLen = b.bufLen;
+ fileLen = b.fileLen;
+ bufPos = b.bufPos;
+ stream = b.stream;
+ // keep destructor from closing the stream
+ //b.stream = null;
+ isUserStream = b.isUserStream;
+ // keep destructor from closing the stream
+ b.isUserStream = true;
+ }
- public static string/*!*/ ReadToEOL() {
- int x = buf.IndexOf('\n', pos);
- if (x == -1) {
- string s = buf.Substring(pos);
- pos = buf.Length;
- return s;
- } else {
- string s = buf.Substring(pos, x+1 - pos); // also include the '\n'
- pos = x+1;
- return s;
- }
- }
+ ~Buffer() { Close(); }
+
+ protected void Close() {
+ if (!isUserStream && stream != null) {
+ stream.Close();
+ //stream = null;
+ }
+ }
+
+ public virtual int Read () {
+ if (bufPos < bufLen) {
+ return buf[bufPos++];
+ } else if (Pos < fileLen) {
+ Pos = Pos; // shift buffer start to Pos
+ return buf[bufPos++];
+ } else if (stream != null && !stream.CanSeek && ReadNextStreamChunk() > 0) {
+ return buf[bufPos++];
+ } else {
+ return EOF;
+ }
+ }
- public static int Pos {
- get { return pos; }
- set {
- if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value;
- }
- }
-}
+ public int Peek () {
+ int curPos = Pos;
+ int ch = Read();
+ Pos = curPos;
+ return ch;
+ }
+
+ public string! GetString (int beg, int end) {
+ int len = 0;
+ char[] buf = new char[end - beg];
+ int oldPos = Pos;
+ Pos = beg;
+ while (Pos < end) buf[len++] = (char) Read();
+ Pos = oldPos;
+ return new String(buf, 0, len);
+ }
+ public int Pos {
+ get { return bufPos + bufStart; }
+ set {
+ if (value >= fileLen && stream != null && !stream.CanSeek) {
+ // Wanted position is after buffer and the stream
+ // is not seek-able e.g. network or console,
+ // thus we have to read the stream manually till
+ // the wanted position is in sight.
+ while (value >= fileLen && ReadNextStreamChunk() > 0);
+ }
+ if (value < 0 || value > fileLen) {
+ throw new FatalError("buffer out of bounds access, position: " + value);
+ }
+ if (value >= bufStart && value < bufStart + bufLen) { // already in buffer
+ bufPos = value - bufStart;
+ } else if (stream != null) { // must be swapped in
+ stream.Seek(value, SeekOrigin.Begin);
+ bufLen = stream.Read(buf, 0, buf.Length);
+ bufStart = value; bufPos = 0;
+ } else {
+ // set the position to the end of the file, Pos will return fileLen.
+ bufPos = fileLen - bufStart;
+ }
+ }
+ }
+
+ // 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.
+ private int ReadNextStreamChunk() {
+ int free = buf.Length - bufLen;
+ if (free == 0) {
+ // in the case of a growing input stream
+ // we can neither seek in the stream, nor can we
+ // foresee the maximum length, thus we must adapt
+ // the buffer size on demand.
+ byte[] newBuf = new byte[bufLen * 2];
+ Array.Copy(buf, newBuf, bufLen);
+ buf = newBuf;
+ free = bufLen;
+ }
+ int read = stream.Read(buf, bufLen, free);
+ if (read > 0) {
+ fileLen = bufLen = (bufLen + read);
+ return read;
+ }
+ // end of stream reached
+ return 0;
+ }
+}
+
+//-----------------------------------------------------------------------------------
+// UTF8Buffer
+//-----------------------------------------------------------------------------------
+public class UTF8Buffer: Buffer {
+ public UTF8Buffer(Buffer! b): base(b) {}
+
+ public override int Read() {
+ int ch;
+ do {
+ ch = base.Read();
+ // until we find a utf8 start (0xxxxxxx or 11xxxxxx)
+ } while ((ch >= 128) && ((ch & 0xC0) != 0xC0) && (ch != EOF));
+ if (ch < 128 || ch == EOF) {
+ // nothing to do, first 127 chars are the same in ascii and utf8
+ // 0xxxxxxx or end of file character
+ } else if ((ch & 0xF0) == 0xF0) {
+ // 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx
+ int c1 = ch & 0x07; ch = base.Read();
+ int c2 = ch & 0x3F; ch = base.Read();
+ int c3 = ch & 0x3F; ch = base.Read();
+ int c4 = ch & 0x3F;
+ ch = (((((c1 << 6) | c2) << 6) | c3) << 6) | c4;
+ } else if ((ch & 0xE0) == 0xE0) {
+ // 1110xxxx 10xxxxxx 10xxxxxx
+ int c1 = ch & 0x0F; ch = base.Read();
+ int c2 = ch & 0x3F; ch = base.Read();
+ int c3 = ch & 0x3F;
+ ch = (((c1 << 6) | c2) << 6) | c3;
+ } else if ((ch & 0xC0) == 0xC0) {
+ // 110xxxxx 10xxxxxx
+ int c1 = ch & 0x1F; ch = base.Read();
+ int c2 = ch & 0x3F;
+ ch = (c1 << 6) | c2;
+ }
+ return ch;
+ }
+}
+
+//-----------------------------------------------------------------------------------
+// Scanner
+//-----------------------------------------------------------------------------------
public class Scanner {
- const char EOF = '\0';
- const char CR = '\r';
- const char LF = '\n';
- [Microsoft.Contracts.Verify(false)]
+ const char EOL = '\n';
+ const int eofSym = 0; /* pdt */
+ const int maxT = 88;
+ const int noSym = 88;
+
+
+ public Buffer! buffer; // scanner buffer
+
+ Token! t; // current token
+ int ch; // current input character
+ int pos; // byte position of current character
+ int col; // column number of current character
+ int line; // line number of current character
+ int oldEols; // EOLs that appeared in a comment;
+ static readonly Hashtable! start; // maps first token character to start state
+
+ 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[0] = 58;
- start[33] = 41;
- start[34] = 6;
- start[35] = 2;
- start[36] = 2;
- start[37] = 51;
- start[38] = 34;
- start[39] = 2;
- start[40] = 11;
- start[41] = 12;
- start[42] = 24;
- start[43] = 47;
- start[44] = 14;
- start[45] = 49;
- start[46] = 2;
- start[47] = 50;
- start[48] = 9;
- start[49] = 9;
- start[50] = 9;
- start[51] = 9;
- start[52] = 9;
- start[53] = 9;
- start[54] = 9;
- start[55] = 9;
- start[56] = 9;
- start[57] = 9;
- start[58] = 13;
- start[59] = 10;
- start[60] = 17;
- start[61] = 21;
- start[62] = 18;
- start[63] = 2;
- start[65] = 2;
- start[66] = 2;
- start[67] = 2;
- start[68] = 2;
- start[69] = 2;
- start[70] = 2;
- start[71] = 2;
- start[72] = 2;
- start[73] = 2;
- start[74] = 2;
- start[75] = 2;
- start[76] = 2;
- start[77] = 2;
- start[78] = 2;
- start[79] = 2;
- start[80] = 2;
- start[81] = 2;
- start[82] = 2;
- start[83] = 2;
- start[84] = 2;
- start[85] = 2;
- start[86] = 2;
- start[87] = 2;
- start[88] = 2;
- start[89] = 2;
- start[90] = 2;
- start[91] = 15;
- start[92] = 1;
- start[93] = 16;
- start[94] = 2;
- start[95] = 2;
- start[96] = 2;
- start[97] = 2;
- start[98] = 2;
- start[99] = 2;
- start[100] = 2;
- start[101] = 2;
- start[102] = 2;
- start[103] = 2;
- start[104] = 2;
- start[105] = 2;
- start[106] = 2;
- start[107] = 2;
- start[108] = 2;
- start[109] = 2;
- start[110] = 2;
- start[111] = 2;
- start[112] = 2;
- start[113] = 2;
- start[114] = 2;
- start[115] = 2;
- start[116] = 2;
- start[117] = 2;
- start[118] = 2;
- start[119] = 2;
- start[120] = 2;
- start[121] = 2;
- start[122] = 2;
- start[123] = 19;
- start[124] = 37;
- start[125] = 20;
- start[126] = 2;
- start[172] = 52;
- start[955] = 55;
- start[8226] = 57;
- start[8656] = 33;
- start[8658] = 32;
- start[8660] = 29;
- start[8704] = 53;
- start[8707] = 54;
- start[8743] = 36;
- start[8744] = 39;
- start[8800] = 44;
- start[8804] = 45;
- start[8805] = 46;
+ start = new Hashtable(128);
+ for (int i = 35; i <= 36; ++i) start[i] = 2;
+ for (int i = 39; i <= 39; ++i) start[i] = 2;
+ for (int i = 46; i <= 46; ++i) start[i] = 2;
+ for (int i = 63; i <= 63; ++i) start[i] = 2;
+ 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] = 9;
+ for (int i = 34; i <= 34; ++i) start[i] = 6;
+ start[92] = 1;
+ start[59] = 10;
+ start[40] = 11;
+ start[41] = 12;
+ start[58] = 47;
+ start[44] = 13;
+ start[91] = 14;
+ start[93] = 15;
+ start[60] = 48;
+ start[62] = 49;
+ start[123] = 50;
+ start[125] = 51;
+ start[61] = 52;
+ start[42] = 18;
+ start[8660] = 21;
+ start[8658] = 23;
+ start[8656] = 24;
+ start[38] = 25;
+ start[8743] = 27;
+ start[124] = 28;
+ start[8744] = 30;
+ start[33] = 53;
+ start[8800] = 34;
+ start[8804] = 35;
+ start[8805] = 36;
+ start[43] = 54;
+ start[45] = 38;
+ start[47] = 39;
+ start[37] = 40;
+ start[172] = 41;
+ start[8704] = 42;
+ start[8707] = 43;
+ start[955] = 44;
+ start[8226] = 46;
+ start[Buffer.EOF] = -1;
+
}
- const int noSym = 88;
- static short[] start = new short[16385];
-
-
- static Token/*!*/ t; // current token
- static char ch; // current input character
- static int pos; // column number of current character
- static int line; // line number of current character
- static int lineStart; // start position of current line
- static Queue! oldEols; // EOLs that appeared in a comment;
- static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner
- static string Filename;
-
- ///<summary>
- ///Initializes the scanner. Note: first fill the Buffer.
- ///</summary>
- ///<param name="filename">File name used for error reporting</param>
- public static void Init (string filename) {
- Filename = filename;
- pos = -1; line = 1; lineStart = 0;
- oldEols = new Queue();
- NextCh();
- ignore = new BitArray(16384);
- ignore[9] = true; ignore[10] = true; ignore[13] = true; ignore[32] = true;
-
- }
-
- private static void NextCh() {
- if (oldEols.Count > 0) {
- ch = (char) ((!)oldEols.Dequeue());
- } else {
- while (true) {
- ch = (char)Buffer.Read(); pos++;
- if (ch == Buffer.eof) {
- ch = EOF;
- } else if (ch == LF) {
- line++;
- lineStart = pos + 1;
-
- } else if (ch == '#' && pos == lineStart) {
- int prLine = line;
- int prColumn = pos - lineStart; // which is 0
-
- string hashLine = Buffer.ReadToEOL(); pos += hashLine.Length;
- line++;
- lineStart = pos + 1;
-
- hashLine = hashLine.TrimEnd(null);
- if (hashLine.StartsWith("line ") || hashLine == "line") {
- // parse #line pragma: #line num [filename]
- string h = hashLine.Substring(4).TrimStart(null);
- int x = h.IndexOf(' ');
- if (x == -1) {
- x = h.Length; // this will be convenient below when we look for a filename
- }
- try {
- int li = int.Parse(h.Substring(0, x));
-
- h = h.Substring(x).Trim();
-
- // act on #line
- line = li;
- if (h.Length != 0) {
- // a filename was specified
- Filename = h;
- }
- continue; // successfully parsed and acted on the #line pragma
-
- } catch (FormatException) {
- // just fall down through to produce an error message
- }
- Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
- continue;
- }
-
- Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
- continue;
- }
- return;
- }
- }
- }
-
- - static bool Comment0() {
- int level = 1, line0 = line, lineStart0 = lineStart;
+
+ [NotDelayed]
+ public Scanner (string! fileName, Errors! errorHandler) {
+ this.errorHandler = errorHandler;
+ pt = tokens = new Token(); // first token is a dummy
+ t = new Token(); // dummy because t is a non-null field
+ try {
+ Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
+ buffer = new Buffer(stream, false);
+ Filename = fileName;
+ base();
+ Init();
+ } catch (IOException) {
+ throw new FatalError("Cannot open file " + fileName);
+ }
+ }
+
+ [NotDelayed]
+ public Scanner (Stream! s, Errors! errorHandler, string! fileName) {
+ pt = tokens = new Token(); // first token is a dummy
+ t = new Token(); // dummy because t is a non-null field
+ buffer = new Buffer(s, true);
+ this.errorHandler = errorHandler;
+ this.Filename = fileName;
+ base();
+ Init();
+ }
+
+ void Init() {
+ pos = -1; line = 1; col = 0;
+ oldEols = 0;
+ NextCh();
+ if (ch == 0xEF) { // check optional byte order mark for UTF-8
+ NextCh(); int ch1 = ch;
+ NextCh(); int ch2 = ch;
+ if (ch1 != 0xBB || ch2 != 0xBF) {
+ throw new FatalError(String.Format("illegal byte order mark: EF {0,2:X} {1,2:X}", ch1, ch2));
+ }
+ buffer = new UTF8Buffer(buffer); col = 0;
+ NextCh();
+ }
+ pt = tokens = new Token(); // first token is a dummy
+ }
+
+ string! ReadToEOL(){
+ int p = buffer.Pos;
+ int 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;
+ while (ch != EOL && ch != Buffer.EOF){
+ 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;
+ }
+ string! s = buffer.GetString(p, buffer.Pos);
+ return s;
+ }
+
+ void NextCh() {
+ if (oldEols > 0) { ch = EOL; oldEols--; }
+ else {
+// pos = buffer.Pos;
+// ch = buffer.Read(); col++;
+// // 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;
+// if (ch == EOL) { line++; col = 0; }
+
+ while (true) {
+ pos = buffer.Pos;
+ ch = buffer.Read(); col++;
+ // 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;
+ if (ch == EOL) {
+ line++; col = 0;
+ } else if (ch == '#' && col == 1) {
+ int prLine = line;
+ int prColumn = 0;
+
+ string! hashLine = ReadToEOL();
+ col = 0;
+ line++;
+
+ hashLine = hashLine.TrimEnd(null);
+ if (hashLine.StartsWith("line ") || hashLine == "line") {
+ // parse #line pragma: #line num [filename]
+ string h = hashLine.Substring(4).TrimStart(null);
+ int x = h.IndexOf(' ');
+ if (x == -1) {
+ x = h.Length; // this will be convenient below when we look for a filename
+ }
+ try {
+ int li = int.Parse(h.Substring(0, x));
+
+ h = h.Substring(x).Trim();
+
+ // act on #line
+ line = li;
+ if (h.Length != 0) {
+ // a filename was specified
+ Filename = h;
+ }
+ continue; // successfully parsed and acted on the #line pragma
+
+ } catch (FormatException) {
+ // just fall down through to produce an error message
+ }
+ this.errorHandler.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
+ continue;
+ }
+
+ this.errorHandler.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
+ continue;
+ }
+ return;
+ }
+
+
+ }
+
+ }
+
+ void AddCh() {
+ if (tlen >= tval.Length) {
+ char[] newBuf = new char[2 * tval.Length];
+ Array.Copy(tval, 0, newBuf, 0, tval.Length);
+ tval = newBuf;
+ }
+ if (ch != Buffer.EOF) {
+ tval[tlen++] = (char) ch;
+ NextCh();
+ }
+ }
+
+
+
+ bool Comment0() {
+ int level = 1, pos0 = pos, line0 = line, col0 = col;
NextCh();
if (ch == '/') {
NextCh();
for(;;) {
if (ch == 10) {
level--;
- if (level == 0) {
- while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
- NextCh(); return true;
- }
+ if (level == 0) { oldEols = line - line0; NextCh(); return true; }
NextCh();
- } else if (ch == EOF) return false;
+ } else if (ch == Buffer.EOF) return false;
else NextCh();
}
} else {
- if (ch==CR) {line--; lineStart = lineStart0;}
- pos = pos - 2; Buffer.Pos = pos+1; NextCh();
+ buffer.Pos = pos0; NextCh(); line = line0; col = col0;
}
return false;
}
- - static bool Comment1() {
- int level = 1, line0 = line, lineStart0 = lineStart;
+
+ bool Comment1() {
+ int level = 1, pos0 = pos, line0 = line, col0 = col;
NextCh();
if (ch == '*') {
NextCh();
@@ -463,10 +508,7 @@ public class Scanner { NextCh();
if (ch == '/') {
level--;
- if (level == 0) {
- while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
- NextCh(); return true;
- }
+ if (level == 0) { oldEols = line - line0; NextCh(); return true; }
NextCh();
}
} else if (ch == '/') {
@@ -474,19 +516,18 @@ public class Scanner { if (ch == '*') {
level++; NextCh();
}
- } else if (ch == EOF) return false;
+ } else if (ch == Buffer.EOF) return false;
else NextCh();
}
} else {
- if (ch==CR) {line--; lineStart = lineStart0;}
- pos = pos - 2; Buffer.Pos = pos+1; NextCh();
+ buffer.Pos = pos0; NextCh(); line = line0; col = col0;
}
return false;
}
-
- static void CheckLiteral() {
- switch (t.val) {
+
+ void CheckLiteral() {
+ switch (t.val) {
case "var": t.kind = 6; break;
case "where": t.kind = 12; break;
case "int": t.kind = 13; break;
@@ -524,197 +565,229 @@ public class Scanner { case "exists": t.kind = 82; break;
case "lambda": t.kind = 84; break;
default: break;
+ }
+ }
- }
- }
-
- public static Token/*!*/ Scan() {
- while (ignore[ch]) { NextCh(); }
- if (ch == '/' && Comment0() || ch == '/' && Comment1() ) return Scan();
- t = new Token();
- t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;
- int state = (/*^ (!) ^*/ start)[ch];
- StringBuilder buf = new StringBuilder(16);
- buf.Append(ch); NextCh();
-
- switch (state) {
- case 0: {t.kind = noSym; goto done;} // NextCh already done
+ Token! NextToken() {
+ while (ch == ' ' ||
+ ch >= 9 && ch <= 10 || ch == 13
+ ) NextCh();
+ if (ch == '/' && Comment0() ||ch == '/' && Comment1()) return NextToken();
+ int recKind = noSym;
+ int recEnd = pos;
+ t = new Token();
+ t.pos = pos; t.col = col; t.line = line;
+ t.filename = this.Filename;
+ int state;
+ if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }
+ else { state = 0; }
+ tlen = 0; AddCh();
+
+ switch (state) {
+ case -1: { t.kind = eofSym; break; } // NextCh already done
+ case 0: {
+ if (recKind != noSym) {
+ tlen = recEnd - t.pos;
+ SetScannerBehindT();
+ }
+ t.kind = recKind; break;
+ } // NextCh already done
case 1:
- if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;}
- else {t.kind = noSym; goto done;}
+ if (ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~') {AddCh(); goto case 2;}
+ else {goto case 0;}
case 2:
- if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;}
- else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}
+ recEnd = pos; recKind = 1;
+ if (ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~') {AddCh(); goto case 2;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 3:
- if (ch == 'v') {buf.Append(ch); NextCh(); goto case 4;}
- else {t.kind = noSym; goto done;}
+ if (ch == 'v') {AddCh(); goto case 4;}
+ else {goto case 0;}
case 4:
- if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}
- else {t.kind = noSym; goto done;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 5;}
+ else {goto case 0;}
case 5:
- if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}
- else {t.kind = 2; goto done;}
+ recEnd = pos; recKind = 2;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 5;}
+ else {t.kind = 2; break;}
case 6:
- if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 7;}
- else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 6;}
- else {t.kind = noSym; goto done;}
+ if (ch == '"') {AddCh(); goto case 7;}
+ else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 6;}
+ else {goto case 0;}
case 7:
- {t.kind = 4; goto done;}
+ {t.kind = 4; break;}
case 8:
- if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 8;}
- else {t.kind = 5; goto done;}
+ recEnd = pos; recKind = 5;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 8;}
+ else {t.kind = 5; break;}
case 9:
- if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 9;}
- else if (ch == 'b') {buf.Append(ch); NextCh(); goto case 3;}
- else if (ch == '.') {buf.Append(ch); NextCh(); goto case 8;}
- else {t.kind = 3; goto done;}
+ recEnd = pos; recKind = 3;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
+ else if (ch == 'b') {AddCh(); goto case 3;}
+ else if (ch == '.') {AddCh(); goto case 8;}
+ else {t.kind = 3; break;}
case 10:
- {t.kind = 7; goto done;}
+ {t.kind = 7; break;}
case 11:
- {t.kind = 8; goto done;}
+ {t.kind = 8; break;}
case 12:
- {t.kind = 9; goto done;}
+ {t.kind = 9; break;}
case 13:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 25;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 56;}
- else {t.kind = 10; goto done;}
+ {t.kind = 11; break;}
case 14:
- {t.kind = 11; goto done;}
+ {t.kind = 15; break;}
case 15:
- {t.kind = 15; goto done;}
+ {t.kind = 16; break;}
case 16:
- {t.kind = 16; goto done;}
+ {t.kind = 36; break;}
case 17:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}
- else if (ch == ':') {buf.Append(ch); NextCh(); goto case 43;}
- else {t.kind = 17; goto done;}
+ {t.kind = 37; break;}
case 18:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 40;}
- else {t.kind = 18; goto done;}
+ {t.kind = 44; break;}
case 19:
- if (ch == '{') {buf.Append(ch); NextCh(); goto case 22;}
- else {t.kind = 25; goto done;}
+ {t.kind = 49; break;}
case 20:
- if (ch == '}') {buf.Append(ch); NextCh(); goto case 23;}
- else {t.kind = 26; goto done;}
+ {t.kind = 52; break;}
case 21:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;}
- else {t.kind = 29; goto done;}
+ {t.kind = 53; break;}
case 22:
- {t.kind = 36; goto done;}
+ {t.kind = 54; break;}
case 23:
- {t.kind = 37; goto done;}
+ {t.kind = 55; break;}
case 24:
- {t.kind = 44; goto done;}
+ {t.kind = 57; break;}
case 25:
- {t.kind = 49; goto done;}
+ if (ch == '&') {AddCh(); goto case 26;}
+ else {goto case 0;}
case 26:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 27;}
- else {t.kind = 63; goto done;}
+ {t.kind = 58; break;}
case 27:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 28;}
- else {t.kind = 56; goto done;}
+ {t.kind = 59; break;}
case 28:
- {t.kind = 52; goto done;}
+ if (ch == '|') {AddCh(); goto case 29;}
+ else {goto case 0;}
case 29:
- {t.kind = 53; goto done;}
+ {t.kind = 60; break;}
case 30:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 31;}
- else {t.kind = 62; goto done;}
+ {t.kind = 61; break;}
case 31:
- {t.kind = 54; goto done;}
+ {t.kind = 64; break;}
case 32:
- {t.kind = 55; goto done;}
+ {t.kind = 65; break;}
case 33:
- {t.kind = 57; goto done;}
+ {t.kind = 66; break;}
case 34:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 67; break;}
case 35:
- {t.kind = 58; goto done;}
+ {t.kind = 68; break;}
case 36:
- {t.kind = 59; goto done;}
+ {t.kind = 69; break;}
case 37:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 38;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 70; break;}
case 38:
- {t.kind = 60; goto done;}
+ {t.kind = 72; break;}
case 39:
- {t.kind = 61; goto done;}
+ {t.kind = 73; break;}
case 40:
- {t.kind = 64; goto done;}
+ {t.kind = 74; break;}
case 41:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 42;}
- else {t.kind = 75; goto done;}
+ {t.kind = 76; break;}
case 42:
- {t.kind = 65; goto done;}
+ {t.kind = 81; break;}
case 43:
- {t.kind = 66; goto done;}
+ {t.kind = 83; break;}
case 44:
- {t.kind = 67; goto done;}
+ {t.kind = 85; break;}
case 45:
- {t.kind = 68; goto done;}
+ {t.kind = 86; break;}
case 46:
- {t.kind = 69; goto done;}
+ {t.kind = 87; break;}
case 47:
- if (ch == '+') {buf.Append(ch); NextCh(); goto case 48;}
- else {t.kind = 71; goto done;}
+ recEnd = pos; recKind = 10;
+ if (ch == '=') {AddCh(); goto case 19;}
+ else if (ch == ':') {AddCh(); goto case 45;}
+ else {t.kind = 10; break;}
case 48:
- {t.kind = 70; goto done;}
+ recEnd = pos; recKind = 17;
+ if (ch == '=') {AddCh(); goto case 55;}
+ else if (ch == ':') {AddCh(); goto case 33;}
+ else {t.kind = 17; break;}
case 49:
- {t.kind = 72; goto done;}
+ recEnd = pos; recKind = 18;
+ if (ch == '=') {AddCh(); goto case 31;}
+ else {t.kind = 18; break;}
case 50:
- {t.kind = 73; goto done;}
+ recEnd = pos; recKind = 25;
+ if (ch == '{') {AddCh(); goto case 16;}
+ else {t.kind = 25; break;}
case 51:
- {t.kind = 74; goto done;}
+ recEnd = pos; recKind = 26;
+ if (ch == '}') {AddCh(); goto case 17;}
+ else {t.kind = 26; break;}
case 52:
- {t.kind = 76; goto done;}
+ recEnd = pos; recKind = 29;
+ if (ch == '=') {AddCh(); goto case 56;}
+ else {t.kind = 29; break;}
case 53:
- {t.kind = 81; goto done;}
+ recEnd = pos; recKind = 75;
+ if (ch == '=') {AddCh(); goto case 32;}
+ else {t.kind = 75; break;}
case 54:
- {t.kind = 83; goto done;}
+ recEnd = pos; recKind = 71;
+ if (ch == '+') {AddCh(); goto case 37;}
+ else {t.kind = 71; break;}
case 55:
- {t.kind = 85; goto done;}
+ recEnd = pos; recKind = 63;
+ if (ch == '=') {AddCh(); goto case 57;}
+ else {t.kind = 63; break;}
case 56:
- {t.kind = 86; goto done;}
+ recEnd = pos; recKind = 62;
+ if (ch == '>') {AddCh(); goto case 22;}
+ else {t.kind = 62; break;}
case 57:
- {t.kind = 87; goto done;}
- case 58: {t.kind = 0; goto done;}
- }
- done:
- t.val = buf.ToString();
- return t;
- }
+ recEnd = pos; recKind = 56;
+ if (ch == '>') {AddCh(); goto case 20;}
+ else {t.kind = 56; break;}
-} // end Scanner
+ }
+ 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 () {
+ if (tokens.next == null) {
+ return NextToken();
+ } else {
+ pt = tokens = tokens.next;
+ return tokens;
+ }
+ }
+ // peek for the next token, ignore pragmas
+ public Token! Peek () {
+ do {
+ if (pt.next == null) {
+ pt.next = NextToken();
+ }
+ pt = pt.next;
+ } while (pt.kind > maxT); // skip pragmas
+
+ return pt;
+ }
-public delegate void ErrorProc(int n, string filename, int line, int col);
+ // make sure that peeking starts at the current scan position
+ public void ResetPeek () { pt = tokens; }
-public class Errors {
- public static int count = 0; // number of errors detected
- public static ErrorProc/*!*/ SynErr; // syntactic errors
-
- public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors
- ConsoleColor color = Console.ForegroundColor;
- Console.ForegroundColor = ConsoleColor.Red;
- Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);
- Console.ForegroundColor = color;
- count++;
- }
-
- public static void SemErr(IToken! tok, string! msg) { // semantic errors
- SemErr(tok.filename, tok.line, tok.col, msg);
- }
-
- public static void Exception (string s) {
- ConsoleColor color = Console.ForegroundColor;
- Console.ForegroundColor = ConsoleColor.Red;
- Console.WriteLine(s);
- Console.ForegroundColor = color;
- System.Environment.Exit(0);
- }
+} // end Scanner
+
+public delegate void ErrorProc(int n, string filename, int line, int col);
-} // Errors
-} // end namespace
+}
\ No newline at end of file |