From 456b38819dd1bdafdf2baaa59125ecf9910722ed Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 21 Nov 2011 22:40:44 -0800
Subject: 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.

---
 Dafny/Printer.cs | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'Dafny/Printer.cs')

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 {
-- 
cgit v1.2.3