All ...Seq classes now gone

2 files changed, 7 insertions, 18 deletions

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index f7860169..a25781af 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -40,7 +40,7 @@ namespace Microsoft.Boogie.TypeErasure {
                                    new TypedIdent(Token.NoToken, "res",

                                                    cce.NonNull(types)[types.Length - 1]),

                                    false);

-      return new Function(Token.NoToken, name, ToSeq(typeParams), args, result);

+      return new Function(Token.NoToken, name, new List<TypeVariable>(typeParams), args, result);

     }

 

     public static Function BoogieFunction(string name, params Type[] types) {

@@ -80,7 +80,7 @@ namespace Microsoft.Boogie.TypeErasure {
       return new List<T>(args);

     }

 

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

+    public static List<TypeVariable/*!*/>/*!*/ ToList(List<TypeVariable> seq) {

       Contract.Requires(seq != null);

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

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

@@ -91,17 +91,6 @@ namespace Microsoft.Boogie.TypeErasure {
       return res;

     }

 

-    public static TypeVariableSeq ToSeq(List<TypeVariable/*!*/>/*!*/ list) {

-      Contract.Requires(cce.NonNullElements(list));

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

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

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

-        Contract.Assert(var != null);

-        res.Add(var);

-      }

-      return res;

-    }

-

     public static List<T>/*!*/ Intersect<T>(List<T> a, List<T> b) {

       Contract.Requires(b != null);

       Contract.Requires(a != null);

@@ -991,7 +980,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, List<Type> instantiations) {

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

       Contract.Requires(instantiations != null);

       Contract.Requires(boundTypeParams != null);

       Contract.Requires(rawType != null);

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index c78d7fba..c6b5eee6 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -338,14 +338,14 @@ namespace Microsoft.Boogie.TypeErasure
 

     // distinguish between implicit and explicit type parameters

     internal static void SeparateTypeParams(List<Type/*!*/>/*!*/ valueArgumentTypes,

-                                            TypeVariableSeq/*!*/ allTypeParams,

+                                            List<TypeVariable>/*!*/ allTypeParams,

                                             out List<TypeVariable/*!*/>/*!*/ implicitParams,

                                             out List<TypeVariable/*!*/>/*!*/ explicitParams) {

       Contract.Requires(cce.NonNullElements(valueArgumentTypes));

       Contract.Requires(allTypeParams != null);

       Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out implicitParams)));

       Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out explicitParams)));

-      TypeVariableSeq/*!*/ varsInInParamTypes = new TypeVariableSeq();

+      List<TypeVariable>/*!*/ varsInInParamTypes = new List<TypeVariable>();

       foreach (Type/*!*/ t in valueArgumentTypes) {

         Contract.Assert(t != null);

         varsInInParamTypes.AppendWithoutDups(t.FreeVariables);

@@ -679,7 +679,7 @@ namespace Microsoft.Boogie.TypeErasure
       // parameters are split into the implicit parameters, and into the parameters

       // that have to be given explicitly

       TypeAxiomBuilderPremisses.SeparateTypeParams(originalInTypes,

-                                                   HelperFuns.ToSeq(originalTypeParams),

+                                                   new List<TypeVariable>(originalTypeParams),

                                                    out implicitTypeParams,

                                                    out explicitTypeParams);

 

@@ -1318,7 +1318,7 @@ namespace Microsoft.Boogie.TypeErasure
       return HandleFunctionOp(untypedFun.Fun, typeArgs, node, bindings);

     }

 

-    private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, TypeVariableSeq allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams) {

+    private List<Type/*!*/>/*!*/ ExtractTypeArgs(VCExprNAry node, List<TypeVariable> allTypeParams, List<TypeVariable/*!*/>/*!*/ explicitTypeParams) {

       Contract.Requires(allTypeParams != null);

       Contract.Requires(node != null);

       Contract.Requires(cce.NonNullElements(explicitTypeParams));