Did more refactoring.

6 files changed, 77 insertions, 39 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index baefd09a..38a83b12 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -296,7 +296,36 @@ namespace Microsoft.Boogie {
 

   public class Program : Absy {

     [Rep]

-    public List<Declaration/*!*/>/*!*/ TopLevelDeclarations;

+    private List<Declaration/*!*/>/*!*/ topLevelDeclarations;

+

+    public IEnumerable<Declaration> TopLevelDeclarations

+    {

+      get

+      {

+        return topLevelDeclarations;

+      }

+    }

+

+    public void AddTopLevelDeclaration(Declaration decl)

+    {

+      topLevelDeclarations.Add(decl);

+    }

+

+    public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)

+    {

+      topLevelDeclarations.AddRange(decls);

+    }

+

+    public void RemoveTopLevelDeclarations(Predicate<Declaration> match)

+    {

+      topLevelDeclarations.RemoveAll(match);

+    }

+

+    public void ClearTopLevelDeclarations()

+    {

+      topLevelDeclarations.Clear();

+    }

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));

@@ -306,13 +335,13 @@ namespace Microsoft.Boogie {
 

     public Program()

       : base(Token.NoToken) {

-      this.TopLevelDeclarations = new List<Declaration>();

+      this.topLevelDeclarations = new List<Declaration>();

     }

 

     public void Emit(TokenTextWriter stream) {

       Contract.Requires(stream != null);

       stream.SetToken(this);

-      this.TopLevelDeclarations.Emit(stream);

+      this.topLevelDeclarations.Emit(stream);

     }

 

     public void ProcessDatatypeConstructors() {

@@ -329,17 +358,18 @@ namespace Microsoft.Boogie {
         constructors.Add(func.Name, constructor);

         prunedTopLevelDeclarations.Add(constructor);

       }

-      TopLevelDeclarations = prunedTopLevelDeclarations;

+      ClearTopLevelDeclarations();

+      AddTopLevelDeclarations(prunedTopLevelDeclarations);

     

       foreach (DatatypeConstructor f in constructors.Values) {

         for (int i = 0; i < f.InParams.Count; i++) {

           DatatypeSelector selector = new DatatypeSelector(f, i);

           f.selectors.Add(selector);

-          TopLevelDeclarations.Add(selector);

+          AddTopLevelDeclaration(selector);

         }

         DatatypeMembership membership = new DatatypeMembership(f);

         f.membership = membership;

-        TopLevelDeclarations.Add(membership);

+        AddTopLevelDeclaration(membership);

       }

     }

 

@@ -385,7 +415,8 @@ namespace Microsoft.Boogie {
         }

         prunedTopLevelDecls.Add(d);

       }

-      TopLevelDeclarations = prunedTopLevelDecls;

+      ClearTopLevelDeclarations();

+      AddTopLevelDeclarations(prunedTopLevelDecls);

 

       foreach (var v in Variables) {

         v.ResolveWhere(rc);

@@ -1067,8 +1098,8 @@ namespace Microsoft.Boogie {
         foreach (Implementation/*!*/ loopImpl in loopImpls)

         {

             Contract.Assert(loopImpl != null);

-            TopLevelDeclarations.Add(loopImpl);

-            TopLevelDeclarations.Add(loopImpl.Proc);

+            AddTopLevelDeclaration(loopImpl);

+            AddTopLevelDeclaration(loopImpl.Proc);

         }

         return fullMap;

     }

@@ -1098,7 +1129,7 @@ namespace Microsoft.Boogie {
       invariantGenerationCounter++;

       ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });

       ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) });

-      TopLevelDeclarations.Add(ExistentialBooleanConstant);

+      AddTopLevelDeclaration(ExistentialBooleanConstant);

       return ExistentialBooleanConstant;

     }

 

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index e954944f..644a5d3d 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -31,7 +31,7 @@ readonly StructuredCmd/*!*/ dummyStructuredCmd;
 ///Returns the number of parsing errors encountered.  If 0, "program" returns as

 ///the parsed program.

 ///</summary>

