diff options
| -rw-r--r-- | Source/Core/Absy.cs | 46 | ||||
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 16 | ||||
| -rw-r--r-- | Source/Core/AbsyType.cs | 54 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 6 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 6 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasureArguments.cs | 12 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasurePremisses.cs | 8 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 6 |
10 files changed, 66 insertions, 92 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 6e131606..9d857e22 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1290,7 +1290,7 @@ namespace Microsoft.Boogie { stream.Write(this, level, "type ");
EmitAttributes(stream);
stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(Name));
- if (TypeParameters.Length > 0)
+ if (TypeParameters.Count > 0)
stream.Write(" ");
TypeParameters.Emit(stream, " ");
stream.Write(" = ");
@@ -2151,7 +2151,7 @@ namespace Microsoft.Boogie { // type parameters only occur in the output type
call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());
Expr def = Expr.Eq(call, definition);
- if (quantifiedTypeVars.Length != 0 || dummies.Length != 0) {
+ if (quantifiedTypeVars.Count != 0 || dummies.Length != 0) {
def = new ForallExpr(tok, quantifiedTypeVars, dummies,
kv,
new Trigger(tok, true, new ExprSeq(call), null),
@@ -2843,7 +2843,7 @@ namespace Microsoft.Boogie { Contract.Assume(this.Proc != null);
- if (this.TypeParameters.Length != Proc.TypeParameters.Length) {
+ if (this.TypeParameters.Count != Proc.TypeParameters.Count) {
tc.Error(this, "mismatched number of type parameters in procedure implementation: {0}",
this.Name);
} else {
@@ -2876,14 +2876,14 @@ namespace Microsoft.Boogie { } else {
// unify the type parameters so that types can be compared
Contract.Assert(Proc != null);
- Contract.Assert(this.TypeParameters.Length == Proc.TypeParameters.Length);
+ Contract.Assert(this.TypeParameters.Count == Proc.TypeParameters.Count);
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =
new Dictionary<TypeVariable/*!*/, Type/*!*/>();
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst2 =
new Dictionary<TypeVariable/*!*/, Type/*!*/>();
- for (int i = 0; i < this.TypeParameters.Length; ++i) {
+ for (int i = 0; i < this.TypeParameters.Count; ++i) {
TypeVariable/*!*/ newVar =
new TypeVariable(Token.NoToken, Proc.TypeParameters[i].Name);
Contract.Assert(newVar != null);
@@ -3293,7 +3293,7 @@ namespace Microsoft.Boogie { }
}
- public sealed class TypeVariableSeq : PureCollections.Sequence {
+ public sealed class TypeVariableSeq : List<TypeVariable> {
public TypeVariableSeq(params TypeVariable[]/*!*/ args)
: base(args) {
Contract.Requires(args != null);
@@ -3302,28 +3302,12 @@ namespace Microsoft.Boogie { : base(varSeq) {
Contract.Requires(varSeq != null);
}
- /* PR: the following two constructors cause Spec# crashes
- public TypeVariableSeq(TypeVariable! var)
- : base(new TypeVariable! [] { var })
- {
- }
- public TypeVariableSeq()
- : base(new TypeVariable![0])
- {
- } */
- public new TypeVariable/*!*/ this[int index] {
- get {
- Contract.Ensures(Contract.Result<TypeVariable>() != null);
-
- return cce.NonNull((TypeVariable)base[index]);
- }
- set {
- base[index] = value;
- }
+ public void Remove() {
+ RemoveAt(Count - 1);
}
public void AppendWithoutDups(TypeVariableSeq s1) {
Contract.Requires(s1 != null);
- for (int i = 0; i < s1.card; i++) {
+ for (int i = 0; i < s1.Count; i++) {
TypeVariable/*!*/ next = s1[i];
Contract.Assert(next != null);
if (!this.Contains(next))
@@ -3341,19 +3325,9 @@ namespace Microsoft.Boogie { v.Emit(stream);
}
}
- public new TypeVariable[] ToArray() {
- Contract.Ensures(Contract.Result<TypeVariable[]>() != null);
- TypeVariable[]/*!*/ n = new TypeVariable[Length];
- int ct = 0;
- foreach (TypeVariable/*!*/ var in this) {
- Contract.Assert(var != null);
- n[ct++] = var;
- }
- return n;
- }
public List<TypeVariable/*!*/>/*!*/ ToList() {
Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
- List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(Length);
+ List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(Count);
foreach (TypeVariable/*!*/ var in this) {
Contract.Assert(var != null);
res.Add(var);
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index cca59323..6e719e60 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -65,7 +65,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Length > 0);
+ Contract.Requires(dummies.Length + typeParameters.Count > 0);
TypeParameters = typeParameters;
Dummies = dummies;
Attributes = kv;
@@ -427,7 +427,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParams.Length > 0);
+ Contract.Requires(dummies.Length + typeParams.Count > 0);
}
public ForallExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
@@ -449,7 +449,7 @@ namespace Microsoft.Boogie { Contract.Requires(dummies != null);
Contract.Requires(typeParams != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length + typeParams.Length > 0);
+ Contract.Requires(dummies.Length + typeParams.Count > 0);
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -473,7 +473,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParams.Length > 0);
+ Contract.Requires(dummies.Length + typeParams.Count > 0);
}
public ExistsExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
@@ -521,7 +521,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Length > 0);
+ Contract.Requires(dummies.Length + typeParameters.Count > 0);
Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
@@ -663,7 +663,7 @@ namespace Microsoft.Boogie { TypeVariableSeq/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
Contract.Assert(unmentionedParameters != null);
- if (unmentionedParameters.Length > 0) {
+ if (unmentionedParameters.Count > 0) {
// all the type parameters that do not occur in dummy types
// have to occur in triggers
@@ -702,7 +702,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Length > 0);
+ Contract.Requires(dummies.Length + typeParameters.Count > 0);
}
public override BinderKind Kind {
@@ -737,7 +737,7 @@ namespace Microsoft.Boogie { TypeVariableSeq/*!*/ unmentionedParameters = GetUnmentionedTypeParameters();
Contract.Assert(unmentionedParameters != null);
- if (unmentionedParameters.Length > 0) {
+ if (unmentionedParameters.Count > 0) {
tc.Error(this, "the type variable {0} does not occur in types of the lambda parameters", unmentionedParameters[0]);
}
}
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 20ff8446..dd558f94 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -114,7 +114,7 @@ namespace Microsoft.Boogie { [Pure]
public static bool IsIdempotent(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ unifier) {
Contract.Requires(cce.NonNullDictionaryAndValues(unifier));
- return Contract.ForAll(unifier.Values, t => Contract.ForAll(0, t.FreeVariables.Length, var =>
+ return Contract.ForAll(unifier.Values, t => Contract.ForAll(0, t.FreeVariables.Count, var =>
!unifier.ContainsKey(t.FreeVariables[var])));
}
@@ -219,7 +219,7 @@ namespace Microsoft.Boogie { public bool IsClosed {
get {
- return FreeVariables.Length == 0;
+ return FreeVariables.Count == 0;
}
}
@@ -467,7 +467,7 @@ namespace Microsoft.Boogie { Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type);
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Contains(typeParams[index])));
+ Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index])));
if (!formal.Unify(actual)) {
Contract.Assume(tc != null); // caller expected no errors
@@ -484,7 +484,7 @@ namespace Microsoft.Boogie { Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type);
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !actual.FreeVariables.Contains(typeParams[var])));
+ Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !actual.FreeVariables.Contains(typeParams[var])));
if (!formal.Unify(actual)) {
Contract.Assume(tc != null); // caller expected no errors
@@ -529,14 +529,14 @@ namespace Microsoft.Boogie { opName, actualIns.Length);
// if there are no type parameters, we can still return the result
// type and hope that the type checking proceeds
- return typeParams.Length == 0 ? formalOuts : null;
+ return typeParams.Count == 0 ? formalOuts : null;
} else if (actualOuts != null && formalOuts.Count != actualOuts.Length) {
tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",
opName, actualOuts.Length);
// if there are no type parameters, we can still return the result
// type and hope that the type checking proceeds
actualTypeParams = new List<Type>();
- return typeParams.Length == 0 ? formalOuts : null;
+ return typeParams.Count == 0 ? formalOuts : null;
}
int previousErrorCount = tc.ErrorCount;
@@ -560,7 +560,7 @@ namespace Microsoft.Boogie { // in case we have been able to substitute all type parameters,
// we can still return the result type and hope that the
// type checking proceeds in a meaningful manner
- if (Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Contains(typeParams[index])))
+ if (Contract.ForAll(0, typeParams.Count, index => !resultFreeVars.Contains(typeParams[index])))
return actualResults;
else
// otherwise there is no point in returning the result type,
@@ -568,7 +568,7 @@ namespace Microsoft.Boogie { return null;
}
- Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !resultFreeVars.Contains(typeParams[index])));
+ Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !resultFreeVars.Contains(typeParams[index])));
return actualResults;
}
@@ -595,7 +595,7 @@ namespace Microsoft.Boogie { // all type parameters have to be substituted with concrete types
TypeVariableSeq/*!*/ resFreeVars = res.FreeVariables;
Contract.Assert(resFreeVars != null);
- Contract.Assert(Contract.ForAll(0, typeParams.Length, var => !resFreeVars.Contains(typeParams[var])));
+ Contract.Assert(Contract.ForAll(0, typeParams.Count, var => !resFreeVars.Contains(typeParams[var])));
return res;
}
@@ -656,7 +656,7 @@ namespace Microsoft.Boogie { Type actual = actualArgs[i];
// if the type variables to be matched occur in the actual
// argument types, something has gone very wrong
- Contract.Assert(Contract.ForAll(0, typeParams.Length, index => !actual.FreeVariables.Contains(typeParams[index])));
+ Contract.Assert(Contract.ForAll(0, typeParams.Count, index => !actual.FreeVariables.Contains(typeParams[index])));
if (!formal.Unify(actual)) {
Contract.Assume(false); // caller expected no errors
@@ -672,7 +672,7 @@ namespace Microsoft.Boogie { public static void EmitOptionalTypeParams(TokenTextWriter stream, TypeVariableSeq typeParams) {
Contract.Requires(typeParams != null);
Contract.Requires(stream != null);
- if (typeParams.Length > 0) {
+ if (typeParams.Count > 0) {
stream.Write("<");
typeParams.Emit(stream, ","); // default binding strength of 0 is ok
stream.Write(">");
@@ -685,8 +685,8 @@ namespace Microsoft.Boogie { Contract.Requires(argumentTypes != null);
Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
- Contract.Ensures(Contract.Result<TypeVariableSeq>().Length == typeParams.Length);
- if (typeParams.Length == 0) {
+ Contract.Ensures(Contract.Result<TypeVariableSeq>().Count == typeParams.Count);
+ if (typeParams.Count == 0) {
return typeParams;
}
@@ -704,7 +704,7 @@ namespace Microsoft.Boogie { }
}
- if (sortedTypeParams.Length < typeParams.Length)
+ if (sortedTypeParams.Count < typeParams.Count)
// add the type parameters not mentioned in "argumentTypes" in
// the end of the list (this can happen for quantifiers)
sortedTypeParams.AppendWithoutDups(typeParams);
@@ -1332,7 +1332,7 @@ Contract.Requires(that != null); // fourth case: the identifier denotes a type synonym
TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name);
if (synDecl != null) {
- if (Arguments.Count != synDecl.TypeParameters.Length) {
+ if (Arguments.Count != synDecl.TypeParameters.Count) {
rc.Error(this,
"type synonym received wrong number of arguments: {0}",
synDecl);
@@ -2566,7 +2566,7 @@ Contract.Requires(that != null); Contract.Requires(token != null);
Contract.Requires(decl != null);
Contract.Requires(arguments != null);
- Contract.Requires(arguments.Count == decl.TypeParameters.Length);
+ Contract.Requires(arguments.Count == decl.TypeParameters.Count);
this.Decl = decl;
this.Arguments = arguments;
@@ -3150,7 +3150,7 @@ Contract.Requires(that != null); that = TypeProxy.FollowProxy(that.Expanded);
MapType thatMapType = that as MapType;
if (thatMapType == null ||
- this.TypeParameters.Length != thatMapType.TypeParameters.Length ||
+ this.TypeParameters.Count != thatMapType.TypeParameters.Count ||
this.Arguments.Count != thatMapType.Arguments.Count)
return false;
@@ -3176,7 +3176,7 @@ Contract.Requires(that != null); } finally {
// make sure that the bound variables are removed again
- for (int i = 0; i < this.TypeParameters.Length; ++i) {
+ for (int i = 0; i < this.TypeParameters.Count; ++i) {
thisBoundVariables.Remove();
thatBoundVariables.Remove();
}
@@ -3196,7 +3196,7 @@ Contract.Requires(that != null); MapType thatMapType = that as MapType;
if (thatMapType == null ||
- this.TypeParameters.Length != thatMapType.TypeParameters.Length ||
+ this.TypeParameters.Count != thatMapType.TypeParameters.Count ||
this.Arguments.Count != thatMapType.Arguments.Count)
return false;
@@ -3206,7 +3206,7 @@ Contract.Requires(that != null); Dictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst1 =
new Dictionary<TypeVariable/*!*/, Type/*!*/>();
TypeVariableSeq freshies = new TypeVariableSeq();
- for (int i = 0; i < this.TypeParameters.Length; i++) {
+ for (int i = 0; i < this.TypeParameters.Count; i++) {
TypeVariable tp0 = this.TypeParameters[i];
TypeVariable tp1 = thatMapType.TypeParameters[i];
TypeVariable freshVar = new TypeVariable(tp0.tok, tp0.Name);
@@ -3226,7 +3226,7 @@ Contract.Requires(that != null); good &= r0.Unify(r1, unifiableVariables, result);
// Finally, check that none of the bound variables has escaped
- if (good && freshies.Length != 0) {
+ if (good && freshies.Count != 0) {
// This is done by looking for occurrences of the fresh variables in the
// non-substituted types ...
TypeVariableSeq freeVars = this.FreeVariables;
@@ -3317,7 +3317,7 @@ Contract.Assert(var != null); private bool collisionsPossible(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
Contract.Requires(cce.NonNullDictionaryAndValues(subst));
// PR: could be written more efficiently
- return Contract.Exists(0, TypeParameters.Length, i => subst.ContainsKey(TypeParameters[i]) || Contract.Exists(subst.Values, t => t.FreeVariables.Contains(TypeParameters[i])));
+ return Contract.Exists(0, TypeParameters.Count, i => subst.ContainsKey(TypeParameters[i]) || Contract.Exists(subst.Values, t => t.FreeVariables.Contains(TypeParameters[i])));
}
public override Type Substitute(IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst) {
@@ -3357,7 +3357,7 @@ Contract.Assert(var != null); [Pure]
public override int GetHashCode(TypeVariableSeq boundVariables) {
//Contract.Requires(boundVariables != null);
- int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Count;
+ int res = 7643761 * TypeParameters.Count + 65121 * Arguments.Count;
foreach (TypeVariable/*!*/ var in this.TypeParameters) {
Contract.Assert(var != null);
@@ -3370,7 +3370,7 @@ Contract.Assert(var != null); }
res = res * 7 + Result.GetHashCode(boundVariables);
- for (int i = 0; i < this.TypeParameters.Length; ++i)
+ for (int i = 0; i < this.TypeParameters.Count; ++i)
boundVariables.Remove();
return res;
@@ -3586,15 +3586,15 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); public static TypeParamInstantiation/*!*/ From(TypeVariableSeq typeParams, List<Type/*!*/>/*!*/ actualTypeParams) {
Contract.Requires(cce.NonNullElements(actualTypeParams));
Contract.Requires(typeParams != null);
- Contract.Requires(typeParams.Length == actualTypeParams.Count);
+ Contract.Requires(typeParams.Count == actualTypeParams.Count);
Contract.Ensures(Contract.Result<TypeParamInstantiation>() != null);
- if (typeParams.Length == 0)
+ if (typeParams.Count == 0)
return EMPTY;
List<TypeVariable/*!*/>/*!*/ typeParamList = new List<TypeVariable/*!*/>();
IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
- for (int i = 0; i < typeParams.Length; ++i) {
+ for (int i = 0; i < typeParams.Count; ++i) {
typeParamList.Add(typeParams[i]);
dict.Add(typeParams[i], actualTypeParams[i]);
}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index bd6b1da3..51381625 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -294,7 +294,7 @@ namespace Microsoft.Boogie outParams.Add(y);
map[x] = new IdentifierExpr(Token.NoToken, y);
}
- Contract.Assume(callCmd.Proc.TypeParameters.Length == 0);
+ Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);
Substitution subst = Substituter.SubstitutionFromHashtable(map);
foreach (Requires req in callCmd.Proc.Requires)
{
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 7bd21d02..7b172d30 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1775,13 +1775,13 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
- if (typeParams.Length + ds.Length > 0)
+ if (typeParams.Count + ds.Length > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 89 || la.kind == 90) {
Exists();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
- if (typeParams.Length + ds.Length > 0)
+ if (typeParams.Count + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 91 || la.kind == 92) {
Lambda();
@@ -1789,7 +1789,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (trig != null)
SemErr("triggers not allowed in lambda expressions");
- if (typeParams.Length + ds.Length > 0)
+ if (typeParams.Count + ds.Length > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
} else SynErr(123);
Expect(10);
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);
|