Allow multiple calc/block statements in a hint. Removed the empty calc test from dafny2/Calculations, as it actually belongs in dafny0.

7 files changed, 59 insertions, 41 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index a5865a6f..c972c5c4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -424,7 +424,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt), new List<Nullable<BinaryExpr.Opcode>>(s.CustomOps));

+          r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), new List<Nullable<BinaryExpr.Opcode>>(s.CustomOps));

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 90ff7bc5..cf74fc30 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1221,25 +1221,21 @@ CalcStmt<out Statement/*!*/ s>
 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      Token x;

      BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;     

-     List<Expression/*!*/> lines = new List<Expression/*!*/>();

-     List<Statement> hints = new List<Statement>(); 

-     List<BinaryExpr.Opcode?> customOps = new List<BinaryExpr.Opcode?>();

+     var lines = new List<Expression/*!*/>();

+     var hints = new List<BlockStmt/*!*/>(); 

+     var customOps = new List<BinaryExpr.Opcode?>();

      BinaryExpr.Opcode? maybeOp;

      Expression/*!*/ e;

-     BlockStmt/*!*/ block;

-     Statement/*!*/ h;

-     IToken bodyStart, bodyEnd, opTok;

+     BlockStmt/*!*/ h;

+     IToken opTok;

   .)

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

-      )

+    {

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

       ( 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

@@ -1280,6 +1276,20 @@ CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
                           .)

   )

   .

+Hint<out BlockStmt s>

+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty

+     var subhints = new List<Statement/*!*/>(); 

+     IToken bodyStart, bodyEnd;

+     BlockStmt/*!*/ block;

+     Statement/*!*/ calc;

+     Token x = la;

+  .)

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

+  | CalcStmt<out calc>                                (. subhints.Add(calc); .)

+  }

+  (. s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container 

+  .)

+  .

 /*------------------------------------------------------------------------*/

 Expression<out Expression/*!*/ e>

 =

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 36fadb07..6ae273b6 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2666,7 +2666,7 @@ 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 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 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; // expression l0 op ln, filled in during resolution in order to get the correct op

@@ -2685,7 +2685,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(CustomOps.Count == Hints.Count);

     }

 

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

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

       : base(tok)

     {

       Contract.Requires(tok != null);

@@ -2694,6 +2694,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(hints != null);

       Contract.Requires(customOps != null);

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

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

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

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

       this.Op = op;

@@ -2708,7 +2709,7 @@ namespace Microsoft.Dafny {
     {

       get {

         foreach (var h in Hints) {

-            if (h != null) yield return h;

+          yield return h;

         }

       }

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index e255a317..ff45ecf0 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1620,14 +1620,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;

 		BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;     

-		List<Expression/*!*/> lines = new List<Expression/*!*/>();

-		List<Statement> hints = new List<Statement>(); 

-		List<BinaryExpr.Opcode?> customOps = new List<BinaryExpr.Opcode?>();

+		var lines = new List<Expression/*!*/>();

+		var hints = new List<BlockStmt/*!*/>(); 

+		var customOps = new List<BinaryExpr.Opcode?>();

 		BinaryExpr.Opcode? maybeOp;

 		Expression/*!*/ e;

-		BlockStmt/*!*/ block;

-		Statement/*!*/ h;

-		IToken bodyStart, bodyEnd, opTok;

+		BlockStmt/*!*/ h;

+		IToken opTok;

 		

 		Expect(75);

 		x = t; 

@@ -1641,15 +1640,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			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); 

-				}

+				Hint(out h);

+				hints.Add(h); 

 				if (StartOf(14)) {

 					CalcOp(out opTok, out op);

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

@@ -2017,6 +2009,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else SynErr(173);

 	}

 

+	void Hint(out BlockStmt s) {

+		Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty

+		var subhints = new List<Statement/*!*/>(); 

+		IToken bodyStart, bodyEnd;

+		BlockStmt/*!*/ block;

+		Statement/*!*/ calc;

+		Token x = la;

+		

+		while (la.kind == 6 || la.kind == 75) {

+			if (la.kind == 6) {

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

+				subhints.Add(block); 

+			} else {

+				CalcStmt(out calc);

+				subhints.Add(calc); 

+			}

+		}

+		s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container 

+		

+	}

+

 	void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null);

 		x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/;

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index eab62134..b284f539 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -578,9 +578,9 @@ namespace Microsoft.Dafny {
           var e = s.Lines[i];

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

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

-          if (h != null) {

+          foreach (var st in h.Body) {

             Indent(lineInd);

-            PrintStatement(h, lineInd);

+            PrintStatement(st, lineInd);

             wr.WriteLine();

           }

           Indent(lineInd);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0876d0eb..ecb53bd5 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3160,11 +3160,8 @@ namespace Microsoft.Dafny
             }

             e0 = e1;

           }

-          foreach (var h in s.Hints)

-          {

-            if (h != null) {

-              ResolveStatement(h, true, method);

-            }

+          foreach (var h in s.Hints) {

+            ResolveStatement(h, true, method);

           }

           if (s.Steps.Count > 0) {

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

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 531bb51a..b4f5a4dc 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4008,10 +4008,7 @@ namespace Microsoft.Dafny {
 

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

             var b = new Bpl.StmtListBuilder();

-            var h = s.Hints[i];

-            if (h != null) {

-              TrStmt(h, b, locals, etran);

-            }

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

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

             b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

             if (i == s.Steps.Count - 1) {