Start (some parsing and resolution) of adding algebraic datatypes to Dafny.

Included VSI-Benchmarks in standard tests.

1 files changed, 31 insertions, 3 deletions

diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index 68b9e132..24ccb44e 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -22,9 +22,13 @@ namespace Microsoft.Dafny {
         wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);

       }

       wr.WriteLine("// {0}", prog.Name);

-      foreach (ClassDecl c in prog.Classes) {

+      foreach (TopLevelDecl d in prog.Classes) {

         wr.WriteLine();

-        PrintClass(c);

+        if (d is ClassDecl) {

+          PrintClass((ClassDecl)d);

+        } else {

+          PrintDatatype((DatatypeDecl)d);

+        }

       }

     }

     

@@ -57,7 +61,9 @@ namespace Microsoft.Dafny {
     }

     

     void PrintClassMethodHelper(string! kind, Attributes attrs, string! modifiers, string! name, List<TypeParameter!>! typeArgs) {

-      wr.Write("{0} ", kind);

+      if (kind.Length != 0) {

+        wr.Write("{0} ", kind);

+      }

       PrintAttributes(attrs);

       wr.Write(modifiers);

       wr.Write(name);

@@ -72,6 +78,19 @@ namespace Microsoft.Dafny {
       }

     }

     

+    public void PrintDatatype(DatatypeDecl! dt) {

+      PrintClassMethodHelper("datatype", dt.Attributes, "", dt.Name, dt.TypeArgs);

+      if (dt.Ctors.Count == 0) {

+        wr.WriteLine(" { }");

+      } else {

+        wr.WriteLine(" {");

+        foreach (DatatypeCtor ctor in dt.Ctors) {

+          PrintCtor(ctor);

+        }

+        wr.WriteLine("}");

+      }

+    }

+    

     public void PrintAttributes(Attributes a) {

       if (a != null) {

         PrintAttributes(a.Prev);

@@ -129,6 +148,15 @@ namespace Microsoft.Dafny {
       }

     }

     

+    public void PrintCtor(DatatypeCtor! ctor) {

+      Indent(IndentAmount);

+      PrintClassMethodHelper("", ctor.Attributes, "", ctor.Name, ctor.TypeArgs);

+      if (ctor.Formals.Count != 0) {

+        PrintFormals(ctor.Formals);

+      }

+      wr.WriteLine(";");

+    }

+    

     // ----------------------------- PrintMethod -----------------------------

 

     const int IndentAmount = 2;