Changed calc syntax (custom operators are now written before the hint)

6 files changed, 21 insertions, 19 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index daf3cc67..79d4cb64 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1328,10 +1328,9 @@ CalcStmt<out Statement/*!*/ s>
                                                           .)

   ]

   "{"

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

+  [ Expression<out e>                                     (. lines.Add(e); customOp = null; .)

     ";"

     {

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

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

                                                              if (maybeOp == null) {

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

@@ -1341,7 +1340,8 @@ CalcStmt<out Statement/*!*/ s>
                                                              }

                                                           .)

       ]                                                   (. customOps.Add(customOp); .)

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

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

+      Expression<out e>                                   (. lines.Add(e); customOp = null; .)

       ";"

     }

   ]

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 62898785..72b0a3f9 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1835,11 +1835,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(6);

 		if (StartOf(14)) {

 			Expression(out e);

-			lines.Add(e); 

+			lines.Add(e); customOp = null; 

 			Expect(15);

 			while (StartOf(19)) {

-				Hint(out h);

-				hints.Add(h); customOp = null; 

 				if (StartOf(18)) {

 					CalcOp(out opTok, out op);

 					maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);

@@ -1852,8 +1850,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					

 				}

 				customOps.Add(customOp); 

+				Hint(out h);

+				hints.Add(h); 

 				Expression(out e);

-				lines.Add(e); 

+				lines.Add(e); customOp = null; 

 				Expect(15);

 			}

 		}

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index 9e44f62e..80775896 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -12,8 +12,8 @@ method CalcTest0(s: seq<int>) {
 	if (|s| > 0) {
 		calc {
 			s[0]; // OK: well-formed in this context
-			{ assert s[0] == s[0]; }
-			<= s[0];
+			<= { assert s[0] == s[0]; }
+			s[0];
 		}
 	}
 }
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index 1caffe0c..eb7ae766 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -239,8 +239,9 @@ method FindWinner'<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns
         2 * Count(a, up, |a|, K);

         { Lemma_Split(a, lo, up, |a|, K); }

         2 * Count(a, lo, |a|, K) - 2 * Count(a, lo, up, K);

-        { assert HasMajority(a, lo, |a|, K); } // loop invariant (1)

-        > |a| - lo - 2 * Count(a, lo, up, K);

+        > { assert HasMajority(a, lo, |a|, K); } // loop invariant (1)

+        |a| - lo - 2 * Count(a, lo, up, K);

+        >= 

         { if (k == K) {

             calc {

               2 * Count(a, lo, up, K);              

@@ -251,15 +252,15 @@ method FindWinner'<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns
           } else {

             calc {

               2 * Count(a, lo, up, K);

-              { Lemma_Unique(a, lo, up, k, K); }

-              <= 2 * ((up - lo) - Count(a, lo, up, k));

+              <= { Lemma_Unique(a, lo, up, k, K); }

+              2 * ((up - lo) - Count(a, lo, up, k));

               { assert 2 * Count(a, lo, up, k) == up - lo; } // k has 50% among a[lo..up]

               up - lo;

             }

           }

           assert 2 * Count(a, lo, up, K) <= up - lo;

         }

-        >= |a| - lo - (up - lo);

+        |a| - lo - (up - lo);

         |a| - up;

       }

       assert HasMajority(a, up, |a|, K);

@@ -323,6 +324,7 @@ method FindWinner''<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) return
         2 * Count(a, lo, |a|, K) > |a| - lo;

         { Lemma_Split(a, lo, up, |a|, K); }

         2 * Count(a, lo, up, K) + 2 * Count(a, up, |a|, K) > |a| - lo;

+        ==> 

         { if (k == K) {

             calc {

               2 * Count(a, lo, up, K);

@@ -343,7 +345,7 @@ method FindWinner''<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) return
           assert 2 * Count(a, lo, up, K) <= up - lo;

         }

         // subtract off Count(a, lo, up, K) from the LHS and subtract off the larger amount up - lo from the RHS

-        ==> 2 * Count(a, up, |a|, K) > (|a| - lo) - (up - lo);

+        2 * Count(a, up, |a|, K) > (|a| - lo) - (up - lo);

         2 * Count(a, up, |a|, K) > |a| - up;

         HasMajority(a, up, |a|, K);

       }	

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index c94c18d2..dcd41077 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -19,8 +19,8 @@ method M(a: int, b: int, c: int, x: int)
     f(f(a, b), c);

     { assert f(a, b) == x; }

     f(x, c);

-    { assert c <= x; Monotonicity(c, x); }

-    <= f(x, x);

+    <= { assert c <= x; Monotonicity(c, x); }

+    f(x, x);

     { DiagonalIdentity(x); }

     x;

   }

diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index d3ff244a..7497618c 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -28,8 +28,8 @@ ghost method lemma_ping(j: nat, n: nat)
       j <= n;

       { lemma_ping(j - 1, n - 1); }

       j - 1 <= f(n - 1);

-      { lemma_ping(j - 1, f(n - 1)); }

-      ==> j - 1 <= f(f(n - 1));

+      ==> { lemma_ping(j - 1, f(n - 1)); }

+      j - 1 <= f(f(n - 1));

       // (0)

       j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);

       ==> j - 1 < f(n);