Allow empty calc statements

7 files changed, 104 insertions, 91 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 646d6ee4..90ff7bc5 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -1230,30 +1230,31 @@ CalcStmt<out Statement/*!*/ s>
      Statement/*!*/ h;

      IToken bodyStart, bodyEnd, opTok;

   .)

-  "calc"                                                (. x = t; .)

-  [ CalcOp<out opTok, out calcOp> ]                     (. resOp = calcOp; .)

+  "calc"                                                  (. x = t; .)

+  [ CalcOp<out opTok, out calcOp> ]                       (. resOp = calcOp; .)

   "{"

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

-  ";"

-  { 

-    ( BlockStmt<out block, out bodyStart, out bodyEnd>  (. hints.Add(block); .)

-    | CalcStmt<out h>                                   (. hints.Add(h); .)

-    |                                                   (. hints.Add(null); .)

-    )

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

-                                                           if (maybeOp == null) {

-                                                             customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor

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

-                                                           } else {

-                                                             customOps.Add(op);

-                                                             resOp = (BinaryExpr.Opcode)maybeOp;                                                              

-                                                           }

-                                                        .)

-    |                                                   (. customOps.Add(null); .)

-    )

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

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

     ";"

-  }

+    { 

+      ( BlockStmt<out block, out bodyStart, out bodyEnd>  (. hints.Add(block); .)

+      | CalcStmt<out h>                                   (. hints.Add(h); .)

+      |                                                   (. hints.Add(null); .)

+      )

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

+                                                             if (maybeOp == null) {

+                                                               customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor

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

+                                                             } else {

+                                                               customOps.Add(op);

+                                                               resOp = (BinaryExpr.Opcode)maybeOp;                                                              

+                                                             }

+                                                          .)

+      |                                                   (. customOps.Add(null); .)

+      )

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

+      ";"

+    }

+  ]

   "}"

   (. s = new CalcStmt(x, calcOp, lines, hints, customOps); .)

   .

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 36f0aace..36fadb07 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -2666,10 +2666,10 @@ namespace Microsoft.Dafny {
   {

     public readonly BinaryExpr.Opcode/*!*/ Op; // main operator of the calculation

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

-    public readonly List<Statement> Hints;  // Hints[i] comes after line i; null denotes an empty an empty hint

+    public readonly List<Statement> Hints;  // Hints[i] comes after line i; null denotes an empty hint

     public readonly List<BinaryExpr.Opcode?> CustomOps; // CustomOps[i] comes after line i; null denotes the absence of a custom operator

     public readonly List<BinaryExpr/*!*/> Steps; // expressions li op l<i + 1>, filled in during resolution in order to get the correct op

-    public BinaryExpr Result; // expressions l0 op ln, filled in during resolution in order to get the correct op

+    public BinaryExpr Result; // expression l0 op ln, filled in during resolution in order to get the correct op

 

     public static readonly BinaryExpr.Opcode/*!*/ DefaultOp = BinaryExpr.Opcode.Eq; 

 

@@ -2681,24 +2681,21 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Hints != null);

       Contract.Invariant(CustomOps != null);

       Contract.Invariant(Steps != null);

-      Contract.Invariant(Lines.Count > 0);

-      Contract.Invariant(Hints.Count == Lines.Count - 1);

-      Contract.Invariant(CustomOps.Count == Lines.Count - 1);

+      Contract.Invariant(Hints.Count == Math.Max(Lines.Count - 1, 0));

+      Contract.Invariant(CustomOps.Count == Hints.Count);

     }

 

     public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<Statement> hints, List<BinaryExpr.Opcode?> customOps)

-      // Attributes attrs?

       : base(tok)

     {

       Contract.Requires(tok != null);

       Contract.Requires(ValidOp(op));

       Contract.Requires(lines != null);

-      Contract.Requires(cce.NonNullElements(lines));

       Contract.Requires(hints != null);

-      Contract.Requires(lines.Count > 0);

-      Contract.Requires(hints.Count == lines.Count - 1);

       Contract.Requires(customOps != null);

-      Contract.Requires(customOps.Count == lines.Count - 1);

+      Contract.Requires(cce.NonNullElements(lines));

+      Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0));

+      Contract.Requires(customOps.Count == hints.Count);

       this.Op = op;

       this.Lines = lines;

       this.Hints = hints;

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 3a310cd9..e255a317 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1636,36 +1636,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		resOp = calcOp; 

 		Expect(6);

-		Expression(out e);

-		lines.Add(e); 

-		Expect(14);

