From 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 28 Sep 2015 13:16:15 -0700
Subject: 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.

---
 Binaries/DafnyRuntime.cs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'Binaries')

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);
-- 
cgit v1.2.3