More refactoring

6 files changed, 35 insertions, 67 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 2a654298..6b0fcdb3 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3209,6 +3209,12 @@ namespace Microsoft.Boogie {
   // Generic Sequences

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

 

+  public static class ListFactory {

+    public static List<T> MakeList<T>(params T[]/*!*/ args) {

+      return new List<T>(args);

+    }

+  }

+

   public sealed class VariableSeq : List<Variable> {

     public VariableSeq(params Variable[]/*!*/ args)

       : base(args) {

@@ -3256,15 +3262,6 @@ namespace Microsoft.Boogie {
       : base(varSeq) {

       Contract.Requires(varSeq != null);

     }

-    public List<Type/*!*/>/*!*/ ToList() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));

-      List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Count);

-      foreach (Type/*!*/ t in this) {

-        Contract.Assert(t != null);

-        res.Add(t);

-      }

-      return res;

-    }

     public void Emit(TokenTextWriter stream, string separator) {

       Contract.Requires(separator != null);

       Contract.Requires(stream != null);

@@ -3310,15 +3307,6 @@ namespace Microsoft.Boogie {
         v.Emit(stream);

       }

     }

-    public List<TypeVariable/*!*/>/*!*/ ToList() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));

-      List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(Count);

-      foreach (TypeVariable/*!*/ var in this) {

-        Contract.Assert(var != null);

-        res.Add(var);

-      }

-      return res;

-    }

   }

 

   public sealed class IdentifierExprSeq : List<IdentifierExpr> {

@@ -3417,26 +3405,6 @@ namespace Microsoft.Boogie {
         n[s.Count + i] = t[i];

       return new ExprSeq(n);

     }

-    public void Emit(TokenTextWriter stream) {

-      Contract.Requires(stream != null);

-      string sep = "";

-      foreach (Expr/*!*/ e in this) {

-        Contract.Assert(e != null);

-        stream.Write(sep);

-        sep = ", ";

-        e.Emit(stream);

-      }

-    }

-    public TypeSeq/*!*/ ToTypeSeq {

-      get {

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

-

-        TypeSeq res = new TypeSeq();

-        foreach (Expr e in this)

-          res.Add(cce.NonNull(e).Type);

-        return res;

-      }

-    }

   }

 

   public sealed class StringSeq : List<String> {

@@ -3444,16 +3412,6 @@ namespace Microsoft.Boogie {
       : base(args) {

       Contract.Requires(args != null);

     }

-    public void Emit(TokenTextWriter stream) {

-      Contract.Requires(stream != null);

-      string sep = "";

-      foreach (string/*!*/ s in this) {

-        Contract.Assert(s != null);

-        stream.Write(sep);

-        sep = ", ";

-        stream.Write(s);

-      }

-    }

   }

 

   public sealed class BlockSeq : List<Block> {

@@ -3483,22 +3441,29 @@ namespace Microsoft.Boogie {
         d.Emit(stream, 0);

       }

     }

-  }

-  public sealed class DeclarationSeq : List<Declaration> {

-    public void Emit(TokenTextWriter stream) {

+

+    public static void Emit(this StringSeq ss, TokenTextWriter stream) {

       Contract.Requires(stream != null);

-      bool first = true;

-      foreach (Declaration d in this) {

-        if (d == null)

-          continue;

-        if (first) {

-          first = false;

-        } else {

-          stream.WriteLine();

-        }

-        d.Emit(stream, 0);

+      string sep = "";

+      foreach (string/*!*/ s in ss) {

+        Contract.Assert(s != null);

+        stream.Write(sep);

+        sep = ", ";

+        stream.Write(s);

       }

     }

+

+    public static void Emit(this ExprSeq ts, TokenTextWriter stream) {

+      Contract.Requires(stream != null);

+      string sep = "";

+      foreach (Expr/*!*/ e in ts) {

+        Contract.Assert(e != null);

+        stream.Write(sep);

+        sep = ", ";

+        e.Emit(stream);

+      }

+    }

+

   }

   #endregion

 

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 944bbe08..fe2b9a4c 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -11,6 +11,7 @@ namespace Microsoft.Boogie {
   using System;

   using System.Collections;

   using System.Diagnostics;

+  using System.Linq;

   using System.Collections.Generic;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 6b064669..219cb3e6 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -160,7 +160,7 @@ PRODUCTIONS
 /*------------------------------------------------------------------------*/

 BoogiePL

 = (. VariableSeq/*!*/ vs;

-     DeclarationSeq/*!*/ ds;

+     List<Declaration>/*!*/ ds;

      Axiom/*!*/ ax;

      List<Declaration/*!*/>/*!*/ ts;

      Procedure/*!*/ pr;

@@ -439,9 +439,9 @@ OrderSpec<.out bool ChildrenComplete, out List<ConstantParent/*!*/> Parents.>
   .

 

 /*------------------------------------------------------------------------*/

-Function<out DeclarationSeq/*!*/ ds>

+Function<out List<Declaration>/*!*/ ds>

 = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null);

-     ds = new DeclarationSeq(); IToken/*!*/ z;

+     ds = new List<Declaration>(); IToken/*!*/ z;

      IToken/*!*/ typeParamTok;

      var typeParams = new TypeVariableSeq();

      var arguments = new VariableSeq();

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index f6347b37..ed5b88ae 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -208,7 +208,7 @@ private class BvBounds : Expr {
 

 	void BoogiePL() {

 		VariableSeq/*!*/ vs;

-		DeclarationSeq/*!*/ ds;

+		List<Declaration>/*!*/ ds;

 		Axiom/*!*/ ax;

 		List<Declaration/*!*/>/*!*/ ts;

 		Procedure/*!*/ pr;

@@ -320,9 +320,9 @@ private class BvBounds : Expr {
 		Expect(8);

 	}

 

-	void Function(out DeclarationSeq/*!*/ ds) {

+	void Function(out List<Declaration>/*!*/ ds) {

 		Contract.Ensures(Contract.ValueAtReturn(out ds) != null);

-		ds = new DeclarationSeq(); IToken/*!*/ z;

+		ds = new List<Declaration>(); IToken/*!*/ z;

 		IToken/*!*/ typeParamTok;

 		var typeParams = new TypeVariableSeq();

 		var arguments = new VariableSeq();

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index c28d9b4c..d887a70f 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -8,6 +8,7 @@ using System.Text;
 using System.IO;

 using System.Collections;

 using System.Collections.Generic;

+using System.Linq;

 using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 1dd1cac9..67280bea 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -9,6 +9,7 @@ using System.IO;
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

+using System.Linq;

 using Microsoft.Basetypes;

 

 // Some visitor skeletons for the VCExpression AST