summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyRuntime.cs5
-rw-r--r--Source/Dafny/Compiler.cs76
-rw-r--r--Source/Dafny/DafnyAst.cs6
-rw-r--r--Test/dafny0/RangeCompilation.dfy25
-rw-r--r--Test/dafny0/RangeCompilation.dfy.expect6
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 15:28:43 +0000