Refactoring of TypeVariableSeq

5 files changed, 17 insertions, 17 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 37bcda96..6273f056 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -1163,7 +1163,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

         // substitute the formals with the actual parameters in the body

         var tparms = app.Func.TypeParameters;

-        Contract.Assert(typeArgs.Count == tparms.Length);

+        Contract.Assert(typeArgs.Count == tparms.Count);

         for (int i = 0; i < typeArgs.Count; ++i)

           subst[tparms[i]] = typeArgs[i];

         SubstitutingVCExprVisitor/*!*/ substituter = new SubstitutingVCExprVisitor(Gen);

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 77e54945..48bb3354 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -83,7 +83,7 @@ namespace Microsoft.Boogie.TypeErasure {
     public static List<TypeVariable/*!*/>/*!*/ ToList(TypeVariableSeq seq) {

       Contract.Requires(seq != null);

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

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

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

       foreach (TypeVariable/*!*/ var in seq) {

         Contract.Assert(var != null);

         res.Add(var);

@@ -923,7 +923,7 @@ namespace Microsoft.Boogie.TypeErasure {
       if (!ClassRepresentations.TryGetValue(abstractedType, out res)) {

         int num = ClassRepresentations.Count;

         TypeCtorDecl/*!*/ synonym =

-          new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Length);

+          new TypeCtorDecl(Token.NoToken, "MapType" + num, abstractedType.FreeVariables.Count);

 

         Function/*!*/ select, store;

         GenSelectStoreFunctions(abstractedType, synonym, out select, out store);

@@ -1000,7 +1000,7 @@ namespace Microsoft.Boogie.TypeErasure {
       if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))

         return rawType;

 

-      if (Contract.ForAll(0, rawType.FreeVariables.Length, var => !boundTypeParams.Contains(rawType.FreeVariables[var]))) {

+      if (Contract.ForAll(0, rawType.FreeVariables.Count, var => !boundTypeParams.Contains(rawType.FreeVariables[var]))) {

         // Bingo!

         // if the type does not contain any bound variables, we can simply

         // replace it with a type variable

diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs
index 49c7fe8e..79a3286b 100644
--- a/Source/VCExpr/TypeErasureArguments.cs
+++ b/Source/VCExpr/TypeErasureArguments.cs
@@ -112,11 +112,11 @@ namespace Microsoft.Boogie.TypeErasure {
             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type)) {

           res = fun;

         } else {

-          Type[]/*!*/ types = new Type[fun.TypeParameters.Length + fun.InParams.Length + 1];

+          Type[]/*!*/ types = new Type[fun.TypeParameters.Count + fun.InParams.Length + 1];

 

           int i = 0;

           // the first arguments are the explicit type parameters

-          for (int j = 0; j < fun.TypeParameters.Length; ++j) {

+          for (int j = 0; j < fun.TypeParameters.Count; ++j) {

             types[i] = T;

             i = i + 1;

           }

@@ -177,8 +177,8 @@ Contract.Ensures(Contract.ValueAtReturn(out select) != null);
 Contract.Ensures(Contract.ValueAtReturn(out store) != null);

       Contract.Assert(synonym.Name != null);

       string/*!*/ baseName = synonym.Name;

-      int typeParamNum = abstractedType.FreeVariables.Length +

-                         abstractedType.TypeParameters.Length;

+      int typeParamNum = abstractedType.FreeVariables.Count +

+                         abstractedType.TypeParameters.Count;

 

       int arity = typeParamNum + abstractedType.Arguments.Count;

 

@@ -238,9 +238,9 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null);
         store.AddAttribute("builtin", "store");

       } else {

         AxBuilder.AddTypeAxiom(GenMapAxiom0(select, store,

-                 abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));

+                 abstractedType.TypeParameters.Count, abstractedType.FreeVariables.Count));

         AxBuilder.AddTypeAxiom(GenMapAxiom1(select, store,

-                 abstractedType.TypeParameters.Length, abstractedType.FreeVariables.Length));

+                 abstractedType.TypeParameters.Count, abstractedType.FreeVariables.Count));

       }

     }

 

diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs
index 12f8d7e3..c28d9b4c 100644
--- a/Source/VCExpr/TypeErasurePremisses.cs
+++ b/Source/VCExpr/TypeErasurePremisses.cs
@@ -350,8 +350,8 @@ namespace Microsoft.Boogie.TypeErasure
         varsInInParamTypes.AppendWithoutDups(t.FreeVariables);

       }

 

-      implicitParams = new List<TypeVariable/*!*/>(allTypeParams.Length);

-      explicitParams = new List<TypeVariable/*!*/>(allTypeParams.Length);

+      implicitParams = new List<TypeVariable/*!*/>(allTypeParams.Count);

+      explicitParams = new List<TypeVariable/*!*/>(allTypeParams.Count);

 

       foreach (TypeVariable/*!*/ var in allTypeParams) {

         Contract.Assert(var != null);

@@ -375,7 +375,7 @@ namespace Microsoft.Boogie.TypeErasure
         // not have to be changed

         if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&

             UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&

-            fun.TypeParameters.Length == 0) {

+            fun.TypeParameters.Count == 0) {

           res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());

         } else {

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

@@ -640,7 +640,7 @@ namespace Microsoft.Boogie.TypeErasure
       Contract.Ensures(Contract.ValueAtReturn(out mapTypeSynonym) != null);

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

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

-      typeParams = new List<TypeVariable/*!*/>(abstractedType.TypeParameters.Length + abstractedType.FreeVariables.Length);

+      typeParams = new List<TypeVariable/*!*/>(abstractedType.TypeParameters.Count + abstractedType.FreeVariables.Count);

       typeParams.AddRange(abstractedType.TypeParameters.ToList());

       typeParams.AddRange(abstractedType.FreeVariables.ToList());

 

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index f56b6978..90dcb2de 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -1436,7 +1436,7 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(cce.NonNullElements(args));

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

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

-      Contract.Assert(TypeParamArity == mapType.TypeParameters.Length);

+      Contract.Assert(TypeParamArity == mapType.TypeParameters.Count);

       IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();

       for (int i = 0; i < TypeParamArity; ++i)

         subst.Add(mapType.TypeParameters[i], typeArgs[i]);

@@ -1790,14 +1790,14 @@ namespace Microsoft.Boogie.VCExprAST {
     }

     public override int TypeParamArity {

       get {

-        return Func.TypeParameters.Length;

+        return Func.TypeParameters.Count;

       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

       //Contract.Requires(cce.NonNullElements(typeArgs));

       //Contract.Requires(cce.NonNullElements(args));

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

-      Contract.Assert(TypeParamArity == Func.TypeParameters.Length);

+      Contract.Assert(TypeParamArity == Func.TypeParameters.Count);

       if (TypeParamArity == 0)

         return cce.NonNull(Func.OutParams[0]).TypedIdent.Type;

       IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>(TypeParamArity);