summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyQuant.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core/AbsyQuant.cs')
-rw-r--r--Source/Core/AbsyQuant.cs25
1 files changed, 13 insertions, 12 deletions
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index a6382eb4..e42df50f 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -12,6 +12,7 @@ namespace Microsoft.Boogie {
using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
+ using System.Linq;
using Microsoft.Boogie.AbstractInterpretation;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
@@ -65,7 +66,7 @@ namespace Microsoft.Boogie {
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Count > 0);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
TypeParameters = typeParameters;
Dummies = dummies;
Attributes = kv;
@@ -159,7 +160,7 @@ namespace Microsoft.Boogie {
rc.PopVarContext();
// establish a canonical order of the type parameters
- this.TypeParameters = Type.SortTypeParams(TypeParameters, Dummies.ToTypeSeq, null);
+ this.TypeParameters = Type.SortTypeParams(TypeParameters, new TypeSeq(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);
} finally {
rc.TypeBinderState = previousTypeBinderState;
@@ -192,7 +193,7 @@ namespace Microsoft.Boogie {
protected TypeVariableSeq GetUnmentionedTypeParameters() {
Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
- TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);
+ TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(new TypeSeq(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));
Contract.Assert(dummyParameters != null);
TypeVariableSeq/*!*/ unmentionedParameters = new TypeVariableSeq();
foreach (TypeVariable/*!*/ var in TypeParameters) {
@@ -427,21 +428,21 @@ namespace Microsoft.Boogie {
Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParams.Count > 0);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
}
public ForallExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public ForallExpr(IToken tok, VariableSeq dummies, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public ForallExpr(IToken tok, TypeVariableSeq typeParams, VariableSeq dummies, Expr body)
: base(tok, typeParams, dummies, null, null, body) {
@@ -449,7 +450,7 @@ namespace Microsoft.Boogie {
Contract.Requires(dummies != null);
Contract.Requires(typeParams != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length + typeParams.Count > 0);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -473,21 +474,21 @@ namespace Microsoft.Boogie {
Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParams.Count > 0);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
}
public ExistsExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public ExistsExpr(IToken tok, VariableSeq dummies, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -521,7 +522,7 @@ namespace Microsoft.Boogie {
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Count > 0);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
@@ -702,7 +703,7 @@ namespace Microsoft.Boogie {
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Count > 0);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
}
public override BinderKind Kind {