From 4be2ab852c127558c04119958fd0b462ff2e6493 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 22 Jul 2013 21:33:35 -0700 Subject: Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in code (as opposed to contracts). --- Source/Core/Absy.cs | 2 +- Source/Core/AbsyType.cs | 10 +++++----- Source/Core/CommandLineOptions.cs | 3 ++- Source/Core/ResolutionContext.cs | 3 ++- Source/VCExpr/Boogie2VCExpr.cs | 3 ++- Source/VCExpr/Clustering.cs | 5 +++-- Source/VCExpr/LetBindingSorter.cs | 3 ++- Source/VCExpr/TermFormulaFlattening.cs | 5 +++-- Source/VCExpr/TypeErasure.cs | 7 ++++--- Source/VCExpr/TypeErasureArguments.cs | 3 ++- Source/VCExpr/TypeErasurePremisses.cs | 12 ++++++------ Source/VCExpr/VCExprASTVisitors.cs | 12 ++++++------ Source/VCGeneration/OrderingAxioms.cs | 3 ++- 13 files changed, 40 insertions(+), 31 deletions(-) diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 0436f846..2817acdc 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1343,7 +1343,7 @@ namespace Microsoft.Boogie { foreach (TypeSynonymDecl/*!*/ decl in synonymDecls) { Contract.Assert(decl != null); if (!resolved.Contains(decl) && - Contract.ForAll(deps[decl], d => resolved.Contains(d))) { + deps[decl].All(d => resolved.Contains(d))) { decl.Resolve(rc); resolved.Add(decl); } diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 75cb7f4a..911062a7 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -115,8 +115,7 @@ namespace Microsoft.Boogie { [Pure] public static bool IsIdempotent(IDictionary/*!*/ unifier) { Contract.Requires(cce.NonNullDictionaryAndValues(unifier)); - return Contract.ForAll(unifier.Values, t => Contract.ForAll(0, t.FreeVariables.Count, var => - !unifier.ContainsKey(t.FreeVariables[var]))); + return unifier.Values.All(val => val.FreeVariables.All(var => !unifier.ContainsKey(var))); } @@ -561,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.Count, index => !resultFreeVars.Contains(typeParams[index]))) + if (typeParams.All(param => !resultFreeVars.Contains(param))) return actualResults; else // otherwise there is no point in returning the result type, @@ -1552,7 +1551,7 @@ Contract.Requires(that != null); // this is not a bound variable and can possibly be matched on that // that must not contain any bound variables List! thatFreeVars = that.FreeVariables; - if (Contract.Exists(thatBoundVariables, var=> thatFreeVars.Has(var))) + if (thatBoundVariables.Any(var=> thatFreeVars.Has(var))) throw UNIFICATION_FAILED; // otherwise, in case that is a typevariable it cannot be bound and @@ -3318,7 +3317,8 @@ Contract.Assert(var != null); private bool collisionsPossible(IDictionary/*!*/ subst) { Contract.Requires(cce.NonNullDictionaryAndValues(subst)); // PR: could be written more efficiently - return Contract.Exists(0, TypeParameters.Count, 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]))); + return TypeParameters.Any(param => subst.ContainsKey(param) || subst.Values.Any(val => val.FreeVariables.Contains(param))); } public override Type Substitute(IDictionary/*!*/ subst) { diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2fe78648..db7551ce 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -8,6 +8,7 @@ using System.Collections; using System.Collections.Generic; using System.Collections.Specialized; using System.IO; +using System.Linq; using System.Diagnostics; using System.Diagnostics.Contracts; @@ -1425,7 +1426,7 @@ namespace Microsoft.Boogie { // no preference return true; } - return Contract.Exists(ProcsToCheck, s => 0 <= methodFullname.IndexOf(s)); + return ProcsToCheck.Any(s => 0 <= methodFullname.IndexOf(s)); } public virtual StringCollection ParseNamedArgumentList(string argList) { diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index f3a27517..71471413 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -7,6 +7,7 @@ namespace Microsoft.Boogie { using System.Collections; using System.Collections.Generic; using System; + using System.Linq; using System.Diagnostics.Contracts; [ContractClass(typeof(IErrorSinkContracts))] @@ -565,7 +566,7 @@ namespace Microsoft.Boogie { public bool InFrame(Variable v) { Contract.Requires(v != null); Contract.Requires(Frame != null); - return Contract.Exists(0, Frame.Count, ie => Frame[ie].Decl == v); + return Frame.Any(f => f.Decl == v); } } } diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 22ba09be..0b92b1c3 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -6,6 +6,7 @@ using System; using System.Text; using System.IO; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -36,7 +37,7 @@ namespace Microsoft.Boogie.VCExprAST { if (kinds.IndexOf(',') < 0) { return IsProverCommandSupported(kinds); } else { - return Contract.Exists(kinds.Split(',', ' '), k => IsProverCommandSupported(k)); + return kinds.Split(',', ' ').Any(k => IsProverCommandSupported(k)); } } diff --git a/Source/VCExpr/Clustering.cs b/Source/VCExpr/Clustering.cs index 1efc3606..1ab10107 100644 --- a/Source/VCExpr/Clustering.cs +++ b/Source/VCExpr/Clustering.cs @@ -6,6 +6,7 @@ using System; using System.Text; using System.IO; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -398,12 +399,12 @@ namespace Microsoft.Boogie.Clustering { public bool RepresentationIsRenaming(IDictionary/*!*/ globalVars) { Contract.Requires(cce.NonNullDictionaryAndValues(globalVars)); - if (!Contract.ForAll(Representation, pair => pair.Key.Expr0 is VCExprVar && pair.Key.Expr1 is VCExprVar && !globalVars.ContainsKey(cce.NonNull((VCExprVar)pair.Key.Expr0)) && !globalVars.ContainsKey(cce.NonNull((VCExprVar/*!*/)pair.Key.Expr1)))) + if (!Representation.Any(pair => pair.Key.Expr0 is VCExprVar && pair.Key.Expr1 is VCExprVar && !globalVars.ContainsKey(cce.NonNull((VCExprVar)pair.Key.Expr0)) && !globalVars.ContainsKey(cce.NonNull((VCExprVar/*!*/)pair.Key.Expr1)))) return false; // check that all substituted variables are distinct // TODO: optimise return - Contract.ForAll(Representation, pair1 => Contract.ForAll(Representation, pair2 => pair1.Value.Equals(pair2.Value) || !pair1.Key.Expr0.Equals(pair2.Key.Expr0) && !pair1.Key.Expr1.Equals(pair2.Key.Expr1))); + Representation.All(pair1 => Representation.All(pair2 => pair1.Value.Equals(pair2.Value) || !pair1.Key.Expr0.Equals(pair2.Key.Expr0) && !pair1.Key.Expr1.Equals(pair2.Key.Expr1))); } public void RepresentationSize(IDictionary/*!*/ globalVars, out int expr0Size, out int expr1Size) { diff --git a/Source/VCExpr/LetBindingSorter.cs b/Source/VCExpr/LetBindingSorter.cs index 97d71e27..474770d0 100644 --- a/Source/VCExpr/LetBindingSorter.cs +++ b/Source/VCExpr/LetBindingSorter.cs @@ -6,6 +6,7 @@ using System; using System.Text; using System.IO; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -87,7 +88,7 @@ Contract.Ensures(Contract.Result() != null); } } - if (Contract.Exists(boundVars, pair=> pair.Value.InvOccurrencesNum > 0)) + if (boundVars.Any(pair=> pair.Value.InvOccurrencesNum > 0)) System.Diagnostics.Debug.Fail("Cyclic let-bindings"); Contract.Assert(node.Length == sortedBindings.Count); diff --git a/Source/VCExpr/TermFormulaFlattening.cs b/Source/VCExpr/TermFormulaFlattening.cs index 7111939a..9198d753 100644 --- a/Source/VCExpr/TermFormulaFlattening.cs +++ b/Source/VCExpr/TermFormulaFlattening.cs @@ -6,6 +6,7 @@ using System; using System.Text; using System.IO; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -99,8 +100,8 @@ Contract.Ensures(cce.NonNullElements(Contract.Result>())) foreach (KeyValuePair pair in Bindings) { Contract.Assert(cce.NonNullElements(pair)); coll.Collect(pair.Key); - if (Contract.Exists(boundVars, var => coll.FreeTermVars.ContainsKey(var)) || - Contract.Exists(boundTypeVars, var => coll.FreeTypeVars.Contains(var))) + if (boundVars.Any(var => coll.FreeTermVars.ContainsKey(var)) || + boundTypeVars.Any(var => coll.FreeTypeVars.Contains(var))) res.Add(Gen.LetBinding(pair.Value, pair.Key)); coll.Reset(); } diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index a25781af..9614f9f8 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -6,6 +6,7 @@ using System; using System.Text; using System.IO; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -989,7 +990,7 @@ namespace Microsoft.Boogie.TypeErasure { if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType)) return rawType; - if (Contract.ForAll(0, rawType.FreeVariables.Count, var => !boundTypeParams.Contains(rawType.FreeVariables[var]))) { + if (rawType.FreeVariables.All(var => !boundTypeParams.Contains(var))) { // Bingo! // if the type does not contain any bound variables, we can simply // replace it with a type variable @@ -1361,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure { List/*!*/ newArgs = MutateSeq(node, bindings, newPolarity); Type/*!*/ oldType = node[0].Type; if (AxBuilder.UnchangedType(oldType) && - Contract.ForAll(1, node.Arity, i => node[i].Type.Equals(oldType))) + node.All(e => e.Type.Equals(oldType))) return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType)); else return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U)); @@ -1568,7 +1569,7 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(cce.NonNullElements(Contract.Result>())); VariableCastCollector/*!*/ collector = new VariableCastCollector(axBuilder); Contract.Assert(collector != null); - if (Contract.Exists(newNode.Triggers, trigger => trigger.Pos)) { + if (newNode.Triggers.Any(trigger => trigger.Pos)) { // look in the given triggers foreach (VCTrigger/*!*/ trigger in newNode.Triggers) { Contract.Assert(trigger != null); diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index 00259ecd..8885cbc7 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -6,6 +6,7 @@ using System; using System.Text; using System.IO; +using System.Linq; using System.Collections; using System.Collections.Generic; using System.Diagnostics.Contracts; @@ -108,7 +109,7 @@ namespace Microsoft.Boogie.TypeErasure { // if all of the parameters are int or bool, the function does // not have to be changed - if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) && + if (fun.InParams.All(param => UnchangedType(cce.NonNull(param).TypedIdent.Type)) && UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type)) { res = fun; } else { diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index c6b5eee6..fc3d1214 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -374,7 +374,7 @@ namespace Microsoft.Boogie.TypeErasure // if all of the parameters are int or bool, the function does // not have to be changed - if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) && + if (fun.InParams.All(param => UnchangedType(cce.NonNull(param).TypedIdent.Type)) && UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) && fun.TypeParameters.Count == 0) { res = new UntypedFunction(fun, new List(), new List()); @@ -641,9 +641,9 @@ 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(abstractedType.TypeParameters.Count + abstractedType.FreeVariables.Count); - typeParams.AddRange(abstractedType.TypeParameters.ToList()); - typeParams.AddRange(abstractedType.FreeVariables.ToList()); + typeParams = new List(); + typeParams.AddRange(abstractedType.TypeParameters); + typeParams.AddRange(abstractedType.FreeVariables); originalIndexTypes = new List(abstractedType.Arguments.Count + 1); List/*!*/ mapTypeParams = new List(); @@ -1115,7 +1115,7 @@ namespace Microsoft.Boogie.TypeErasure if (typeVarBindings.Count < node.TypeParameters.Count) { foreach (TypeVariable/*!*/ var in node.TypeParameters) { Contract.Assert(var != null); - if (!Contract.Exists(typeVarBindings, b => b.V.Equals(var))) + if (typeVarBindings.All(b => b.V.Equals(var))) newBoundVars.Add((VCExprVar)bindings.TypeVariableBindings[var]); } } @@ -1196,7 +1196,7 @@ namespace Microsoft.Boogie.TypeErasure Dictionary/*!*/ freeVars = FreeVariableCollector.FreeTermVariables(e); Contract.Assert(freeVars != null && cce.NonNullElements(freeVars.Keys)); - if (Contract.Exists(typeVarBindings, b => freeVars.ContainsKey(b.V))) { + if (typeVarBindings.Any(b => freeVars.ContainsKey(b.V))) { exprsWithLets.Add(Gen.Let(typeVarBindings, e)); changed = true; } else { diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 67280bea..10c06abf 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -1072,13 +1072,13 @@ namespace Microsoft.Boogie.VCExprAST { public bool TermSubstIsEmpty { get { - return Contract.ForAll(TermSubsts, dict => dict.Count == 0); + return TermSubsts.All(dict => dict.Count == 0); } } public bool TypeSubstIsEmpty { get { - return Contract.ForAll(TypeSubsts, dict => dict.Count == 0); + return TypeSubsts.All(dict => dict.Count == 0); ; } } @@ -1173,15 +1173,15 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(boundVars)); Contract.Requires(substitution != null); // variables can be shadowed by a binder - if (Contract.Exists(typeParams, var => substitution.ContainsKey(var)) || - Contract.Exists(boundVars, var => substitution.ContainsKey(var))) + if (typeParams.Any(var => substitution.ContainsKey(var)) || + boundVars.Any(var => substitution.ContainsKey(var))) return true; // compute the codomain of the substitution FreeVariableCollector coll = substitution.Codomains; Contract.Assert(coll != null); // variables could be captured when applying the substitution - return Contract.Exists(typeParams, var => coll.FreeTypeVars.Contains(var)) || - Contract.Exists(boundVars, var => coll.FreeTermVars.ContainsKey(var)); + return typeParams.Any(var => coll.FreeTypeVars.Contains(var)) || + boundVars.Any(var => coll.FreeTermVars.ContainsKey(var)); } // can be overwritten if names of bound variables are to be changed diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs index b8a98def..dbb97764 100644 --- a/Source/VCGeneration/OrderingAxioms.cs +++ b/Source/VCGeneration/OrderingAxioms.cs @@ -7,6 +7,7 @@ using System; using System.Collections.Generic; using System.IO; using System.Text; +using System.Linq; using System.Diagnostics.Contracts; using Microsoft.Boogie.VCExprAST; @@ -286,7 +287,7 @@ namespace Microsoft.Boogie { VCExpr maxDescendants = Gen.Eq(cAsVar, w); foreach (Constant d in Constants) { Contract.Assert(d != null); - if (d.Parents != null && Contract.Exists(d.Parents, p => c.Equals(p.Parent.Decl))) + if (d.Parents != null && d.Parents.Any(p => c.Equals(p.Parent.Decl))) maxDescendants = Gen.Or(maxDescendants, Gen.AtMost(w, Translator.LookupVariable(d))); } -- cgit v1.2.3