Pretty-print calc statements

1 files changed, 23 insertions, 0 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 24941ce1..627ec1b5 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -8,6 +8,7 @@ using System.IO;
 using System.Collections.Generic;

 using System.Diagnostics.Contracts;

 using System.Numerics;

+using System.Linq;

 using Bpl = Microsoft.Boogie;

 

 namespace Microsoft.Dafny {

@@ -559,6 +560,28 @@ namespace Microsoft.Dafny {
         }

         PrintStatement(s.Body, indent);

 

+      } else if (stmt is CalcStmt) {

+        CalcStmt s = (CalcStmt)stmt;

+        wr.Write("calc");

+        wr.WriteLine(" {");

+        int stepInd = indent + IndentAmount;

+        Indent(stepInd);

+        PrintExpression(s.Steps[0], stepInd);

+        wr.WriteLine(";");

+        var pairs = s.Hints.Zip(s.Steps.Skip(1), (h, e) => Tuple.Create(h, e));

+        foreach (var pair in pairs) {

+          if (pair.Item1 != null) {

+            Indent(stepInd);

+            PrintStatement(pair.Item1, stepInd);

+            wr.WriteLine();

+          }

+          Indent(stepInd);

+          PrintExpression(pair.Item2, stepInd);

+          wr.WriteLine(";");

+        }

+        Indent(indent);

+        wr.Write("}");

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         wr.Write("match ");