Fixed pretty printing of calc statements to use the new(-since-long) format.

Disallow dangling operator in calc (which had also allowed soundness bug).
Don't reprove the test files in dafny0 after testing their pretty printing.

6 files changed, 176 insertions, 297 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2a7aec1e..9432b54d 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1451,9 +1451,10 @@ CalcStmt<out Statement/*!*/ s>
      Expression/*!*/ e;

      BlockStmt/*!*/ h;

      IToken opTok;

+     IToken danglingOperator = null;

   .)

   "calc"                                                  (. x = t; .)

-  [ CalcOp<out opTok, out calcOp>                         (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-trasitive calcOp (like !=)

+  [ CalcOp<out opTok, out calcOp>                         (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)

                                                              if (maybeOp == null) {

                                                                SemErr(opTok, "the main operator of a calculation must be transitive");

                                                              }

@@ -1461,26 +1462,32 @@ CalcStmt<out Statement/*!*/ s>
                                                           .)

   ]

   "{"

-  { Expression<out e>                                     (. lines.Add(e); stepOp = calcOp; .)

+  { Expression<out e>                                     (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .)

     ";"

     [ CalcOp<out opTok, out op>                           (. maybeOp = resOp.ResultOp(op);

                                                              if (maybeOp == null) {

                                                                SemErr(opTok, "this operator cannot continue this calculation");

                                                              } else {

                                                                stepOp = op;

-                                                               resOp = maybeOp;                                                              

+                                                               resOp = maybeOp;

+                                                               danglingOperator = opTok;

                                                              }

                                                           .)

     ]                                                   (. stepOps.Add(stepOp); .)

-    Hint<out h>                                         (. hints.Add(h); .)

+    Hint<out h>                                         (. hints.Add(h);

+                                                           if (h.Body.Count != 0) { danglingOperator = null; }

+                                                        .)

   }

   "}"

   (.

+    if (danglingOperator != null) {

+      SemErr(danglingOperator, "a calculation cannot end with an operator");

+    }

     if (lines.Count > 0) {

-	  // Repeat the last line to create a dummy line for the dangling hint

-	  lines.Add(lines[lines.Count - 1]);

+      // Repeat the last line to create a dummy line for the dangling hint

+      lines.Add(lines[lines.Count - 1]);

     }  

-	s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); 

+    s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); 

   .)

   .

 CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 9f7e96bb..4e0611f7 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1989,12 +1989,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ e;

 		BlockStmt/*!*/ h;

 		IToken opTok;

+		IToken danglingOperator = null;

 		

 		Expect(85);

 		x = t; 

 		if (StartOf(21)) {

 			CalcOp(out opTok, out calcOp);

-			maybeOp = calcOp.ResultOp(calcOp); // guard against non-trasitive calcOp (like !=)

+			maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=)

 			if (maybeOp == null) {

 			 SemErr(opTok, "the main operator of a calculation must be transitive");

 			}

@@ -2004,7 +2005,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(8);

 		while (StartOf(16)) {

 			Expression(out e);

-			lines.Add(e); stepOp = calcOp; 

+			lines.Add(e); stepOp = calcOp; danglingOperator = null; 

 			Expect(7);

 			if (StartOf(21)) {

 				CalcOp(out opTok, out op);

@@ -2013,18 +2014,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				 SemErr(opTok, "this operator cannot continue this calculation");

 				} else {

 				 stepOp = op;

-				 resOp = maybeOp;                                                              

+				 resOp = maybeOp;

+				 danglingOperator = opTok;

 				}

 				

 			}

 			stepOps.Add(stepOp); 

 			Hint(out h);

-			hints.Add(h); 

+			hints.Add(h);

+			if (h.Body.Count != 0) { danglingOperator = null; }

+			

 		}

 		Expect(9);

+		if (danglingOperator != null) {

+		 SemErr(danglingOperator, "a calculation cannot end with an operator");

+		}

 		if (lines.Count > 0) {

-		// Repeat the last line to create a dummy line for the dangling hint

-		lines.Add(lines[lines.Count - 1]);

+		 // Repeat the last line to create a dummy line for the dangling hint

+		 lines.Add(lines[lines.Count - 1]);

 		}  

 		s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); 

 		

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 868d73f5..a7ca8f96 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -669,27 +669,34 @@ namespace Microsoft.Dafny {
         }

         wr.WriteLine("{");

         int lineInd = indent + IndentAmount;

