Boogie: Renaming core sources in preparation for port commit

*The deletion part of the rename did not occur

1 files changed, 0 insertions, 539 deletions

diff --git a/Source/Core/ResolutionContext.ssc b/Source/Core/ResolutionContext.ssc
deleted file mode 100644
index 10ff7d87..00000000
--- a/Source/Core/ResolutionContext.ssc
+++ /dev/null
@@ -1,539 +0,0 @@
-//-----------------------------------------------------------------------------

-//

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

-        }

-    }

-}