Added type synonyms. (No support yet for these in refinements.)

9 files changed, 237 insertions, 168 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 15c43d05..3c6fe107 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -30,6 +30,10 @@ namespace Microsoft.Dafny
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

         return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes));

+      } else if (d is TypeSynonymDecl) {

+        var dd = (TypeSynonymDecl)d;

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

+        return new TypeSynonymDecl(Tok(dd.tok), dd.Name, tps, m, CloneType(dd.Rhs), CloneAttributes(dd.Attributes));

       } else if (d is TupleTypeDecl) {

         var dd = (TupleTypeDecl)d;

         return new TupleTypeDecl(dd.Dims, dd.Module);

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 1e5ba1ba..b5d145aa 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -115,6 +115,8 @@ namespace Microsoft.Dafny {
           if (d is ArbitraryTypeDecl) {

             var at = (ArbitraryTypeDecl)d;

             Error("Arbitrary type ('{0}') cannot be compiled", at.FullName);

+          } else if (d is TypeSynonymDecl) {

+            // do nothing, just bypass type synonyms in the compiler

           } else if (d is DatatypeDecl) {

             var dt = (DatatypeDecl)d;

             Indent(indent);

@@ -868,16 +870,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      while (true) {

-        TypeProxy tp = type as TypeProxy;

-        if (tp == null) {

-          break;

-        } else if (tp.T == null) {

-          // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

-          return "object";

-        } else {

-          type = tp.T;

-        }

+      type = type.NormalizeExpand();

+      if (type is TypeProxy) {

+        // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

+        return "object";

       }

 

       if (type is BoolType) {

@@ -968,16 +964,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<string>() != null);

 

-      while (true) {

-        TypeProxy tp = type as TypeProxy;

-        if (tp == null) {

-          break;

-        } else if (tp.T == null) {

-          // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

-          return "null";

-        } else {

-          type = tp.T;

-        }

+      type = type.NormalizeExpand();

+      if (type is TypeProxy) {

+        // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

+        return "null";

       }

 

       if (type is BoolType) {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index d516b421..b42e0633 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -189,7 +189,7 @@ IGNORE cr + lf + tab
 /*------------------------------------------------------------------------*/

 PRODUCTIONS

 Dafny

-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;

      List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

      ModuleDecl submodule;

      // to support multiple files, create a default module only if theModule is null

@@ -213,7 +213,7 @@ Dafny
   { SubModuleDecl<defaultModule, out submodule> (. defaultModule.TopLevelDecls.Add(submodule); .)

   | ClassDecl<defaultModule, out c>             (. defaultModule.TopLevelDecls.Add(c); .)

   | DatatypeDecl<defaultModule, out dt>         (. defaultModule.TopLevelDecls.Add(dt); .)

-  | ArbitraryTypeDecl<defaultModule, out at>    (. defaultModule.TopLevelDecls.Add(at); .)

+  | OtherTypeDecl<defaultModule, out td>        (. defaultModule.TopLevelDecls.Add(td); .)

   | IteratorDecl<defaultModule, out iter>       (. defaultModule.TopLevelDecls.Add(iter); .)

 

   | ClassMemberDecl<membersDefaultClass, false>

@@ -234,7 +234,7 @@ Dafny
   EOF

   .

 SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>

-= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

+= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;

      Attributes attrs = null;  IToken/*!*/ id;

      List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;

      List<IToken> idRefined = null, idPath = null, idAssignment = null;

@@ -254,7 +254,7 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule>
         { SubModuleDecl<module, out sm>                (. module.TopLevelDecls.Add(sm); .)

         | ClassDecl<module, out c>                     (. module.TopLevelDecls.Add(c); .)

         | DatatypeDecl<module, out dt>                 (. module.TopLevelDecls.Add(dt); .)

-        | ArbitraryTypeDecl<module, out at>            (. module.TopLevelDecls.Add(at); .)

+        | OtherTypeDecl<module, out td>                (. module.TopLevelDecls.Add(td); .)

         | IteratorDecl<module, out iter>               (. module.TopLevelDecls.Add(iter); .)

         | ClassMemberDecl<namedModuleDefaultClassMembers, false>

         }

@@ -393,16 +393,25 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }

   SYNC ";"

   .

-ArbitraryTypeDecl<ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at>

+OtherTypeDecl<ModuleDefinition/*!*/ module, out TopLevelDecl td>

 = (. IToken/*!*/ id;

      Attributes attrs = null;

      var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

+     List<TypeParameter> typeArgs;

+     Type ty;

   .)

   "type"

   { Attribute<ref attrs> }

-  NoUSIdent<out id>

+  NoUSIdent<out id>            (. td = null; .)

   [ "(" "==" ")"               (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)

-  ]                            (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)

+  |                            (. typeArgs = new List<TypeParameter>(); .)

+    [ GenericParameters<typeArgs> ]

+    "="

+    Type<out ty>               (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)

+  ]                            (. if (td == null) {

+                                    td = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);

+                                  }

+                               .)

   [ SYNC ";"

       // This semi-colon used to be required, but it seems silly to have it.

       // To stage the transition toward not having it at all, let's make it optional for now.  Then,

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 2077fe7e..acdeae1b 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -313,14 +313,13 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// Return the most constrained version of "this".

+    /// Return the most constrained version of "this", getting to the bottom of proxies.

     /// </summary>

-    /// <returns></returns>

     public Type Normalize() {

       Contract.Ensures(Contract.Result<Type>() != null);

       Type type = this;

       while (true) {

-        TypeProxy pt = type as TypeProxy;

+        var pt = type as TypeProxy;

         if (pt != null && pt.T != null) {

           type = pt.T;

         } else {

@@ -329,6 +328,35 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Return the type that "this" stands for, getting to the bottom of proxies and following type synonyms.

+    /// </summary>

+    public Type NormalizeExpand() {

+      Contract.Ensures(Contract.Result<Type>() != null);

+      Contract.Ensures(!(Contract.Result<Type>() is TypeProxy) || ((TypeProxy)Contract.Result<Type>()).T == null);  // return a proxy only if .T == null

+      Type type = this;

+      while (true) {

+        var pt = type as TypeProxy;

+        if (pt != null && pt.T != null) {

+          type = pt.T;

+        } else {

+          var syn = type.AsTypeSynonym;

+          if (syn != null) {

+            // Instantiate with the actual type arguments

+            if (syn.TypeArgs.Count == 0) {

+              // this optimization seems worthwhile

+              type = syn.Rhs;

+            } else {

+              var subst = Resolver.TypeSubstitutionMap(syn.TypeArgs, ((UserDefinedType)type).TypeArgs);

+              type = Resolver.SubstType(syn.Rhs, subst);

+            }

+          } else {

+            return type;

+          }

+        }

+      }

+    }

+

     [Pure]

     public abstract bool Equals(Type that);

 

@@ -357,6 +385,16 @@ namespace Microsoft.Dafny {
         return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;

       }

     }

+    public TypeSynonymDecl AsTypeSynonym {

+      get {

+        var udt = this as UserDefinedType;

+        if (udt == null) {

+          return null;

+        } else {

+          return udt.ResolvedClass as TypeSynonymDecl;

+        }

+      }

+    }

     public bool IsDatatype {

       get {

         return AsDatatype != null;

@@ -430,6 +468,11 @@ namespace Microsoft.Dafny {
     public bool IsOrdered {

       get { return !IsTypeParameter && !IsCoDatatype; }

     }

+

+    public void ForeachTypeComponent(Action<Type> action) {

+      action(this);

+      TypeArgs.ForEach(action);

+    }

   }

 

   /// <summary>

@@ -449,7 +492,7 @@ namespace Microsoft.Dafny {
       return "bool";

     }

     public override bool Equals(Type that) {

-      return that.Normalize() is BoolType;

+      return that.NormalizeExpand() is BoolType;

     }

   }

 

@@ -459,7 +502,7 @@ namespace Microsoft.Dafny {
       return "int";

     }

     public override bool Equals(Type that) {

-      return that.Normalize() is IntType;

+      return that.NormalizeExpand() is IntType;

     }

   }

 

@@ -477,7 +520,7 @@ namespace Microsoft.Dafny {
       return "real";

     }

     public override bool Equals(Type that) {

-      return that.Normalize() is RealType;

+      return that.NormalizeExpand() is RealType;

     }

   }

 

@@ -488,7 +531,7 @@ namespace Microsoft.Dafny {
       return "object";

     }

     public override bool Equals(Type that) {

-      return that.Normalize() is ObjectType;

+      return that.NormalizeExpand() is ObjectType;

     }

   }

 

@@ -541,7 +584,7 @@ namespace Microsoft.Dafny {
     public override string CollectionTypeName { get { return "set"; } }

     [Pure]

     public override bool Equals(Type that) {

-      var t = that.Normalize() as SetType;

+      var t = that.NormalizeExpand() as SetType;

       return t != null && Arg.Equals(t.Arg);

     }

   }

@@ -552,7 +595,7 @@ namespace Microsoft.Dafny {
     }

     public override string CollectionTypeName { get { return "multiset"; } }

     public override bool Equals(Type that) {

-      var t = that.Normalize() as MultiSetType;

+      var t = that.NormalizeExpand() as MultiSetType;

       return t != null && Arg.Equals(t.Arg);

     }

   }

@@ -562,7 +605,7 @@ namespace Microsoft.Dafny {
     }

     public override string CollectionTypeName { get { return "seq"; } }

     public override bool Equals(Type that) {

-      var t = that.Normalize() as SeqType;

+      var t = that.NormalizeExpand() as SeqType;

       return t != null && Arg.Equals(t.Arg);

     }

   }

@@ -600,7 +643,7 @@ namespace Microsoft.Dafny {
       return CollectionTypeName + targs;

     }

     public override bool Equals(Type that) {

-      var t = that.Normalize() as MapType;

+      var t = that.NormalizeExpand() as MapType;

       return t != null && Arg.Equals(t.Arg) && Range.Equals(t.Range);

     }

   }

@@ -716,7 +759,7 @@ namespace Microsoft.Dafny {
     }

 

     public override bool Equals(Type that) {

-      var t = that.Normalize() as UserDefinedType;

+      var t = that.NormalizeExpand() as UserDefinedType;

       return t != null && ResolvedClass == t.ResolvedClass && ResolvedParam == t.ResolvedParam;

     }

 

@@ -727,7 +770,7 @@ namespace Microsoft.Dafny {
     public static UserDefinedType DenotesClass(Type type) {

       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<UserDefinedType>() == null || Contract.Result<UserDefinedType>().ResolvedClass is ClassDecl);

-      type = type.Normalize();

+      type = type.NormalizeExpand();

       UserDefinedType ct = type as UserDefinedType;

       if (ct != null && ct.ResolvedClass is ClassDecl) {

         return ct;

@@ -751,9 +794,6 @@ namespace Microsoft.Dafny {
     [Pure]

     public override string TypeName(ModuleDefinition context) {

       Contract.Ensures(Contract.Result<string>() != null);

-      /* if (ResolvedParam != null) {

-        return ResolvedParam.FullName();

-      } else */ 

       if (BuiltIns.IsTupleTypeName(Name)) {

         return "(" + Util.Comma(",", TypeArgs, ty => ty.TypeName(context)) + ")";

       } else {

@@ -825,9 +865,9 @@ namespace Microsoft.Dafny {
       }

     }

     public override bool Equals(Type that) {

-      var i = Normalize();

+      var i = NormalizeExpand();

       if (i is TypeProxy) {

-        var u = that.Normalize() as TypeProxy;

+        var u = that.NormalizeExpand() as TypeProxy;

         return u != null && object.ReferenceEquals(i, u);

       } else {

         return i.Equals(that);

@@ -1720,7 +1760,7 @@ namespace Microsoft.Dafny {
         return "_increasingInt";

       }

       public override bool Equals(Type that) {

-        return that.Normalize() is EverIncreasingType;

+        return that.NormalizeExpand() is EverIncreasingType;

       }

     }

 

@@ -1892,6 +1932,20 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class TypeSynonymDecl : TopLevelDecl

+  {

+    public readonly Type Rhs;

+    public TypeSynonymDecl(IToken tok, string name, List<TypeParameter> typeArgs, ModuleDefinition module, Type rhs, Attributes attributes)

+      : base(tok, name, module, typeArgs, attributes) {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(typeArgs != null);

+      Contract.Requires(module != null);

+      Contract.Requires(rhs != null);

+      Rhs = rhs;

+    }

+  }

+

   [ContractClass(typeof(IVariableContracts))]

   public interface IVariable {

     string Name {

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

     }

     Type type;

-    //[Pure(false)]  // TODO: if Type gets the status of [Frozen], then this attribute is not needed

     public Type Type {

       get {

         Contract.Ensures(Contract.Result<Type>() != null);

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

     public readonly Type OptionalType;  // this is the type mentioned in the declaration, if any

     internal Type type;  // this is the declared or inferred type of the variable; it is non-null after resolution (even if resolution fails)

-    //[Pure(false)]

     public Type Type {

       get {

         Contract.Ensures(Contract.Result<Type>() != null);

@@ -4195,13 +4247,10 @@ namespace Microsoft.Dafny {
 

     protected Type type;

     public Type Type {  // filled in during resolution

-      [Verify(false)]  // TODO: how do we allow Type.get to modify type and still be [Pure]?

-      [Additive]  // validity of proper subclasses is not required

       get {

         Contract.Ensures(type != null || Contract.Result<Type>() == null);  // useful in conjunction with postcondition of constructor

         return type == null ? null : type.Normalize();

       }

-      [NoDefaultContract]  // no particular validity of 'this' is required, except that it not be committed

       set {

         Contract.Requires(!WasResolved());  // set it only once

         Contract.Requires(value != null);

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 6a161f19..7e98ff9a 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -237,7 +237,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 

 

 	void Dafny() {

-		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

+		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;

 		List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();

 		ModuleDecl submodule;

 		// to support multiple files, create a default module only if theModule is null

@@ -279,8 +279,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 				break;

 			}

 			case 32: {

-				ArbitraryTypeDecl(defaultModule, out at);

-				defaultModule.TopLevelDecls.Add(at); 

+				OtherTypeDecl(defaultModule, out td);

+				defaultModule.TopLevelDecls.Add(td); 

 				break;

 			}

 			case 34: {

@@ -310,7 +310,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 	}

 

 	void SubModuleDecl(ModuleDefinition parent, out ModuleDecl submodule) {

-		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; IteratorDecl iter;

+		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;

 		Attributes attrs = null;  IToken/*!*/ id;

 		List<MemberDecl/*!*/> namedModuleDefaultClassMembers = new List<MemberDecl>();;

 		List<IToken> idRefined = null, idPath = null, idAssignment = null;

@@ -355,8 +355,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 					break;

 				}

 				case 32: {

-					ArbitraryTypeDecl(module, out at);

-					module.TopLevelDecls.Add(at); 

+					OtherTypeDecl(module, out td);

+					module.TopLevelDecls.Add(td); 

 					break;

 				}

 				case 34: {

@@ -484,23 +484,39 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		

 	}

 

-	void ArbitraryTypeDecl(ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at) {

+	void OtherTypeDecl(ModuleDefinition/*!*/ module, out TopLevelDecl td) {

 		IToken/*!*/ id;

 		Attributes attrs = null;

 		var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

+		List<TypeParameter> typeArgs;

+		Type ty;

 		

 		Expect(32);

 		while (la.kind == 9) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 11) {

-			Get();

-			Expect(33);

-			Expect(12);

-			eqSupport = TypeParameter.EqualitySupportValue.Required; 

+		td = null; 

+		if (la.kind == 11 || la.kind == 21 || la.kind == 38) {

+			if (la.kind == 11) {

+				Get();

+				Expect(33);

+				Expect(12);

+				eqSupport = TypeParameter.EqualitySupportValue.Required; 

+			} else {

+				typeArgs = new List<TypeParameter>(); 

+				if (la.kind == 38) {

+					GenericParameters(typeArgs);

+				}

+				Expect(21);

+				Type(out ty);

+				td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); 

+			}

 		}

-		at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); 

+		if (td == null) {

+		 td = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);

+		}

+		

 		if (la.kind == 8) {

 			while (!(la.kind == 0 || la.kind == 8)) {SynErr(133); Get();}

 			Get();

@@ -1016,6 +1032,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		Type(out ty);

 	}

 

+	void Type(out Type/*!*/ ty) {

+		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; 

+		TypeAndToken(out tok, out ty);

+	}

+

 	void GIdentType(bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);

@@ -1048,11 +1069,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
 		

 	}

 

-	void Type(out Type/*!*/ ty) {

-		Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; 

-		TypeAndToken(out tok, out ty);

-	}

-

 	void LocalIdentTypeOptional(out LocalVariable var, bool isGhost) {

 		IToken id;  Type ty;  Type optType = null;

 		

@@ -3934,7 +3950,7 @@ public class Errors {
 			case 130: s = "this symbol not expected in DatatypeDecl"; break;

 			case 131: s = "invalid DatatypeDecl"; break;

 			case 132: s = "this symbol not expected in DatatypeDecl"; break;

-			case 133: s = "this symbol not expected in ArbitraryTypeDecl"; break;

+			case 133: s = "this symbol not expected in OtherTypeDecl"; break;

 			case 134: s = "this symbol not expected in IteratorDecl"; break;

 			case 135: s = "invalid IteratorDecl"; break;

 			case 136: s = "invalid ClassMemberDecl"; break;

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 440fcc68..49121848 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -142,6 +142,14 @@ namespace Microsoft.Dafny {
             wr.Write("(==)");

           }

           wr.WriteLine();

+        } else if (d is TypeSynonymDecl) {

+          var syn = (TypeSynonymDecl)d;

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

+          Indent(indent);

+          PrintClassMethodHelper("type", syn.Attributes, syn.Name, syn.TypeArgs);

+          wr.Write(" = ");

+          PrintType(syn.Rhs);

+          wr.WriteLine();

         } else if (d is DatatypeDecl) {

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

           PrintDatatype((DatatypeDecl)d, indent);

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 70fdae85..5ddcef55 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -429,6 +429,8 @@ namespace Microsoft.Dafny
     public static bool ResolvedTypesAreTheSame(Type prev, Type next) {

       Contract.Requires(prev != null);

       Contract.Requires(next != null);

+      prev = prev.NormalizeExpand();

+      next = next.NormalizeExpand();

       if (prev is TypeProxy || next is TypeProxy)

         return false;

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index f3e3ce93..40864ac8 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -528,6 +528,7 @@ namespace Microsoft.Dafny
       var datatypeDependencies = new Graph<IndDatatypeDecl>();

       var codatatypeDependencies = new Graph<CoDatatypeDecl>();

       int prevErrorCount = ErrorCount;

+      ResolveAttributes(m.Attributes, false, new NoContext(m.Module));

       ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);

       if (ErrorCount == prevErrorCount) {

         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies);

@@ -750,6 +751,8 @@ namespace Microsoft.Dafny
           // nothing to do

         } else if (d is ArbitraryTypeDecl) {

           // nothing more to register

+        } else if (d is TypeSynonymDecl) {

+          // nothing more to register

 

         } else if (d is IteratorDecl) {

           var iter = (IteratorDecl)d;

@@ -899,14 +902,14 @@ namespace Microsoft.Dafny
 

                   List<TypeParameter> tyvars = cop.TypeArgs.ConvertAll(cloner.CloneTypeParam);

 

-	          /*

+                  /*

                   Dictionary<TypeParameter, Type> su = new Dictionary<TypeParameter, Type>();

                   for (int i = 0; i < tyvars.Count; i++) {

                     su[cop.TypeArgs[i]] = new UserDefinedType(tyvars[i].tok, tyvars[i].Name, tyvars[i]);

                   }

                   var sub = new Translator.Substituter(null, new Dictionary<IVariable, Expression>(), su, null);

-		  // We would like to apply this substitution the new body... he-hum

-		  */

+                  // We would like to apply this substitution the new body... he-hum

+                  */

 

                   // create prefix predicate

                   cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.IsStatic,

@@ -1039,6 +1042,10 @@ namespace Microsoft.Dafny
       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

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

+      } else if (d is TypeSynonymDecl) {

+        var dd = (TypeSynonymDecl)d;

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

+        return new TypeSynonymDecl(dd.tok, dd.Name, tps, m, CloneType(dd.Rhs), null);

       } else if (d is TupleTypeDecl) {

         var dd = (TupleTypeDecl)d;

         return new TupleTypeDecl(dd.Dims, dd.Module);

@@ -1402,12 +1409,23 @@ namespace Microsoft.Dafny
       Contract.Requires(declarations != null);

       Contract.Requires(datatypeDependencies != null);

       Contract.Requires(codatatypeDependencies != null);

+

+      var typeSynonymDependencies = new Graph<TypeSynonymDecl>();

       foreach (TopLevelDecl d in declarations) {

         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

         ResolveTypeParameters(d.TypeArgs, true, d);

         if (d is ArbitraryTypeDecl) {

           // nothing to do

+        } else if (d is TypeSynonymDecl) {

+          var syn = (TypeSynonymDecl)d;

+          ResolveType(syn.tok, syn.Rhs, ResolveTypeOptionEnum.AllowPrefix, syn.TypeArgs);

+          syn.Rhs.ForeachTypeComponent(ty => {

+            var s = ty.AsTypeSynonym;

+            if (s != null) {

+              typeSynonymDependencies.AddEdge(syn, s);

+            }

+          });

         } else if (d is IteratorDecl) {

           ResolveIteratorSignature((IteratorDecl)d);

         } else if (d is ClassDecl) {

@@ -1431,6 +1449,14 @@ namespace Microsoft.Dafny
         }

         allTypeParameters.PopMarker();

       }

+

+      // perform acyclicity test on type synonyms

+      var cycle = typeSynonymDependencies.TryFindCycle();

+      if (cycle != null) {

+        Contract.Assert(cycle.Count != 0);

+        var erste = cycle[0];

+        Error(erste.tok, "Cycle among type synonyms: {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);

+      }

     }

 

     public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies, Graph<CoDatatypeDecl/*!*/>/*!*/ codatatypeDependencies) {

@@ -1440,19 +1466,21 @@ namespace Microsoft.Dafny
 

       int prevErrorCount = ErrorCount;

 

-      // Resolve the meat of classes, and the type parameters of all top-level type declarations

+      // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations

       foreach (TopLevelDecl d in declarations) {

         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

         ResolveTypeParameters(d.TypeArgs, false, d);

+        if (!(d is IteratorDecl)) {

+          // Note, attributes of iterators are resolved by ResolvedIterator, after registering any names in the iterator signature

+          ResolveAttributes(d.Attributes, false, new NoContext(d.Module));

+        }

         if (d is IteratorDecl) {

           var iter = (IteratorDecl)d;

           ResolveIterator(iter);

           ResolveClassMemberBodies(iter);  // resolve the automatically generated members

-

         } else if (d is ClassDecl) {

           var cl = (ClassDecl)d;

-          ResolveAttributes(cl.Attributes, false, new NoContext(cl.Module));

           ResolveClassMemberBodies(cl);

         }

         allTypeParameters.PopMarker();

@@ -2435,8 +2463,8 @@ namespace Microsoft.Dafny
       protected override bool VisitOneExpr(Expression expr, ref bool st) {

         if (expr is BinaryExpr) {

           var e = (BinaryExpr)expr;

-          var t0 = e.E0.Type.Normalize();

-          var t1 = e.E1.Type.Normalize();

+          var t0 = e.E0.Type.NormalizeExpand();

+          var t1 = e.E1.Type.NormalizeExpand();

           switch (e.Op) {

             case BinaryExpr.Opcode.Eq:

             case BinaryExpr.Opcode.Neq:

@@ -2516,7 +2544,7 @@ namespace Microsoft.Dafny
       public void CheckEqualityTypes_Type(IToken tok, Type type) {

         Contract.Requires(tok != null);

         Contract.Requires(type != null);

-        type = type.Normalize();

+        type = type.NormalizeExpand();

         if (type is BasicType) {

           // fine

         } else if (type is SetType) {

@@ -2661,7 +2689,7 @@ namespace Microsoft.Dafny
       Contract.Requires(tp != null);

       Contract.Requires(type != null);

 

-      type = type.Normalize();

+      type = type.NormalizeExpand();

       if (type is BasicType) {

       } else if (type is SetType) {

         var st = (SetType)type;

@@ -3001,7 +3029,7 @@ namespace Microsoft.Dafny
             } else {

               var otherDt = arg.Type.AsIndDatatype;

               if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.ConsultTypeArguments) {  // datatype is in a different SCC

-                var otherUdt = (UserDefinedType)arg.Type.Normalize();

+                var otherUdt = (UserDefinedType)arg.Type.NormalizeExpand();

                 var i = 0;

                 foreach (var otherTp in otherDt.TypeArgs) {

                   if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

@@ -3029,7 +3057,7 @@ namespace Microsoft.Dafny
             foreach (var arg in ctor.Formals) {

               var otherDt = arg.Type.AsIndDatatype;

               if (otherDt != null && otherDt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed) { // otherDt lives in the same SCC

-                var otherUdt = (UserDefinedType)arg.Type.Normalize();

+                var otherUdt = (UserDefinedType)arg.Type.NormalizeExpand();

                 var i = 0;

                 foreach (var otherTp in otherDt.TypeArgs) {

                   if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

@@ -3804,11 +3832,6 @@ namespace Microsoft.Dafny
         for (int i = 0; i < n; i++) {

           typeArgs.Add(new InferredTypeProxy());

         }

-      /*

-      } else if (option.Opt == ResolveTypeOptionEnum.AllowExact && defaultTypeArguments.Count != n) {

-        // the number of default arguments is not exactly what we need, so don't add anything

-      } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefix && defaultTypeArguments.Count < n) {

-      */

       } else if (option.Opt == ResolveTypeOptionEnum.AllowPrefix && defaultTypeArguments.Count < n) {

         // there aren't enough default arguments, so don't do anything

       } else {

@@ -3833,27 +3856,15 @@ namespace Microsoft.Dafny
     public bool UnifyTypes(Type a, Type b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

-      while (a is TypeProxy) {

-        TypeProxy proxy = (TypeProxy)a;

-        if (proxy.T == null) {

-          // merge a and b; to avoid cycles, first get to the bottom of b

-          while (b is TypeProxy && ((TypeProxy)b).T != null) {

-            b = ((TypeProxy)b).T;

-          }

-          return AssignProxy(proxy, b);

-        } else {

-          a = proxy.T;

-        }

-      }

 

-      while (b is TypeProxy) {

-        TypeProxy proxy = (TypeProxy)b;

-        if (proxy.T == null) {

-          // merge a and b (we have already got to the bottom of a)

-          return AssignProxy(proxy, a);

-        } else {

-          b = proxy.T;

-        }

+      a = a.NormalizeExpand();

+      b = b.NormalizeExpand();

+      if (a is TypeProxy) {

+        // merge a and b (cycles are avoided even if b is a TypeProxy, since we have got to the bottom of both a and b)

+        return AssignProxy((TypeProxy)a, b);

+      } else if (b is TypeProxy) {

+        // merge a and b

+        return AssignProxy((TypeProxy)b, a);

       }

 

 #if !NO_CHEAP_OBJECT_WORKAROUND

@@ -3888,8 +3899,8 @@ namespace Microsoft.Dafny
         if (!(b is UserDefinedType)) {

           return false;

         }

-        UserDefinedType aa = (UserDefinedType)a;

-        UserDefinedType bb = (UserDefinedType)b;

+        var aa = (UserDefinedType)a;

+        var bb = (UserDefinedType)b;

         if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) {

           // these are both resolved class/datatype types

           Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count);

@@ -4719,11 +4730,11 @@ namespace Microsoft.Dafny
         }

         UserDefinedType sourceType = null;

         DatatypeDecl dtd = null;

-        Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

-        if (s.Source.Type.IsDatatype) {

-          sourceType = (UserDefinedType)s.Source.Type;

+        if (s.Source.Type.NormalizeExpand().IsDatatype) {

+          sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();

           dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);

         }

+        var subst = new Dictionary<TypeParameter, Type>();

         Dictionary<string, DatatypeCtor> ctors;

         if (dtd == null) {

           Error(s.Source, "the type of the match source expression must be a datatype (instead found {0})", s.Source.Type);

@@ -5669,7 +5680,7 @@ namespace Microsoft.Dafny
       Contract.Ensures(Contract.Result<MemberDecl>() == null || Contract.ValueAtReturn(out nptype) != null);

 

       nptype = null;  // prepare for the worst

-      receiverType = receiverType.Normalize();

+      receiverType = receiverType.NormalizeExpand();

       if (receiverType is TypeProxy) {

         Error(tok, "type of the receiver is not fully determined at this program point", receiverType);

         return null;

@@ -5739,7 +5750,7 @@ namespace Microsoft.Dafny
     /// <summary>

     /// If the substitution has no effect, the return value is pointer-equal to 'type'

     /// </summary>

-    public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/, Type/*!*/>/*!*/ subst) {

+    public static Type SubstType(Type type, Dictionary<TypeParameter, Type> subst) {

       Contract.Requires(type != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(subst));

       Contract.Ensures(Contract.Result<Type>() != null);

@@ -6642,11 +6653,11 @@ namespace Microsoft.Dafny
         Contract.Assert(me.Source.Type != null);  // follows from postcondition of ResolveExpression

         UserDefinedType sourceType = null;

         DatatypeDecl dtd = null;

-        Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();

-        if (me.Source.Type.IsDatatype) {

-          sourceType = (UserDefinedType)me.Source.Type;

+        if (me.Source.Type.NormalizeExpand().IsDatatype) {

+          sourceType = (UserDefinedType)me.Source.Type.NormalizeExpand();

           dtd = cce.NonNull((DatatypeDecl)sourceType.ResolvedClass);

         }

+        var subst = new Dictionary<TypeParameter, Type>();

         Dictionary<string, DatatypeCtor> ctors;

         if (dtd == null) {

           Error(me.Source, "the type of the match source expression must be a datatype (instead found {0})", me.Source.Type);

@@ -7338,7 +7349,7 @@ namespace Microsoft.Dafny
 

         bool itIsAMethod = false;

         if (allowMethodCall) {

-          var udt = r.Type.Normalize() as UserDefinedType;

+          var udt = r.Type.NormalizeExpand() as UserDefinedType;

           if (udt != null && udt.ResolvedClass != null) {

             Dictionary<string, MemberDecl> members;

             if (udt.ResolvedClass is ClassDecl) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a77590b4..30178e39 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -364,6 +364,8 @@ namespace Microsoft.Dafny {
           currentDeclaration = d;

           if (d is ArbitraryTypeDecl) {

             AddTypeDecl((ArbitraryTypeDecl)d);

+          } else if (d is TypeSynonymDecl) {

+            // do nothing, just bypass type synonyms in the translation

           } else if (d is DatatypeDecl) {

             AddDatatype((DatatypeDecl)d);

           } else if (d is ModuleDecl) {

@@ -4908,16 +4910,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(predef != null);

       Contract.Ensures(Contract.Result<Bpl.Type>() != null);

 

-      while (true) {

-        TypeProxy tp = type as TypeProxy;

-        if (tp == null) {

-          break;

-        } else if (tp.T == null) {

-          // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

-          return predef.RefType;

-        } else {

-          type = tp.T;

-        }

+      type = type.NormalizeExpand();

+      if (type is TypeProxy) {

+        // unresolved proxy; just treat as ref, since no particular type information is apparently needed for this type

+        return predef.RefType;

       }

 

       if (type is BoolType) {

@@ -4995,16 +4991,10 @@ namespace Microsoft.Dafny {
 

     public static bool ModeledAsBoxType(Type t) {

       Contract.Requires(t != null);

-      while (true) {

-        TypeProxy tp = t as TypeProxy;

-        if (tp == null) {

-          break;

-        } else if (tp.T == null) {

-          // unresolved proxy

-          return false;

-        } else {

-          t = tp.T;

-        }

+      t = t.NormalizeExpand();

+      if (t is TypeProxy) {

+        // unresolved proxy

+        return false;

       }

       return t.IsTypeParameter;

     }

@@ -7272,7 +7262,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

       var r = GetWhereClause(tok, x, type, etran);

-      type = type.Normalize();

+      type = type.NormalizeExpand();

       if (type.IsDatatype) {

         UserDefinedType udt = (UserDefinedType)type;

         var oneOfTheCases = FunctionCall(tok, "$IsA#" + udt.ResolvedClass.FullSanitizedName, Bpl.Type.Bool, x);

@@ -7286,27 +7276,28 @@ namespace Microsoft.Dafny {
     Bpl.Expr TypeToTy(Type type) {

       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

-      var tok = Token.NoToken;

+

+      type = type.NormalizeExpand();

 

       if (type is SetType) {

-        return FunctionCall(tok, "TSet", predef.Ty, TypeToTy(((CollectionType)type).Arg));

+        return FunctionCall(Token.NoToken, "TSet", predef.Ty, TypeToTy(((CollectionType)type).Arg));

       } else if (type is MultiSetType) {

-        return FunctionCall(tok, "TMultiSet", predef.Ty, TypeToTy(((CollectionType)type).Arg));

+        return FunctionCall(Token.NoToken, "TMultiSet", predef.Ty, TypeToTy(((CollectionType)type).Arg));

       } else if (type is SeqType) {

-        return FunctionCall(tok, "TSeq", predef.Ty, TypeToTy(((CollectionType)type).Arg));

+        return FunctionCall(Token.NoToken, "TSeq", predef.Ty, TypeToTy(((CollectionType)type).Arg));

       } else if (type is MapType) {

-        return FunctionCall(tok, "TMap", predef.Ty, 

+        return FunctionCall(Token.NoToken, "TMap", predef.Ty, 

           TypeToTy(((MapType)type).Domain),

           TypeToTy(((MapType)type).Range)); 

       } else if (type is BoolType) {

-        return new Bpl.IdentifierExpr(tok, "TBool", predef.Ty);

+        return new Bpl.IdentifierExpr(Token.NoToken, "TBool", predef.Ty);

       } else if (type is RealType) {

-        return new Bpl.IdentifierExpr(tok, "TReal", predef.Ty);

+        return new Bpl.IdentifierExpr(Token.NoToken, "TReal", predef.Ty);

       } else if (type is NatType) {

         // (Nat needs to come before Int)

-        return new Bpl.IdentifierExpr(tok, "TNat", predef.Ty);

+        return new Bpl.IdentifierExpr(Token.NoToken, "TNat", predef.Ty);

       } else if (type is IntType) {

-        return new Bpl.IdentifierExpr(tok, "TInt", predef.Ty);

+        return new Bpl.IdentifierExpr(Token.NoToken, "TInt", predef.Ty);

       } else if (type.IsTypeParameter) {

         return trTypeParam(type.AsTypeParameter);              

       } else if (type is ObjectType) {

@@ -7320,13 +7311,8 @@ namespace Microsoft.Dafny {
           args.Add(TypeToTy(ch));

         }

         return ClassTyCon(((UserDefinedType)type), args);      

-      } else if (type is TypeProxy || type is InferredTypeProxy || type is ParamTypeProxy) {

-        Type proxied = ((TypeProxy)type).T;

-        if (proxied == null && type is ParamTypeProxy) {

-          return trTypeParam(((ParamTypeProxy)type).orig);

-        } else {

-          return TypeToTy(proxied);

-        }

+      } else if (type is ParamTypeProxy) {

+        return trTypeParam(((ParamTypeProxy)type).orig);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

@@ -7417,18 +7403,12 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

 

-      while (true) {

-        TypeProxy proxy = type as TypeProxy;

-        if (proxy == null) {

-          break;

-        } else if (proxy.T == null) {

-          // Unresolved proxy

-          // Omit where clause (in other places, unresolved proxies are treated as a reference type; we could do that here too, but

-          // we might as well leave out the where clause altogether).

-          return null;

-        } else {

-          type = proxy.T;

-        }

+      type = type.NormalizeExpand();

+      if (type is TypeProxy) {

+        // Unresolved proxy

+        // Omit where clause (in other places, unresolved proxies are treated as a reference type; we could do that here too, but

+        // we might as well leave out the where clause altogether).

+        return null;

       }

 

       if (type is NatType) {

@@ -7448,7 +7428,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

 

-      if (type.Normalize() is BoolType) {

+      if (type.NormalizeExpand() is BoolType) {

         return FunctionCall(box.tok, BuiltinFunction.IsCanonicalBoolBox, null, box);

       } else {

         return Bpl.Expr.True;