Refactoring of VariableSeq and TypeSeq

3 files changed, 7 insertions, 7 deletions

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);