diff options
Diffstat (limited to 'Source/Dafny/Printer.cs')
| -rw-r--r-- | Source/Dafny/Printer.cs | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index fe602f86..36658e2f 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 {
@@ -620,6 +621,40 @@ namespace Microsoft.Dafny { }
PrintStatement(s.Body, indent);
+ } else if (stmt is CalcStmt) {
+ CalcStmt s = (CalcStmt)stmt;
+ wr.Write("calc ");
+ if (s.Op != CalcStmt.DefaultOp) {
+ wr.Write(BinaryExpr.OpcodeString(s.Op));
+ wr.Write(" ");
+ }
+ wr.WriteLine("{");
+ int lineInd = indent + IndentAmount;
+ 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];
+ var op = s.CustomOps[i - 1];
+ foreach (var st in h.Body) {
+ Indent(lineInd);
+ PrintStatement(st, lineInd);
+ wr.WriteLine();
+ }
+ Indent(lineInd);
+ if (op != null && (BinaryExpr.Opcode)op != s.Op) {
+ wr.Write(BinaryExpr.OpcodeString((BinaryExpr.Opcode)op));
+ wr.Write(" ");
+ }
+ PrintExpression(e, lineInd);
+ wr.WriteLine(";");
+ }
+ Indent(indent);
+ wr.Write("}");
+
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
wr.Write("match ");
|