diff options
| author |  rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
| commit | d06300cc9bc9f9c7002fb8e555cf172053cdfa5c (patch) | |
| tree | 6c19f930d2b568d7d5128b0642e9d823f6014d6b /Dafny/Printer.cs | |
| parent | bd9003ec46d72f74c3284a63713336da630769ff (diff) | |
Dafny: added "choose" operator on sets
Diffstat (limited to 'Dafny/Printer.cs')
| -rw-r--r-- | Dafny/Printer.cs | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 0b6d4446..629a0f89 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -834,18 +834,29 @@ namespace Microsoft.Dafny { string op;
int opBindingStrength;
switch (e.Op) {
+ case UnaryExpr.Opcode.SetChoose:
+ op = "choose"; opBindingStrength = -1; break;
case UnaryExpr.Opcode.Not:
op = "!"; opBindingStrength = 0x60; break;
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary opcode
}
- bool parensNeeded = opBindingStrength < contextBindingStrength ||
- (fragileContext && opBindingStrength == contextBindingStrength);
+ if (opBindingStrength == -1) {
+ // print as a function
+ wr.Write(op);
+ wr.Write("(");
+ PrintExpression(e.E);
+ wr.Write(")");
+ } else {
+ // print as an operator
+ bool parensNeeded = opBindingStrength < contextBindingStrength ||
+ (fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded) { wr.Write("("); }
- wr.Write(op);
- PrintExpr(e.E, opBindingStrength, false, -1);
- if (parensNeeded) { wr.Write(")"); }
+ if (parensNeeded) { wr.Write("("); }
+ wr.Write(op);
+ PrintExpr(e.E, opBindingStrength, false, -1);
+ if (parensNeeded) { wr.Write(")"); }
+ }
}
} else if (expr is BinaryExpr) {
|