-        if (s.Lines.Count > 0) {

+        int lineCount = s.Lines.Count == 0 ? 0 : s.Lines.Count - 1;  // if nonempty, .Lines always contains a duplicated last line

+        // The number of op/hints is commonly one less than the number of lines, but

+        // it can also equal the number of lines for empty calc's and for calc's with

+        // a dangling hint.

+        int hintCount = s.Lines.Count != 0 && s.Hints.Last().Body.Count == 0 ? lineCount - 1 : lineCount;

+        for (var i = 0; i < lineCount; i++) {

+          var e = s.Lines[i];

+          var op = s.StepOps[i];

+          var h = s.Hints[i];

+          // print the line

           Indent(lineInd);

-          PrintExpression(s.Lines.First(), lineInd);

+          PrintExpression(e, lineInd);

           wr.WriteLine(";");

-        }

-        for (var i = 1; i < s.Lines.Count; i++){

-          var e = s.Lines[i];

-          var h = s.Hints[i - 1];

-          var op = s.StepOps[i - 1];

+          if (i == hintCount) {

+            break;

+          }

+          // print the operator, if any

+          if (!s.Op.Equals(op)) {

+            Indent(indent);  // this lines up with the "calc"

+            PrintCalcOp(op);

+            wr.WriteLine();

+          }

+          // print the hints

           foreach (var st in h.Body) {

             Indent(lineInd);

             PrintStatement(st, lineInd);

             wr.WriteLine();

           }

-          Indent(lineInd);

-          if (!s.Op.Equals(op)) {

-            PrintCalcOp(op);

-            wr.Write(" ");

-          }

-          PrintExpression(e, lineInd);

-          wr.WriteLine(";");

         }

         Indent(indent);

         wr.Write("}");

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a1dd639f..045900ae 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1824,34 +1824,6 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met
 TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods

 5 resolution/type errors detected in TailCalls.dfy

 

--------------------- Calculations.dfy --------------------

-Calculations.dfy(3,4): Error: index out of range

-Execution trace:

-    (0,0): anon0

-    (0,0): anon24_Then

-Calculations.dfy(8,13): Error: index out of range

-Execution trace:

-    (0,0): anon0

-    (0,0): anon26_Then

-Calculations.dfy(8,17): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon26_Then

-Calculations.dfy(52,11): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    Calculations.dfy(47,2): anon5_Else

-Calculations.dfy(75,13): Error: index out of range

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-Calculations.dfy(75,17): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-

-Dafny program verifier finished with 6 verified, 6 errors

-

 -------------------- IteratorResolution.dfy --------------------

 IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field

 IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)

@@ -2259,209 +2231,51 @@ Execution trace:
     (0,0): anon0

 

 Dafny program verifier finished with 87 verified, 33 errors

-out.tmp.dfy(33,11): Error: index out of range

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(69,37): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-out.tmp.dfy(70,52): Error: possible division by zero

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Else

-    (0,0): anon3

-    (0,0): anon13_Else

-out.tmp.dfy(71,22): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    (0,0): anon12_Then

-    (0,0): anon3

-    (0,0): anon13_Then

-    (0,0): anon6

-out.tmp.dfy(88,24): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-    out.tmp.dfy(87,5): anon8_LoopHead

-    (0,0): anon8_LoopBody

-    (0,0): anon9_Then

-out.tmp.dfy(122,5): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

-out.tmp.dfy(135,9): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-out.tmp.dfy(137,9): Error: call may violate context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-out.tmp.dfy(177,9): Error: assignment may update an object field not in the enclosing context's modifies clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon22_Else

-    (0,0): anon24_Else

-    (0,0): anon26_Else

-    (0,0): anon28_Then

-    (0,0): anon29_Then

-    (0,0): anon19

