Dafny: fixed resolution bug for inductive datatypes (previous check did not handle generic datatypes correctly)

Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code)
Dafny: added "codatatype" declaration (syntax only for now)

1 files changed, 9 insertions, 3 deletions

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index a10cb4bf..c73ffda8 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -136,11 +136,17 @@ namespace Microsoft.Dafny {
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);

-      } else if (d is DatatypeDecl) {

-        var dd = (DatatypeDecl)d;

+      } else if (d is IndDatatypeDecl) {

+        var dd = (IndDatatypeDecl)d;

         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var ctors = dd.Ctors.ConvertAll(CloneCtor);

-        var dt = new DatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);

+        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);

+        return dt;

+      } else if (d is CoDatatypeDecl) {

+        var dd = (CoDatatypeDecl)d;

+        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

+        var ctors = dd.Ctors.ConvertAll(CloneCtor);

+        var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);

         return dt;

       } else if (d is ClassDecl) {

         var dd = (ClassDecl)d;