Allowing dangling hints in calculations.

7 files changed, 107 insertions, 73 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 71dec0d7..f9dff93f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1393,10 +1393,9 @@ CalcStmt<out Statement/*!*/ s>
                                                           .)

   ]

   "{"

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

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

     ";"

-    {

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

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

                                                              if (maybeOp == null) {

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

                                                              } else {

@@ -1404,14 +1403,17 @@ CalcStmt<out Statement/*!*/ s>
                                                                resOp = maybeOp;                                                              

                                                              }

                                                           .)

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

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

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

-      ";"

-    }

-  ]

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

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

+  }

   "}"

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

+  (.

+    if (lines.Count > 0) {

+	  // 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); 

+  .)

   .

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

 = (. var binOp = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b58f392c..31e9b112 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3271,12 +3271,12 @@ namespace Microsoft.Dafny {
 

     }

 

-    public readonly List<Expression/*!*/> Lines;

+    public readonly List<Expression/*!*/> Lines;  // Last line is dummy, in order to form a proper step with the dangling hint

     public readonly List<BlockStmt/*!*/> Hints;   // Hints[i] comes after line i; block statement is used as a container for multiple sub-hints

     public readonly CalcOp/*!*/ Op;               // main operator of the calculation

     public readonly List<CalcOp/*!*/> StepOps;    // StepOps[i] comes after line i

     public CalcOp/*!*/ ResultOp;                  // conclusion operator

-    public readonly List<Expression/*!*/> Steps;  // expressions li op l<i + 1>, filled in during resolution

+    public readonly List<Expression/*!*/> Steps;  // expressions li op l<i + 1>, filled in during resolution (last step is dummy)

     public Expression Result;                     // expression l0 ResultOp ln, filled in during resolution

 

     public static readonly CalcOp/*!*/ DefaultOp = new BinaryCalcOp(BinaryExpr.Opcode.Eq); 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index daf3763c..3e427747 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1914,32 +1914,32 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 		}

 		Expect(6);

-		if (StartOf(15)) {

+		while (StartOf(15)) {

 			Expression(out e);

 			lines.Add(e); stepOp = calcOp; 

 			Expect(19);

-			while (StartOf(21)) {

-				if (StartOf(20)) {

-					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;                                                              

-					}

-					

+			if (StartOf(20)) {

+				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;                                                              

 				}

-				stepOps.Add(stepOp); 

-				Hint(out h);

-				hints.Add(h); 

-				Expression(out e);

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

-				Expect(19);

+				

 			}

+			stepOps.Add(stepOp); 

+			Hint(out h);

+			hints.Add(h); 

 		}

 		Expect(7);

+		if (lines.Count > 0) {

+		// 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); 

+		

 	}

 

 	void ReturnStmt(out Statement/*!*/ s) {

@@ -1955,7 +1955,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 			returnTok = t; isYield = true; 

 		} else SynErr(182);

-		if (StartOf(22)) {

+		if (StartOf(21)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

 			while (la.kind == 28) {

@@ -2070,7 +2070,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 20 || la.kind == 68) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(23)) {

+		} else if (StartOf(22)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

 			while (la.kind == 20 || la.kind == 68) {

@@ -2134,7 +2134,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		decreases = new List<Expression/*!*/>();

 		mod = null;

 		

-		while (StartOf(24)) {

+		while (StartOf(23)) {

 			if (la.kind == 42 || la.kind == 75) {

 				Invariant(out invariant);

 				while (!(la.kind == 0 || la.kind == 19)) {SynErr(186); Get();}

@@ -2388,7 +2388,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpliesExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0);

-		if (StartOf(25)) {

+		if (StartOf(24)) {

 			if (la.kind == 91 || la.kind == 92) {

 				ImpliesOp();

 				x = t; 

@@ -2412,7 +2412,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void LogicalExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

-		if (StartOf(26)) {

+		if (StartOf(25)) {

 			if (la.kind == 95 || la.kind == 96) {

 				AndOp();

 				x = t; 

@@ -2466,7 +2466,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(27)) {

+		if (StartOf(26)) {

 			RelOp(out x, out op, out k);

 			firstOpTok = x; 

 			Term(out e1);

@@ -2479,7 +2479,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 e = new TernaryExpr(x, op == BinaryExpr.Opcode.Eq ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp, k, e0, e1);

 			}

 			

-			while (StartOf(27)) {

+			while (StartOf(26)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

 				 ops = new List<BinaryExpr.Opcode>();

@@ -2746,7 +2746,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				}

 			} else if (la.kind == 1) {

 				MapComprehensionExpr(x, out e);

-			} else if (StartOf(28)) {

+			} else if (StartOf(27)) {

 				SemErr("map must be followed by literal in brackets or comprehension."); 

 			} else SynErr(201);

 			break;

@@ -3018,7 +3018,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(31);

-		} else if (StartOf(29)) {

+		} else if (StartOf(28)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

 		} else SynErr(210);

 	}

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

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(30)) {

+		if (StartOf(29)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 28) {

@@ -3372,7 +3372,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,T,T,x, x,x,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

 		{x,T,T,x, x,x,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

 		{x,T,T,x, x,x,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

 		{x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0fb2b3bb..573a221f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4035,17 +4035,19 @@ namespace Microsoft.Dafny
           ResolveExpression(e0, true, codeContext);

           Contract.Assert(e0.Type != null);  // follows from postcondition of ResolveExpression

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

-            var e1 = s.Lines[i];

-            ResolveExpression(e1, true, codeContext);

-            Contract.Assert(e1.Type != null);  // follows from postcondition of ResolveExpression

-            if (!UnifyTypes(e0.Type, e1.Type)) {

-              Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);

-            } else {

-              var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator                

-              ResolveExpression(step, true, codeContext);

-              s.Steps.Add(step);            

+            if (i < s.Lines.Count - 1 || prevErrorCount == ErrorCount) { // do not resolve the dummy step if there were errors, it might generate more errors

+              var e1 = s.Lines[i];

+              ResolveExpression(e1, true, codeContext);

+              Contract.Assert(e1.Type != null);  // follows from postcondition of ResolveExpression

+              if (!UnifyTypes(e0.Type, e1.Type)) {

+                Error(e1, "all lines in a calculation must have the same type (got {0} after {1})", e1.Type, e0.Type);

+              } else {

+                var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator                

+                ResolveExpression(step, true, codeContext);

+                s.Steps.Add(step);            

+              }

+              e0 = e1;

             }

-            e0 = e1;

           }

                   

           // clear the labels for the duration of checking the hints, because break statements are not allowed to leave a forall statement

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 356b36a7..2d01f59d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5236,8 +5236,10 @@ namespace Microsoft.Dafny {
         if (s.Lines.Count > 0) {          

           Bpl.IfCmd ifCmd = null;

           Bpl.StmtListBuilder b;

+          // if the dangling hint is empty, do not generate anything for the dummy step

+          var stepCount = s.Hints.Last().Body.Count == 0 ? s.Steps.Count - 1 : s.Steps.Count; 

           // check steps:

-          for (int i = s.Steps.Count; 0 <= --i; ) {            

+          for (int i = stepCount; 0 <= --i; ) {            

             b = new Bpl.StmtListBuilder();

             // assume wf[line<i>]:

             AddComment(b, stmt, "assume wf[lhs]");

@@ -5252,24 +5254,26 @@ namespace Microsoft.Dafny {
             // hint:

             AddComment(b, stmt, "Hint" + i.ToString());

             TrStmt(s.Hints[i], b, locals, etran);

-            // check well formedness of the goal line:

-            AddComment(b, stmt, "assert wf[rhs]");

-            if (s.Steps[i] is TernaryExpr) {

-              // check the prefix-equality limit

-              var index = ((TernaryExpr) s.Steps[i]).E0;

-              b.Add(AssertNS(index.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(index)), "prefix-equality limit must be at least 0"));

-            }

-            TrStmt_CheckWellformed(CalcStmt.Rhs(s.Steps[i]), b, locals, etran, false);

-            bool splitHappened;

-            var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);

-            // assert step:

-            AddComment(b, stmt, "assert line" + i.ToString() + " " + s.StepOps[i].ToString() + " line" + (i + 1).ToString());

-            if (!splitHappened) {

-              b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));

-            } else {

-              foreach (var split in ss) {

-                if (split.IsChecked) {

-                  b.Add(AssertNS(s.Lines[i + 1].tok, split.E, "the calculation step between the previous line and this line might not hold"));

+            if (i < s.Steps.Count - 1) { // non-dummy step

+              // check well formedness of the goal line:

+              AddComment(b, stmt, "assert wf[rhs]");

+              if (s.Steps[i] is TernaryExpr) {

+                // check the prefix-equality limit

+                var index = ((TernaryExpr) s.Steps[i]).E0;

+                b.Add(AssertNS(index.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(index)), "prefix-equality limit must be at least 0"));

+              }

+              TrStmt_CheckWellformed(CalcStmt.Rhs(s.Steps[i]), b, locals, etran, false);

+              bool splitHappened;

+              var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);

+              // assert step:

+              AddComment(b, stmt, "assert line" + i.ToString() + " " + s.StepOps[i].ToString() + " line" + (i + 1).ToString());

+              if (!splitHappened) {

+                b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));

+              } else {

+                foreach (var split in ss) {

+                  if (split.IsChecked) {

+                    b.Add(AssertNS(s.Lines[i + 1].tok, split.E, "the calculation step between the previous line and this line might not hold"));

+                  }

                 }

               }

             }

@@ -5285,7 +5289,7 @@ namespace Microsoft.Dafny {
           ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);

           builder.Add(ifCmd);

           // assume result:

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

+          if (s.Steps.Count > 1) {            

             builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));

           }

         }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 38b7c120..769c66ca 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1685,8 +1685,16 @@ 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 5 verified, 4 errors

+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

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 54a9a3d4..59191ac3 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -60,4 +60,23 @@ function CalcTest3(s: seq<int>): int {
 		|s|;
 	}
 	s[0]
-}
\ No newline at end of file
+}
+
+// dangling hints:
+method CalcTest4(s: seq<int>) 
+	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
+	}
+	
+}