Dafny: internal renaming

2 files changed, 56 insertions, 56 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 57623068..18721cf3 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1160,11 +1160,11 @@ namespace Microsoft.Dafny {
           var ind = indent + i * IndentAmount;

           var bound = s.Bounds[i];

           var bv = s.BoundVars[i];

-          if (bound is QuantifierExpr.BoolBoundedPool) {

+          if (bound is ComprehensionExpr.BoolBoundedPool) {

             Indent(ind);

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.IntBoundedPool) {

-            var b = (QuantifierExpr.IntBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.IntBoundedPool) {

+            var b = (ComprehensionExpr.IntBoundedPool)bound;

             SpillLetVariableDecls(b.LowerBound, ind);

             SpillLetVariableDecls(b.UpperBound, ind);

             Indent(ind);

@@ -1173,22 +1173,22 @@ namespace Microsoft.Dafny {
             wr.Write("; @{0} < ", bv.CompileName);

             TrExpr(b.UpperBound);

             wr.Write("; @{0}++) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.SetBoundedPool) {

-            var b = (QuantifierExpr.SetBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var b = (ComprehensionExpr.SetBoundedPool)bound;

             SpillLetVariableDecls(b.Set, ind);

             Indent(ind);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Set);

             wr.Write(").Elements) { ");

-          } else if (bound is QuantifierExpr.SeqBoundedPool) {

-            var b = (QuantifierExpr.SeqBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var b = (ComprehensionExpr.SeqBoundedPool)bound;

             SpillLetVariableDecls(b.Seq, ind);

             Indent(ind);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Seq);

             wr.Write(").UniqueElements) { ");

-          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

-            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+            var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

@@ -2053,32 +2053,32 @@ namespace Microsoft.Dafny {
           var bound = e.Bounds[i];

           var bv = e.BoundVars[i];

           // emit:  Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)

-          if (bound is QuantifierExpr.BoolBoundedPool) {

+          if (bound is ComprehensionExpr.BoolBoundedPool) {

             wr.Write("Dafny.Helpers.QuantBool(");

-          } else if (bound is QuantifierExpr.IntBoundedPool) {

-            var b = (QuantifierExpr.IntBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.IntBoundedPool) {

+            var b = (ComprehensionExpr.IntBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantInt(");

             TrExpr(b.LowerBound);

             wr.Write(", ");

             TrExpr(b.UpperBound);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.SetBoundedPool) {

-            var b = (QuantifierExpr.SetBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSet(");

             TrExpr(b.Set);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.MapBoundedPool) {

-            var b = (QuantifierExpr.MapBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.MapBoundedPool) {

+            var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantMap(");

             TrExpr(b.Map);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.SeqBoundedPool) {

-            var b = (QuantifierExpr.SeqBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantSeq(");

             TrExpr(b.Seq);

             wr.Write(", ");

-          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

-            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+            var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantDatatype(");

 

             wr.Write("{0}.AllSingletonConstructors, ", DtName(b.Decl));

@@ -2120,32 +2120,32 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < n; i++) {

           var bound = e.Bounds[i];

           var bv = e.BoundVars[i];

-          if (bound is QuantifierExpr.BoolBoundedPool) {

+          if (bound is ComprehensionExpr.BoolBoundedPool) {

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.IntBoundedPool) {

-            var b = (QuantifierExpr.IntBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.IntBoundedPool) {

+            var b = (ComprehensionExpr.IntBoundedPool)bound;

             wr.Write("for (var @{0} = ", bv.CompileName);

             TrExpr(b.LowerBound);

             wr.Write("; @{0} < ", bv.CompileName);

             TrExpr(b.UpperBound);

             wr.Write("; @{0}++) {{ ", bv.CompileName);

-          } else if (bound is QuantifierExpr.SetBoundedPool) {

-            var b = (QuantifierExpr.SetBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SetBoundedPool) {

+            var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Set);

             wr.Write(").Elements) { ");

-          } else if (bound is QuantifierExpr.MapBoundedPool) {

-            var b = (QuantifierExpr.MapBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.MapBoundedPool) {

+            var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Map);

             wr.Write(").Domain) { ");

-          } else if (bound is QuantifierExpr.SeqBoundedPool) {

-            var b = (QuantifierExpr.SeqBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+            var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

             TrExpr(b.Seq);

             wr.Write(").Elements) { ");

-          } else if (bound is QuantifierExpr.DatatypeBoundedPool) {

-            var b = (QuantifierExpr.DatatypeBoundedPool)bound;

+          } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+            var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected BoundedPool type

@@ -2189,27 +2189,27 @@ namespace Microsoft.Dafny {
         Contract.Assert(e.Bounds.Count == n && n == 1);

         var bound = e.Bounds[0];

         var bv = e.BoundVars[0];

-        if (bound is QuantifierExpr.BoolBoundedPool) {

+        if (bound is ComprehensionExpr.BoolBoundedPool) {

           wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

-        } else if (bound is QuantifierExpr.IntBoundedPool) {

-          var b = (QuantifierExpr.IntBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.IntBoundedPool) {

+          var b = (ComprehensionExpr.IntBoundedPool)bound;

           wr.Write("for (var @{0} = ", bv.CompileName);

           TrExpr(b.LowerBound);

           wr.Write("; @{0} < ", bv.CompileName);

           TrExpr(b.UpperBound);

           wr.Write("; @{0}++) {{ ", bv.CompileName);

-        } else if (bound is QuantifierExpr.SetBoundedPool) {

-          var b = (QuantifierExpr.SetBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.SetBoundedPool) {

+          var b = (ComprehensionExpr.SetBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

           TrExpr(b.Set);

           wr.Write(").Elements) { ");

-        } else if (bound is QuantifierExpr.MapBoundedPool) {

-          var b = (QuantifierExpr.MapBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.MapBoundedPool) {

+          var b = (ComprehensionExpr.MapBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

           TrExpr(b.Map);

           wr.Write(").Domain) { ");

-        } else if (bound is QuantifierExpr.SeqBoundedPool) {

-          var b = (QuantifierExpr.SeqBoundedPool)bound;

+        } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+          var b = (ComprehensionExpr.SeqBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

           TrExpr(b.Seq);

           wr.Write(").Elements) { ");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b9cc8a55..6534d2ba 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -5001,7 +5001,7 @@ namespace Microsoft.Dafny
     ///      variable only has lower bounds, no upper bounds)

     /// Requires "expr" to be successfully resolved.

     /// </summary>

-    public static List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, bool returnAllBounds, List<BoundVar> missingBounds) {

+    public static List<ComprehensionExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, bool returnAllBounds, List<BoundVar> missingBounds) {

       Contract.Requires(tok != null);

       Contract.Requires(bvars != null);

       Contract.Requires(missingBounds != null);

@@ -5010,29 +5010,29 @@ namespace Microsoft.Dafny
       Contract.Ensures(

         (returnAllBounds && Contract.OldValue(missingBounds.Count) <= missingBounds.Count) ||

         (!returnAllBounds &&

-         Contract.Result<List<QuantifierExpr.BoundedPool>>() != null &&

-         Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count &&

+         Contract.Result<List<ComprehensionExpr.BoundedPool>>() != null &&

+         Contract.Result<List<ComprehensionExpr.BoundedPool>>().Count == bvars.Count &&

          Contract.OldValue(missingBounds.Count) == missingBounds.Count) ||

         (!returnAllBounds &&

-         Contract.Result<List<QuantifierExpr.BoundedPool>>() == null &&

+         Contract.Result<List<ComprehensionExpr.BoundedPool>>() == null &&

          Contract.OldValue(missingBounds.Count) < missingBounds.Count));

 

-      var bounds = new List<QuantifierExpr.BoundedPool>();

+      var bounds = new List<ComprehensionExpr.BoundedPool>();

       bool foundError = false;

       for (int j = 0; j < bvars.Count; j++) {

         var bv = bvars[j];

         if (bv.Type is BoolType) {

           // easy

-          bounds.Add(new QuantifierExpr.BoolBoundedPool());

+          bounds.Add(new ComprehensionExpr.BoolBoundedPool());

         } else if (bv.Type.IsIndDatatype && (bv.Type.AsIndDatatype).HasFinitePossibleValues) {

-          bounds.Add(new QuantifierExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

+          bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));

         } else {

           // Go through the conjuncts of the range expression to look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

           bool foundBoundsForBv = false;

           if (lowerBound != null) {

-            bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));

+            bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

             lowerBound = null;

             foundBoundsForBv = true;

           }

@@ -5050,34 +5050,34 @@ namespace Microsoft.Dafny
             switch (c.ResolvedOp) {

               case BinaryExpr.ResolvedOpcode.InSet:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

+                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.Subset:

                 if (returnAllBounds && whereIsBv == 1) {

-                  bounds.Add(new QuantifierExpr.SuperSetBoundedPool(e0));

+                  bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(e0));

                   foundBoundsForBv = true;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InMultiSet:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

+                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InSeq:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));

+                  bounds.Add(new ComprehensionExpr.SeqBoundedPool(e1));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InMap:

                 if (whereIsBv == 0) {

-                  bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

+                  bounds.Add(new ComprehensionExpr.SetBoundedPool(e1));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

@@ -5085,12 +5085,12 @@ namespace Microsoft.Dafny
               case BinaryExpr.ResolvedOpcode.EqCommon:

                 if (bv.Type is IntType) {

                   var otherOperand = whereIsBv == 0 ? e1 : e0;

-                  bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

+                  bounds.Add(new ComprehensionExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

                   foundBoundsForBv = true;

                   if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 } else if (returnAllBounds && bv.Type is SetType) {

                   var otherOperand = whereIsBv == 0 ? e1 : e0;

-                  bounds.Add(new QuantifierExpr.SuperSetBoundedPool(otherOperand));

+                  bounds.Add(new ComprehensionExpr.SuperSetBoundedPool(otherOperand));

                   foundBoundsForBv = true;

                 }

                 break;

@@ -5117,7 +5117,7 @@ namespace Microsoft.Dafny
             if ((lowerBound != null && upperBound != null) ||

                 (returnAllBounds && (lowerBound != null || upperBound != null))) {

               // we have found two halves

-              bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));

+                  bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));

               lowerBound = null;

               upperBound = null;

               foundBoundsForBv = true;