Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in code (as opposed to contracts).

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<TypeVariable/*!*/, Type/*!*/>/*!*/ 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<TypeVariable>! 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<TypeVariable/*!*/, Type/*!*/>/*!*/ 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<TypeVariable/*!*/, Type/*!*/>/*!*/ 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<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ 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<VCExprVar/*!*/, VCExprVar/*!*/>/*!*/ 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<VCExpr>() != 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<List<VCExprLetBinding>>()))
       foreach (KeyValuePair<VCExpr, VCExprVar> 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<VCExpr/*!*/>/*!*/ 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<List<VCExprVar>>()));

       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<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());

@@ -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<TypeVariable/*!*/>(abstractedType.TypeParameters.Count + abstractedType.FreeVariables.Count);

-      typeParams.AddRange(abstractedType.TypeParameters.ToList());

-      typeParams.AddRange(abstractedType.FreeVariables.ToList());

+      typeParams = new List<TypeVariable/*!*/>();

+      typeParams.AddRange(abstractedType.TypeParameters);

+      typeParams.AddRange(abstractedType.FreeVariables);

 

       originalIndexTypes = new List<Type/*!*/>(abstractedType.Arguments.Count + 1);

       List<Type>/*!*/ mapTypeParams = new List<Type>();

@@ -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<VCExprVar/*!*/, object>/*!*/ 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)));

       }