Dafny: Merge

1 files changed, 14 insertions, 15 deletions

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 36b5f791..4b0b6ec1 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -45,6 +45,9 @@ namespace Microsoft.Dafny {
           if (i++ != 0) { wr.WriteLine(); }

           Indent(indent);

           PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());

+          if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {

+            wr.Write("(==)");

+          }

           wr.WriteLine(";");

         } else if (d is DatatypeDecl) {

           if (i++ != 0) { wr.WriteLine(); }

@@ -146,7 +149,10 @@ namespace Microsoft.Dafny {
 

       wr.Write(" {0}", name);

       if (typeArgs.Count != 0) {

-        wr.Write("<" + Util.Comma(", ", typeArgs, tp => tp.Name) + ">");

+        wr.Write("<" +

+                 Util.Comma(", ", typeArgs,

+                   tp => tp.Name + (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Required? "(==)": ""))

+                 + ">");

       }

     }

 

@@ -422,24 +428,14 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (stmt is AssertStmt) {

-        Expression expr = ((AssertStmt)stmt).Expr;

-

-        wr.Write("assert");

-

-        if (stmt.HasAttributes())

-        {

+      if (stmt is PredicateStmt) {

+        Expression expr = ((PredicateStmt)stmt).Expr;

+        wr.Write(stmt is AssertStmt ? "assert" : "assume");

+        if (stmt.HasAttributes()) {

           PrintAttributes(stmt.Attributes);

         }

-

         wr.Write(" ");

         PrintExpression(expr);

-

-        wr.Write(";");

-

-      } else if (stmt is AssumeStmt) {

-        wr.Write("assume ");

-        PrintExpression(((AssumeStmt)stmt).Expr);

         wr.Write(";");

 

       } else if (stmt is PrintStmt) {

@@ -624,6 +620,9 @@ namespace Microsoft.Dafny {
         } else if (s.S is AssertStmt) {

           Contract.Assert(s.ConditionOmitted);

           wr.Write("assert ...;");

+        } else if (s.S is AssumeStmt) {

+          Contract.Assert(s.ConditionOmitted);

+          wr.Write("assume ...;");

         } else if (s.S is IfStmt) {

           PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);

         } else if (s.S is WhileStmt) {