diff options
| author |  Rustan Leino <unknown> | 2015-08-20 17:23:24 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-08-20 17:23:24 -0700 |
| commit | 566fdf1676e0d7d6060767febbfa7a0378300e99 (patch) | |
| tree | 48b9ddec4a84dd3242ebd39641f70a5d5cbd22c2 /Source/Dafny/Compiler.cs | |
| parent | 270b34fc36dcfc781e8f49df5339cb2e10e69828 (diff) | |
Fixed compilation that involve enumeration over native-type newtype values.
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 76 |
1 files changed, 48 insertions, 28 deletions
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);
|