-		while (StartOf(15)) {

-			if (la.kind == 6) {

-				BlockStmt(out block, out bodyStart, out bodyEnd);

-				hints.Add(block); 

-			} else if (la.kind == 75) {

-				CalcStmt(out h);

-				hints.Add(h); 

-			} else {

-				hints.Add(null); 

-			}

-			if (StartOf(14)) {

-				CalcOp(out opTok, out op);

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

-				if (maybeOp == null) {

-				 customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor

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

-				} else {

-				 customOps.Add(op);

-				 resOp = (BinaryExpr.Opcode)maybeOp;                                                              

-				}

-				

-			} else if (StartOf(10)) {

-				customOps.Add(null); 

-			} else SynErr(162);

+		if (StartOf(10)) {

 			Expression(out e);

 			lines.Add(e); 

 			Expect(14);

+			while (StartOf(15)) {

+				if (la.kind == 6) {

+					BlockStmt(out block, out bodyStart, out bodyEnd);

+					hints.Add(block); 

+				} else if (la.kind == 75) {

+					CalcStmt(out h);

+					hints.Add(h); 

+				} else {

+					hints.Add(null); 

+				}

+				if (StartOf(14)) {

+					CalcOp(out opTok, out op);

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

+					if (maybeOp == null) {

+					 customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor

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

+					} else {

+					 customOps.Add(op);

+					 resOp = (BinaryExpr.Opcode)maybeOp;                                                              

+					}

+					

+				} else if (StartOf(10)) {

+					customOps.Add(null); 

+				} else SynErr(162);

+				Expression(out e);

+				lines.Add(e); 

+				Expect(14);

+			}

 		}

 		Expect(7);

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

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 2051a54e..eab62134 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -569,9 +569,11 @@ namespace Microsoft.Dafny {
         }

         wr.WriteLine("{");

         int lineInd = indent + IndentAmount;

-        Indent(lineInd);

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

-        wr.WriteLine(";");

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

+          Indent(lineInd);

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

+          wr.WriteLine(";");

+        }

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

           var e = s.Lines[i];

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

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index a2710c38..0876d0eb 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -3134,41 +3134,45 @@ namespace Microsoft.Dafny
         var prevErrorCount = ErrorCount;

         CalcStmt s = (CalcStmt)stmt;

         s.IsGhost = true;

-        Contract.Assert(s.Lines.Count > 0); // follows from the invariant of CalcStatement

-        var resOp = s.Op;

-        var e0 = s.Lines.First();

-        ResolveExpression(e0, true);

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

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

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

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

-          } else {

-            BinaryExpr step;

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

-            if (op == null) {              

-              step = new BinaryExpr(e0.tok, s.Op, e0, e1); // Use calc-wide operator

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

+          var resOp = s.Op;

+          var e0 = s.Lines.First();

+          ResolveExpression(e0, true);

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

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

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

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

             } else {

-              step = new BinaryExpr(e0.tok, (BinaryExpr.Opcode)op, e0, e1); // Use custom line operator

-              Contract.Assert(CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op) != null); // This was checked during parsing

-              resOp = (BinaryExpr.Opcode)CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op);

+              BinaryExpr step;

+              var op = s.CustomOps[i - 1];

+              if (op == null) {              

+                step = new BinaryExpr(e0.tok, s.Op, e0, e1); // Use calc-wide operator

+              } else {

+                step = new BinaryExpr(e0.tok, (BinaryExpr.Opcode)op, e0, e1); // Use custom line operator

+                Contract.Assert(CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op) != null); // This was checked during parsing

+                resOp = (BinaryExpr.Opcode)CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op);

+              }

+              ResolveExpression(step, true);

+              s.Steps.Add(step);            

             }

-            ResolveExpression(step, true);

-            s.Steps.Add(step);            

+            e0 = e1;

           }

-          e0 = e1;

-        }

-        foreach (var h in s.Hints)

-        {

-          if (h != null) {

-            ResolveStatement(h, true, method);

+          foreach (var h in s.Hints)

+          {

+            if (h != null) {

+              ResolveStatement(h, true, method);

+            }

+          }

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

+            s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());

+            ResolveExpression(s.Result, true);

           }

         }

-        s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());

-        ResolveExpression(s.Result, true);

         Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);

+        Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == 0 || s.Result != null);

 

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 9bd16f3f..675e62e8 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -4002,6 +4002,7 @@ namespace Microsoft.Dafny {
         AddComment(builder, stmt, "calc statement");

         // NadiaTodo: check well-formedness of lines

         if (s.Steps.Count > 0) {

+          Contract.Assert(s.Result != null); // established by the resolver

           Bpl.IfCmd ifCmd = null;

           Bpl.StmtList els = null;

 

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 8e3a4426..c48f2000 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -210,3 +210,9 @@ ghost method Window(xs: List, ys: List)
     true;

   }

 }

+

+// Empty calculations are also allowed, but they don't generate any Boogie code.

+ghost method Empty()

+{

+	calc {}

+}