From 350d32403f7441df525f871f3853ca9b660211fe Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 22 Jul 2013 23:03:55 +0100
Subject: All ...Seq classes now gone

---
 Source/VCExpr/TypeErasure.cs          | 17 +++--------------
 Source/VCExpr/TypeErasurePremisses.cs |  8 ++++----
 2 files changed, 7 insertions(+), 18 deletions(-)

(limited to 'Source/VCExpr')

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));
-- 
cgit v1.2.3