Dafny: Since it's no longer true that all types support equality at run-time (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.

1 files changed, 6 insertions, 0 deletions

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index fb46ba4b..498546c3 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -71,6 +71,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(); }

@@ -149,6 +152,9 @@ namespace Microsoft.Dafny {
         foreach (TypeParameter tp in typeArgs) {

           Contract.Assert(tp != null);

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

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

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

+          }

           sep = ", ";

         }

         wr.Write(">");