From 12f3c4d7f530265c966bc72764d17e08a47aa4c0 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 21:17:07 +0100 Subject: Started to remove ...Seq classes --- Source/VCExpr/Boogie2VCExpr.cs | 6 +++--- Source/VCExpr/TypeErasure.cs | 24 ++++++++++++------------ Source/VCExpr/TypeErasureArguments.cs | 6 +++--- Source/VCExpr/TypeErasurePremisses.cs | 6 +++--- Source/VCExpr/VCExprAST.cs | 8 ++++---- 5 files changed, 25 insertions(+), 25 deletions(-) (limited to 'Source/VCExpr') diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 6509bc30..b3574b94 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -492,7 +492,7 @@ namespace Microsoft.Boogie.VCExprAST { return new VCQuantifierInfos(qid, node.SkolemId, false, node.Attributes); } - private string getQidNameFromQKeyValue(VariableSeq vars, QKeyValue attributes) { + private string getQidNameFromQKeyValue(List vars, QKeyValue attributes) { Contract.Requires(vars != null); // Check for a 'qid, name' pair in keyvalues string qid = QKeyValue.FindStringAttribute(attributes, "qid"); @@ -872,9 +872,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false); throw new cce.UnreachableException(); } - public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) { + public override List VisitVariableSeq(List variableSeq) { //Contract.Requires(variableSeq != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); Contract.Assert(false); throw new cce.UnreachableException(); } diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index e6384e67..f7860169 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -31,7 +31,7 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires(Contract.ForAll(0, types.Length, i => types[i] != null)); Contract.Ensures(Contract.Result() != null); - VariableSeq args = new VariableSeq(); + List args = new List(); for (int i = 0; i < types.Length - 1; ++i) args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg" + i, cce.NonNull(types[i])), @@ -511,12 +511,12 @@ namespace Microsoft.Boogie.TypeErasure { TypeCtorDecl/*!*/ uDecl = new TypeCtorDecl(Token.NoToken, "U", 0); UDecl = uDecl; - Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new TypeSeq()); + Type/*!*/ u = new CtorType(Token.NoToken, uDecl, new List()); U = u; TypeCtorDecl/*!*/ tDecl = new TypeCtorDecl(Token.NoToken, "T", 0); TDecl = tDecl; - Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new TypeSeq()); + Type/*!*/ t = new CtorType(Token.NoToken, tDecl, new List()); T = t; Ctor = HelperFuns.BoogieFunction("Ctor", t, Type.Int); @@ -940,14 +940,14 @@ namespace Microsoft.Boogie.TypeErasure { /////////////////////////////////////////////////////////////////////////// - public Function Select(MapType rawType, out TypeSeq instantiations) { + public Function Select(MapType rawType, out List instantiations) { Contract.Requires((rawType != null)); Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); Contract.Ensures(Contract.Result() != null); return AbstractAndGetRepresentation(rawType, out instantiations).Select; } - public Function Store(MapType rawType, out TypeSeq instantiations) { + public Function Store(MapType rawType, out List instantiations) { Contract.Requires((rawType != null)); Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); Contract.Ensures(Contract.Result() != null); @@ -955,10 +955,10 @@ namespace Microsoft.Boogie.TypeErasure { } private MapTypeClassRepresentation - AbstractAndGetRepresentation(MapType rawType, out TypeSeq instantiations) { + AbstractAndGetRepresentation(MapType rawType, out List instantiations) { Contract.Requires((rawType != null)); Contract.Ensures(Contract.ValueAtReturn(out instantiations) != null); - instantiations = new TypeSeq(); + instantiations = new List(); MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations); return GetClassRepresentation(abstraction); } @@ -966,7 +966,7 @@ namespace Microsoft.Boogie.TypeErasure { public CtorType AbstractMapType(MapType rawType) { Contract.Requires(rawType != null); Contract.Ensures(Contract.Result() != null); - TypeSeq/*!*/ instantiations = new TypeSeq(); + List/*!*/ instantiations = new List(); MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations); MapTypeClassRepresentation repr = GetClassRepresentation(abstraction); @@ -975,11 +975,11 @@ namespace Microsoft.Boogie.TypeErasure { } // TODO: cache the result of this operation - protected MapType ThinOutMapType(MapType rawType, TypeSeq instantiations) { + protected MapType ThinOutMapType(MapType rawType, List instantiations) { Contract.Requires(instantiations != null); Contract.Requires(rawType != null); Contract.Ensures(Contract.Result() != null); - TypeSeq/*!*/ newArguments = new TypeSeq(); + List/*!*/ newArguments = new List(); foreach (Type/*!*/ subtype in rawType.Arguments) { Contract.Assert(subtype != null); newArguments.Add(ThinOutType(subtype, rawType.TypeParameters, @@ -991,7 +991,7 @@ namespace Microsoft.Boogie.TypeErasure { } // the instantiations of inserted type variables, the order corresponds to the order in which "AbstractionVariable(int)" delivers variables - private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, TypeSeq instantiations) { + private Type/*!*/ ThinOutType(Type rawType, TypeVariableSeq boundTypeParams, List instantiations) { Contract.Requires(instantiations != null); Contract.Requires(boundTypeParams != null); Contract.Requires(rawType != null); @@ -1027,7 +1027,7 @@ namespace Microsoft.Boogie.TypeErasure { // // traverse the subtypes CtorType/*!*/ rawCtorType = rawType.AsCtor; - TypeSeq/*!*/ newArguments = new TypeSeq(); + List/*!*/ newArguments = new List(); foreach (Type/*!*/ subtype in rawCtorType.Arguments) { Contract.Assert(subtype != null); newArguments.Add(ThinOutType(subtype, boundTypeParams, diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index 8e4bc7ab..00259ecd 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -627,7 +627,7 @@ Contract.Ensures(Contract.Result() != null); if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) { MapType/*!*/ rawType = node[0].Type.AsMap; Contract.Assert(rawType != null); - TypeSeq/*!*/ abstractionInstantiation; + List/*!*/ abstractionInstantiation; Function/*!*/ select = AxBuilder.MapTypeAbstracter.Select(rawType, out abstractionInstantiation); Contract.Assert(abstractionInstantiation != null); @@ -647,7 +647,7 @@ Contract.Ensures(Contract.Result() != null); if (!NewOpCache.TryGetValue(originalOpTypes, out newOpTypes)) { MapType/*!*/ rawType = node[0].Type.AsMap; - TypeSeq/*!*/ abstractionInstantiation; + List/*!*/ abstractionInstantiation; Function/*!*/ store = AxBuilder.MapTypeAbstracter.Store(rawType, out abstractionInstantiation); @@ -660,7 +660,7 @@ Contract.Ensures(Contract.Result() != null); private OpTypesPair TypesPairForSelectStore(VCExprNAry/*!*/ node, Function/*!*/ untypedOp, // instantiation of the abstract map type parameters - TypeSeq/*!*/ abstractionInstantiation) { + List/*!*/ abstractionInstantiation) { Contract.Requires(node != null); Contract.Requires(untypedOp != null); Contract.Requires(abstractionInstantiation != null); diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index ec2d47bd..c78d7fba 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -646,7 +646,7 @@ namespace Microsoft.Boogie.TypeErasure typeParams.AddRange(abstractedType.FreeVariables.ToList()); originalIndexTypes = new List(abstractedType.Arguments.Count + 1); - TypeSeq/*!*/ mapTypeParams = new TypeSeq(); + List/*!*/ mapTypeParams = new List(); foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) { Contract.Assert(var != null); mapTypeParams.Add(var); @@ -1271,7 +1271,7 @@ namespace Microsoft.Boogie.TypeErasure MapType/*!*/ mapType = node[0].Type.AsMap; Contract.Assert(mapType != null); - TypeSeq/*!*/ instantiations; // not used + List/*!*/ instantiations; // not used Function/*!*/ select = AxBuilder.MapTypeAbstracter.Select(mapType, out instantiations); Contract.Assert(select != null); @@ -1291,7 +1291,7 @@ namespace Microsoft.Boogie.TypeErasure Contract.Requires(bindings != null); Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); - TypeSeq/*!*/ instantiations; // not used + List/*!*/ instantiations; // not used Function/*!*/ store = AxBuilder.MapTypeAbstracter.Store(node[0].Type.AsMap, out instantiations); Contract.Assert(store != null); diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 3961f096..41f1e207 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -31,7 +31,7 @@ namespace Microsoft.Boogie { if (ControlFlowFunction == null) { Formal/*!*/ first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true); Formal/*!*/ second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true); - VariableSeq inputs = new VariableSeq(); + List inputs = new List(); inputs.Add(first); inputs.Add(second); Formal/*!*/ returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false); @@ -728,11 +728,11 @@ namespace Microsoft.Boogie.VCExprAST { return res; } - public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex) { + public static List ToTypeSeq(VCExpr[] exprs, int startIndex) { Contract.Requires(exprs != null); Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null))); - Contract.Ensures(Contract.Result() != null); - TypeSeq/*!*/ res = new TypeSeq(); + Contract.Ensures(Contract.Result>() != null); + List/*!*/ res = new List(); for (int i = startIndex; i < exprs.Length; ++i) res.Add(cce.NonNull(exprs[i]).Type); return res; -- cgit v1.2.3