1 files changed, 18 insertions, 4 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 99ebe8da..4faa85f2 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -169,7 +169,7 @@ namespace Microsoft.Dafny {
           return true;

         } else {

           UserDefinedType udt = this as UserDefinedType;

-          return udt != null && udt.ResolvedParam == null && !(udt.ResolvedClass is DatatypeDecl);

+          return udt != null && udt.ResolvedParam == null && udt.ResolvedClass is ClassDecl;

         }

       }

     }

@@ -201,7 +201,6 @@ namespace Microsoft.Dafny {
     }

     public bool IsTypeParameter {

       get {

-        Contract.Ensures(!Contract.Result<bool>() || this is UserDefinedType && ((UserDefinedType)this).ResolvedParam != null);

         UserDefinedType ct = this as UserDefinedType;

         return ct != null && ct.ResolvedParam != null;

       }

@@ -601,7 +600,6 @@ namespace Microsoft.Dafny {
       : base(tok, name, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

-

     }

   }

 

@@ -653,7 +651,6 @@ namespace Microsoft.Dafny {
       Contract.Invariant(cce.NonNullElements(TypeArgs));

     }

 

-

     public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs, Attributes attributes)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

@@ -920,6 +917,23 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType

+  {

+    public readonly TypeParameter TheType;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(TheType != null && Name == TheType.Name);

+    }

+

+    public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes)

+      : base(tok, name, module, new List<TypeParameter>(), attributes) {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(module != null);

+      TheType = new TypeParameter(tok, name);

+    }

+  }

+

   [ContractClass(typeof(IVariableContracts))]

   public interface IVariable {

     string/*!*/ Name {