//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.IO;
using System.Collections;
using System.Collections.Generic;
using System.Text;
using Microsoft.Contracts;


namespace Microsoft.Boogie {

  [Immutable]
  public interface IToken {
    int kind {get; set; }         // token kind
    string filename {get; set; }  // token file
    int pos {get; set; }          // token position in the source text (starting at 0)
    int col {get; set; }          // token column (starting at 0)
    int line {get; set; }         // token line (starting at 1)
    string/*!*/ val {get; set; }  // token value

    bool IsValid { get; }
  }
  
  [Immutable]
  public class Token : IToken {
    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 static IToken! NoToken = new Token();

    public Token();
    public Token(int linenum, int colnum) {
      this._line = linenum;
      this._col = colnum;
      base();
    }

    public int kind {
      get { return this._kind; }
      set { this._kind = value; }
    }
    
    public string filename{
      get { return this._filename; }
      set { this._filename = value; }
    }
    
    public int pos{
      get { return this._pos; }
      set { this._pos = value; }
    }
    
    public int col{
      get { return this._col; }
      set { this._col = value; }
    }
    
    public int line{
      get { return this._line; }
      set { this._line = value; }
    }
    
    public string/*!*/ val{
      get { return this._val; }
      set { this._val = value; }
    }
    
    public bool IsValid { get { return this._filename != null; } }
  }

}

namespace BoogiePL {

using Microsoft.Boogie;

public class Buffer {
  static string/*!*/ buf;
  static int bufLen;
  static int pos;
  public const int eof = '\uffff';
  
  public static void Fill(StreamReader! 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(StreamReader! 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());
  }

  // "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;
    }
  }

  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;
    }
  }

  public static int Pos {
    get { return pos; }
    set {
      if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value;
    }
  }
}



public class Scanner {
  const char EOF = '\0';
  const char CR  = '\r';
  const char LF  = '\n';
  [Microsoft.Contracts.Verify(false)]
	static Scanner() {
		start[0] = 57;
		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[8226] = 56;
		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;
	}
	const int noSym = 85;
	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;
		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 "var": t.kind = 6; break;
			case "where": t.kind = 12; break;
			case "int": t.kind = 13; break;
			case "bool": t.kind = 14; break;
			case "const": t.kind = 19; break;
			case "unique": t.kind = 20; break;
			case "extends": t.kind = 21; break;
			case "complete": t.kind = 22; break;
			case "function": t.kind = 23; break;
			case "returns": t.kind = 24; break;
			case "axiom": t.kind = 27; break;
			case "type": t.kind = 28; break;
			case "procedure": t.kind = 30; break;
			case "implementation": t.kind = 31; break;
			case "modifies": t.kind = 32; break;
			case "free": t.kind = 33; break;
			case "requires": t.kind = 34; break;
			case "ensures": t.kind = 35; 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 "call": t.kind = 50; break;
			case "forall": t.kind = 51; break;
			case "false": t.kind = 77; break;
			case "true": t.kind = 78; break;
			case "old": t.kind = 79; break;
			case "exists": t.kind = 81; 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 >= '#' && 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;}
			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;}
			case 3:
				if (ch == 'v') {buf.Append(ch); NextCh(); goto case 4;}
				else {t.kind = noSym; goto done;}
			case 4:
				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}
				else {t.kind = noSym; goto done;}
			case 5:
				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}
				else {t.kind = 2; goto done;}
			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;}
			case 7:
				{t.kind = 4; goto done;}
			case 8:
				if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 8;}
				else {t.kind = 5; goto done;}
			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;}
			case 10:
				{t.kind = 7; goto done;}
			case 11:
				{t.kind = 8; goto done;}
			case 12:
				{t.kind = 9; goto done;}
			case 13:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 25;}
				else if (ch == ':') {buf.Append(ch); NextCh(); goto case 55;}
				else {t.kind = 10; goto done;}
			case 14:
				{t.kind = 11; goto done;}
			case 15:
				{t.kind = 15; goto done;}
			case 16:
				{t.kind = 16; goto done;}
			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;}
			case 18:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 40;}
				else {t.kind = 18; goto done;}
			case 19:
				if (ch == '{') {buf.Append(ch); NextCh(); goto case 22;}
				else {t.kind = 25; goto done;}
			case 20:
				if (ch == '}') {buf.Append(ch); NextCh(); goto case 23;}
				else {t.kind = 26; goto done;}
			case 21:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;}
				else {t.kind = 29; goto done;}
			case 22:
				{t.kind = 36; goto done;}
			case 23:
				{t.kind = 37; goto done;}
			case 24:
				{t.kind = 44; goto done;}
			case 25:
				{t.kind = 49; goto done;}
			case 26:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 27;}
				else {t.kind = 63; goto done;}
			case 27:
				if (ch == '>') {buf.Append(ch); NextCh(); goto case 28;}
				else {t.kind = 56; goto done;}
			case 28:
				{t.kind = 52; goto done;}
			case 29:
				{t.kind = 53; goto done;}
			case 30:
				if (ch == '>') {buf.Append(ch); NextCh(); goto case 31;}
				else {t.kind = 62; goto done;}
			case 31:
				{t.kind = 54; goto done;}
			case 32:
				{t.kind = 55; goto done;}
			case 33:
				{t.kind = 57; goto done;}
			case 34:
				if (ch == '&') {buf.Append(ch); NextCh(); goto case 35;}
				else {t.kind = noSym; goto done;}
			case 35:
				{t.kind = 58; goto done;}
			case 36:
				{t.kind = 59; goto done;}
			case 37:
				if (ch == '|') {buf.Append(ch); NextCh(); goto case 38;}
				else {t.kind = noSym; goto done;}
			case 38:
				{t.kind = 60; goto done;}
			case 39:
				{t.kind = 61; goto done;}
			case 40:
				{t.kind = 64; goto done;}
			case 41:
				if (ch == '=') {buf.Append(ch); NextCh(); goto case 42;}
				else {t.kind = 75; goto done;}
			case 42:
				{t.kind = 65; goto done;}
			case 43:
				{t.kind = 66; goto done;}
			case 44:
				{t.kind = 67; goto done;}
			case 45:
				{t.kind = 68; goto done;}
			case 46:
				{t.kind = 69; goto done;}
			case 47:
				if (ch == '+') {buf.Append(ch); NextCh(); goto case 48;}
				else {t.kind = 71; goto done;}
			case 48:
				{t.kind = 70; goto done;}
			case 49:
				{t.kind = 72; goto done;}
			case 50:
				{t.kind = 73; goto done;}
			case 51:
				{t.kind = 74; goto done;}
			case 52:
				{t.kind = 76; goto done;}
			case 53:
				{t.kind = 80; goto done;}
			case 54:
				{t.kind = 82; goto done;}
			case 55:
				{t.kind = 83; goto done;}
			case 56:
				{t.kind = 84; goto done;}
			case 57: {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
    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);
  }

} // Errors

} // end namespace