diff options
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 39 |
1 files changed, 36 insertions, 3 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1da5e7b2..ce693036 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1255,8 +1255,8 @@ namespace Microsoft.Dafny { wr.Write(e.SuffixName);
if (parensNeeded) { wr.Write(")"); }
- } else if (expr is FieldSelectExpr) {
- FieldSelectExpr e = (FieldSelectExpr)expr;
+ } else if (expr is MemberSelectExpr) {
+ MemberSelectExpr e = (MemberSelectExpr)expr;
// determine if parens are needed
int opBindingStrength = 0x70;
bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&
@@ -1268,7 +1268,7 @@ namespace Microsoft.Dafny { PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
wr.Write(".");
}
- wr.Write(e.FieldName);
+ wr.Write(e.MemberName);
if (parensNeeded) { wr.Write(")"); }
} else if (expr is SeqSelectExpr) {
@@ -1337,6 +1337,23 @@ namespace Microsoft.Dafny { wr.Write("]");
if (parensNeeded) { wr.Write(")"); }
}
+ } else if (expr is ApplyExpr) {
+ var e = (ApplyExpr)expr;
+ // determine if parens are needed
+ int opBindingStrength = 0x70;
+ bool parensNeeded =
+ opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
+
+ if (parensNeeded) { wr.Write("("); }
+
+ PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ wr.Write("(");
+ PrintExpressionList(e.Args, false);
+ wr.Write(")");
+
+ if (parensNeeded) { wr.Write(")"); }
+
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
// determine if parens are needed
@@ -1626,6 +1643,22 @@ namespace Microsoft.Dafny { wr.Write(" :: ");
PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);
if (parensNeeded) { wr.Write(")"); }
+
+ } else if (expr is LambdaExpr) {
+ var e = (LambdaExpr)expr;
+ wr.Write("(");
+ wr.Write(Util.Comma(e.BoundVars, bv => bv.DisplayName + ":" + bv.Type));
+ wr.Write(")");
+ if (e.Range != null) {
+ wr.Write(" requires ");
+ PrintExpression(e.Range, false);
+ }
+ foreach (var read in e.Reads) {
+ wr.Write(" reads ");
+ PrintExpression(read.E, false);
+ }
+ wr.Write(e.OneShot ? " -> " : " => ");
+ PrintExpression(e.Body, isFollowedBySemicolon);
} else if (expr is WildcardExpr) {
wr.Write("*");
|