Fix printing for ForallStmt. Previously we traverse the resolved forall

expressions to get the attributes for the forallstmt, which is flawed since the
forallexpr could have been splitted into different subquantifiers each with
different triggers.  PrintExpression already knows how to print out
splitted forall expressions, so we use it to print the resolved forall
expressions instead.

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 {