Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.

1 files changed, 7 insertions, 1 deletions

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 5b9ba1d6..9f012509 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -62,7 +62,13 @@ namespace Microsoft.Dafny {
       int i = 0;

       foreach (TopLevelDecl d in classes) {

         Contract.Assert(d != null);

-        if (d is DatatypeDecl) {

+        if (d is ArbitraryTypeDecl) {

+          var at = (ArbitraryTypeDecl)d;

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

+          Indent(indent);

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

+          wr.WriteLine(";");

+        } else if (d is DatatypeDecl) {

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

           PrintDatatype((DatatypeDecl)d, indent);

         } else {