diff options
| author |  leino <unknown> | 2015-09-28 13:16:15 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 13:16:15 -0700 |
| commit | 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch) | |
| tree | cb89d6ef66c96bfa171f954898548f295a3cabc0 /Source/Dafny/Compiler.cs | |
| parent | ebaaa36321463925dc9030455e87ae17732b2353 (diff) | |
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.
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 477acabf..cdd968cf 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1566,6 +1566,9 @@ namespace Microsoft.Dafny { if (bound is ComprehensionExpr.BoolBoundedPool) {
Indent(ind);
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ Indent(ind);
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
Indent(ind);
@@ -1777,6 +1780,8 @@ namespace Microsoft.Dafny { Indent(ind);
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllChars) {{ @{1} = {0};", tmpVar, bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
@@ -2831,6 +2836,8 @@ namespace Microsoft.Dafny { // emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("Dafny.Helpers.QuantBool(");
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("Dafny.Helpers.QuantChar(");
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
wr.Write("Dafny.Helpers.QuantInt(");
@@ -2898,6 +2905,8 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[i];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
@@ -2971,6 +2980,8 @@ namespace Microsoft.Dafny { var bv = e.BoundVars[0];
if (bound is ComprehensionExpr.BoolBoundedPool) {
wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
} else if (bound is ComprehensionExpr.IntBoundedPool) {
var b = (ComprehensionExpr.IntBoundedPool)bound;
if (AsNativeType(bv.Type) != null) {
|