-out.tmp.dfy(199,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Then

-out.tmp.dfy(205,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon3

-    (0,0): anon7_Then

-out.tmp.dfy(207,14): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon3

-    (0,0): anon7_Else

-out.tmp.dfy(245,24): Error BP5002: A precondition for this call might not hold.

-out.tmp.dfy(226,30): Related location: This is the precondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    out.tmp.dfy(242,19): anon3_Else

-    (0,0): anon2

-out.tmp.dfy(265,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(275,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-out.tmp.dfy(388,14): Error: assertion violation

+

+Dafny program verifier finished with 0 verified, 0 errors

+

+-------------------- LetExpr.dfy --------------------

+LetExpr.dfy(5,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    out.tmp.dfy(384,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    out.tmp.dfy(384,5): anon8_Else

-    (0,0): anon9_Then

-out.tmp.dfy(414,14): Error: assertion violation

+LetExpr.dfy(104,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

-    (0,0): anon3

-out.tmp.dfy(451,3): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(445,11): Related location: This is the postcondition that might not hold.

+    (0,0): anon11_Then

+

+Dafny program verifier finished with 28 verified, 2 errors

+

+Dafny program verifier finished with 0 verified, 0 errors

+

+-------------------- Calculations.dfy --------------------

+Calculations.dfy(3,6): Error: index out of range

 Execution trace:

     (0,0): anon0

-    (0,0): anon18_Else

-    (0,0): anon23_Then

     (0,0): anon24_Then

-    (0,0): anon15

-    (0,0): anon25_Else

-out.tmp.dfy(475,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon7

-out.tmp.dfy(480,10): Error: assertion violation

+Calculations.dfy(8,15): Error: index out of range

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(490,4): Error: cannot prove termination; try supplying a decreases clause

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-out.tmp.dfy(498,10): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(499,41): Related location: This is the postcondition that might not hold.

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-out.tmp.dfy(544,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

-out.tmp.dfy(558,20): Error: left-hand sides 0 and 1 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-    (0,0): anon28_Then

-    (0,0): anon4

-    (0,0): anon29_Then

-    (0,0): anon30_Then

-    (0,0): anon9

-    (0,0): anon31_Then

-    (0,0): anon32_Then

-    (0,0): anon12

-out.tmp.dfy(560,15): Error: left-hand sides 1 and 2 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon27_Then

-    out.tmp.dfy(553,17): anon28_Else

-    (0,0): anon4

-    (0,0): anon29_Else

-    (0,0): anon30_Then

-    (0,0): anon9

-    (0,0): anon31_Else

-    (0,0): anon35_Then

-    (0,0): anon36_Then

-    (0,0): anon37_Then

-    (0,0): anon22

-    (0,0): anon38_Then

-out.tmp.dfy(567,25): Error: target object may be null

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(580,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(606,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(625,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon9_Then

-    (0,0): anon4

-    (0,0): anon10_Then

-    (0,0): anon7

-out.tmp.dfy(639,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

-Execution trace:

-    (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon6_Then

-    (0,0): anon3

-out.tmp.dfy(641,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+    (0,0): anon26_Then

+Calculations.dfy(8,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

-out.tmp.dfy(655,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+    (0,0): anon26_Then

+Calculations.dfy(52,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-

-Dafny program verifier finished with 87 verified, 33 errors

-

--------------------- LetExpr.dfy --------------------

-LetExpr.dfy(5,12): Error: assertion violation

+    Calculations.dfy(47,3): anon5_Else

+Calculations.dfy(75,15): Error: index out of range

 Execution trace:

     (0,0): anon0

-LetExpr.dfy(104,21): Error: assertion violation

+    (0,0): anon12_Then

+Calculations.dfy(75,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon11_Then

+    (0,0): anon12_Then

 

-Dafny program verifier finished with 28 verified, 2 errors

-out.tmp.dfy(66,12): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-out.tmp.dfy(157,21): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon11_Then

+Dafny program verifier finished with 9 verified, 6 errors

 

-Dafny program verifier finished with 28 verified, 2 errors

+Dafny program verifier finished with 0 verified, 0 errors

 

 Dafny program verifier finished with 37 verified, 0 errors

 Compiled assembly into Compilation.exe

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 59191ac3..f10d2e45 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -1,29 +1,29 @@
 method CalcTest0(s: seq<int>) {
-	calc {
-		s[0]; // error: ill-formed line
-	}
-	
-	calc {
-		2;
-		{ assert s[0] == 1; } // error: ill-formed hint
-		1 + 1;
-	}
-	
-	if (|s| > 0) {
-		calc {
-			s[0]; // OK: well-formed in this context
-			<= { assert s[0] == s[0]; }
-			s[0];
-		}
-	}
-	assume forall x :: x in s ==> x >= 0;
-	calc {
-		0 < |s|;
-	==>	{ assert s[0] >= 0; }   // OK: well-formed after previous line
-		s[0] >= 0;                // OK: well-formed after previous line
+  calc {
+    s[0]; // error: ill-formed line
+  }
+  
+  calc {
+    2;
+    { assert s[0] == 1; } // error: ill-formed hint
+    1 + 1;
+  }
+  
+  if (|s| > 0) {
+    calc {
+      s[0]; // OK: well-formed in this context
+      <= { assert s[0] == s[0]; }
+      s[0];
+    }
+  }
+  assume forall x :: x in s ==> x >= 0;
+  calc {
+    0 < |s|;
+  ==>  { assert s[0] >= 0; }  // OK: well-formed after previous line
+    s[0] >= 0;                // OK: well-formed after previous line
   <==> { assert s[0] >= 0; }  // OK: well-formed when the previous line is well-formed
     s[0] > 0 || s[0] == 0;    // OK: well-formed when the previous line is well-formed
-	}
+  }
   
   calc { // same as the last one, but well-formedness is checked in reverse order
     s[0] + 1 > 0;
@@ -35,48 +35,92 @@ method CalcTest0(s: seq<int>) {
 }
 
 method CalcTest1(x: int, y: int) {
-	calc {
-		x + y;
-		{ assume x == 0; }
-		y;
-	}
-	assert x == 0; // OK: follows from x + y == y;
+  calc {
+    x + y;
+    { assume x == 0; }
+    y;
+  }
+  assert x == 0; // OK: follows from x + y == y;
 }
 
 method CalcTest2(x: int, y: int) {
-	calc {
-		x + y;
-		{ assume x == 0; }
-		y + x;
-	}
-	assert x == 0; // error: even though assumed above, is not exported by the calculation
+  calc {
+    x + y;
+    { assume x == 0; }
+    y + x;
+  }
+  assert x == 0; // error: even though assumed above, is not exported by the calculation
 }
 
 // calc expression:
 function CalcTest3(s: seq<int>): int {
-	calc < {
-		0;
-		{ assume |s| == 5; }
-		|s|;
-	}
-	s[0]
+  calc < {
+    0;
+    { assume |s| == 5; }
+    |s|;
+  }
+  s[0]
 }
 
 // dangling hints:
 method CalcTest4(s: seq<int>) 
-	requires forall n | n in s :: n > 0;
+  requires forall n | n in s :: n > 0;
 {
-	calc {
-		1 + 1;
-		{ assert 1 + 1 == 2; }
-	}
-	calc {
-		2;
-		{ assert s[0] > 0; } // error: ill-formed hint
-	}
-	calc {
-		|s| > 0;
-	==> { assert s[0] > 0; } // okay
-	}
-	
+  calc {
+    1 + 1;
+    { assert 1 + 1 == 2; }
+  }
+  calc {
+    2;
+    { assert s[0] > 0; } // error: ill-formed hint
+  }
+  calc {
+    |s| > 0;
+  ==> { assert s[0] > 0; } // okay
+  }
+  
 }
+
+// ------------- tests for the pretty printer -------------
+
+lemma CalcPrinting()
+{
+  calc < {
+    2;
+  <= { SubLemma(); }
+    3;
+    5;
+  < { assert 5 < 6 <= 5+1; SubLemma(); assert 6 < 7; }
+    7;
+    11;
+    { SubLemma(); } // dangling hint
+  }
+  calc < {
+    13;
+  }
+  calc {
+    17;
+  == { SubLemma(); }  // dangling hint, following operator
+  }
+  calc <= {
+    19;
+  <=
+    { SubLemma(); }
+    { assert 19 + 23 == 42; }
+    calc { 811; }
+    { assert 42 < 100; }
+    23;
+    { calc < {
+      71; { assert 71 % 19 != 0; } 73;
+    } }
+    29;
+    calc < {
+      311; 313; 331;
+    }
+    31;
+  }
+  calc {
+  }
+}
+
+lemma SubLemma()
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 61f7c2c2..ae80dc89 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -26,7 +26,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy

             Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

-            Calculations.dfy IteratorResolution.dfy Iterators.dfy

+            IteratorResolution.dfy Iterators.dfy

             RankPos.dfy RankNeg.dfy

             Computations.dfy ComputationsNeg.dfy

             Include.dfy) do (

@@ -41,11 +41,11 @@ for %%f in (Superposition.dfy) do (
   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f

 )

 

-for %%f in (SmallTests.dfy LetExpr.dfy) do (

+for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f

-  %DAFNY_EXE% /compile:0 %* out.tmp.dfy

+  %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy

 )

 

 %DAFNY_EXE% %* Compilation.dfy