Fixed compilation that involve enumeration over native-type newtype values.

5 files changed, 89 insertions, 29 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 7d3799d8..dfb8cf38 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1060,6 +1060,11 @@ namespace Dafny
         }

       }

     }

+    public static IEnumerable<BigInteger> IntegerRange(BigInteger lo, BigInteger hi) {

+      for (var j = lo; j < hi; j++) {

+        yield return j;

+      }

+    }

     // pre: b != 0

     // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

     public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index f2cc5d23..8bfa5fa9 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -117,7 +117,19 @@ namespace Microsoft.Dafny {
           } else if (d is TypeSynonymDecl) {

             // do nothing, just bypass type synonyms in the compiler

           } else if (d is NewtypeDecl) {

-            // do nothing, just bypass newtypes in the compiler

+            var nt = (NewtypeDecl)d;

+            Indent(indent);

+            wr.WriteLine("public class @{0} {{", nt.CompileName);

+            if (nt.NativeType != null) {

+              Indent(indent + IndentAmount);

+              wr.WriteLine("public static System.Collections.Generic.IEnumerable<{0}> IntegerRange(BigInteger lo, BigInteger hi) {{", nt.NativeType.Name);

+              Indent(indent + 2 * IndentAmount);

+              wr.WriteLine("for (var j = lo; j < hi; j++) {{ yield return ({0})j; }}", nt.NativeType.Name);

+              Indent(indent + IndentAmount);

+              wr.WriteLine("}");

+            }

+            Indent(indent);

+            wr.WriteLine("}");

           } else if (d is DatatypeDecl) {

             var dt = (DatatypeDecl)d;

             Indent(indent);

@@ -676,7 +688,7 @@ namespace Microsoft.Dafny {
     }

 

     string DtName(DatatypeDecl decl) {

-      return decl.Module.IsDefaultModule ? decl.CompileName : decl.FullCompileName;

+      return decl.FullCompileName;

     }

     string DtCtorName(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

@@ -1560,11 +1572,15 @@ namespace Microsoft.Dafny {
           } else if (bound is ComprehensionExpr.IntBoundedPool) {

             var b = (ComprehensionExpr.IntBoundedPool)bound;

             Indent(ind);

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

+            if (AsNativeType(bv.Type) != null) {

+              wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);

+            } else {

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

+            }

             TrExpr(b.LowerBound);

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

+            wr.Write(", ");

             TrExpr(b.UpperBound);

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

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

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

             Indent(ind);

@@ -1766,27 +1782,23 @@ namespace Microsoft.Dafny {
           wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is ComprehensionExpr.IntBoundedPool) {

           var b = (ComprehensionExpr.IntBoundedPool)bound;

-          // (tmpVar is not used in this case)

-          if (b.LowerBound != null) {

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

+          if (AsNativeType(bv.Type) != null) {

+            wr.Write("foreach (var @{0} in @{1}.IntegerRange(", tmpVar, bv.Type.AsNewtype.FullCompileName);

+          } else {

+            wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", tmpVar);

+          }

+          if (b.LowerBound == null) {

+            wr.Write("null");

+          } else {

             TrExpr(b.LowerBound);

-            wr.WriteLine(";");

-            Indent(ind);

-            if (b.UpperBound != null) {

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

-              TrExpr(b.UpperBound);

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

-            } else {

-              wr.WriteLine("for (;; @{0}++) {{ ", bv.CompileName);

-            }

+          }

+          wr.Write(", ");

+          if (b.UpperBound == null) {

+            wr.Write("null");

           } else {

-            Contract.Assert(b.UpperBound != null);

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

             TrExpr(b.UpperBound);

-            wr.WriteLine(";");

-            Indent(ind);

-            wr.WriteLine("for (;; @{0}--) {{ ", bv.CompileName);

           }

+          wr.WriteLine(")) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is AssignSuchThatStmt.WiggleWaggleBound) {

           wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllIntegers) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is ComprehensionExpr.SetBoundedPool) {

@@ -2891,11 +2903,15 @@ namespace Microsoft.Dafny {
             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

           } else if (bound is ComprehensionExpr.IntBoundedPool) {

             var b = (ComprehensionExpr.IntBoundedPool)bound;

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

+            if (AsNativeType(bv.Type) != null) {

+              wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);

+            } else {

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

+            }

             TrExpr(b.LowerBound);

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

+            wr.Write(", ");

             TrExpr(b.UpperBound);

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

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

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

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

@@ -2960,11 +2976,15 @@ namespace Microsoft.Dafny {
           wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

         } else if (bound is ComprehensionExpr.IntBoundedPool) {

           var b = (ComprehensionExpr.IntBoundedPool)bound;

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

+          if (AsNativeType(bv.Type) != null) {

+            wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);

+          } else {

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

+          }

           TrExpr(b.LowerBound);

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

+          wr.Write(", ");

           TrExpr(b.UpperBound);

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

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

         } else if (bound is ComprehensionExpr.SetBoundedPool) {

           var b = (ComprehensionExpr.SetBoundedPool)bound;

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

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 7328d8dd..d78ae170 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1967,7 +1967,11 @@ namespace Microsoft.Dafny {
     }

     public string FullCompileName {

       get {

-        return Module.CompileName + ".@" + CompileName;

+        if (!Module.IsDefaultModule) {

+          return Module.CompileName + ".@" + CompileName;

+        } else {

+          return CompileName;

+        }

       }

     }

   }

diff --git a/Test/dafny0/RangeCompilation.dfy b/Test/dafny0/RangeCompilation.dfy
new file mode 100644
index 00000000..de8ca68e
--- /dev/null
+++ b/Test/dafny0/RangeCompilation.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /compile:3 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+newtype Byte = x | 0 <= x < 256

+predicate method GoodByte(b: Byte) {

+  b % 3 == 2

+}

+predicate method GoodInteger(i: int) {

+  i % 5 == 4

+}

+

+method Main() {

+  assert GoodByte(11) && GoodInteger(24);

+  var b: Byte :| GoodByte(b);

+  var i: int :| 0 <= i < 256 && GoodInteger(i);

+  print "b=", b, "  i=", i, "\n";

+  var m0 := new MyClass;

+  var m17 := new M17.AnotherClass;

+}

+

+class MyClass { }

+

+module M17 {

+  class AnotherClass { }

+}

diff --git a/Test/dafny0/RangeCompilation.dfy.expect b/Test/dafny0/RangeCompilation.dfy.expect
new file mode 100644
index 00000000..c3275d12
--- /dev/null
+++ b/Test/dafny0/RangeCompilation.dfy.expect
@@ -0,0 +1,6 @@
+

+Dafny program verifier finished with 5 verified, 0 errors

+Program compiled successfully

+Running...

+

+b=2  i=4