//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.Boogie
{
    using System.Collections;
    using System.Collections.Generic;
    using System;
    using Microsoft.SpecSharp.Collections;
    using Microsoft.Contracts;

    public interface IErrorSink
    {
        void Error(IToken! tok, string! msg);
    }
    
    public class CheckingContext
    {
        // ------------------------------  Error counting  ------------------------------
        
        IErrorSink errorSink;
        int errors;
        
        public CheckingContext(IErrorSink errorSink)
        {
            this.errorSink = errorSink;
        }
        
        public int ErrorCount 
        {
            get { return errors; }
            set { errors = value; }
        }

        public void Error(Absy! subject, string! msg, params object[]! args) 
        {
            Error(subject.tok, msg, args);
        }

        public virtual void Error(IToken! tok, string! msg)
        {
            errors++;
            if (errorSink == null) {
                ConsoleColor col = Console.ForegroundColor;
                Console.ForegroundColor = ConsoleColor.Red;
                Console.WriteLine("{0}({1},{2}): Error: {3}",
                    tok.filename, tok.line, tok.col-1,
                    msg);
                Console.ForegroundColor = col;
            } else {
                errorSink.Error(tok, msg);
            }
        }

        private string! Format(string! msg, params object[] args) {
          if (System.Type.GetType("Mono.Runtime") != null) {  // MONO
            // something in mono seems to be broken so that calling
            // NamedDeclarations.ToString (and similar ToString methods)
            // causes a stack overflow. We therefore convert those to
            // strings by hand
            object[] fixedArgs = new object [((!)args).Length];
            for (int i = 0; i < args.Length; ++i) {
              if (args[i] is NamedDeclaration) {
                fixedArgs[i] = ((NamedDeclaration!)args[i]).Name;
              } else if (args[i] is Type) {
                System.IO.StringWriter buffer = new System.IO.StringWriter();
                using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
                  ((Type!)args[i]).Emit(stream);
                }
                fixedArgs[i] = buffer.ToString();
              } else if (args[i] is Expr) {
                System.IO.StringWriter buffer = new System.IO.StringWriter();
                using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
                  ((Expr!)args[i]).Emit(stream, 0, false);
                }
                fixedArgs[i] = buffer.ToString();
              } else {
                fixedArgs[i] = args[i];
              }
            }
            args = fixedArgs;
          }
          return string.Format(msg, args);
        }

        public void Error(IToken! tok, string! msg, params object[] args) 
        {
            Error(tok, Format(msg, args));
        }

        public void Warning(Absy! subject, string! msg, params object[]! args) 
        {
            Warning(subject.tok, msg, args);
        }

        public virtual void Warning(IToken! tok, string! msg)
        {
            // warnings are currently always written to the console
            ConsoleColor col = Console.ForegroundColor;
            Console.ForegroundColor = ConsoleColor.DarkYellow;
            Console.WriteLine("{0}({1},{2}): Warning: {3}",
                              tok.filename, tok.line, tok.col-1,
                              msg);
            Console.ForegroundColor = col;
        }

        public void Warning(IToken! tok, string! msg, params object[] args) 
        {
            Warning(tok, Format(msg, args));
        }
    }

    public class ResolutionContext : CheckingContext
    {
        public ResolutionContext(IErrorSink errorSink) 
        {
            base(errorSink);
        }
        
        // ------------------------------  Boogie 2 Types  -------------------------

        // user-defined types, which can be either TypeCtorDecl or TypeSynonymDecl
        Hashtable /*string->NamedDeclaration*/! types = new Hashtable /*string->NamedDeclaration*/ ();

        /// <summary>
        /// Checks if name coincides with the name of a bitvector type.  If so, reports an error and
        /// returns true; otherwise, returns false.
        /// </summary>
        private bool CheckBvNameClashes(Absy! absy, string! name) {
            if (name.StartsWith("bv") && name.Length > 2) {
                for (int i = 2; i < name.Length; ++i)
                    if (!char.IsDigit(name[i])) return false;
                Error(absy, "type name: {0} is registered for bitvectors", name);
                return true;
            }
            return false;
        }

        public void AddType(NamedDeclaration! td) 
        {
            assert (td is TypeCtorDecl) || (td is TypeSynonymDecl);

            string! name = (!)td.Name;
            if (CheckBvNameClashes(td, name))
                return;  // error has already been reported

            if (types[name] != null) 
            {
                Error(td, "more than one declaration of type name: {0}", name);
            } 
            else 
            {
                types.Add(name, td);
            }
        }

        /// <summary>
        /// Returns the declaration of the named type, or null if
        /// no such type is declared. Also return null if the type
        /// declared with the given name is not a constructor but a
        /// type synonym
        /// </summary>
        /// <param name="name"></param>
        /// <returns></returns>
        public TypeCtorDecl LookUpType(string! name) 
        {
          return types[name] as TypeCtorDecl;
        }
        
        public TypeSynonymDecl LookUpTypeSynonym(string! name) 
        {
            return types[name] as TypeSynonymDecl;
        }
        
        // ------------------------------  Boogie 2 Type Binders  ------------------------------

        List<TypeVariable!>! typeBinders = new List<TypeVariable!>(5);
        
        public void AddTypeBinder(TypeVariable! td) {
          if (CheckBvNameClashes(td, td.Name)) {
            return;
          }
          if (types.ContainsKey(td.Name)) {
            Error(td, "name is already reserved for type constructor: {0}", td.Name);
            return;
          }
          for (int i = 0; i < typeBinders.Count; i++) {
            if (typeBinders[i].Name == td.Name) {
              Error(td, "more than one declaration of type variable: {0}", td.Name);
              return;
            }
          }
          typeBinders.Add(td);
        }
        
        public int TypeBinderState {
          get { return typeBinders.Count; }
          set { typeBinders.RemoveRange(value, typeBinders.Count - value); }
        }
        
        /// <summary>
        /// Returns the declaration of the named type binder, or null if
        /// no such binder is declared.
        /// </summary>
        public TypeVariable LookUpTypeBinder(string! name) 
        {
          for (int i = typeBinders.Count; 0 <= --i; ) {
            TypeVariable! td = typeBinders[i];
            if (td.Name == name) {
              return td;
            }
          }
          return null;  // not present
        }
        
        // ------------------------------  Types  ------------------------------

        // user-defined types
  //      Hashtable /*string->TypeDecl*/! types = new Hashtable /*string->TypeDecl*/ ();
/*
        public void AddType(TypeDecl! td) 
        {
            string! name = (!)td.Name;

            if (name.StartsWith("bv") && name.Length > 2) {
                bool isBv = true;
                for (int i = 2; i < name.Length; ++i)
                    if (!char.IsDigit(name[i])) isBv = false;
                if (isBv)
                    Error(td, "type name: {0} is registered for bitvectors", name);
            }

            if (types[name] != null) 
            {
                Error(td, "more than one declaration of type name: {0}", name);
            } 
            else 
            {
                types.Add(name, td);
            }
        }
*/
        /// <summary>
        /// Returns the declaration of the named type, or null if
        /// no such type is declared.
        /// </summary>
        /// <param name="name"></param>
        /// <returns></returns>
    /*    public TypeDecl LookUpType(string! name) 
        {
            return (TypeDecl)types[name];
        }
      */  
        // ------------------------------  Type Binders  ------------------------------
/*
        List<TypeBinderDecl!>! typeBinders = new List<TypeBinderDecl!>(5);
        
        public void AddTypeBinder(TypeBinderDecl! td) {
          for (int i = 0; i < typeBinders.Count; i++) {
            if (typeBinders[i].Name == td.Name) {
              Error(td, "more than one declaration of type binder name: {0}", td.Name);
              return;
            }
          }
          typeBinders.Add(td);
        }
        
        public int TypeBinderState {
          get { return typeBinders.Count; }
          set { typeBinders.RemoveRange(value, typeBinders.Count - value); }
        }
        
        /// <summary>
        /// Returns the declaration of the named type binder, or null if
        /// no such binder is declared.
        /// </summary>
        public TypeDecl LookUpTypeBinder(string! name) 
        {
          for (int i = typeBinders.Count; 0 <= --i; ) {
            TypeBinderDecl td = typeBinders[i];
            if (td.Name == name) {
              return td;
            }
          }
          return null;  // not present
        }
  */      
        // ------------------------------  Variables  ------------------------------

        class VarContextNode 
        {
            public readonly Hashtable /*string->Variable*/! VarSymbols = new Hashtable /*string->Variable*/();
            public /*maybe null*/ VarContextNode ParentContext;
            public readonly bool Opaque;

            public VarContextNode(/*maybe null*/ VarContextNode parentContext, bool opaque) 
            {
                ParentContext = parentContext;
                Opaque = opaque;
            }
        }

        // symbolic constants, global variables, local variables, formals, expression-bound variables
        VarContextNode! varContext = new VarContextNode(null, false);

        /// <summary>
        /// Adds a variable context.
        /// </summary>
        public void PushVarContext() 
        {
            varContext = new VarContextNode(varContext, false);
        }

        /// <summary>
        /// Adds an opaque variable context, that is, one that blocks all previously pushed contexts.
        /// </summary>
        public void PushOpaqueVarContext()
        {
            varContext = new VarContextNode(varContext, true);
        }
        
        /// <summary>
        /// Requires there to be more than one variable context.
        /// </summary>
        public void PopVarContext() 
        {
            assert varContext.ParentContext != null;
            varContext = varContext.ParentContext;
        }

        public void AddVariable(Variable! var, bool global) 
        {
            if (FindVariable((!)var.Name, !global) != null) 
            {
                Error(var, "more than one declaration of variable name: {0}", var.Name);
            } 
            else 
            {
                varContext.VarSymbols.Add(var.Name, var);
            }
        }

        /// <summary>
        /// Returns the declaration of the named variable, or null if
        /// no such variable is declared.
        /// </summary>
        /// <param name="name"></param>
        /// <returns></returns>
        public Variable LookUpVariable(string! name) 
        {
            return FindVariable(name, false);
        }

        Variable FindVariable(string! name, bool ignoreTopLevelVars) 
        {
          VarContextNode c = varContext;
          bool lookOnlyForConstants = false;
          do {
            if (ignoreTopLevelVars && c.ParentContext == null) {
              // this is the top level and we're asked to ignore the top level; hence, we're done
              break;
            }

            Variable var = (Variable)c.VarSymbols[name];
            if (var != null && (!lookOnlyForConstants || var is Constant)) {
              return var;
            }
            // not at this level
            
            if (c.Opaque) {
              // from here on, only constants can be looked up
              lookOnlyForConstants = true;
            }
            c = c.ParentContext;
          } while (c != null);
          
          // not present in the relevant levels
          return null;
        }

        // ------------------------------  Functions/Procedures  ------------------------------

        // uninterpreted function symbols, procedures
        Hashtable /*string->DeclWithFormals*/! funcdures = new Hashtable /*string->DeclWithFormals*/ ();

        public void AddProcedure(DeclWithFormals! proc) 
        {
            if (funcdures[(!)proc.Name] != null) 
            {
                Error(proc, "more than one declaration of function/procedure name: {0}", proc.Name);
            } 
            else 
            {
                funcdures.Add(proc.Name, proc);
            }
        }

        /// <summary>
        /// Returns the declaration of the named function/procedure, or null if
        /// no such function or procedure is declared.
        /// </summary>
        /// <param name="name"></param>
        /// <returns></returns>
        public DeclWithFormals LookUpProcedure(string! name) 
        {
            return (DeclWithFormals)funcdures[name];
        }

        // ------------------------------  Blocks  ------------------------------

        class ProcedureContext {
            public readonly Hashtable! /*string->Block!*/ Blocks;
            public readonly ProcedureContext Next;
            public ProcedureContext(ProcedureContext next) {
                Blocks = new Hashtable /*string->Block!*/ ();
                Next = next;
            }
        }
        /*maybe null*/ ProcedureContext procedureContext;  // stack of procedure contexts
        public bool HasProcedureContext {
          get { return procedureContext != null; }
        }

        /// <summary>
        /// Pushes a new procedure context.
        /// </summary>
        public void PushProcedureContext() 
          ensures HasProcedureContext;
        {
          procedureContext = new ProcedureContext(procedureContext);
        }

        /// <summary>
        /// Requires there to be a procedure context.  Pops it.
        /// </summary>
        public void PopProcedureContext() 
          requires HasProcedureContext;
        {
          assert procedureContext != null;  // follows from precondition
          procedureContext = procedureContext.Next;
        }

        /// <summary>
        /// Requires there to be a procedure context.
        /// </summary>
        /// <param name="block"></param>
        public void AddBlock(Block! block) 
          requires HasProcedureContext;
        {
            assert procedureContext != null;  // follows from precondition
            Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;
            if (blocks[block.Label] != null) 
            {
                Error(block, "more than one declaration of block name: {0}", block.Label);
            } 
            else 
            {
                blocks.Add(block.Label, block);
            }
        }

        /// <summary>
        /// Requires there to be a procedure context.
        /// Returns the declaration of the named block, or null if
        /// no such block is declared.
        /// </summary>
        /// <param name="name"></param>
        /// <returns></returns>
        public Block LookUpBlock(string! name)
          requires HasProcedureContext;
        {
            assert procedureContext != null;  // follows from precondition
            Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;
            return (Block)blocks[name];
        }

        // ------------------------------  Flags  ------------------------------

        public enum State { StateLess, Single, Two }
        State stateMode = State.Single;

        /// <summary>
        /// To increase our confidence in that the caller knows what it's doing, we only allow
        /// the state mode to be changed in and out of the State.Single mode.
        /// </summary>
        public State StateMode {
          get {
            return stateMode;
          }
          set {
            assert value != stateMode;
            assert stateMode == State.Single || value == State.Single;
            expose (this) {
              stateMode = value;
            }
          }
        }
        
        bool triggerMode = false;

        /// <summary>
        /// Setting TriggerMode is allowed only if the setting has the effect of toggling the
        /// boolean.  That is, TriggerMode can be set to true only if it previously was false,
        /// and TriggerMode can be set to false only if it previously was true.
        /// </summary>
        public bool TriggerMode 
        {
            get 
            {
                return triggerMode;
            }
            set 
            {
                assert triggerMode != value;
                expose (this) {
                    triggerMode = value;
                }
            }
        }
    }

    public class TypecheckingContext : CheckingContext 
    {
        public IdentifierExprSeq Frame;  // used in checking the assignment targets of implementation bodies

        public TypecheckingContext(IErrorSink errorSink) 
        {
            base(errorSink);
        }
        
        public bool InFrame(Variable! v)
            requires Frame != null;
        {
            return exists{IdentifierExpr! ie in Frame; ie.Decl == v};
        }
    }
}