Started to remove ...Seq classes

5 files changed, 25 insertions, 25 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 6509bc30..b3574b94 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -492,7 +492,7 @@ namespace Microsoft.Boogie.VCExprAST {
       return new VCQuantifierInfos(qid, node.SkolemId, false, node.Attributes);

     }

 

-    private string getQidNameFromQKeyValue(VariableSeq vars, QKeyValue attributes) {

+    private string getQidNameFromQKeyValue(List<Variable> vars, QKeyValue attributes) {

       Contract.Requires(vars != null);

       // Check for a 'qid, name' pair in keyvalues

       string qid = QKeyValue.FindStringAttribute(attributes, "qid");

@@ -872,9 +872,9 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

-    public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) {

+    public override List<Variable> VisitVariableSeq(List<Variable> variableSeq) {

       //Contract.Requires(variableSeq != null);

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

+      Contract.Ensures(Contract.Result<List<Variable>>() != null);

       Contract.Assert(false);

       throw new cce.UnreachableException();

     }

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index e6384e67..f7860169 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -31,7 +31,7 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Requires(Contract.ForAll(0, types.Length, i => types[i] != null));

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

 

-      VariableSeq args = new VariableSeq();

+      List<Variable> args = new List<Variable>();

       for (int i = 0; i < types.Length - 1; ++i)

         args.Add(new Formal(Token.NoToken,

                              new TypedIdent(Token.NoToken, "arg" + i, cce.NonNull(types[i])),

@@ -511,12 +511,12 @@ namespace Microsoft.Boogie.TypeErasure {
 

       TypeCtorDecl/*!*/ uDecl = new TypeCtorDecl(Token.NoToken, "U", 0);

       UDecl = uDecl;

-      Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new TypeSeq());

+      Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new List<Type>());

       U = u;

 

       TypeCtorDecl/*!*/ tDecl = new TypeCtorDecl(Token.NoToken, "T", 0);

       TDecl = tDecl;

-      Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new TypeSeq());

+      Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new List<Type>());

       T = t;

 

       Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int);

