Dafny: Added map comprehensions and updated display syntax

1 files changed, 18 insertions, 0 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 38ec17fc..6cf71fa1 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1190,6 +1190,24 @@ namespace Microsoft.Dafny {
         }

         if (parensNeeded) { wr.Write(")"); }

 

+      } else if (expr is MapComprehension) {

+        var e = (MapComprehension)expr;

+        bool parensNeeded = !isRightmost;

+        if (parensNeeded) { wr.Write("("); }

+        wr.Write("map ");

+        string sep = "";

+        foreach (BoundVar bv in e.BoundVars) {

+          wr.Write("{0}{1}", sep, bv.Name);

+          sep = ", ";

+          PrintType(": ", bv.Type);

+        }

+        PrintAttributes(e.Attributes);

+        wr.Write(" | ");

+        PrintExpression(e.Range);

+        wr.Write(" :: ");

+        PrintExpression(e.Term);

+        if (parensNeeded) { wr.Write(")"); }

+

       } else if (expr is WildcardExpr) {

         wr.Write("*");