Changed computation of ghosts until pass 2 of resolution.

Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.

1 files changed, 13 insertions, 0 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index d1a3c092..4dda19fe 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1012,6 +1012,12 @@ namespace Dafny
         return pred(false) || pred(true);

       }

     }

+    public static bool QuantChar(bool frall, System.Predicate<char> pred) {

+      for (int i = 0; i < 0x10000; i++) {

+        if (pred((char)i) != frall) { return !frall; }

+      }

+      return frall;

+    }

     public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {

       for (BigInteger i = lo; i < hi; i++) {

         if (pred(i) != frall) { return !frall; }

@@ -1051,6 +1057,13 @@ namespace Dafny
         yield return true;

       }

     }

+    public static IEnumerable<char> AllChars {

+      get {

+        for (int i = 0; i < 0x10000; i++) {

+          yield return (char)i;

+        }

+      }

+    }

     public static IEnumerable<BigInteger> AllIntegers {

       get {

         yield return new BigInteger(0);