-public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {

   Contract.Requires(filename != null);

   Contract.Requires(cce.NonNullElements(defines,true));

 

@@ -41,25 +41,25 @@ public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/>
 

   if (filename == "stdin.bpl") {

     var s = ParserHelper.Fill(Console.In, defines);

-    return Parse(s, filename, out program);

+    return Parse(s, filename, out program, useBaseName);

   } else {

     FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);

     var s = ParserHelper.Fill(stream, defines);

-    var ret = Parse(s, filename, out program);

+    var ret = Parse(s, filename, out program, useBaseName);

     stream.Close();

     return ret;

   }

 }

 

 

-public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {

+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {

   Contract.Requires(s != null);

   Contract.Requires(filename != null);

 

   byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));

   MemoryStream ms = new MemoryStream(buffer,false);

   Errors errors = new Errors();

-  Scanner scanner = new Scanner(ms, errors, filename);

+  Scanner scanner = new Scanner(ms, errors, filename, useBaseName);

 

   Parser parser = new Parser(scanner, errors, false);

   parser.Parse();

@@ -168,31 +168,31 @@ BoogiePL
   .)

   { Consts<out vs>             (. foreach(Bpl.Variable/*!*/ v in vs){

                                     Contract.Assert(v != null);

-                                    Pgm.TopLevelDeclarations.Add(v);

+                                    Pgm.AddTopLevelDeclaration(v);

                                   }

                                .)

   | Function<out ds>           (. foreach(Bpl.Declaration/*!*/ d in ds){

                                     Contract.Assert(d != null);

-                                    Pgm.TopLevelDeclarations.Add(d);

+                                    Pgm.AddTopLevelDeclaration(d);

                                   }

                                .)

-  | Axiom<out ax>              (. Pgm.TopLevelDeclarations.Add(ax); .)

+  | Axiom<out ax>              (. Pgm.AddTopLevelDeclaration(ax); .)

   | UserDefinedTypes<out ts>   (. foreach(Declaration/*!*/ td in ts){

                                     Contract.Assert(td != null);

-                                    Pgm.TopLevelDeclarations.Add(td);

+                                    Pgm.AddTopLevelDeclaration(td);

                                   }

                                .)

   | GlobalVars<out vs>         (. foreach(Bpl.Variable/*!*/ v in vs){

                                     Contract.Assert(v != null);

-                                    Pgm.TopLevelDeclarations.Add(v);

+                                    Pgm.AddTopLevelDeclaration(v);

                                   }

                                .)

-  | Procedure<out pr, out im>  (. Pgm.TopLevelDeclarations.Add(pr);

+  | Procedure<out pr, out im>  (. Pgm.AddTopLevelDeclaration(pr);

                                    if (im != null) {

-                                     Pgm.TopLevelDeclarations.Add(im);

+                                     Pgm.AddTopLevelDeclaration(im);

                                    }

                                .)

-  | Implementation<out nnim>   (. Pgm.TopLevelDeclarations.Add(nnim); .)

+  | Implementation<out nnim>   (. Pgm.AddTopLevelDeclaration(nnim); .)

   }

   EOF

   .

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index 45c68fdd..603f7e72 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -44,10 +44,10 @@ namespace Microsoft.Boogie {
 

       Desugar(prog, out axioms, out functions);

       foreach (var f in functions) {

-        prog.TopLevelDeclarations.Add(f);

+        prog.AddTopLevelDeclaration(f);

       }

       foreach (var a in axioms) {

-        prog.TopLevelDeclarations.Add(new Axiom(a.tok, a));

+        prog.AddTopLevelDeclaration(new Axiom(a.tok, a));

       }

     }

 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 2149e12c..25be7f27 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -12,6 +12,8 @@ using Bpl = Microsoft.Boogie;
 using System;

 using System.Diagnostics.Contracts;

 

+namespace Microsoft.Boogie {

+

 

 

 public class Parser {

@@ -218,7 +220,7 @@ private class BvBounds : Expr {
 				Consts(out vs);

 				foreach(Bpl.Variable/*!*/ v in vs){

 				 Contract.Assert(v != null);

-				 Pgm.TopLevelDeclarations.Add(v);

+				 Pgm.AddTopLevelDeclaration(v);

 				}

 				

 				break;

@@ -227,21 +229,21 @@ private class BvBounds : Expr {
 				Function(out ds);

 				foreach(Bpl.Declaration/*!*/ d in ds){

 				 Contract.Assert(d != null);

-				 Pgm.TopLevelDeclarations.Add(d);

+				 Pgm.AddTopLevelDeclaration(d);

 				}

 				

 				break;

 			}

 			case 29: {

 				Axiom(out ax);

-				Pgm.TopLevelDeclarations.Add(ax); 

+				Pgm.AddTopLevelDeclaration(ax); 

 				break;

 			}

 			case 30: {

 				UserDefinedTypes(out ts);

 				foreach(Declaration/*!*/ td in ts){

 				 Contract.Assert(td != null);

-				 Pgm.TopLevelDeclarations.Add(td);

+				 Pgm.AddTopLevelDeclaration(td);

 				}

 				

 				break;

@@ -250,23 +252,23 @@ private class BvBounds : Expr {
 				GlobalVars(out vs);

 				foreach(Bpl.Variable/*!*/ v in vs){

 				 Contract.Assert(v != null);

-				 Pgm.TopLevelDeclarations.Add(v);

+				 Pgm.AddTopLevelDeclaration(v);

 				}

 				

 				break;

 			}

 			case 32: {

 				Procedure(out pr, out im);

-				Pgm.TopLevelDeclarations.Add(pr);

+				Pgm.AddTopLevelDeclaration(pr);

 				if (im != null) {

-				  Pgm.TopLevelDeclarations.Add(im);

+				  Pgm.AddTopLevelDeclaration(im);

 				}

 				

 				break;

 			}

 			case 33: {

 				Implementation(out nnim);

-				Pgm.TopLevelDeclarations.Add(nnim); 

+				Pgm.AddTopLevelDeclaration(nnim); 

 				break;

 			}

 			}

@@ -2286,3 +2288,4 @@ public class FatalError: Exception {
 }

 

 

+}
\ No newline at end of file
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index b050fcdd..5b5c0306 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -8,7 +8,7 @@ using System.Diagnostics.Contracts;
 using Microsoft.Boogie;

 

 

-

+namespace Microsoft.Boogie {

 

 //-----------------------------------------------------------------------------------

 // Buffer

@@ -296,7 +296,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName) : base() {

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName = false) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -313,7 +313,7 @@ public class Scanner {
 	}

 

 //	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName) : base() {

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName = false) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -325,7 +325,7 @@ public class Scanner {
 		Init();

 	}

 

-    private string GetBaseName(string fileName) {

+    string GetBaseName(string fileName) {

         return System.IO.Path.GetFileName(fileName); // Return basename

     }

 

@@ -807,3 +807,4 @@ public class Scanner {
 public delegate void ErrorProc(int n, string filename, int line, int col);

 

 

+}
\ No newline at end of file
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index d4be8ed4..3f3ad5ae 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -9,6 +9,7 @@
 

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

+using System.Linq;

 

 namespace Microsoft.Boogie {

   [ContractClass(typeof(VisitorContracts))]

@@ -429,7 +430,9 @@ namespace Microsoft.Boogie {
     public virtual Program VisitProgram(Program node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Program>() != null);

-      node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);

+      var decls = node.TopLevelDeclarations.ToList();

+      node.ClearTopLevelDeclarations();

+      node.AddTopLevelDeclarations(this.VisitDeclarationList(decls));

       return node;

     }

     public virtual QKeyValue VisitQKeyValue(QKeyValue node) {

@@ -979,7 +982,7 @@ namespace Microsoft.Boogie {
       public override Program VisitProgram(Program node)

       {

           Contract.Ensures(Contract.Result<Program>() == node);

-          this.VisitDeclarationList(node.TopLevelDeclarations);

+          this.VisitDeclarationList(node.TopLevelDeclarations.ToList());

           return node;

       }

       public override QKeyValue VisitQKeyValue(QKeyValue node) {