@@ -940,14 +940,14 @@ namespace Microsoft.Boogie.TypeErasure {
 

     ///////////////////////////////////////////////////////////////////////////

 

-    public Function Select(MapType rawType, out TypeSeq instantiations) {

+    public Function Select(MapType rawType, out List<Type> instantiations) {

       Contract.Requires((rawType != null));

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

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

       return AbstractAndGetRepresentation(rawType, out instantiations).Select;

     }

 

-    public Function Store(MapType rawType, out TypeSeq instantiations) {

+    public Function Store(MapType rawType, out List<Type> instantiations) {

       Contract.Requires((rawType != null));

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

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

@@ -955,10 +955,10 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     private MapTypeClassRepresentation

-            AbstractAndGetRepresentation(MapType rawType, out TypeSeq instantiations) {

+            AbstractAndGetRepresentation(MapType rawType, out List<Type> instantiations) {

       Contract.Requires((rawType != null));

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

-      instantiations = new TypeSeq();

+      instantiations = new List<Type>();

       MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);

       return GetClassRepresentation(abstraction);

     }

@@ -966,7 +966,7 @@ namespace Microsoft.Boogie.TypeErasure {
     public CtorType AbstractMapType(MapType rawType) {

       Contract.Requires(rawType != null);

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

-      TypeSeq/*!*/ instantiations = new TypeSeq();

+      List<Type>/*!*/ instantiations = new List<Type>();

       MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);

 

       MapTypeClassRepresentation repr = GetClassRepresentation(abstraction);

@@ -975,11 +975,11 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     // TODO: cache the result of this operation

-    protected MapType ThinOutMapType(MapType rawType, TypeSeq instantiations) {

+    protected MapType ThinOutMapType(MapType rawType, List<Type> instantiations) {

       Contract.Requires(instantiations != null);

       Contract.Requires(rawType != null);

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

-      TypeSeq/*!*/ newArguments = new TypeSeq();

+      List<Type>/*!*/ newArguments = new List<Type>();

       foreach (Type/*!*/ subtype in rawType.Arguments) {

         Contract.Assert(subtype != null);

         newArguments.Add(ThinOutType(subtype, rawType.TypeParameters,

@@ -991,7 +991,7 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables

-    private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, TypeSeq instantiations) {

+    private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, List<Type> instantiations) {

       Contract.Requires(instantiations != null);

       Contract.Requires(boundTypeParams != null);

       Contract.Requires(rawType != null);

@@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.TypeErasure {
         //

         // traverse the subtypes

         CtorType/*!*/ rawCtorType = rawType.AsCtor;

-        TypeSeq/*!*/ newArguments = new TypeSeq();

+        List<Type>/*!*/ newArguments = new List<Type>();

         foreach (Type/*!*/ subtype in rawCtorType.Arguments) {

           Contract.Assert(subtype != null);

           newArguments.Add(ThinOutType(subtype, boundTypeParams,

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 8e4bc7ab..00259ecd 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -627,7 +627,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
       if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

         MapType/*!*/ rawType = node[0].Type.AsMap;

         Contract.Assert(rawType != null);

-        TypeSeq/*!*/ abstractionInstantiation;

+        List<Type>/*!*/ abstractionInstantiation;

         Function/*!*/ select =

           AxBuilder.MapTypeAbstracter.Select(rawType, out abstractionInstantiation);

         Contract.Assert(abstractionInstantiation != null);

@@ -647,7 +647,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 

       if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) {

         MapType/*!*/ rawType = node[0].Type.AsMap;

-        TypeSeq/*!*/ abstractionInstantiation;

+        List<Type>/*!*/ abstractionInstantiation;

         Function/*!*/ store =

           AxBuilder.MapTypeAbstracter.Store(rawType, out abstractionInstantiation);

 

@@ -660,7 +660,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null);
 

     private OpTypesPair TypesPairForSelectStore(VCExprNAry/*!*/ node, Function/*!*/ untypedOp,

       // instantiation of the abstract map type parameters

-                                                TypeSeq/*!*/ abstractionInstantiation) {

+                                                List<Type>/*!*/ abstractionInstantiation) {

       Contract.Requires(node != null);

       Contract.Requires(untypedOp != null);

       Contract.Requires(abstractionInstantiation != null);

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index ec2d47bd..c78d7fba 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -646,7 +646,7 @@ namespace Microsoft.Boogie.TypeErasure
       typeParams.AddRange(abstractedType.FreeVariables.ToList());

 

       originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);

-      TypeSeq/*!*/ mapTypeParams = new TypeSeq();

+      List<Type>/*!*/ mapTypeParams = new List<Type>();

       foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {

         Contract.Assert(var != null);

         mapTypeParams.Add(var);

@@ -1271,7 +1271,7 @@ namespace Microsoft.Boogie.TypeErasure
 

       MapType/*!*/ mapType = node[0].Type.AsMap;

       Contract.Assert(mapType != null);

-      TypeSeq/*!*/ instantiations; // not used

+      List<Type>/*!*/ instantiations; // not used

       Function/*!*/ select =

         AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations);

       Contract.Assert(select != null);

@@ -1291,7 +1291,7 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Requires(bindings != null);

       Contract.Requires(node != null);

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

-      TypeSeq/*!*/ instantiations; // not used

+      List<Type>/*!*/ instantiations; // not used

       Function/*!*/ store =

         AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations);

       Contract.Assert(store != null);

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 3961f096..41f1e207 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -31,7 +31,7 @@ namespace Microsoft.Boogie {
       if (ControlFlowFunction == null) {

         Formal/*!*/ first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);

         Formal/*!*/ second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);

-        VariableSeq inputs = new VariableSeq();

+        List<Variable> inputs = new List<Variable>();

         inputs.Add(first);

         inputs.Add(second);

         Formal/*!*/ returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);

@@ -728,11 +728,11 @@ namespace Microsoft.Boogie.VCExprAST {
       return res;

     }

 

-    public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex) {

+    public static List<Type> ToTypeSeq(VCExpr[] exprs, int startIndex) {

       Contract.Requires(exprs != null);

       Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));

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

-      TypeSeq/*!*/ res = new TypeSeq();

+      Contract.Ensures(Contract.Result<List<Type>>() != null);

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

       for (int i = startIndex; i < exprs.Length; ++i)

         res.Add(cce.NonNull(exprs[i]).Type);

       return res;