diff options
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 29 |
1 files changed, 26 insertions, 3 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 24375f7b..d9b6abae 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1371,9 +1371,9 @@ namespace Microsoft.Dafny { if (parensNeeded) { wr.Write("("); }
wr.Write("var ");
string sep = "";
- foreach (var v in e.Vars) {
- wr.Write("{0}{1}", sep, v.DisplayName);
- PrintType(": ", v.Type);
+ foreach (var lhs in e.LHSs) {
+ wr.Write(sep);
+ PrintCasePattern(lhs);
sep = ", ";
}
if (e.Exact) {
@@ -1529,6 +1529,29 @@ namespace Microsoft.Dafny { }
}
+ void PrintCasePattern(CasePattern pat) {
+ Contract.Requires(pat != null);
+ var v = pat.Var;
+ if (v != null) {
+ wr.Write(v.DisplayName);
+ if (v.Type is NonProxyType || DafnyOptions.O.DafnyPrintResolvedFile != null) {
+ PrintType(": ", v.Type);
+ }
+ } else {
+ wr.Write(pat.Id);
+ if (pat.Arguments != null) {
+ wr.Write("(");
+ var sep = "";
+ foreach (var arg in pat.Arguments) {
+ wr.Write(sep);
+ PrintCasePattern(arg);
+ sep = ", ";
+ }
+ wr.Write(")");
+ }
+ }
+ }
+
private void PrintQuantifierDomain(List<BoundVar> boundVars, Attributes attrs, Expression range) {
Contract.Requires(boundVars != null);
string sep = "";
|