From 07e15dce2315f99bcbc7b3aa558653feec9de906 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 22:51:04 +0100 Subject: ExprSeq: farewell --- Source/Core/Absy.cs | 40 +++----------------- Source/Core/AbsyCmd.cs | 21 ++--------- Source/Core/AbsyExpr.cs | 86 +++++++++++++++++++++--------------------- Source/Core/AbsyQuant.cs | 8 ++-- Source/Core/AbsyType.cs | 12 +++--- Source/Core/BoogiePL.atg | 30 +++++++-------- Source/Core/Duplicator.cs | 6 +-- Source/Core/LambdaHelper.cs | 6 +-- Source/Core/LinearSets.cs | 52 ++++++++++++------------- Source/Core/OwickiGries.cs | 8 ++-- Source/Core/Parser.cs | 30 +++++++-------- Source/Core/StandardVisitor.cs | 8 ++-- Source/Core/Util.cs | 2 +- 13 files changed, 132 insertions(+), 177 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 23935658..29f826f7 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -398,9 +398,9 @@ namespace Microsoft.Boogie { Contract.Assert(header != null); List inputs = new List(); List outputs = new List(); - ExprSeq callInputs1 = new ExprSeq(); + List callInputs1 = new List(); List callOutputs1 = new List(); - ExprSeq callInputs2 = new ExprSeq(); + List callInputs2 = new List(); List callOutputs2 = new List(); List lhss = new List(); List rhss = new List(); @@ -2134,7 +2134,7 @@ namespace Microsoft.Boogie { Contract.Requires(definition != null); List dummies = new List(); - ExprSeq callArgs = new ExprSeq(); + List callArgs = new List(); int i = 0; foreach (Formal/*!*/ f in InParams) { Contract.Assert(f != null); @@ -2157,7 +2157,7 @@ namespace Microsoft.Boogie { if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) { def = new ForallExpr(tok, quantifiedTypeVars, dummies, kv, - new Trigger(tok, true, new ExprSeq(call), null), + new Trigger(tok, true, new List { call }, null), def); } DefinitionAxiom = new Axiom(tok, def); @@ -3234,36 +3234,6 @@ namespace Microsoft.Boogie { } } - public sealed class ExprSeq : List { - public ExprSeq(params Expr[]/*!*/ args) - : base(args) { - Contract.Requires(args != null); - } - public ExprSeq(ExprSeq/*!*/ exprSeq) - : base(exprSeq) { - Contract.Requires(exprSeq != null); - } - - public static ExprSeq operator +(ExprSeq a, ExprSeq b) { - if (a == null) - throw new ArgumentNullException("a"); - if (b == null) - throw new ArgumentNullException("b"); - return Append(a, b); - } - - public static ExprSeq Append(ExprSeq s, ExprSeq t) { - Contract.Requires(t != null); - Contract.Requires(s != null); - Expr[] n = new Expr[s.Count + t.Count]; - for (int i = 0; i < s.Count; i++) - n[i] = s[i]; - for (int i = 0; i < t.Count; i++) - n[s.Count + i] = t[i]; - return new ExprSeq(n); - } - } - public static class Emitter { public static void Declarations(List/*!*/ decls, TokenTextWriter stream) { Contract.Requires(stream != null); @@ -3292,7 +3262,7 @@ namespace Microsoft.Boogie { } } - public static void Emit(this ExprSeq ts, TokenTextWriter stream) { + public static void Emit(this List ts, TokenTextWriter stream) { Contract.Requires(stream != null); string sep = ""; foreach (Expr/*!*/ e in ts) { diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index d1f3a845..57f48f02 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -981,7 +981,7 @@ namespace Microsoft.Boogie { public static AssignCmd/*!*/ MapAssign(IToken tok, IdentifierExpr/*!*/ map, - ExprSeq/*!*/ indexes, Expr/*!*/ rhs) { + List/*!*/ indexes, Expr/*!*/ rhs) { Contract.Requires(tok != null); Contract.Requires(map != null); @@ -1468,7 +1468,7 @@ namespace Microsoft.Boogie { } // we use the same typechecking code as in MapSelect - ExprSeq/*!*/ selectArgs = new ExprSeq(); + List/*!*/ selectArgs = new List(); foreach (Expr/*!*/ e in Indexes) { Contract.Assert(e != null); selectArgs.Add(e); @@ -1756,21 +1756,6 @@ namespace Microsoft.Boogie { errorData = value; } } - public CallCmd(IToken tok, string callee, ExprSeq ins, List outs) - : this(tok, callee, ins.ToList(), outs.ToList()) { - Contract.Requires(outs != null); - Contract.Requires(ins != null); - Contract.Requires(callee != null); - Contract.Requires(tok != null); - //List/*!*/ insList = new List(); - //List/*!*/ outsList = new List(); - //foreach (Expr e in ins) - // if(e!=null) - // insList.Add(e); - //foreach (IdentifierExpr e in outs) - // if(e!=null) - // outsList.Add(e); - } public CallCmd(IToken tok, string callee, List ins, List outs) : base(tok, null) { Contract.Requires(outs != null); @@ -1987,7 +1972,7 @@ namespace Microsoft.Boogie { List/*!*/ formalInTypes = new List(); List/*!*/ formalOutTypes = new List(); - ExprSeq/*!*/ actualIns = new ExprSeq(); + List/*!*/ actualIns = new List(); List/*!*/ actualOuts = new List(); for (int i = 0; i < Ins.Count; ++i) { if (Ins[i] != null) { diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index b3b2289b..dcc6d6e2 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -90,7 +90,7 @@ namespace Microsoft.Boogie { Contract.Requires(e1 != null); Contract.Requires(x != null); Contract.Ensures(Contract.Result() != null); - return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1)); + return new NAryExpr(x, new UnaryOperator(x, op), new List { e1 }); } public static NAryExpr Binary(IToken x, BinaryOperator.Opcode op, Expr e0, Expr e1) { @@ -98,7 +98,7 @@ namespace Microsoft.Boogie { Contract.Requires(e0 != null); Contract.Requires(x != null); Contract.Ensures(Contract.Result() != null); - return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e0, e1)); + return new NAryExpr(x, new BinaryOperator(x, op), new List { e0, e1 }); } public static NAryExpr Binary(BinaryOperator.Opcode op, Expr e0, Expr e1) { @@ -339,7 +339,7 @@ namespace Microsoft.Boogie { Contract.Requires(map != null); Contract.Requires(x != null); Contract.Ensures(Contract.Result() != null); - ExprSeq/*!*/ allArgs = new ExprSeq(); + List/*!*/ allArgs = new List(); allArgs.Add(map); foreach (Expr/*!*/ a in args) { Contract.Assert(a != null); @@ -376,7 +376,7 @@ namespace Microsoft.Boogie { Contract.Requires(args.Length > 0); // zero or more indices, plus the value Contract.Ensures(Contract.Result() != null); - ExprSeq/*!*/ allArgs = new ExprSeq(); + List/*!*/ allArgs = new List(); allArgs.Add(map); foreach (Expr/*!*/ a in args) { Contract.Assert(a != null); @@ -390,7 +390,7 @@ namespace Microsoft.Boogie { Contract.Requires(subexpr != null); Contract.Requires(x != null); Contract.Ensures(Contract.Result() != null); - ExprSeq/*!*/ args = new ExprSeq(); + List/*!*/ args = new List(); args.Add(subexpr); return new NAryExpr(x, new TypeCoercion(x, type), args); } @@ -945,7 +945,7 @@ namespace Microsoft.Boogie { /// /// /// - void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext); + void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext); void Resolve(ResolutionContext/*!*/ rc, Expr/*!*/ subjectForErrorReporting); @@ -968,14 +968,14 @@ namespace Microsoft.Boogie { /// /// /// - Type Typecheck(ref ExprSeq/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc); + Type Typecheck(ref List/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc); // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null}); /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - Type/*!*/ ShallowType(ExprSeq/*!*/ args); + Type/*!*/ ShallowType(List/*!*/ args); T Dispatch(IAppliableVisitor/*!*/ visitor); } @@ -991,7 +991,7 @@ namespace Microsoft.Boogie { } } - public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { Contract.Requires(args != null); Contract.Requires(stream != null); throw new NotImplementedException(); @@ -1009,7 +1009,7 @@ namespace Microsoft.Boogie { } } - public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public Type Typecheck(ref List args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { Contract.Requires(args != null); Contract.Requires(tc != null); Contract.Ensures(Contract.ValueAtReturn(out args) != null); @@ -1018,7 +1018,7 @@ namespace Microsoft.Boogie { throw new NotImplementedException(); } - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); @@ -1105,7 +1105,7 @@ namespace Microsoft.Boogie { } } - public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.SetToken(ref this.tok); @@ -1139,7 +1139,7 @@ namespace Microsoft.Boogie { } } - public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public Type Typecheck(ref List args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { //Contract.Requires(tc != null); //Contract.Requires(args != null); Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); @@ -1173,7 +1173,7 @@ namespace Microsoft.Boogie { this.FunctionName, arg0type); return null; } - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); switch (this.op) { @@ -1319,7 +1319,7 @@ namespace Microsoft.Boogie { } } - public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.SetToken(ref this.tok); @@ -1444,7 +1444,7 @@ namespace Microsoft.Boogie { return 2; } } - public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public Type Typecheck(ref List args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { //Contract.Requires(tc != null); //Contract.Requires(args != null); Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); @@ -1538,7 +1538,7 @@ namespace Microsoft.Boogie { return null; } - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); switch (this.op) { @@ -1588,7 +1588,7 @@ namespace Microsoft.Boogie { case Opcode.Neq: if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) { expr.Fun = new BinaryOperator(tok, Opcode.Iff); - arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new ExprSeq(arg1)); + arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new List { arg1 }); // ugly ... there should be some more general approach, // e.g., to typecheck the whole expression again @@ -1765,7 +1765,7 @@ namespace Microsoft.Boogie { return Func.GetHashCode(); } - virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + virtual public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); this.name.Emit(stream, 0xF0, false); @@ -1791,7 +1791,7 @@ namespace Microsoft.Boogie { return Func.InParams.Count; } } - public virtual Type Typecheck(ref ExprSeq actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public virtual Type Typecheck(ref List actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { //Contract.Requires(tc != null); //Contract.Requires(actuals != null); Contract.Ensures(Contract.ValueAtReturn(out actuals) != null); @@ -1824,7 +1824,7 @@ namespace Microsoft.Boogie { return actualResultType[0]; } } - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(name.Type != null); @@ -1860,7 +1860,7 @@ namespace Microsoft.Boogie { } } - public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, + public void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(args != null); //Contract.Requires(stream != null); @@ -1894,7 +1894,7 @@ namespace Microsoft.Boogie { } } - public Type Typecheck(ref ExprSeq/*!*/ args, + public Type Typecheck(ref List/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc) { //Contract.Requires(args != null); @@ -1912,7 +1912,7 @@ namespace Microsoft.Boogie { return this.Type; } - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return this.Type; @@ -1991,7 +1991,7 @@ namespace Microsoft.Boogie { } } - virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + virtual public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.Write(this.name); @@ -2005,7 +2005,7 @@ namespace Microsoft.Boogie { //Contract.Requires(rc != null); } - public virtual Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public virtual Type Typecheck(ref List args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { //Contract.Requires(tc != null); //Contract.Requires(args != null); Contract.Ensures(args != null); @@ -2022,7 +2022,7 @@ namespace Microsoft.Boogie { return this.type; } - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return this.type; @@ -2038,7 +2038,7 @@ namespace Microsoft.Boogie { [Additive] [Peer] public IAppliable/*!*/ Fun; - public ExprSeq/*!*/ Args; + public List/*!*/ Args; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Fun != null); @@ -2051,7 +2051,7 @@ namespace Microsoft.Boogie { public TypeParamInstantiation TypeParameters = null; [Captured] - public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, ExprSeq/*!*/ args) + public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, List/*!*/ args) : base(tok) { Contract.Requires(tok != null); Contract.Requires(fun != null); @@ -2188,7 +2188,7 @@ namespace Microsoft.Boogie { return Arity.GetHashCode() * 2823; } - public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, + public void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(args != null); //Contract.Requires(stream != null); @@ -2196,7 +2196,7 @@ namespace Microsoft.Boogie { Emit(args, stream, contextBindingStrength, fragileContext, false); } - public static void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, + public static void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext, bool withRhs) { Contract.Requires(args != null); @@ -2248,7 +2248,7 @@ namespace Microsoft.Boogie { // the AssignCmd maps can also be // represented by non-expressions Absy/*!*/ map, - ExprSeq/*!*/ indexes, + List/*!*/ indexes, // the type parameters, in this context, are the parameters of the // potentially polymorphic map type. Because it might happen that // the whole map type is unknown and represented using a MapTypeProxy, @@ -2290,13 +2290,13 @@ namespace Microsoft.Boogie { } } - public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public Type Typecheck(ref List args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { //Contract.Requires(tc != null); //Contract.Requires(args != null); Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); Contract.Assume(args.Count == Arity + 1); - ExprSeq actualArgs = new ExprSeq(); + List actualArgs = new List(); for (int i = 1; i < args.Count; ++i) actualArgs.Add(args[i]); @@ -2307,7 +2307,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Expr a0 = cce.NonNull(args[0]); @@ -2369,7 +2369,7 @@ namespace Microsoft.Boogie { return Arity.GetHashCode() * 28231; } - public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, + public void Emit(List/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(args != null); //Contract.Requires(stream != null); @@ -2390,7 +2390,7 @@ namespace Microsoft.Boogie { } // it is assumed that each of the arguments has already been typechecked - public static Type Typecheck(ExprSeq/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, + public static Type Typecheck(List/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc, IToken/*!*/ typeCheckingSubject, string/*!*/ opName) { @@ -2401,7 +2401,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); // part of the type checking works exactly as for MapSelect - ExprSeq selectArgs = new ExprSeq(); + List selectArgs = new List(); for (int i = 1; i < args.Count - 1; ++i) selectArgs.Add(args[i]); Type resultType = @@ -2424,7 +2424,7 @@ namespace Microsoft.Boogie { return cce.NonNull(args[0]).Type; } - public Type Typecheck(ref ExprSeq/*!*/ args, + public Type Typecheck(ref List/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc) { //Contract.Requires(args != null); @@ -2438,7 +2438,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return cce.NonNull(args[0]).ShallowType; @@ -2486,7 +2486,7 @@ namespace Microsoft.Boogie { return 1; } - public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { + public void Emit(List args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); //Contract.Requires(args != null); stream.SetToken(ref this.tok); @@ -2512,7 +2512,7 @@ namespace Microsoft.Boogie { } } - public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { + public Type Typecheck(ref List args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) { //Contract.Requires(tc != null); //Contract.Requires(args != null); Contract.Ensures(args != null); @@ -2539,7 +2539,7 @@ namespace Microsoft.Boogie { /// /// Returns the result type of the IAppliable, supposing the argument are of the correct types. /// - public Type ShallowType(ExprSeq args) { + public Type ShallowType(List args) { //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return cce.NonNull(args[1]).ShallowType; diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 5fdc3e68..fe0748a9 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -326,7 +326,7 @@ namespace Microsoft.Boogie { public class Trigger : Absy { public readonly bool Pos; [Rep] - public ExprSeq/*!*/ Tr; + public List/*!*/ Tr; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Tr != null); @@ -336,7 +336,7 @@ namespace Microsoft.Boogie { public Trigger Next; - public Trigger(IToken tok, bool pos, ExprSeq tr) + public Trigger(IToken tok, bool pos, List tr) : this(tok, pos, tr, null) { Contract.Requires(tr != null); Contract.Requires(tok != null); @@ -344,7 +344,7 @@ namespace Microsoft.Boogie { Contract.Requires(pos || tr.Count == 1); } - public Trigger(IToken/*!*/ tok, bool pos, ExprSeq/*!*/ tr, Trigger next) + public Trigger(IToken/*!*/ tok, bool pos, List/*!*/ tr, Trigger next) : base(tok) { Contract.Requires(tok != null); Contract.Requires(tr != null); @@ -584,7 +584,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); FunctionCall fn = node.Fun as FunctionCall; if (fn != null && cce.NonNull(fn.Func).NeverTrigger) { - parent.Triggers = new Trigger(fn.Func.tok, false, new ExprSeq(node), parent.Triggers); + parent.Triggers = new Trigger(fn.Func.tok, false, new List { node} , parent.Triggers); } return base.VisitNAryExpr(node); } diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index e5fad05d..64c4b699 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -366,7 +366,7 @@ namespace Microsoft.Boogie { public static IDictionary! MatchArgumentTypes(TypeVariableSeq! typeParams, List! formalArgs, - ExprSeq! actualArgs, + List! actualArgs, List formalOuts, List actualOuts, string! opName, @@ -438,7 +438,7 @@ namespace Microsoft.Boogie { public static IDictionary/*!*/ MatchArgumentTypes(TypeVariableSeq/*!*/ typeParams, List/*!*/ formalArgs, - ExprSeq/*!*/ actualArgs, + List/*!*/ actualArgs, List formalOuts, List actualOuts, string/*!*/ opName, @@ -508,7 +508,7 @@ namespace Microsoft.Boogie { public static List CheckArgumentTypes(TypeVariableSeq/*!*/ typeParams, out List/*!*/ actualTypeParams, List/*!*/ formalIns, - ExprSeq/*!*/ actualIns, + List/*!*/ actualIns, List/*!*/ formalOuts, List actualOuts, IToken/*!*/ typeCheckingSubject, @@ -631,7 +631,7 @@ namespace Microsoft.Boogie { #else /// /// like Type.CheckArgumentTypes, but assumes no errors - /// (and only does arguments, not results; and takes actuals as List, not ExprSeq) + /// (and only does arguments, not results; and takes actuals as List, not List) /// public static IDictionary/*!*/ InferTypeParameters(TypeVariableSeq/*!*/ typeParams, @@ -2354,7 +2354,7 @@ Contract.Requires(that != null); constraints.Add(c); } - public Type CheckArgumentTypes(ExprSeq/*!*/ actualArgs, + public Type CheckArgumentTypes(List/*!*/ actualArgs, out TypeParamInstantiation/*!*/ tpInstantiation, IToken/*!*/ typeCheckingSubject, string/*!*/ opName, @@ -3480,7 +3480,7 @@ Contract.Assert(var != null); //------------ result type. Null is returned if so many type checking //------------ errors occur that the situation is hopeless - public Type CheckArgumentTypes(ExprSeq/*!*/ actualArgs, + public Type CheckArgumentTypes(List/*!*/ actualArgs, out TypeParamInstantiation/*!*/ tpInstantiation, IToken/*!*/ typeCheckingSubject, string/*!*/ opName, diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index dec0b3a8..294abba3 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -24,7 +24,7 @@ readonly Expr/*!*/ dummyExpr; readonly Cmd/*!*/ dummyCmd; readonly Block/*!*/ dummyBlock; readonly Bpl.Type/*!*/ dummyType; -readonly Bpl.ExprSeq/*!*/ dummyExprSeq; +readonly Bpl.List/*!*/ dummyExprSeq; readonly TransferCmd/*!*/ dummyTransferCmd; readonly StructuredCmd/*!*/ dummyStructuredCmd; @@ -86,7 +86,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr); dummyBlock = new Block(Token.NoToken, "dummyBlock", new List(), new ReturnCmd(Token.NoToken)); dummyType = new BasicType(Token.NoToken, SimpleType.Bool); - dummyExprSeq = new ExprSeq (); + dummyExprSeq = new List (); dummyTransferCmd = new ReturnCmd(Token.NoToken); dummyStructuredCmd = new BreakCmd(Token.NoToken, null); } @@ -993,8 +993,8 @@ WhiteSpaceIdents/*!*/ xs> . /*------------------------------------------------------------------------*/ -Expressions -= (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq(); .) +Expressions/*!*/ es> += (. Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List(); .) Expression (. es.Add(e); .) { "," Expression (. es.Add(e); .) } @@ -1194,10 +1194,10 @@ ArrayExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1; bool store; bool bvExtract; - ExprSeq/*!*/ allArgs = dummyExprSeq; + List/*!*/ allArgs = dummyExprSeq; .) AtomExpression - { "[" (. x = t; allArgs = new ExprSeq (); + { "[" (. x = t; allArgs = new List (); allArgs.Add(e); store = false; bvExtract = false; .) [ @@ -1238,7 +1238,7 @@ ArrayExpression /*------------------------------------------------------------------------*/ AtomExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; - ExprSeq/*!*/ es; List/*!*/ ds; Trigger trig; + List/*!*/ es; List/*!*/ ds; Trigger trig; TypeVariableSeq/*!*/ typeParams; IdentifierExpr/*!*/ id; QKeyValue kv; @@ -1255,7 +1255,7 @@ AtomExpression | Ident (. id = new IdentifierExpr(x, x.val); e = id; .) [ "(" ( Expressions (. e = new NAryExpr(x, new FunctionCall(id), es); .) - | /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); .) + | /* empty */ (. e = new NAryExpr(x, new FunctionCall(id), new List()); .) ) ")" ] @@ -1268,12 +1268,12 @@ AtomExpression | "int" (. x = t; .) "(" Expression - ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); .) + ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List(e)); .) | "real" (. x = t; .) "(" Expression - ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); .) + ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List(e)); .) | "(" ( Expression (. if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + @@ -1349,7 +1349,7 @@ Attribute . AttributeOrTrigger -= (. IToken/*!*/ tok; Expr/*!*/ e; ExprSeq/*!*/ es; += (. IToken/*!*/ tok; Expr/*!*/ e; List/*!*/ es; string key; List parameters; object/*!*/ param; .) @@ -1364,9 +1364,9 @@ AttributeOrTrigger if (parameters.Count == 1 && parameters[0] is Expr) { e = (Expr)parameters[0]; if(trig==null){ - trig = new Trigger(tok, false, new ExprSeq(e), null); + trig = new Trigger(tok, false, new List(e), null); } else { - trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null)); + trig.AddLast(new Trigger(tok, false, new List(e), null)); } } else { this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter"); @@ -1380,7 +1380,7 @@ AttributeOrTrigger } .) | - Expression (. es = new ExprSeq(e); .) + Expression (. es = new List(e); .) { "," Expression (. es.Add(e); .) } (. if (trig==null) { trig = new Trigger(tok, true, es, null); @@ -1408,7 +1408,7 @@ IfThenElseExpression Expr/*!*/ e0, e1, e2; e = dummyExpr; .) "if" (. tok = t; .) Expression "then" Expression "else" Expression - (. e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); .) + (. e = new NAryExpr(tok, new IfThenElse(tok), new List(e0, e1, e2)); .) . diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 2d220a35..1d221bb7 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -159,10 +159,10 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return base.VisitExpr((Expr)node.Clone()); } - public override ExprSeq VisitExprSeq(ExprSeq list) { + public override List VisitExprSeq(List list) { //Contract.Requires(list != null); - Contract.Ensures(Contract.Result() != null); - return base.VisitExprSeq(new ExprSeq(list)); + Contract.Ensures(Contract.Result>() != null); + return base.VisitExprSeq(new List(list)); } public override ForallExpr VisitForallExpr(ForallExpr node) { //Contract.Requires(node != null); diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index ede25c0e..a461db22 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -97,8 +97,8 @@ namespace Microsoft.Boogie { // this is ugly, the output will depend on hashing order Dictionary subst = new Dictionary(); List formals = new List(); - ExprSeq callArgs = new ExprSeq(); - ExprSeq axCallArgs = new ExprSeq(); + List callArgs = new List(); + List axCallArgs = new List(); List dummies = new List(lambda.Dummies); TypeVariableSeq freeTypeVars = new TypeVariableSeq(); List fnTypeVarActuals = new List(); @@ -160,7 +160,7 @@ namespace Microsoft.Boogie { NAryExpr body = Expr.Eq(select, bb); body.Type = Type.Bool; body.TypeParameters = SimpleTypeParamInstantiation.EMPTY; - Trigger trig = new Trigger(select.tok, true, new ExprSeq(select)); + Trigger trig = new Trigger(select.tok, true, new List { select }); lambdaAxioms.Add(new ForallExpr(tok, forallTypeVariables, dummies, lambda.Attributes, trig, body)); NAryExpr call = new NAryExpr(tok, fcall, callArgs); diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 00caea52..5b9aee5f 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -425,7 +425,7 @@ namespace Microsoft.Boogie foreach (var domainName in linearDomains.Keys) { var domain = linearDomains[domainName]; - callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False))); + callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False })); } } else if (callCmd.InParallelWith != null) @@ -435,7 +435,7 @@ namespace Microsoft.Boogie foreach (var domainName in linearDomains.Keys) { var domain = linearDomains[domainName]; - callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False))); + callCmd.Ins.Add(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False })); } callCmd = callCmd.InParallelWith; } @@ -452,7 +452,7 @@ namespace Microsoft.Boogie var domainName = FindDomainName(v); var domain = linearDomains[domainName]; IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName])); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] }); } foreach (var domainName in linearDomains.Keys) { @@ -552,7 +552,7 @@ namespace Microsoft.Boogie public Expr Singleton(Expr e, string domainName) { var domain = linearDomains[domainName]; - return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.False)), e, Expr.True); + return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }), e, Expr.True); } List MkAssignLhss(params Variable[] args) @@ -579,10 +579,10 @@ namespace Microsoft.Boogie foreach (Variable v in scope) { IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new ExprSeq(new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)))); - e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new ExprSeq(new IdentifierExpr(Token.NoToken, partition), e)); - e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e)); - e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new ExprSeq(Expr.True))); + Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } ); + e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List { new IdentifierExpr(Token.NoToken, partition), e } ); + e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } ); + e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.True })); disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr); } return new ExistsExpr(Token.NoToken, new List { partition }, disjointExpr); @@ -622,13 +622,13 @@ namespace Microsoft.Boogie IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new ExprSeq(aie, bie)); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie)); + var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List { aie, bie } ); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie } ); var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or, - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)), - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie))); + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie } ), + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie} )); var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List { a, b }, null, - new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), + new Trigger(Token.NoToken, true, new List { mapApplTerm }), new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); axiomExpr.Typecheck(new TypecheckingContext(null)); axioms.Add(new Axiom(Token.NoToken, axiomExpr)); @@ -650,13 +650,13 @@ namespace Microsoft.Boogie IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new ExprSeq(aie, bie)); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie)); + var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List { aie, bie }); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp, - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)), - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie))); + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie }), + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie })); var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List { a, b }, null, - new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), + new Trigger(Token.NoToken, true, new List { mapApplTerm }), new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); axiomExpr.Typecheck(new TypecheckingContext(null)); axioms.Add(new Axiom(Token.NoToken, axiomExpr)); @@ -674,12 +674,12 @@ namespace Microsoft.Boogie BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), - new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.True)), xie)); + new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.True }), xie }); var trueAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, trueTerm); trueAxiomExpr.Typecheck(new TypecheckingContext(null)); axioms.Add(new Axiom(Token.NoToken, trueAxiomExpr)); var falseTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), - new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new ExprSeq(Expr.False)), xie)); + new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List { Expr.False }), xie }); var falseAxiomExpr = new ForallExpr(Token.NoToken, new List { x }, Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, falseTerm)); falseAxiomExpr.Typecheck(new TypecheckingContext(null)); axioms.Add(new Axiom(Token.NoToken, falseAxiomExpr)); @@ -701,13 +701,13 @@ namespace Microsoft.Boogie IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new ExprSeq(aie, bie)); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(mapApplTerm, xie)); + var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List { aie, bie }); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { mapApplTerm, xie }); var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq, - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(aie, xie)), - new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(bie, xie))); + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { aie, xie }), + new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { bie, xie })); var axiomExpr = new ForallExpr(Token.NoToken, new TypeVariableSeq(), new List { a, b }, null, - new Trigger(Token.NoToken, true, new ExprSeq(mapApplTerm)), + new Trigger(Token.NoToken, true, new List { mapApplTerm }), new ForallExpr(Token.NoToken, new List { x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, rhsTerm))); axiomExpr.Typecheck(new TypecheckingContext(null)); axioms.Add(new Axiom(Token.NoToken, axiomExpr)); @@ -726,7 +726,7 @@ namespace Microsoft.Boogie IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a); BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType)); IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x); - var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new ExprSeq(new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new ExprSeq(aie)), xie)); + var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List { aie }), xie }); var axiomExpr = new ForallExpr(Token.NoToken, new List { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie)); axiomExpr.Typecheck(new TypecheckingContext(null)); axioms.Add(new Axiom(Token.NoToken, axiomExpr)); diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 4815c781..90cfce97 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -182,7 +182,7 @@ namespace Microsoft.Boogie private void AddCallToYieldProc(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) { - ExprSeq exprSeq = new ExprSeq(); + List exprSeq = new List(); foreach (string domainName in linearTypechecker.linearDomains.Keys) { exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName])); @@ -208,7 +208,7 @@ namespace Microsoft.Boogie var domainName = linearTypechecker.FindDomainName(v); var domain = linearTypechecker.linearDomains[domainName]; IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName])); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); } return domainNameToExpr; } @@ -597,7 +597,7 @@ namespace Microsoft.Boogie if (domainName == null) continue; var domain = linearTypechecker.linearDomains[domainName]; IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new ExprSeq(v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName])); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { v.TypedIdent.Type is MapType ? ie : linearTypechecker.Singleton(ie, domainName), domainNameToExpr[domainName] }); } foreach (string domainName in linearTypechecker.linearDomains.Keys) { @@ -744,7 +744,7 @@ namespace Microsoft.Boogie int labelCount = 0; foreach (Procedure proc in yieldCheckerProcs) { - ExprSeq exprSeq = new ExprSeq(); + List exprSeq = new List(); foreach (Variable v in inputs) { exprSeq.Add(new IdentifierExpr(Token.NoToken, v)); diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 17e4b0fb..3064ae0f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -44,7 +44,7 @@ readonly Expr/*!*/ dummyExpr; readonly Cmd/*!*/ dummyCmd; readonly Block/*!*/ dummyBlock; readonly Bpl.Type/*!*/ dummyType; -readonly Bpl.ExprSeq/*!*/ dummyExprSeq; +readonly List/*!*/ dummyExprSeq; readonly TransferCmd/*!*/ dummyTransferCmd; readonly StructuredCmd/*!*/ dummyStructuredCmd; @@ -106,7 +106,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr); dummyBlock = new Block(Token.NoToken, "dummyBlock", new List(), new ReturnCmd(Token.NoToken)); dummyType = new BasicType(Token.NoToken, SimpleType.Bool); - dummyExprSeq = new ExprSeq (); + dummyExprSeq = new List (); dummyTransferCmd = new ReturnCmd(Token.NoToken); dummyStructuredCmd = new BreakCmd(Token.NoToken, null); } @@ -1324,8 +1324,8 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else SynErr(110); } - void Expressions(out ExprSeq/*!*/ es) { - Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq(); + void Expressions(out List/*!*/ es) { + Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new List(); Expression(out e); es.Add(e); while (la.kind == 12) { @@ -1624,12 +1624,12 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; Expr/*!*/ index0 = dummyExpr; Expr/*!*/ e1; bool store; bool bvExtract; - ExprSeq/*!*/ allArgs = dummyExprSeq; + List/*!*/ allArgs = dummyExprSeq; AtomExpression(out e); while (la.kind == 17) { Get(); - x = t; allArgs = new ExprSeq (); + x = t; allArgs = new List (); allArgs.Add(e); store = false; bvExtract = false; if (StartOf(15)) { @@ -1688,7 +1688,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void AtomExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd; - ExprSeq/*!*/ es; List/*!*/ ds; Trigger trig; + List/*!*/ es; List/*!*/ ds; Trigger trig; TypeVariableSeq/*!*/ typeParams; IdentifierExpr/*!*/ id; QKeyValue kv; @@ -1731,7 +1731,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Expressions(out es); e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 10) { - e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); + e = new NAryExpr(x, new FunctionCall(id), new List()); } else SynErr(122); Expect(10); } @@ -1752,7 +1752,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Expect(9); Expression(out e); Expect(10); - e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); + e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new List { e }); break; } case 15: { @@ -1761,7 +1761,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Expect(9); Expression(out e); Expect(10); - e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); + e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new List { e }); break; } case 9: { @@ -1901,7 +1901,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expression(out e1); Expect(41); Expression(out e2); - e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); + e = new NAryExpr(tok, new IfThenElse(tok), new List { e0, e1, e2 }); } void CodeExpression(out List/*!*/ locals, out List/*!*/ blocks) { @@ -1961,7 +1961,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) { - IToken/*!*/ tok; Expr/*!*/ e; ExprSeq/*!*/ es; + IToken/*!*/ tok; Expr/*!*/ e; List/*!*/ es; string key; List parameters; object/*!*/ param; @@ -1984,9 +1984,9 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { if (parameters.Count == 1 && parameters[0] is Expr) { e = (Expr)parameters[0]; if(trig==null){ - trig = new Trigger(tok, false, new ExprSeq(e), null); + trig = new Trigger(tok, false, new List { e }, null); } else { - trig.AddLast(new Trigger(tok, false, new ExprSeq(e), null)); + trig.AddLast(new Trigger(tok, false, new List { e }, null)); } } else { this.SemErr("the 'nopats' quantifier attribute expects a string-literal parameter"); @@ -2001,7 +2001,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); - es = new ExprSeq(e); + es = new List { e }; while (la.kind == 12) { Get(); Expression(out e); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index d8707bc4..4a9ca7a3 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -29,9 +29,9 @@ namespace Microsoft.Boogie { public virtual void TransferStateTo(Visitor targetVisitor) { } - public virtual ExprSeq VisitExprSeq(ExprSeq list) { + public virtual List VisitExprSeq(List list) { Contract.Requires(list != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); for (int i = 0, n = list.Count; i < n; i++) list[i] = (Expr)this.Visit(cce.NonNull(list[i])); return list; @@ -235,9 +235,9 @@ namespace Microsoft.Boogie { Expr e = (Expr)this.Visit(node); return e; } - public override ExprSeq VisitExprSeq(ExprSeq exprSeq) { + public override List VisitExprSeq(List exprSeq) { //Contract.Requires(exprSeq != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); for (int i = 0, n = exprSeq.Count; i < n; i++) exprSeq[i] = this.VisitExpr(cce.NonNull(exprSeq[i])); return exprSeq; diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 09b6664e..c14cb82e 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -369,7 +369,7 @@ namespace Microsoft.Boogie { } else if (e is NAryExpr) { NAryExpr ne = (NAryExpr)e; IAppliable fun = ne.Fun; - ExprSeq eSeq = ne.Args; + List eSeq = ne.Args; if (fun != null) { if ((fun.FunctionName == "$Length" || fun.FunctionName == "$StringLength") && eSeq.Count == 1) { Expr e0 = eSeq[0]; -- cgit v1.2.3