diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-27 19:42:58 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 19:42:58 -0700 |
| commit | 3fb9221272adf771b4b01911ce7e06adee37285d (patch) | |
| tree | 5f59ef6d1fc6f4816bea452282584e4aaa1a97df /Source/Dafny/Compiler.cs | |
| parent | 5359bb957c6a18ee63bf2cede398d20829a97e7b (diff) | |
Dafny: fixed parsing bug that prevented all expressions from occurring in match-case expressions
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 86 |
1 files changed, 46 insertions, 40 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 4b59a386..0fbeb9d6 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -351,45 +351,7 @@ namespace Microsoft.Dafny { wr.Write("(");
WriteFormals("", f.Formals);
wr.WriteLine(") {");
- if (f.Body is MatchExpr) {
- MatchExpr me = (MatchExpr)f.Body;
- // Type source = e;
- // if (source._D is Dt_Ctor0) {
- // FormalType f0 = ((Dt_Ctor0)source._D).a0;
- // ...
- // return Body0;
- // } else if (...) {
- // ...
- // } else if (true) {
- // ...
- // }
-
- string source = "_source" + tmpVarCount;
- tmpVarCount++;
- Indent(indent);
- wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source);
- TrExpr(me.Source);
- wr.WriteLine(";");
-
- int i = 0;
- foreach (MatchCaseExpr mc in me.Cases) {
- MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
-
- Indent(indent + 2*IndentAmount);
- wr.Write("return ");
- TrExpr(mc.Body);
- wr.WriteLine(";");
- i++;
- }
-
- Indent(indent); wr.WriteLine("}");
-
- } else {
- Indent(indent + IndentAmount);
- wr.Write("return ");
- TrExpr(f.Body);
- wr.WriteLine(";");
- }
+ CompileReturnBody(f.Body, indent);
Indent(indent); wr.WriteLine("}");
}
@@ -450,7 +412,51 @@ namespace Microsoft.Dafny { }
}
}
-
+
+ void CompileReturnBody(Expression body, int indent) {
+ body = body.Resolved;
+ if (body is MatchExpr) {
+ MatchExpr me = (MatchExpr)body;
+ // Type source = e;
+ // if (source._D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
+ // ...
+ // return Body0;
+ // } else if (...) {
+ // ...
+ // } else if (true) {
+ // ...
+ // }
+
+ string source = "_source" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent);
+ wr.Write("{0} {1} = ", TypeName(cce.NonNull(me.Source.Type)), source);
+ TrExpr(me.Source);
+ wr.WriteLine(";");
+
+ if (me.Cases.Count == 0) {
+ // the verifier would have proved we never get here; still, we need some code that will compile
+ Indent(indent);
+ wr.WriteLine("throw new System.Exception();");
+ } else {
+ int i = 0;
+ foreach (MatchCaseExpr mc in me.Cases) {
+ MatchCasePrelude(source, cce.NonNull(mc.Ctor), mc.Arguments, i, me.Cases.Count, indent + IndentAmount);
+ CompileReturnBody(mc.Body, indent + IndentAmount);
+ i++;
+ }
+ Indent(indent); wr.WriteLine("}");
+ }
+
+ } else {
+ Indent(indent + IndentAmount);
+ wr.Write("return ");
+ TrExpr(body);
+ wr.WriteLine(";");
+ }
+ }
+
// ----- Type ---------------------------------------------------------------------------------
readonly string DafnySetClass = "Dafny.Set";
|