using System.IO;
using System.Collections;
using System.Collections.Generic;
using System.Text;
using Microsoft.Contracts;
using Bpl = Microsoft.Boogie;
using BoogiePL;


namespace Microsoft.Dafny {

  [Immutable]
  public class Token : Bpl.Token {
    public Token();
    public Token(int linenum, int colnum) {
      base(linenum, colnum);
    }
    public new static Token! NoToken = new Token();
  }

}

namespace Microsoft.Dafny {


public class Scanner {
  const char EOF = '\0';
  const char CR  = '\r';
  const char LF  = '\n';

  [Microsoft.Contracts.Verify(false)]
	static Scanner() {
		start[0] = 54;
		start[33] = 32;
		start[34] = 3;
		start[35] = 45;
		start[37] = 43;
		start[38] = 26;
		start[39] = 1;
		start[40] = 12;
		start[41] = 13;
		start[42] = 14;
		start[43] = 40;
		start[44] = 8;
		start[45] = 41;
		start[46] = 46;
		start[47] = 42;
		start[48] = 2;
		start[49] = 2;
		start[50] = 2;
		start[51] = 2;
		start[52] = 2;
		start[53] = 2;
		start[54] = 2;
		start[55] = 2;
		start[56] = 2;
		start[57] = 2;
		start[58] = 9;
		start[59] = 7;
		start[60] = 10;
		start[61] = 15;
		start[62] = 11;
		start[63] = 1;
		start[65] = 1;
		start[66] = 1;
		start[67] = 1;
		start[68] = 1;
		start[69] = 1;
		start[70] = 1;
		start[71] = 1;
		start[72] = 1;
		start[73] = 1;
		start[74] = 1;
		start[75] = 1;
		start[76] = 1;
		start[77] = 1;
		start[78] = 1;
		start[79] = 1;
		start[80] = 1;
		start[81] = 1;
		start[82] = 1;
		start[83] = 1;
		start[84] = 1;
		start[85] = 1;
		start[86] = 1;
		start[87] = 1;
		start[88] = 1;
		start[89] = 1;
		start[90] = 1;
		start[91] = 47;
		start[92] = 1;
		start[93] = 48;
		start[95] = 1;
		start[96] = 1;
		start[97] = 1;
		start[98] = 1;
		start[99] = 1;
		start[100] = 1;
		start[101] = 1;
		start[102] = 1;
		start[103] = 1;
		start[104] = 1;
		start[105] = 1;
		start[106] = 1;
		start[107] = 1;
		start[108] = 1;
		start[109] = 1;
		start[110] = 1;
		start[111] = 1;
		start[112] = 1;
		start[113] = 1;
		start[114] = 1;
		start[115] = 1;
		start[116] = 1;
		start[117] = 1;
		start[118] = 1;
		start[119] = 1;
		start[120] = 1;
		start[121] = 1;
		start[122] = 1;
		start[123] = 5;
		start[124] = 18;
		start[125] = 6;
		start[172] = 44;
		start[8226] = 53;
		start[8658] = 25;
		start[8660] = 22;
		start[8704] = 50;
		start[8707] = 51;
		start[8743] = 28;
		start[8744] = 30;
		start[8800] = 37;
		start[8804] = 38;
		start[8805] = 39;
	}
	const int noSym = 93;
	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)BoogiePL.Buffer.Read(); pos++;
        if (ch == BoogiePL.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 = BoogiePL.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 (System.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;
		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;
					}
					NextCh();
				} else if (ch == EOF) return false;
				else NextCh();
			}
		} else {
			if (ch==CR) {line--; lineStart = lineStart0;}
			pos = pos - 2; Buffer.Pos = pos+1; NextCh();
		}
		return false;
	}

	static bool Comment1() {
		int level = 1, line0 = line, lineStart0 = lineStart;
		NextCh();
		if (ch == '*') {
			NextCh();
			for(;;) {
				if (ch == '*') {
					NextCh();
					if (ch == '/') {
						level--;
						if (level == 0) {
							while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
							NextCh(); return true;
						}
						NextCh();
					}
				} else if (ch == '/') {
					NextCh();
					if (ch == '*') {
						level++; NextCh();
					}
				} else if (ch == EOF) return false;
				else NextCh();
			}
		} else {
			if (ch==CR) {line--; lineStart = lineStart0;}
			pos = pos - 2; Buffer.Pos = pos+1; NextCh();
		}
		return false;
	}

  
  static void CheckLiteral() {
    switch (t.val) {
			case "class": t.kind = 4; break;
			case "ghost": t.kind = 7; break;
			case "use": t.kind = 8; break;
			case "datatype": t.kind = 9; break;
			case "var": t.kind = 11; break;
			case "method": t.kind = 16; break;
			case "returns": t.kind = 17; break;
			case "modifies": t.kind = 18; break;
			case "free": t.kind = 19; break;
			case "requires": t.kind = 20; break;
			case "ensures": t.kind = 21; break;
			case "bool": t.kind = 24; break;
			case "int": t.kind = 25; break;
			case "set": t.kind = 26; break;
			case "seq": t.kind = 27; break;
			case "object": t.kind = 28; break;
			case "function": t.kind = 29; break;
			case "reads": t.kind = 30; break;
			case "decreases": t.kind = 31; break;
			case "match": t.kind = 33; break;
			case "case": t.kind = 34; break;
			case "label": t.kind = 36; break;
			case "break": t.kind = 37; break;
			case "return": t.kind = 38; break;
			case "new": t.kind = 40; break;
			case "havoc": t.kind = 41; break;
			case "if": t.kind = 42; break;
			case "else": t.kind = 43; break;
			case "while": t.kind = 44; break;
			case "invariant": t.kind = 45; break;
			case "call": t.kind = 46; break;
			case "foreach": t.kind = 47; break;
			case "in": t.kind = 48; break;
			case "assert": t.kind = 50; break;
			case "assume": t.kind = 51; break;
			case "then": t.kind = 52; break;
			case "false": t.kind = 76; break;
			case "true": t.kind = 77; break;
			case "null": t.kind = 78; break;
			case "fresh": t.kind = 81; break;
			case "this": t.kind = 85; break;
			case "old": t.kind = 86; break;
			case "forall": t.kind = 87; break;
			case "exists": t.kind = 89; 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
			case 1:
				if ((ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch >= '_' && ch <= 'z')) {buf.Append(ch); NextCh(); goto case 1;}
				else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}
			case 2:
				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 2;}
				else {t.kind = 2; goto done;}
			case 3:
				if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 4;}
				else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 3;}
				else {t.kind = noSym; goto done;}
			case 4:
				{t.kind = 3; goto done;}
			case 5:
				{t.kind = 5; goto done;}
			case 6:
				{t.kind = 6; goto done;}
			case 7:
				{t.kind = 10; goto done;}
			case 8:
				{t.kind = 12; goto done;}
			case 9:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
				else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}
				else {t.kind = 13; goto done;}
			case 10:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}
				else {t.kind = 14; goto done;}
			case 11:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}
				else {t.kind = 15; goto done;}
			case 12:
				{t.kind = 22; goto done;}
			case 13:
				{t.kind = 23; goto done;}
			case 14:
				{t.kind = 32; goto done;}
			case 15:
				if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;}
				else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
				else {t.kind = noSym; goto done;}
			case 16:
				{t.kind = 35; goto done;}
			case 17:
				{t.kind = 39; goto done;}
			case 18:
				if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}
				else {t.kind = 49; goto done;}
			case 19:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
				else {t.kind = 62; goto done;}
			case 20:
				if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
				else {t.kind = noSym; goto done;}
			case 21:
				{t.kind = 53; goto done;}
			case 22:
				{t.kind = 54; goto done;}
			case 23:
				if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
				else {t.kind = 61; goto done;}
			case 24:
				{t.kind = 55; goto done;}
			case 25:
				{t.kind = 56; goto done;}
			case 26:
				if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
				else {t.kind = noSym; goto done;}
			case 27:
				{t.kind = 57; goto done;}
			case 28:
				{t.kind = 58; goto done;}
			case 29:
				{t.kind = 59; goto done;}
			case 30:
				{t.kind = 60; goto done;}
			case 31:
				{t.kind = 63; goto done;}
			case 32:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
				else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
				else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
				else {t.kind = 74; goto done;}
			case 33:
				{t.kind = 64; goto done;}
			case 34:
				{t.kind = 65; goto done;}
			case 35:
				if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
				else {t.kind = noSym; goto done;}
			case 36:
				{t.kind = 66; goto done;}
			case 37:
				{t.kind = 67; goto done;}
			case 38:
				{t.kind = 68; goto done;}
			case 39:
				{t.kind = 69; goto done;}
			case 40:
				{t.kind = 70; goto done;}
			case 41:
				{t.kind = 71; goto done;}
			case 42:
				{t.kind = 72; goto done;}
			case 43:
				{t.kind = 73; goto done;}
			case 44:
				{t.kind = 75; goto done;}
			case 45:
				{t.kind = 79; goto done;}
			case 46:
				if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
				else {t.kind = 80; goto done;}
			case 47:
				{t.kind = 82; goto done;}
			case 48:
				{t.kind = 83; goto done;}
			case 49:
				{t.kind = 84; goto done;}
			case 50:
				{t.kind = 88; goto done;}
			case 51:
				{t.kind = 90; goto done;}
			case 52:
				{t.kind = 91; goto done;}
			case 53:
				{t.kind = 92; goto done;}
			case 54: {t.kind = 0; goto done;}
    }
    done:
    t.val = buf.ToString();
    return t;
  }

} // end Scanner


public delegate void ErrorProc(int n, string filename, int line, int col);

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
    System.ConsoleColor color = System.Console.ForegroundColor;
    System.Console.ForegroundColor = System.ConsoleColor.Red;
    System.Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);
    System.Console.ForegroundColor = color;
    count++;
  }
  
  public static void SemErr(Bpl.IToken! tok, string! msg) {  // semantic errors
    SemErr(tok.filename, tok.line, tok.col, msg);
  }
  
  public static void Exception (string s) {
    System.ConsoleColor color = System.Console.ForegroundColor;
    System.Console.ForegroundColor = System.ConsoleColor.Red;
    System.Console.WriteLine(s);
    System.Console.ForegroundColor = color;
    System.Environment.Exit(0);
  }

} // Errors

} // end namespace