From 5664c5e30f16b74eae4cdcb0b9ba65d5b030c815 Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 22 Jul 2013 10:54:53 +0100
Subject: Refactoring of VariableSeq and TypeSeq

---
 Source/VCExpr/TypeErasure.cs          | 6 +++---
 Source/VCExpr/TypeErasureArguments.cs | 2 +-
 Source/VCExpr/TypeErasurePremisses.cs | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'Source/VCExpr')

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 9d366c9f..c4a54300 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -469,7 +469,7 @@ namespace Microsoft.Boogie.TypeErasure {
         //
         CtorType ctype = type.AsCtor;
         Function/*!*/ repr = GetTypeCtorRepr(ctype.Decl);
-        List<VCExpr/*!*/>/*!*/ args = new List<VCExpr/*!*/>(ctype.Arguments.Length);
+        List<VCExpr/*!*/>/*!*/ args = new List<VCExpr/*!*/>(ctype.Arguments.Count);
         foreach (Type/*!*/ t in ctype.Arguments) {
           Contract.Assert(t != null);
           args.Add(Type2Term(t, varMapping));
@@ -970,7 +970,7 @@ namespace Microsoft.Boogie.TypeErasure {
       MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations);
 
       MapTypeClassRepresentation repr = GetClassRepresentation(abstraction);
-      Contract.Assume(repr.RepresentingType.Arity == instantiations.Length);
+      Contract.Assume(repr.RepresentingType.Arity == instantiations.Count);
       return new CtorType(Token.NoToken, repr.RepresentingType, instantiations);
     }
 
@@ -1004,7 +1004,7 @@ namespace Microsoft.Boogie.TypeErasure {
         // Bingo!
         // if the type does not contain any bound variables, we can simply
         // replace it with a type variable
-        TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Length);
+        TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Count);
         Contract.Assume(!boundTypeParams.Has(abstractionVar));
         instantiations.Add(rawType);
         return abstractionVar;
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 57218a73..49c7fe8e 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -180,7 +180,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
       int typeParamNum = abstractedType.FreeVariables.Length +
                          abstractedType.TypeParameters.Length;
 
-      int arity = typeParamNum + abstractedType.Arguments.Length;
+      int arity = typeParamNum + abstractedType.Arguments.Count;
 
       Type/*!*/[]/*!*/ selectTypes = new Type/*!*/ [arity + 2];
       Type/*!*/[]/*!*/ storeTypes = new Type/*!*/ [arity + 3];
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index df14eb01..44eb7dbb 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -307,11 +307,11 @@ namespace Microsoft.Boogie.TypeErasure
         // nothing
       } else if (completeType.IsCtor) {
         CtorType/*!*/ ctorType = completeType.AsCtor;
-        if (ctorType.Arguments.Length > 0) {
+        if (ctorType.Arguments.Count > 0) {
           // otherwise there are no chances of extracting any
           // instantiations from this type
           TypeCtorRepr repr = GetTypeCtorReprStruct(ctorType.Decl);
-          for (int i = 0; i < ctorType.Arguments.Length; ++i) {
+          for (int i = 0; i < ctorType.Arguments.Count; ++i) {
             VCExpr/*!*/ newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm);
             Contract.Assert(newInnerTerm != null);
             TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors);
@@ -644,7 +644,7 @@ namespace Microsoft.Boogie.TypeErasure
       typeParams.AddRange(abstractedType.TypeParameters.ToList());
       typeParams.AddRange(abstractedType.FreeVariables.ToList());
 
-      originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Length + 1);
+      originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);
       TypeSeq/*!*/ mapTypeParams = new TypeSeq();
       foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) {
         Contract.Assert(var != null);
-- 
cgit v1.2.3