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 -->namespace {

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)]
-->declarations

  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();
-->initialization
  }
  
  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;
      }
    }
  }
  
-->comment
  
  static void CheckLiteral() {
    switch (t.val) {
-->literals
    }
  }

  public static Token/*!*/ Scan() {
    while (ignore[ch]) { NextCh(); }
-->scan1
    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
-->scan2
    }
    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
$$$