More refactoring: PureCollections.Sequence not used anymore.

7 files changed, 41 insertions, 128 deletions

diff --git a/Source/CodeContractsExtender/cce.cs b/Source/CodeContractsExtender/cce.cs
index 31de9a70..12163c40 100644
--- a/Source/CodeContractsExtender/cce.cs
+++ b/Source/CodeContractsExtender/cce.cs
@@ -124,21 +124,6 @@ public static class cce {
     public UnreachableException() {

     }

   }

-  //[Pure]

-  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

-  //  return true;

-  //}

-  //public static List<T> toList<T>(PureCollections.Sequence s) {

-  //  List<T> toRet = new List<T>();

-  //  foreach (T t in s.elems)

-  //    if(t!=null)

-  //    toRet.Add(t);

-  //  return toRet;

-  //}

-

-  //internal static bool NonNullElements(Set set) {

-  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

-  //}

 

 }

 

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index b29e050c..2a654298 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3321,7 +3321,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class IdentifierExprSeq : PureCollections.Sequence {

+  public sealed class IdentifierExprSeq : List<IdentifierExpr> {

     public IdentifierExprSeq(params IdentifierExpr[]/*!*/ args)

       : base(args) {

       Contract.Requires(args != null);

@@ -3381,7 +3381,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class ExprSeq : PureCollections.Sequence {

+  public sealed class ExprSeq : List<Expr> {

     public ExprSeq(params Expr[]/*!*/ args)

       : base(args) {

       Contract.Requires(args != null);

@@ -3399,10 +3399,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public new Expr Last() {

-      return (Expr)base.Last();

-    }

-

     public static ExprSeq operator +(ExprSeq a, ExprSeq b) {

       if (a == null)

         throw new ArgumentNullException("a");

@@ -3414,11 +3410,11 @@ namespace Microsoft.Boogie {
     public static ExprSeq Append(ExprSeq s, ExprSeq t) {

       Contract.Requires(t != null);

       Contract.Requires(s != null);

-      Expr[] n = new Expr[s.card + t.card];

-      for (int i = 0; i < s.card; i++)

+      Expr[] n = new Expr[s.Count + t.Count];

+      for (int i = 0; i < s.Count; i++)

         n[i] = s[i];

-      for (int i = 0; i < t.card; i++)

-        n[s.card + i] = t[i];

+      for (int i = 0; i < t.Count; i++)

+        n[s.Count + i] = t[i];

       return new ExprSeq(n);

     }

     public void Emit(TokenTextWriter stream) {

@@ -3443,34 +3439,11 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class TokenSeq : PureCollections.Sequence {

-    public TokenSeq(params Token[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public new Token this[int index] {

-      get {

-        return (Token)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

-  }

-

-  public sealed class StringSeq : PureCollections.Sequence {

+  public sealed class StringSeq : List<String> {

     public StringSeq(params string[]/*!*/ args)

       : base(args) {

       Contract.Requires(args != null);

     }

-    public new String this[int index] {

-      get {

-        return (String)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

     public void Emit(TokenTextWriter stream) {

       Contract.Requires(stream != null);

       string sep = "";

@@ -3483,7 +3456,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class BlockSeq : PureCollections.Sequence {

+  public sealed class BlockSeq : List<Block> {

     public BlockSeq(params Block[]/*!*/ args)

       : base(args) {

       Contract.Requires(args != null);

@@ -3492,15 +3465,6 @@ namespace Microsoft.Boogie {
       : base(blockSeq) {

       Contract.Requires(blockSeq != null);

     }

-

-    public new Block this[int index] {

-      get {

-        return (Block)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

   }

 

   public static class Emitter {

@@ -3520,19 +3484,7 @@ namespace Microsoft.Boogie {
       }

     }

   }

-  public sealed class DeclarationSeq : PureCollections.Sequence {

-    public DeclarationSeq(params string[] args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public new Declaration this[int index] {

-      get {

-        return (Declaration)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

+  public sealed class DeclarationSeq : List<Declaration> {

     public void Emit(TokenTextWriter stream) {

       Contract.Requires(stream != null);

       bool first = true;

@@ -3553,7 +3505,7 @@ namespace Microsoft.Boogie {
 

   #region Regular Expressions

   // a data structure to recover the "program structure" from the flow graph

-  public sealed class RESeq : PureCollections.Sequence {

+  public sealed class RESeq : List<RE> {

     public RESeq(params RE[] args)

       : base(args) {

       Contract.Requires(args != null);

@@ -3562,24 +3514,6 @@ namespace Microsoft.Boogie {
       : base(reSeq) {

       Contract.Requires(reSeq != null);

     }

-    public new RE this[int index] {

-      get {

-        return (RE)base[index];

-      }

-      set {

-        base[index] = value;

-      }

-    }

-    //        public void Emit(TokenTextWriter stream)

-    //        {

-    //            string sep = "";

-    //            foreach (RE e in this)

-    //            {

-    //                stream.Write(sep);

-    //                sep = ", ";

-    //                e.Emit(stream);

-    //            }

-    //        }

   }

   public abstract class RE : Cmd {

     public RE()

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index bfa43a1c..e4390634 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -12,6 +12,7 @@ namespace Microsoft.Boogie {
   using System.Collections;

   using System.Diagnostics;

   using System.Collections.Generic;

+  using System.Linq;

   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

   using Set = GSet<object>;

@@ -1755,15 +1756,8 @@ namespace Microsoft.Boogie {
         errorData = value;

       }

     }

-    public static List<T> toList<T>(PureCollections.Sequence seq) {

-      List<T> toRet = new List<T>();

-      foreach (T t in seq)

-        if (t != null)

-          toRet.Add(t);

-      return toRet;

-    }

     public CallCmd(IToken tok, string callee, ExprSeq ins, IdentifierExprSeq outs)

-      : this(tok, callee, toList<Expr>(ins), toList<IdentifierExpr>(outs)) {

+      : this(tok, callee, ins.ToList(), outs.ToList()) {

       Contract.Requires(outs != null);

       Contract.Requires(ins != null);

       Contract.Requires(callee != null);

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 8d81c025..fd09cd20 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2220,7 +2220,7 @@ namespace Microsoft.Boogie {
 

       if (withRhs) {

         stream.Write(" := ");

-        cce.NonNull(args.Last()).Emit(stream);

+        cce.NonNull(args.FindLast(Item => true)).Emit(stream);

       }

 

       stream.Write("]");

@@ -2412,9 +2412,9 @@ namespace Microsoft.Boogie {
         // error messages have already been created by MapSelect.Typecheck

         return null;

       }

-      Type rhsType = cce.NonNull(cce.NonNull(args.Last()).Type);

+      Type rhsType = cce.NonNull(cce.NonNull(args.FindLast(Item => true)).Type);

       if (!resultType.Unify(rhsType)) {

-        tc.Error(cce.NonNull(args.Last()).tok,

+        tc.Error(cce.NonNull(args.FindLast(Item => true)).tok,

                  "right-hand side in {0} with wrong type: {1} (expected: {2})",

                  opName, rhsType, resultType);

         return null;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 0d737dfe..6b064669 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -247,7 +247,7 @@ BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds>
 /*------------------------------------------------------------------------*/

 /* IdsType is used with const declarations */

 IdsType<out List<TypedIdent>/*!*/ tyds>

-= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty; .)

+= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids;  Bpl.Type/*!*/ ty; .)

   Idents<out ids> ":" Type<out ty>

   (. tyds = new List<TypedIdent>();

      foreach(Token/*!*/ id in ids){

@@ -283,7 +283,7 @@ AttributesIdsTypeWhere<. bool allowAttributes, bool allowWhereClauses, string co
 

 /* context is allowed to be null if allowWhereClauses is true */

 IdsTypeWhere<. bool allowWhereClauses, string context, System.Action<TypedIdent> action .>

-= (. TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; .)

+= (. List<IToken>/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; .)

   Idents<out ids> ":" Type<out ty>

   [ "where" Expression<out nne>  (. if (!allowWhereClauses) {

                                       this.SemErr("where clause not allowed on " + context);

@@ -357,7 +357,7 @@ MapType<out Bpl.Type/*!*/ ty>
   .

 

 TypeParams<out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams>

-= (.Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); TokenSeq/*!*/ typeParamToks; .)

+= (.Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks; .)

   "<"    (.  tok = t;  .)

     Idents<out typeParamToks>

   ">"

@@ -561,7 +561,7 @@ UserDefinedTypes<.out List<Declaration/*!*/>/*!*/ ts.>
   .

 

 UserDefinedType<out Declaration/*!*/ decl, QKeyValue kv>

-= (. Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; TokenSeq/*!*/ paramTokens = new TokenSeq ();

+= (. Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List<IToken>/*!*/ paramTokens = new List<IToken> ();

      Bpl.Type/*!*/ body = dummyType; bool synonym = false; .)

   Ident<out id>

   [ WhiteSpaceIdents<out paramTokens> ]

@@ -643,7 +643,7 @@ ProcSignature<bool allowWhereClausesOnFormals, out IToken/*!*/ name, out TypeVar
 

 

 Spec<List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post>

-= (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .)

+= (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; .)

   ( "modifies"

     [ Idents<out ms>        (. foreach(IToken/*!*/ m in ms){

                                  Contract.Assert(m != null);

@@ -749,7 +749,7 @@ StmtList<out StmtList/*!*/ stmtList>
 

 TransferCmd<out TransferCmd/*!*/ tc>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;

-     Token y;  TokenSeq/*!*/ xs;

+     Token y;  List<IToken>/*!*/ xs;

      StringSeq ss = new StringSeq();

   .)

   ( "goto"             (. y = t; .)

@@ -840,7 +840,7 @@ BreakCmd<out BreakCmd/*!*/ bcmd>
 LabelOrCmd<out Cmd c, out IToken label>

 /* ensures (c == null) != (label != null) */

 = (. IToken/*!*/ x; Expr/*!*/ e;

-     TokenSeq/*!*/ xs;

+     List<IToken>/*!*/ xs;

      IdentifierExprSeq ids;

      c = dummyCmd;  label = null;

      Cmd/*!*/ cn;

@@ -977,16 +977,16 @@ Proposition<out Expr/*!*/ e>
   .

 

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

-Idents<out TokenSeq/*!*/ xs>

-= (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); .)

+Idents<out List<IToken>/*!*/ xs>

+= (.Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); .)

   Ident<out id>                 (. xs.Add(id); .)

   { "," Ident<out id>           (. xs.Add(id); .)

   }

   .

 

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

-WhiteSpaceIdents<out TokenSeq/*!*/ xs>

-= (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); .)

+WhiteSpaceIdents<out List<IToken>/*!*/ xs>

+= (. Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); .)

   Ident<out id>                 (. xs.Add(id); .)

   { Ident<out id>               (. xs.Add(id); .)

   }

@@ -1315,7 +1315,7 @@ SpecBlock<out Block/*!*/ b>
 = (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;

      Cmd c;  IToken label;

      CmdSeq cs = new CmdSeq();

-     TokenSeq/*!*/ xs;

+     List<IToken>/*!*/ xs;

      StringSeq ss = new StringSeq();

      b = dummyBlock;

      Expr/*!*/ e;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index d2acca18..2996514f 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -464,11 +464,11 @@ namespace Microsoft.Boogie {
       IdentifierExprSeq havocVars = new IdentifierExprSeq();

       foreach (Variable v in locVars)

       {

-          havocVars.Add(codeCopier.Subst(v));

+          havocVars.Add((IdentifierExpr)codeCopier.Subst(v));

       }

       foreach (Variable v in impl.OutParams)

       {

-          havocVars.Add(codeCopier.Subst(v));

+          havocVars.Add((IdentifierExpr)codeCopier.Subst(v));

       }

       if (havocVars.Count > 0)

       {

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

 

 	void IdsType(out List<TypedIdent>/*!*/ tyds) {

-		Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty; 

+		Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); List<IToken>/*!*/ ids;  Bpl.Type/*!*/ ty; 

 		Idents(out ids);

 		Expect(11);

 		Type(out ty);

@@ -582,8 +582,8 @@ private class BvBounds : Expr {
 		

 	}

 

-	void Idents(out TokenSeq/*!*/ xs) {

-		Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); 

+	void Idents(out List<IToken>/*!*/ xs) {

+		Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); 

 		Ident(out id);

 		xs.Add(id); 

 		while (la.kind == 12) {

@@ -623,7 +623,7 @@ private class BvBounds : Expr {
 	}

 

 	void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent> action ) {

-		TokenSeq/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; 

+		List<IToken>/*!*/ ids;  Bpl.Type/*!*/ ty;  Expr wh = null;  Expr/*!*/ nne; 

 		Idents(out ids);

 		Expect(11);

 		Type(out ty);

@@ -726,7 +726,7 @@ private class BvBounds : Expr {
 	}

 

 	void TypeParams(out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams) {

-		Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); TokenSeq/*!*/ typeParamToks; 

+		Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); List<IToken>/*!*/ typeParamToks; 

 		Expect(19);

 		tok = t;  

 		Idents(out typeParamToks);

@@ -815,7 +815,7 @@ private class BvBounds : Expr {
 	}

 

 	void UserDefinedType(out Declaration/*!*/ decl, QKeyValue kv) {

-		Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; TokenSeq/*!*/ paramTokens = new TokenSeq ();

+		Contract.Ensures(Contract.ValueAtReturn(out decl) != null); IToken/*!*/ id; List<IToken>/*!*/ paramTokens = new List<IToken> ();

 		Bpl.Type/*!*/ body = dummyType; bool synonym = false; 

 		Ident(out id);

 		if (la.kind == 1) {

@@ -838,8 +838,8 @@ private class BvBounds : Expr {
 		

 	}

 

-	void WhiteSpaceIdents(out TokenSeq/*!*/ xs) {

-		Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq(); 

+	void WhiteSpaceIdents(out List<IToken>/*!*/ xs) {

+		Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new List<IToken>(); 

 		Ident(out id);

 		xs.Add(id); 

 		while (la.kind == 1) {

@@ -868,7 +868,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 	}

 

 	void Spec(List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post) {

-		Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; 

+		Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); List<IToken>/*!*/ ms; 

 		if (la.kind == 34) {

 			Get();

 			if (la.kind == 1) {

@@ -991,7 +991,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 

 	void LabelOrCmd(out Cmd c, out IToken label) {

 		IToken/*!*/ x; Expr/*!*/ e;

-		TokenSeq/*!*/ xs;

+		List<IToken>/*!*/ xs;

 		IdentifierExprSeq ids;

 		c = dummyCmd;  label = null;

 		Cmd/*!*/ cn;

@@ -1073,7 +1073,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) {
 

 	void TransferCmd(out TransferCmd/*!*/ tc) {

 		Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;

-		Token y;  TokenSeq/*!*/ xs;

+		Token y;  List<IToken>/*!*/ xs;

 		StringSeq ss = new StringSeq();

 		

 		if (la.kind == 38) {

@@ -1925,7 +1925,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;

 		Cmd c;  IToken label;

 		CmdSeq cs = new CmdSeq();

-		TokenSeq/*!*/ xs;

+		List<IToken>/*!*/ xs;

 		StringSeq ss = new StringSeq();

 		b = dummyBlock;

 		Expr/*!*/ e;