summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Printer.cs174
1 files changed, 82 insertions, 92 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 6010e2f0..accdb9d3 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -842,25 +842,23 @@ namespace Microsoft.Dafny {
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
- Attributes attributes = s.Attributes;
- if (attributes == null && s.ForallExpressions != null) {
- foreach (Expression expr in s.ForallExpressions) {
- ForallExpr e = (ForallExpr)expr;
- attributes = GetSomeAttributes(e);
- if (attributes != null) { break; }
+ if (s.ForallExpressions != null) {
+ foreach (var expr in s.ForallExpressions) {
+ PrintExpression(expr, false, " ensures ");
+ }
+ } else {
+ wr.Write("forall");
+ if (s.BoundVars.Count != 0) {
+ wr.Write(" ");
+ PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
+ }
+ if (s.Ens.Count == 0) {
+ wr.Write(" ");
+ } else {
+ wr.WriteLine();
+ PrintSpec("ensures", s.Ens, indent + IndentAmount, s.Body != null);
+ Indent(indent);
}
- }
- wr.Write("forall");
- if (s.BoundVars.Count != 0) {
- wr.Write(" ");
- PrintQuantifierDomain(s.BoundVars, attributes, s.Range);
- }
- if (s.Ens.Count == 0) {
- wr.Write(" ");
- } else {
- wr.WriteLine();
- PrintSpec("ensures", s.Ens, indent + IndentAmount, s.Body != null);
- Indent(indent);
}
if (s.Body != null) {
PrintStatement(s.Body, indent);
@@ -1007,20 +1005,6 @@ namespace Microsoft.Dafny {
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
- }
-
- private static Attributes GetSomeAttributes(Expression expr) {
- if (expr is ForallExpr) {
- var e = (ForallExpr)expr;
- if (e.Attributes != null) {
- return e.Attributes;
- }
- return GetSomeAttributes(e.SplitQuantifierExpression);
- } else if (expr is BinaryExpr) {
- var e = (BinaryExpr)expr;
- return GetSomeAttributes(e.E0) ?? GetSomeAttributes(e.E1);
- }
- return null;
}
private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {
@@ -1328,6 +1312,11 @@ namespace Microsoft.Dafny {
public void PrintExpression(Expression expr, bool isFollowedBySemicolon, int indent) {
Contract.Requires(expr != null);
PrintExpr(expr, 0, false, true, isFollowedBySemicolon, indent);
+ }
+
+ public void PrintExpression(Expression expr, bool isFollowedBySemicolon, string keyword) {
+ Contract.Requires(expr != null);
+ PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1, keyword);
}
private bool ParensNeeded(int opBindingStrength, int contextBindingStrength, bool fragileContext) {
@@ -1338,7 +1327,7 @@ namespace Microsoft.Dafny {
/// <summary>
/// An indent of -1 means print the entire expression on one line.
/// </summary>
- void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, bool isRightmost, bool isFollowedBySemicolon, int indent, int resolv_count = 2)
+ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, bool isRightmost, bool isFollowedBySemicolon, int indent, string keyword = null, int resolv_count = 2 )
{
Contract.Requires(-1 <= indent);
Contract.Requires(expr != null);
@@ -1439,8 +1428,8 @@ namespace Microsoft.Dafny {
ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
if (parensNeeded) { wr.Write("("); }
- if (!e.Lhs.IsImplicit) {
- PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ if (!e.Lhs.IsImplicit) {
+ PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
wr.Write(".");
}
wr.Write(e.SuffixName);
@@ -1459,8 +1448,8 @@ namespace Microsoft.Dafny {
wr.Write("(");
PrintExpression(e.Lhs, false);
wr.Write(")");
- } else {
- PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ } else {
+ PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
}
wr.Write("(");
PrintExpressionList(e.Args, false);
@@ -1475,8 +1464,8 @@ namespace Microsoft.Dafny {
ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
if (parensNeeded) { wr.Write("("); }
- if (!(e.Obj.IsImplicit)) {
- PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ if (!(e.Obj.IsImplicit)) {
+ PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
wr.Write(".");
}
wr.Write(e.MemberName);
@@ -1488,8 +1477,8 @@ namespace Microsoft.Dafny {
int opBindingStrength = 0x70;
bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
- if (parensNeeded) { wr.Write("("); }
- PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+ if (parensNeeded) { wr.Write("("); }
+ PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent, keyword);
wr.Write("[");
if (e.SelectOne) {
Contract.Assert( e.E0 != null);
@@ -1512,8 +1501,8 @@ namespace Microsoft.Dafny {
int opBindingStrength = 0x70;
bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
- if (parensNeeded) { wr.Write("("); }
- PrintExpr(e.Array, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+ if (parensNeeded) { wr.Write("("); }
+ PrintExpr(e.Array, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent, keyword);
string prefix = "[";
foreach (Expression idx in e.Indices) {
Contract.Assert(idx != null);
@@ -1527,8 +1516,8 @@ namespace Microsoft.Dafny {
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
if (e.ResolvedUpdateExpr != null)
- {
- PrintExpr(e.ResolvedUpdateExpr, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+ {
+ PrintExpr(e.ResolvedUpdateExpr, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, keyword);
}
else
{
@@ -1536,8 +1525,8 @@ namespace Microsoft.Dafny {
int opBindingStrength = 0x70;
bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
- if (parensNeeded) { wr.Write("("); }
- PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+ if (parensNeeded) { wr.Write("("); }
+ PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent, keyword);
wr.Write("[");
PrintExpression(e.Index, false);
wr.Write(" := ");
@@ -1553,7 +1542,7 @@ namespace Microsoft.Dafny {
bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
if (parensNeeded) { wr.Write("("); }
- PrintExpr(e.Root, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+ PrintExpr(e.Root, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent, keyword);
wr.Write(".(");
var sep = "";
foreach (var update in e.Updates) {
@@ -1570,9 +1559,9 @@ namespace Microsoft.Dafny {
int opBindingStrength = 0x70;
bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
- if (parensNeeded) { wr.Write("("); }
-
- PrintExpr(e.Function, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ if (parensNeeded) { wr.Write("("); }
+
+ PrintExpr(e.Function, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
wr.Write("(");
PrintExpressionList(e.Args, false);
wr.Write(")");
@@ -1587,8 +1576,8 @@ namespace Microsoft.Dafny {
ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
if (parensNeeded) { wr.Write("("); }
- if (!e.Receiver.IsImplicit) {
- PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+ if (!e.Receiver.IsImplicit) {
+ PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
wr.Write(".");
}
wr.Write(e.Name);
@@ -1643,8 +1632,8 @@ namespace Microsoft.Dafny {
((UnaryOpExpr)((ParensExpression)e.E).E).Op == UnaryOpExpr.Opcode.Not;
if (parensNeeded) { wr.Write("("); }
- wr.Write(op);
- PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);
+ wr.Write(op);
+ PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1, keyword);
if (parensNeeded) { wr.Write(")"); }
}
@@ -1703,31 +1692,31 @@ namespace Microsoft.Dafny {
string op = BinaryExpr.OpcodeString(e.Op);
if (parensNeeded) { wr.Write("("); }
var sem = !parensNeeded && isFollowedBySemicolon;
- if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {
- PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);
+ if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {
+ PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent, keyword);
wr.WriteLine(" {0}", op);
- Indent(indent);
- PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, indent);
- } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {
- PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);
+ Indent(indent);
+ PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, indent, keyword);
+ } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {
+ PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent, keyword);
wr.WriteLine(" {0}", op);
int ind = indent + IndentAmount;
- Indent(ind);
- PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);
- } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Exp) {
- PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, indent);
+ Indent(ind);
+ PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind, keyword);
+ } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Exp) {
+ PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, indent, keyword);
wr.WriteLine(" {0}", op);
int ind = indent + IndentAmount;
- Indent(ind);
- PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);
+ Indent(ind);
+ PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind, keyword);
} else if (e.Op == BinaryExpr.Opcode.Exp) {
- PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);
- wr.Write(" {0} ", op);
- PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);
- } else {
- PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, -1);
- wr.Write(" {0} ", op);
- PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);
+ PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1, keyword);
+ wr.Write(" {0} ", op);
+ PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1, keyword);
+ } else {
+ PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, -1, keyword);
+ wr.Write(" {0} ", op);
+ PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1, keyword);
}
if (parensNeeded) { wr.Write(")"); }
@@ -1746,12 +1735,12 @@ namespace Microsoft.Dafny {
(opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
if (parensNeeded) { wr.Write("("); }
- var sem = !parensNeeded && isFollowedBySemicolon;
- PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);
+ var sem = !parensNeeded && isFollowedBySemicolon;
+ PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1, keyword);
wr.Write(" {0}#[", e.Op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=");
PrintExpression(e.E0, false);
- wr.Write("] ");
- PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);
+ wr.Write("] ");
+ PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1, keyword);
if (parensNeeded) { wr.Write(")"); }
break;
default:
@@ -1769,8 +1758,8 @@ namespace Microsoft.Dafny {
(opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
if (parensNeeded) { wr.Write("("); }
- var sem = !parensNeeded && isFollowedBySemicolon;
- PrintExpr(e.Operands[0], opBindingStrength, true, false, sem, -1);
+ var sem = !parensNeeded && isFollowedBySemicolon;
+ PrintExpr(e.Operands[0], opBindingStrength, true, false, sem, -1, keyword);
for (int i = 0; i < e.Operators.Count; i++) {
string op = BinaryExpr.OpcodeString(e.Operators[i]);
if (e.PrefixLimits[i] == null) {
@@ -1779,8 +1768,8 @@ namespace Microsoft.Dafny {
wr.Write(" {0}#[", op);
PrintExpression(e.PrefixLimits[i], false);
wr.Write("] ");
- }
- PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), sem, -1);
+ }
+ PrintExpr(e.Operands[i + 1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), sem, -1, keyword);
}
if (parensNeeded) { wr.Write(")"); }
@@ -1808,8 +1797,8 @@ namespace Microsoft.Dafny {
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
- if (DafnyOptions.O.DafnyPrintResolvedFile != null && e.SplitQuantifier != null) {
- PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count);
+ if (DafnyOptions.O.DafnyPrintResolvedFile != null && e.SplitQuantifier != null) {
+ PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, keyword, resolv_count);
return;
}
@@ -1818,8 +1807,9 @@ namespace Microsoft.Dafny {
wr.Write(e is ForallExpr ? "forall" : "exists");
PrintTypeParams(e.TypeArgs); // new!
wr.Write(" ");
- PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);
- wr.Write(" :: ");
+ PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);
+ string s = keyword ?? " :: ";
+ wr.Write("{0}", s);
if (0 <= indent) {
int ind = indent + IndentAmount;
wr.WriteLine();
@@ -1925,8 +1915,8 @@ namespace Microsoft.Dafny {
} else if (expr is ParensExpression) {
var e = (ParensExpression)expr;
- // printing of parentheses is done optimally, not according to the parentheses in the given program
- PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+ // printing of parentheses is done optimally, not according to the parentheses in the given program
+ PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, keyword);
} else if (expr is NegationExpression) {
var e = (NegationExpression)expr;
@@ -1937,8 +1927,8 @@ namespace Microsoft.Dafny {
bool containsNestedNegation = e.E is ParensExpression && ((ParensExpression)e.E).E is NegationExpression;
if (parensNeeded) { wr.Write("("); }
- wr.Write(op);
- PrintExpr(e.E, opBindingStrength, containsNestedNegation, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);
+ wr.Write(op);
+ PrintExpr(e.E, opBindingStrength, containsNestedNegation, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1, keyword);
if (parensNeeded) { wr.Write(")"); }
} else if (expr is MatchExpr) {
@@ -1962,8 +1952,8 @@ namespace Microsoft.Dafny {
} else if (expr is BoxingCastExpr) {
// this is not expected for a parsed program, but we may be called for /trace purposes in the translator
- var e = (BoxingCastExpr)expr;
- PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+ var e = (BoxingCastExpr)expr;
+ PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, keyword);
} else if (expr is Translator.BoogieWrapper) {
wr.Write("[BoogieWrapper]"); // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here
} else {
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 21:41:38 +0000