Dafny: Merge

26 files changed, 1379 insertions, 641 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 3ccdeab1..bfce5122 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -154,7 +154,7 @@ Dafny
     )

   }

   (. // find the default class in the default module, then append membersDefaultClass to its member list

-     DefaultClassDecl defaultClass;

+     DefaultClassDecl defaultClass = null;

      foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

        defaultClass = topleveldecl as DefaultClassDecl;

        if (defaultClass != null) {

@@ -163,9 +163,8 @@ Dafny
        }

      }

      if (defaultClass == null) { // create the default class here, because it wasn't found

-       defaultClass = new DefaultClassDecl();

+       defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);

        defaultModule.TopLevelDecls.Add(defaultClass);

-       defaultClass.Members.AddRange(membersDefaultClass);

      } .)

   EOF

   .

@@ -311,10 +310,13 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
 ArbitraryTypeDecl<ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at>

 = (. IToken/*!*/ id;

      Attributes attrs = null;

+     var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

   .)

   "type"

   { Attribute<ref attrs> }

-  NoUSIdent<out id>               (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)

+  NoUSIdent<out id>

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

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

   SYNC ";"

   .

 GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>

@@ -377,10 +379,16 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
 /*------------------------------------------------------------------------*/

 GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>

 = (. Contract.Requires(cce.NonNullElements(typeArgs));

-     IToken/*!*/ id; .)

+     IToken/*!*/ id;

+     TypeParameter.EqualitySupportValue eqSupport;

+  .)

   "<"

-  NoUSIdent<out id>                       (. typeArgs.Add(new TypeParameter(id, id.val)); .)

-  { "," NoUSIdent<out id>                 (. typeArgs.Add(new TypeParameter(id, id.val)); .)

+  NoUSIdent<out id>              (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)

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

+    ]                        (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)

+  { "," NoUSIdent<out id>        (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)

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

+    ]                        (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)

   }

   ">"

   .

@@ -946,16 +954,13 @@ WhileStmt<out Statement/*!*/ stmt>
     )

     (.

       if (guardOmitted || bodyOmitted) {

-        if (decreases.Count != 0) {

-          SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");

-        }

         if (mod != null) {

           SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

         }

         if (body == null) {

           body = new BlockStmt(x, new List<Statement>());

         }

-        stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(null, null), new Specification<FrameExpression>(null, null), body);

+        stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);

         stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);

       } else {

         stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);

@@ -1051,11 +1056,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
 /*------------------------------------------------------------------------*/

 AssertStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-     Expression/*!*/ e = null; Attributes attrs = null;

+     Expression e = null; Attributes attrs = null;

   .)

-  "assert"                                     (. x = t; s = null;.)

+  "assert"                                     (. x = t; .)

   { IF(IsAttribute()) Attribute<ref attrs> }

-  ( Expression<out e>                 

+  ( Expression<out e>

   | "..."

   )

   ";"

@@ -1067,9 +1072,21 @@ AssertStmt<out Statement/*!*/ s>
   .)

   .

 AssumeStmt<out Statement/*!*/ s>

-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; .)

+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+     Expression e = null; Attributes attrs = null;

+  .)

   "assume"                                     (. x = t; .)

-  Expression<out e> ";"                        (. s = new AssumeStmt(x, e); .)

+  { IF(IsAttribute()) Attribute<ref attrs> }

+  ( Expression<out e>

+  | "..."

+  )

+  (. if (e == null) {

+       s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+     } else {

+       s = new AssumeStmt(x, e, attrs);

+     }

+  .)

+  ";"

   .

 PrintStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index c632f101..8038be10 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -276,8 +276,18 @@ namespace Microsoft.Dafny {
     }

     public bool IsTypeParameter {

       get {

+        return AsTypeParameter != null;

+      }

+    }

+    public TypeParameter AsTypeParameter {

+      get {

         UserDefinedType ct = this as UserDefinedType;

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

+        return ct == null ? null : ct.ResolvedParam;

+      }

+    }

+    public virtual bool SupportsEquality {

+      get {

+        return true;

       }

     }

   }

@@ -325,16 +335,20 @@ namespace Microsoft.Dafny {
 

   public abstract class CollectionType : NonProxyType

   {

-    public readonly Type Arg;

+    public readonly Type Arg;  // denotes the Domain type for a Map

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Arg != null);

     }

-

     public CollectionType(Type arg) {

       Contract.Requires(arg != null);

       this.Arg = arg;

     }

+    public override bool SupportsEquality {

+      get {

+        return Arg.SupportsEquality;

+      }

+    }

   }

 

   public class SetType : CollectionType {

@@ -376,12 +390,14 @@ namespace Microsoft.Dafny {
   }

   public class MapType : CollectionType

   {

-    public Type Domain, Range;

+    public Type Range;

     public MapType(Type domain, Type range) : base(domain) {

       Contract.Requires(domain != null && range != null);

-      Domain = domain;

       Range = range;

     }

+    public Type Domain {

+      get { return Arg; }

+    }

     [Pure]

     public override string ToString() {

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

@@ -522,6 +538,35 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

+

+    public override bool SupportsEquality {

+      get {

+        if (ResolvedClass is ClassDecl) {

+          return true;

+        } else if (ResolvedClass is CoDatatypeDecl) {

+          return false;

+        } else if (ResolvedClass is IndDatatypeDecl) {

+          var dt = (IndDatatypeDecl)ResolvedClass;

+          Contract.Assume(dt.EqualitySupport != IndDatatypeDecl.ES.NotYetComputed);

+          if (dt.EqualitySupport == IndDatatypeDecl.ES.Never) {

+            return false;

+          }

+          Contract.Assert(dt.TypeArgs.Count == TypeArgs.Count);

+          var i = 0;

+          foreach (var tp in dt.TypeArgs) {

+            if (tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype && !TypeArgs[i].SupportsEquality) {

+              return false;

+            }

+            i++;

+          }

+          return true;

+        } else if (ResolvedParam != null) {

+          return ResolvedParam.MustSupportEquality;

+        }

+        Contract.Assume(false);  // the SupportsEquality getter requires the Type to have been successfully resolved

+        return true;

+      }

+    }

   }

 

   public abstract class TypeProxy : Type {

@@ -536,6 +581,15 @@ namespace Microsoft.Dafny {
       Contract.Assume(T == null || cce.IsPeerConsistent(T));

       return T == null ? "?" : T.ToString();

     }

+    public override bool SupportsEquality {

+      get {

+        if (T != null) {

+          return T.SupportsEquality;

+        } else {

+          return base.SupportsEquality;

+        }

+      }

+    }

   }

 

   public abstract class UnrestrictedTypeProxy : TypeProxy {

@@ -596,17 +650,6 @@ namespace Microsoft.Dafny {
   }

 

   /// <summary>

-  /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.

-  /// </summary>

-  public class ObjectsTypeProxy : RestrictedTypeProxy {

-    public override int OrderID {

-      get {

-        return 2;

-      }

-    }

-  }

-

-  /// <summary>

   /// This proxy stands for:

   ///     set(Arg) or seq(Arg) or map(Arg, Range)

   /// </summary>

@@ -623,7 +666,7 @@ namespace Microsoft.Dafny {
     }

     public override int OrderID {

       get {

-        return 3;

+        return 2;

       }

     }

   }

@@ -642,7 +685,7 @@ namespace Microsoft.Dafny {
     }

     public override int OrderID {

       get {

-        return 4;

+        return 3;

       }

     }

   }

@@ -665,7 +708,7 @@ namespace Microsoft.Dafny {
     }

     public override int OrderID {

       get {

-        return 5;

+        return 4;

       }

     }

   }

@@ -730,10 +773,19 @@ namespace Microsoft.Dafny {
         parent = value;

       }

     }

-    public TypeParameter(IToken tok, string name)

+    public enum EqualitySupportValue { Required, InferredRequired, Unspecified }

+    public EqualitySupportValue EqualitySupport;  // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required)

+    public bool MustSupportEquality {

+      get { return EqualitySupport != EqualitySupportValue.Unspecified; }

+    }

+

+    public bool NecessaryForEqualitySupportOfSurroundingInductiveDatatype = false;  // computed during resolution; relevant only when Parent denotes an IndDatatypeDecl

+

+    public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)

       : base(tok, name, null) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

+      EqualitySupport = equalitySupport;

     }

   }

 

@@ -968,7 +1020,10 @@ namespace Microsoft.Dafny {
   public class IndDatatypeDecl : DatatypeDecl

   {

     public DatatypeCtor DefaultCtor;  // set during resolution

-    public bool[] TypeParametersUsedInConstructionByDefaultCtor;  // set during resolution; has same length as

+    public bool[] TypeParametersUsedInConstructionByDefaultCtor;  // set during resolution; has same length as the number of type arguments

+

+    public enum ES { NotYetComputed, Never, ConsultTypeArguments }

+    public ES EqualitySupport = ES.NotYetComputed;

 

     public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List<TypeParameter/*!*/>/*!*/ typeArgs,

       [Captured] List<DatatypeCtor/*!*/>/*!*/ ctors, Attributes attributes)

@@ -1033,13 +1088,15 @@ namespace Microsoft.Dafny {
 

   public abstract class MemberDecl : Declaration {

     public readonly bool IsStatic;

+    public readonly bool IsGhost;

     public TopLevelDecl EnclosingClass;  // filled in during resolution

 

-    public MemberDecl(IToken tok, string name, bool isStatic, Attributes attributes)

+    public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       IsStatic = isStatic;

+      IsGhost = isGhost;

     }

     /// <summary>

     /// Returns className+"."+memberName.  Available only after resolution.

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

 

   public class Field : MemberDecl {

-    public readonly bool IsGhost;

     public readonly bool IsMutable;

     public readonly Type Type;

     [ContractInvariantMethod]

@@ -1079,11 +1135,10 @@ namespace Microsoft.Dafny {
     }

 

     public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)

-      : base(tok, name, false, attributes) {

+      : base(tok, name, false, isGhost, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(type != null);

-      IsGhost = isGhost;

       IsMutable = isMutable;

       Type = type;

     }

@@ -1123,17 +1178,23 @@ namespace Microsoft.Dafny {
   public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType

   {

     public readonly TypeParameter TheType;

+    public TypeParameter.EqualitySupportValue EqualitySupport {

+      get { return TheType.EqualitySupport; }

+    }

+    public bool MustSupportEquality {

+      get { return TheType.MustSupportEquality; }

+    }

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

     }

 

-    public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, Attributes attributes)

+    public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, 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);

+      TheType = new TypeParameter(tok, name, equalitySupport);

     }

   }

 

@@ -1233,7 +1294,7 @@ namespace Microsoft.Dafny {
             return name + nm.Substring(i);

           }

         } else {

-          string nxt = nm.Substring(i, j);

+          string nxt = nm.Substring(i, j - i);

           name = name == null ? nxt : name + nxt;

           switch (nm[j]) {

             case '\'': name += "_k"; break;

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

 

   public class Function : MemberDecl, TypeParameter.ParentType {

-    public readonly bool IsGhost;  // functions are "ghost" by default; a non-ghost function is called a "function method"

     public bool IsRecursive;  // filled in during resolution

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly IToken OpenParen;  // can be null (for predicates), if there are no formals

@@ -1377,11 +1437,14 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Decreases != null);

     }

 

+    /// <summary>

+    /// Note, functions are "ghost" by default; a non-ghost function is called a "function method".

+    /// </summary>

     public Function(IToken tok, string name, bool isStatic, bool isGhost,

                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,

                     List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,

                     Expression body, Attributes attributes, bool signatureOmitted)

-      : base(tok, name, isStatic, attributes) {

+      : base(tok, name, isStatic, isGhost, attributes) {

 

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -1392,7 +1455,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(reads));

       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

-      this.IsGhost = isGhost;

       this.TypeArgs = typeArgs;

       this.OpenParen = openParen;

       this.Formals = formals;

@@ -1421,7 +1483,6 @@ namespace Microsoft.Dafny {
 

   public class Method : MemberDecl, TypeParameter.ParentType

   {

-    public readonly bool IsGhost;

     public readonly bool SignatureIsOmitted;

     public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;

     public readonly List<Formal/*!*/>/*!*/ Ins;

@@ -1452,7 +1513,7 @@ namespace Microsoft.Dafny {
                   [Captured] Specification<Expression>/*!*/ decreases,

                   [Captured] BlockStmt body,

                   Attributes attributes, bool signatureOmitted)

-      : base(tok, name, isStatic, attributes) {

+      : base(tok, name, isStatic, isGhost, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(cce.NonNullElements(typeArgs));

@@ -1462,7 +1523,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(mod != null);

       Contract.Requires(cce.NonNullElements(ens));

       Contract.Requires(decreases != null);

-      this.IsGhost = isGhost;

       this.TypeArgs = typeArgs;

       this.Ins = ins;

       this.Outs = outs;

@@ -1587,60 +1647,40 @@ namespace Microsoft.Dafny {
 

   public abstract class PredicateStmt : Statement

   {

-    [Peer]

     public readonly Expression Expr;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Expr != null);

     }

 

-    [Captured]

     public PredicateStmt(IToken tok, Expression expr, Attributes attrs)

       : base(tok, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-      cce.Owner.AssignSame(this, expr);

       this.Expr = expr;

     }

 

-    [Captured]

     public PredicateStmt(IToken tok, Expression expr)

       : this(tok, expr, null) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-      cce.Owner.AssignSame(this, expr);

       this.Expr = expr;

     }

   }

 

   public class AssertStmt : PredicateStmt {

-    [Captured]

     public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)

       : base(tok, expr, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-    }

-

-    [Captured]

-    public AssertStmt(IToken/*!*/ tok, Expression/*!*/ expr)

-      : this(tok, expr, null) {

-      Contract.Requires(tok != null);

-      Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

     }

   }

 

   public class AssumeStmt : PredicateStmt {

-    [Captured]

-    public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr)

-      : base(tok, expr) {

+    public AssumeStmt(IToken/*!*/ tok, Expression/*!*/ expr, Attributes attrs)

+      : base(tok, expr, attrs) {

       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

-      Contract.Ensures(cce.Owner.Same(this, expr));

-

     }

   }

 

@@ -1720,6 +1760,18 @@ namespace Microsoft.Dafny {
       Attributes = attrs;

     }

     public abstract bool CanAffectPreviouslyKnownExpressions { get; }

+    /// <summary>

+    /// Returns the non-null subexpressions of the AssignmentRhs.

+    /// </summary>

+    public virtual IEnumerable<Expression> SubExpressions {

+      get { yield break; }

+    }

+    /// <summary>

+    /// Returns the non-null sub-statements of the AssignmentRhs.

+    /// </summary>

+    public virtual IEnumerable<Statement> SubStatements{

+      get { yield break; }

+    }

   }

 

   public class ExprRhs : AssignmentRhs

@@ -1737,6 +1789,11 @@ namespace Microsoft.Dafny {
       Expr = expr;

     }

     public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Expr;

+      }

+    }

   }

 

   public class TypeRhs : AssignmentRhs

@@ -1785,6 +1842,23 @@ namespace Microsoft.Dafny {
         return false;

       }

     }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        if (ArrayDimensions != null) {

+          foreach (var e in ArrayDimensions) {

+            yield return e;

+          }

+        }

+      }

+    }

+    public override IEnumerable<Statement> SubStatements {

+      get {

+        if (InitCall != null) {

+          yield return InitCall;

+        }

+      }

+    }

   }

 

   public class CallRhs : AssignmentRhs

@@ -1824,6 +1898,14 @@ namespace Microsoft.Dafny {
         return false;

       }

     }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Receiver;

+        foreach (var e in Args) {

+          yield return e;

+        }

+      }

+    }

   }

 

   public class HavocRhs : AssignmentRhs {

@@ -2060,6 +2142,7 @@ namespace Microsoft.Dafny {
     public Expression/*!*/ Receiver;

     public readonly string/*!*/ MethodName;

     public readonly List<Expression/*!*/>/*!*/ Args;

+    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // create, initialized, and used by resolution (could be deleted once all of resolution is done)

     public Method Method;  // filled in by resolution

 

     public CallStmt(IToken tok, List<Expression/*!*/>/*!*/ lhs, Expression/*!*/ receiver,

@@ -2098,13 +2181,13 @@ namespace Microsoft.Dafny {
     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Thn != null);

-      Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt);

+      Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt || Els is SkeletonStatement);

     }

     public IfStmt(IToken tok, Expression guard, BlockStmt thn, Statement els)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(thn != null);

-      Contract.Requires(els == null || els is BlockStmt || els is IfStmt);

+      Contract.Requires(els == null || els is BlockStmt || els is IfStmt || els is SkeletonStatement);

       this.Guard = guard;

       this.Thn = thn;

       this.Els = els;

@@ -2216,6 +2299,21 @@ namespace Microsoft.Dafny {
     }

   }

 

+  /// <summary>

+  /// This class is really just a WhileStmt, except that it serves the purpose of remembering if the object was created as the result of a refinement

+  /// merge.

+  /// </summary>

+  public class RefinedWhileStmt : WhileStmt

+  {

+    public RefinedWhileStmt(IToken tok, Expression guard,

+                            List<MaybeFreeExpression/*!*/>/*!*/ invariants, Specification<Expression>/*!*/ decreases, Specification<FrameExpression>/*!*/ mod,

+                            BlockStmt/*!*/ body)

+      : base(tok, guard, invariants, decreases, mod, body) {

+      Contract.Requires(tok != null);

+      Contract.Requires(body != null);

+    }

+  }

+

   public class AlternativeLoopStmt : LoopStmt

   {

     public readonly List<GuardedAlternative> Alternatives;

@@ -2382,6 +2480,8 @@ namespace Microsoft.Dafny {
   ///   S == null

   /// * assert ...

   ///   ConditionOmitted == true

+  /// * assume ...

+  ///   ConditionOmitted == true

   /// * if ... { Stmt }

   ///   if ... { Stmt } else ElseStmt

   ///   ConditionOmitted == true

@@ -2850,6 +2950,7 @@ namespace Microsoft.Dafny {
     public readonly Expression/*!*/ Receiver;

     public readonly IToken OpenParen;  // can be null if Args.Count == 0

     public readonly List<Expression/*!*/>/*!*/ Args;

+    public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions;  // create, initialized, and used by resolution (could be deleted once all of resolution is done)

     public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }

     public CoCallResolution CoCall = CoCallResolution.No;  // indicates whether or not the call is a co-recursive call; filled in by resolution

 

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 77e4d2ef..9ad05d3b 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -223,8 +223,8 @@ bool IsAttribute() {
 		 }

 		}

 		if (defaultClass == null) { // create the default class here, because it wasn't found

-      defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);

-		  defaultModule.TopLevelDecls.Add(defaultClass);

+		 defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);

+		 defaultModule.TopLevelDecls.Add(defaultClass);

 		} 

 		Expect(0);

 	}

@@ -309,7 +309,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 23) {

+		if (la.kind == 26) {

 			GenericParameters(typeArgs);

 		}

 		Expect(6);

@@ -345,7 +345,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 23) {

+		if (la.kind == 26) {

 			GenericParameters(typeArgs);

 		}

 		Expect(11);

@@ -370,13 +370,20 @@ bool IsAttribute() {
 	void ArbitraryTypeDecl(ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at) {

 		IToken/*!*/ id;

 		Attributes attrs = null;

+		var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;

 		

 		Expect(22);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

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

+		if (la.kind == 23) {

+			Get();

+			Expect(24);

+			Expect(25);

+			eqSupport = TypeParameter.EqualitySupportValue.Required; 

+		}

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

 		while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();}

 		Expect(12);

 	}

@@ -399,10 +406,10 @@ bool IsAttribute() {
 		}

 		if (la.kind == 20) {

 			FieldDecl(mmod, mm);

-		} else if (la.kind == 44 || la.kind == 45) {

+		} else if (la.kind == 45 || la.kind == 46) {

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

-		} else if (la.kind == 25 || la.kind == 26) {

+		} else if (la.kind == 28 || la.kind == 29) {

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

 		} else SynErr(116);

@@ -443,16 +450,32 @@ bool IsAttribute() {
 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

 		Contract.Requires(cce.NonNullElements(typeArgs));

-		IToken/*!*/ id; 

-		Expect(23);

+		IToken/*!*/ id;

+		TypeParameter.EqualitySupportValue eqSupport;

+		

+		Expect(26);

 		NoUSIdent(out id);

-		typeArgs.Add(new TypeParameter(id, id.val)); 

+		eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

+		if (la.kind == 23) {

+			Get();

+			Expect(24);

+			Expect(25);

+			eqSupport = TypeParameter.EqualitySupportValue.Required; 

+		}

+		typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); 

 		while (la.kind == 21) {

 			Get();

 			NoUSIdent(out id);

-			typeArgs.Add(new TypeParameter(id, id.val)); 

+			eqSupport = TypeParameter.EqualitySupportValue.Unspecified; 

+			if (la.kind == 23) {

+				Get();

+				Expect(24);

+				Expect(25);

+				eqSupport = TypeParameter.EqualitySupportValue.Required; 

+			}

+			typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); 

 		}

-		Expect(24);

+		Expect(27);

 	}

 

 	void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {

@@ -497,9 +520,9 @@ bool IsAttribute() {
 		IToken bodyEnd = Token.NoToken;

 		bool signatureOmitted = false;

 		

-		if (la.kind == 44) {

+		if (la.kind == 45) {

 			Get();

-			if (la.kind == 25) {

+			if (la.kind == 28) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -509,22 +532,22 @@ bool IsAttribute() {
 				Attribute(ref attrs);

 			}

 			NoUSIdent(out id);

-			if (la.kind == 23 || la.kind == 34) {

-				if (la.kind == 23) {

+			if (la.kind == 23 || la.kind == 26) {

+				if (la.kind == 26) {

 					GenericParameters(typeArgs);

 				}

 				Formals(true, isFunctionMethod, formals, out openParen);

 				Expect(5);

 				Type(out returnType);

-			} else if (la.kind == 28) {

+			} else if (la.kind == 31) {

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

 			} else SynErr(119);

-		} else if (la.kind == 45) {

+		} else if (la.kind == 46) {

 			Get();

 			isPredicate = true; 

-			if (la.kind == 25) {

+			if (la.kind == 28) {

 				Get();

 				isFunctionMethod = true; 

 			}

@@ -535,17 +558,17 @@ bool IsAttribute() {
 			}

 			NoUSIdent(out id);

 			if (StartOf(3)) {

-				if (la.kind == 23) {

+				if (la.kind == 26) {

 					GenericParameters(typeArgs);

 				}

-				if (la.kind == 34) {

+				if (la.kind == 23) {

 					Formals(true, isFunctionMethod, formals, out openParen);

 					if (la.kind == 5) {

 						Get();

 						SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 

 					}

 				}

-			} else if (la.kind == 28) {

+			} else if (la.kind == 31) {

 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

@@ -589,10 +612,10 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

-		while (!(la.kind == 0 || la.kind == 25 || la.kind == 26)) {SynErr(122); Get();}

-		if (la.kind == 25) {

+		while (!(la.kind == 0 || la.kind == 28 || la.kind == 29)) {SynErr(122); Get();}

+		if (la.kind == 28) {

 			Get();

-		} else if (la.kind == 26) {

+		} else if (la.kind == 29) {

 			Get();

 			if (allowConstructor) {

 			 isConstructor = true;

@@ -614,17 +637,17 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 23 || la.kind == 34) {

-			if (la.kind == 23) {

+		if (la.kind == 23 || la.kind == 26) {

+			if (la.kind == 26) {

 				GenericParameters(typeArgs);

 			}

 			Formals(true, !mmod.IsGhost, ins, out openParen);

-			if (la.kind == 27) {

+			if (la.kind == 30) {

 				Get();

 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 				Formals(false, !mmod.IsGhost, outs, out openParen);

 			}

-		} else if (la.kind == 28) {

+		} else if (la.kind == 31) {

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

 		} else SynErr(124);

@@ -656,7 +679,7 @@ bool IsAttribute() {
 			Attribute(ref attrs);

 		}

 		NoUSIdent(out id);

-		if (la.kind == 34) {

+		if (la.kind == 23) {

 			FormalsOptionalIds(formals);

 		}

 		ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); 

@@ -664,7 +687,7 @@ bool IsAttribute() {
 

 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 

-		Expect(34);

+		Expect(23);

 		if (StartOf(6)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost)); 

@@ -674,7 +697,7 @@ bool IsAttribute() {
 				formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			}

 		}

-		Expect(35);

+		Expect(25);

 	}

 

 	void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {

@@ -758,22 +781,22 @@ bool IsAttribute() {
 		List<Type/*!*/>/*!*/ gt;

 		

 		switch (la.kind) {

-		case 36: {

+		case 37: {

 			Get();

 			tok = t; 

 			break;

 		}

-		case 37: {

+		case 38: {

 			Get();

 			tok = t;  ty = new NatType(); 

 			break;

 		}

-		case 38: {

+		case 39: {

 			Get();

 			tok = t;  ty = new IntType(); 

 			break;

 		}

-		case 39: {

+		case 40: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -784,7 +807,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 40: {

+		case 41: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -795,7 +818,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 41: {

+		case 42: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -806,7 +829,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 42: {

+		case 43: {

 			Get();

 			tok = t;  gt = new List<Type/*!*/>(); 

 			GenericInstantiation(gt);

@@ -817,7 +840,7 @@ bool IsAttribute() {
 			

 			break;

 		}

-		case 1: case 3: case 43: {

+		case 1: case 3: case 44: {

 			ReferenceType(out tok, out ty);

 			break;

 		}

@@ -827,7 +850,7 @@ bool IsAttribute() {
 

 	void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  bool isGhost; 

-		Expect(34);

+		Expect(23);

 		openParen = t; 

 		if (la.kind == 1 || la.kind == 8) {

 			GIdentType(allowGhostKeyword, out id, out ty, out isGhost);

@@ -838,7 +861,7 @@ bool IsAttribute() {
 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); 

 			}

 		}

-		Expect(35);

+		Expect(25);

 	}

 

 	void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,

@@ -847,7 +870,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

 		while (!(StartOf(7))) {SynErr(126); Get();}

-		if (la.kind == 29) {

+		if (la.kind == 32) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref modAttrs);

@@ -863,18 +886,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			while (!(la.kind == 0 || la.kind == 12)) {SynErr(127); Get();}

 			Expect(12);

-		} else if (la.kind == 30 || la.kind == 31 || la.kind == 32) {

-			if (la.kind == 30) {

+		} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {

+			if (la.kind == 33) {

 				Get();

 				isFree = true; 

 			}

-			if (la.kind == 31) {

+			if (la.kind == 34) {

 				Get();

 				Expression(out e);

 				while (!(la.kind == 0 || la.kind == 12)) {SynErr(128); Get();}

 				Expect(12);

 				req.Add(new MaybeFreeExpression(e, isFree)); 

-			} else if (la.kind == 32) {

+			} else if (la.kind == 35) {

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref ensAttrs);

@@ -884,7 +907,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Expect(12);

 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 

 			} else SynErr(130);

-		} else if (la.kind == 33) {

+		} else if (la.kind == 36) {

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

@@ -912,7 +935,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void FrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e;  IToken/*!*/ id;  string fieldName = null; 

 		Expression(out e);

-		if (la.kind == 48) {

+		if (la.kind == 49) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

@@ -947,7 +970,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {

 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 

-		Expect(23);

+		Expect(26);

 		Type(out ty);

 		gt.Add(ty); 

 		while (la.kind == 21) {

@@ -955,7 +978,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Type(out ty);

 			gt.Add(ty); 

 		}

-		Expect(24);

+		Expect(27);

 	}

 

 	void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {

@@ -964,7 +987,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken moduleName = null;

 		List<Type/*!*/>/*!*/ gt;

 		

-		if (la.kind == 43) {

+		if (la.kind == 44) {

 			Get();

 			tok = t;  ty = new ObjectType(); 

 		} else if (la.kind == 3) {

@@ -988,7 +1011,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				Get();

 				Ident(out tok);

 			}

-			if (la.kind == 23) {

+			if (la.kind == 26) {

 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt, moduleName); 

@@ -998,14 +1021,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

 		Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

-		if (la.kind == 31) {

-			while (!(la.kind == 0 || la.kind == 31)) {SynErr(134); Get();}

+		if (la.kind == 34) {

+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(134); Get();}

 			Get();

 			Expression(out e);

 			while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();}

 			Expect(12);

 			reqs.Add(e); 

-		} else if (la.kind == 46) {

+		} else if (la.kind == 47) {

 			Get();

 			if (StartOf(10)) {

 				PossiblyWildFrameExpression(out fe);

@@ -1018,13 +1041,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			while (!(la.kind == 0 || la.kind == 12)) {SynErr(136); Get();}

 			Expect(12);

-		} else if (la.kind == 32) {

+		} else if (la.kind == 35) {

 			Get();

 			Expression(out e);

 			while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}

 			Expect(12);

 			ens.Add(e); 

-		} else if (la.kind == 33) {

+		} else if (la.kind == 36) {

 			Get();

 			DecreasesList(decreases, false);

 			while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}

@@ -1043,7 +1066,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {

 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 

-		if (la.kind == 47) {

+		if (la.kind == 48) {

 			Get();

 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(8)) {

@@ -1054,7 +1077,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void PossiblyWildExpression(out Expression/*!*/ e) {

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

 		e = dummyExpr; 

-		if (la.kind == 47) {

+		if (la.kind == 48) {

 			Get();

 			e = new WildcardExpr(t); 

 		} else if (StartOf(8)) {

@@ -1083,19 +1106,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s = bs; 

 			break;

 		}

-		case 66: {

+		case 67: {

 			AssertStmt(out s);

 			break;

 		}

-		case 54: {

+		case 55: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 67: {

+		case 68: {

 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 2: case 19: case 34: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

+		case 1: case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

 			UpdateStmt(out s);

 			break;

 		}

@@ -1103,23 +1126,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);

 			break;

 		}

-		case 59: {

+		case 60: {

 			IfStmt(out s);

 			break;

 		}

-		case 63: {

+		case 64: {

 			WhileStmt(out s);

 			break;

 		}

-		case 65: {

+		case 66: {

 			MatchStmt(out s);

 			break;

 		}

-		case 68: {

+		case 69: {

 			ParallelStmt(out s);

 			break;

 		}

-		case 49: {

+		case 50: {

 			Get();

 			x = t; 

 			NoUSIdent(out id);

@@ -1128,14 +1151,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s.Labels = new LList<Label>(new Label(x, id.val), s.Labels); 

 			break;

 		}

-		case 50: {

+		case 51: {

 			Get();

 			x = t; breakCount = 1; label = null; 

 			if (la.kind == 1) {

 				NoUSIdent(out id);

 				label = id.val; 

-			} else if (la.kind == 12 || la.kind == 50) {

-				while (la.kind == 50) {

+			} else if (la.kind == 12 || la.kind == 51) {

+				while (la.kind == 51) {

 					Get();

 					breakCount++; 

 				}

@@ -1145,11 +1168,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

 		}

-		case 51: {

+		case 52: {

 			ReturnStmt(out s);

 			break;

 		}

-		case 28: {

+		case 31: {

 			Get();

 			s = new SkeletonStatement(t); 

 			Expect(12);

@@ -1161,16 +1184,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void AssertStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

-		Expression/*!*/ e = null; Attributes attrs = null;

+		Expression e = null; Attributes attrs = null;

 		

-		Expect(66);

-		x = t; s = null;

+		Expect(67);

+		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

 		if (StartOf(8)) {

 			Expression(out e);

-		} else if (la.kind == 28) {

+		} else if (la.kind == 31) {

 			Get();

 		} else SynErr(146);

 		Expect(12);

@@ -1183,19 +1206,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AssumeStmt(out Statement/*!*/ s) {

-		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Expression/*!*/ e; 

-		Expect(54);

+		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

+		Expression e = null; Attributes attrs = null;

+		

+		Expect(55);

 		x = t; 

-		Expression(out e);

+		while (IsAttribute()) {

+			Attribute(ref attrs);

+		}

+		if (StartOf(8)) {

+			Expression(out e);

+		} else if (la.kind == 31) {

+			Get();

+		} else SynErr(147);

+		if (e == null) {

+		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);

+		} else {

+		 s = new AssumeStmt(x, e, attrs);

+		}

+		

 		Expect(12);

-		s = new AssumeStmt(x, e); 

 	}

 

 	void PrintStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

 		List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();

 		

-		Expect(67);

+		Expect(68);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

@@ -1226,14 +1263,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(12);

 			rhss.Add(new ExprRhs(e, attrs)); 

-		} else if (la.kind == 21 || la.kind == 52 || la.kind == 53) {

+		} else if (la.kind == 21 || la.kind == 53 || la.kind == 54) {

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 21) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			if (la.kind == 52) {

+			if (la.kind == 53) {

 				Get();

 				x = t; 

 				Rhs(out r, lhs0);

@@ -1243,20 +1280,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Rhs(out r, lhs0);

 					rhss.Add(r); 

 				}

-			} else if (la.kind == 53) {

+			} else if (la.kind == 54) {

 				Get();

 				x = t; 

-				if (la.kind == 54) {

+				if (la.kind == 55) {

 					Get();

 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(147);

+			} else SynErr(148);

 			Expect(12);

 		} else if (la.kind == 5) {

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(148);

+		} else SynErr(149);

 		if (suchThat != null) {

 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);

 		} else {

@@ -1287,8 +1324,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LocalIdentTypeOptional(out d, isGhost);

 			lhss.Add(d); 

 		}

-		if (la.kind == 52 || la.kind == 53) {

-			if (la.kind == 52) {

+		if (la.kind == 53 || la.kind == 54) {

+			if (la.kind == 53) {

 				Get();

 				assignTok = t;

 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);

@@ -1304,7 +1341,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {

 				Get();

 				assignTok = t; 

-				if (la.kind == 54) {

+				if (la.kind == 55) {

 					Get();

 					suchThatAssume = t; 

 				}

@@ -1343,25 +1380,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(59);

+		Expect(60);

 		x = t; 

-		if (la.kind == 28 || la.kind == 34) {

-			if (la.kind == 34) {

+		if (la.kind == 23 || la.kind == 31) {

+			if (la.kind == 23) {

 				Guard(out guard);

 			} else {

 				Get();

 				guardOmitted = true; 

 			}

 			BlockStmt(out thn, out bodyStart, out bodyEnd);

-			if (la.kind == 60) {

+			if (la.kind == 61) {

 				Get();

-				if (la.kind == 59) {

+				if (la.kind == 60) {

 					IfStmt(out s);

 					els = s; 

 				} else if (la.kind == 6) {

 					BlockStmt(out bs, out bodyStart, out bodyEnd);

 					els = bs; 

-				} else SynErr(149);

+				} else SynErr(150);

 			}

 			if (guardOmitted) {

 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);

@@ -1372,7 +1409,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 6) {

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(150);

+		} else SynErr(151);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1388,10 +1425,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(63);

+		Expect(64);

 		x = t; 

-		if (la.kind == 28 || la.kind == 34) {

-			if (la.kind == 34) {

+		if (la.kind == 23 || la.kind == 31) {

+			if (la.kind == 23) {

 				Guard(out guard);

 				Contract.Assume(guard == null || cce.Owner.None(guard)); 

 			} else {

@@ -1401,21 +1438,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			if (la.kind == 6) {

 				BlockStmt(out body, out bodyStart, out bodyEnd);

-			} else if (la.kind == 28) {

+			} else if (la.kind == 31) {

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(151);

+			} else SynErr(152);

 			if (guardOmitted || bodyOmitted) {

-			 if (decreases.Count != 0) {

-			   SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops");

-			 }

 			 if (mod != null) {

 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");

 			 }

 			 if (body == null) {

 			   body = new BlockStmt(x, new List<Statement>());

 			 }

-			 stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(null, null), new Specification<FrameExpression>(null, null), body);

+			 stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);

 			 stmt = new SkeletonStatement(stmt, guardOmitted, bodyOmitted);

 			} else {

 			 stmt = new WhileStmt(x, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);

@@ -1425,18 +1459,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives); 

-		} else SynErr(152);

+		} else SynErr(153);

 	}

 

 	void MatchStmt(out Statement/*!*/ s) {

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

 		Token x;  Expression/*!*/ e;  MatchCaseStmt/*!*/ c;

 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>(); 

-		Expect(65);

+		Expect(66);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 61) {

+		while (la.kind == 62) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1456,9 +1490,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(68);

+		Expect(69);

 		x = t; 

-		Expect(34);

+		Expect(23);

 		if (la.kind == 1) {

 			List<BoundVar/*!*/> bvarsX;  Attributes attrsX;  Expression rangeX; 

 			QuantifierDomain(out bvarsX, out attrsX, out rangeX);

@@ -1468,14 +1502,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (bvars == null) { bvars = new List<BoundVar>(); }

 		if (range == null) { range = new LiteralExpr(x, true); }

 		

-		Expect(35);

-		while (la.kind == 30 || la.kind == 32) {

+		Expect(25);

+		while (la.kind == 33 || la.kind == 35) {

 			isFree = false; 

-			if (la.kind == 30) {

+			if (la.kind == 33) {

 				Get();

 				isFree = true; 

 			}

-			Expect(32);

+			Expect(35);

 			Expression(out e);

 			Expect(12);

 			ens.Add(new MaybeFreeExpression(e, isFree)); 

@@ -1489,7 +1523,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<AssignmentRhs> rhss = null;

 		AssignmentRhs r;

 		

-		Expect(51);

+		Expect(52);

 		returnTok = t; 

 		if (StartOf(13)) {

 			Rhs(out r, null);

@@ -1513,27 +1547,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 55) {

+		if (la.kind == 56) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

-			if (la.kind == 14 || la.kind == 34 || la.kind == 56) {

-				if (la.kind == 56) {

+			if (la.kind == 14 || la.kind == 23 || la.kind == 57) {

+				if (la.kind == 57) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(57);

+					Expect(58);

 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);

 					

 				} else if (la.kind == 14) {

 					Get();

 					Ident(out x);

-					Expect(34);

+					Expect(23);

 					args = new List<Expression/*!*/>(); 

 					if (StartOf(8)) {

 						Expressions(args);

 					}

-					Expect(35);

+					Expect(25);

 					initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); 

 				} else {

 					Get();

@@ -1551,7 +1585,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					if (StartOf(8)) {

 						Expressions(args);

 					}

-					Expect(35);

+					Expect(25);

 					if (x != null) {

 					 initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);

 					}

@@ -1564,18 +1598,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

-		} else if (la.kind == 58) {

+		} else if (la.kind == 59) {

 			Get();

 			x = t; 

 			Expression(out e);

 			r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); 

-		} else if (la.kind == 47) {

+		} else if (la.kind == 48) {

 			Get();

 			r = new HavocRhs(t); 

 		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(153);

+		} else SynErr(154);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -1587,16 +1621,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 14 || la.kind == 56) {

+			while (la.kind == 14 || la.kind == 57) {

 				Suffix(ref e);

 			}

 		} else if (StartOf(14)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

-			while (la.kind == 14 || la.kind == 56) {

+			while (la.kind == 14 || la.kind == 57) {

 				Suffix(ref e);

 			}

-		} else SynErr(154);

+		} else SynErr(155);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1612,15 +1646,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

-		Expect(34);

-		if (la.kind == 47) {

+		Expect(23);

+		if (la.kind == 48) {

 			Get();

 			e = null; 

 		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(155);

-		Expect(35);

+		} else SynErr(156);

+		Expect(25);

 	}

 

 	void AlternativeBlock(out List<GuardedAlternative> alternatives) {

@@ -1630,11 +1664,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;

 		

 		Expect(6);

-		while (la.kind == 61) {

+		while (la.kind == 62) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(62);

+			Expect(63);

 			body = new List<Statement>(); 

 			while (StartOf(9)) {

 				Stmt(body);

@@ -1652,22 +1686,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		mod = null;

 		

 		while (StartOf(15)) {

-			if (la.kind == 30 || la.kind == 64) {

+			if (la.kind == 33 || la.kind == 65) {

 				Invariant(out invariant);

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(156); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(157); Get();}

 				Expect(12);

 				invariants.Add(invariant); 

-			} else if (la.kind == 33) {

-				while (!(la.kind == 0 || la.kind == 33)) {SynErr(157); Get();}

+			} else if (la.kind == 36) {

+				while (!(la.kind == 0 || la.kind == 36)) {SynErr(158); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(158); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); Get();}

 				Expect(12);

 			} else {

-				while (!(la.kind == 0 || la.kind == 29)) {SynErr(159); Get();}

+				while (!(la.kind == 0 || la.kind == 32)) {SynErr(160); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1682,7 +1716,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(160); Get();}

+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(161); Get();}

 				Expect(12);

 			}

 		}

@@ -1690,12 +1724,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 30 || la.kind == 64)) {SynErr(161); Get();}

-		if (la.kind == 30) {

+		while (!(la.kind == 0 || la.kind == 33 || la.kind == 65)) {SynErr(162); Get();}

+		if (la.kind == 33) {

 			Get();

 			isFree = true; 

 		}

-		Expect(64);

+		Expect(65);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1710,10 +1744,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		List<Statement/*!*/> body = new List<Statement/*!*/>();

 		

-		Expect(61);

+		Expect(62);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 23) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

@@ -1722,9 +1756,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(35);

+			Expect(25);

 		}

-		Expect(62);

+		Expect(63);

 		while (StartOf(9)) {

 			Stmt(body);

 		}

@@ -1739,7 +1773,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(8)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(162);

+		} else SynErr(163);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1767,7 +1801,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void EquivExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpression(out e0);

-		while (la.kind == 69 || la.kind == 70) {

+		while (la.kind == 70 || la.kind == 71) {

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1778,7 +1812,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void ImpliesExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		LogicalExpression(out e0);

-		if (la.kind == 71 || la.kind == 72) {

+		if (la.kind == 72 || la.kind == 73) {

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

@@ -1787,23 +1821,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void EquivOp() {

-		if (la.kind == 69) {

+		if (la.kind == 70) {

 			Get();

-		} else if (la.kind == 70) {

+		} else if (la.kind == 71) {

 			Get();

-		} else SynErr(163);

+		} else SynErr(164);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

 		if (StartOf(16)) {

-			if (la.kind == 73 || la.kind == 74) {

+			if (la.kind == 74 || la.kind == 75) {

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 

-				while (la.kind == 73 || la.kind == 74) {

+				while (la.kind == 74 || la.kind == 75) {

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1814,7 +1848,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				x = t; 

 				RelationalExpression(out e1);

 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 

-				while (la.kind == 75 || la.kind == 76) {

+				while (la.kind == 76 || la.kind == 77) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

@@ -1825,11 +1859,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void ImpliesOp() {

-		if (la.kind == 71) {

+		if (la.kind == 72) {

 			Get();

-		} else if (la.kind == 72) {

+		} else if (la.kind == 73) {

 			Get();

-		} else SynErr(164);

+		} else SynErr(165);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e) {

@@ -1923,19 +1957,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 73) {

+		if (la.kind == 74) {

 			Get();

-		} else if (la.kind == 74) {

+		} else if (la.kind == 75) {

 			Get();

-		} else SynErr(165);

+		} else SynErr(166);

 	}

 

 	void OrOp() {

-		if (la.kind == 75) {

+		if (la.kind == 76) {

 			Get();

-		} else if (la.kind == 76) {

+		} else if (la.kind == 77) {

 			Get();

-		} else SynErr(166);

+		} else SynErr(167);

 	}

 

 	void Term(out Expression/*!*/ e0) {

@@ -1954,17 +1988,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken y;

 		

 		switch (la.kind) {

-		case 77: {

+		case 24: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Eq; 

 			break;

 		}

-		case 23: {

+		case 26: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Lt; 

 			break;

 		}

-		case 24: {

+		case 27: {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

@@ -2027,14 +2061,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(167); break;

+		default: SynErr(168); break;

 		}

 	}

 

 	void Factor(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

-		while (la.kind == 47 || la.kind == 89 || la.kind == 90) {

+		while (la.kind == 48 || la.kind == 89 || la.kind == 90) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

 			e0 = new BinaryExpr(x, op, e0, e1); 

@@ -2049,7 +2083,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 88) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(168);

+		} else SynErr(169);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

@@ -2069,43 +2103,43 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 20: case 39: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {

+		case 20: case 40: case 55: case 60: case 66: case 67: case 101: case 102: case 103: case 104: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

-			while (la.kind == 14 || la.kind == 56) {

+			while (la.kind == 14 || la.kind == 57) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 56: {

+		case 6: case 57: {

 			DisplayExpr(out e);

 			break;

 		}

-		case 40: {

+		case 41: {

 			MultiSetExpr(out e);

 			break;

 		}

-		case 42: {

+		case 43: {

 			MapExpr(out e);

 			break;

 		}

-		case 2: case 19: case 34: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

+		case 2: case 19: case 23: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {

 			ConstAtomExpression(out e);

-			while (la.kind == 14 || la.kind == 56) {

+			while (la.kind == 14 || la.kind == 57) {

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(169); break;

+		default: SynErr(170); break;

 		}

 	}

 

 	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 

-		if (la.kind == 47) {

+		if (la.kind == 48) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mul; 

 		} else if (la.kind == 89) {

@@ -2114,7 +2148,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 90) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(170);

+		} else SynErr(171);

 	}

 

 	void NegOp() {

@@ -2122,7 +2156,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 91) {

 			Get();

-		} else SynErr(171);

+		} else SynErr(172);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -2133,18 +2167,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 59: {

+		case 60: {

 			Get();

 			x = t; 

 			Expression(out e);

 			Expect(99);

 			Expression(out e0);

-			Expect(60);

+			Expect(61);

 			Expression(out e1);

 			e = new ITEExpr(x, e, e0, e1); 

 			break;

 		}

-		case 65: {

+		case 66: {

 			MatchExpression(out e);

 			break;

 		}

@@ -2152,11 +2186,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			QuantifierGuts(out e);

 			break;

 		}

-		case 39: {

+		case 40: {

 			ComprehensionExpr(out e);

 			break;

 		}

-		case 66: {

+		case 67: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2165,7 +2199,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 

 			break;

 		}

-		case 54: {

+		case 55: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2186,7 +2220,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				IdentTypeOptional(out d);

 				letVars.Add(d); 

 			}

-			Expect(52);

+			Expect(53);

 			Expression(out e);

 			letRHSs.Add(e); 

 			while (la.kind == 21) {

@@ -2199,7 +2233,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(172); break;

+		default: SynErr(173); break;

 		}

 	}

 

@@ -2215,13 +2249,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Ident(out id);

 			idents.Add(id); 

 		}

-		if (la.kind == 34) {

+		if (la.kind == 23) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

 			if (StartOf(8)) {

 				Expressions(args);

 			}

-			Expect(35);

+			Expect(25);

 		}

 		e = new IdentifierSequence(idents, openParen, args); 

 	}

@@ -2235,17 +2269,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 14) {

 			Get();

 			Ident(out id);

-			if (la.kind == 34) {

+			if (la.kind == 23) {

 				Get();

 				IToken openParen = t;  args = new List<Expression/*!*/>();  func = true; 

 				if (StartOf(8)) {

 					Expressions(args);

 				}

-				Expect(35);

+				Expect(25);

 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

 			if (!func) { e = new ExprDotName(id, e, id.val); } 

-		} else if (la.kind == 56) {

+		} else if (la.kind == 57) {

 			Get();

 			x = t; 

 			if (StartOf(8)) {

@@ -2258,11 +2292,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						Expression(out ee);

 						e1 = ee; 

 					}

-				} else if (la.kind == 52) {

+				} else if (la.kind == 53) {

 					Get();

 					Expression(out ee);

 					e1 = ee; 

-				} else if (la.kind == 21 || la.kind == 57) {

+				} else if (la.kind == 21 || la.kind == 58) {

 					while (la.kind == 21) {

 						Get();

 						Expression(out ee);

@@ -2273,7 +2307,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(173);

+				} else SynErr(174);

 			} else if (la.kind == 100) {

 				Get();

 				anyDots = true; 

@@ -2281,7 +2315,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(174);

+			} else SynErr(175);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -2304,8 +2338,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-			Expect(57);

-		} else SynErr(175);

+			Expect(58);

+		} else SynErr(176);

 	}

 

 	void DisplayExpr(out Expression e) {

@@ -2321,15 +2355,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 56) {

+		} else if (la.kind == 57) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(57);

-		} else SynErr(176);

+			Expect(58);

+		} else SynErr(177);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2337,7 +2371,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(40);

+		Expect(41);

 		x = t; 

 		if (la.kind == 6) {

 			Get();

@@ -2347,15 +2381,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new MultiSetDisplayExpr(x, elements);

 			Expect(7);

-		} else if (la.kind == 34) {

+		} else if (la.kind == 23) {

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

-			Expect(35);

+			Expect(25);

 		} else if (StartOf(18)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(177);

+		} else SynErr(178);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2364,16 +2398,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<ExpressionPair/*!*/>/*!*/ elements;

 		e = dummyExpr;

 		

-		Expect(42);

+		Expect(43);

 		x = t; 

-		if (la.kind == 56) {

+		if (la.kind == 57) {

 			Get();

 			elements = new List<ExpressionPair/*!*/>(); 

 			if (StartOf(8)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(57);

+			Expect(58);

 		} else if (la.kind == 1) {

 			BoundVar/*!*/ bv;

 			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();

@@ -2389,7 +2423,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new MapComprehension(x, bvars, range, body); 

 		} else if (StartOf(18)) {

 			SemErr("map must be followed by literal in brackets or comprehension."); 

-		} else SynErr(178);

+		} else SynErr(179);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -2426,27 +2460,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		case 96: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(23);

 			Expression(out e);

-			Expect(35);

+			Expect(25);

 			e = new FreshExpr(x, e); 

 			break;

 		}

 		case 97: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(23);

 			Expression(out e);

-			Expect(35);

+			Expect(25);

 			e = new AllocatedExpr(x, e); 

 			break;

 		}

 		case 98: {

 			Get();

 			x = t; 

-			Expect(34);

+			Expect(23);

 			Expression(out e);

-			Expect(35);

+			Expect(25);

 			e = new OldExpr(x, e); 

 			break;

 		}

@@ -2458,15 +2492,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(19);

 			break;

 		}

-		case 34: {

+		case 23: {

 			Get();

 			x = t; 

 			Expression(out e);

 			e = new ParensExpression(x, e); 

-			Expect(35);

+			Expect(25);

 			break;

 		}

-		default: SynErr(179); break;

+		default: SynErr(180); break;

 		}

 	}

 

@@ -2485,13 +2519,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;

 		elements = new List<ExpressionPair/*!*/>(); 

 		Expression(out d);

-		Expect(52);

+		Expect(53);

 		Expression(out r);

 		elements.Add(new ExpressionPair(d,r)); 

 		while (la.kind == 21) {

 			Get();

 			Expression(out d);

-			Expect(52);

+			Expect(53);

 			Expression(out r);

 			elements.Add(new ExpressionPair(d,r)); 

 		}

@@ -2502,17 +2536,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 106) {

 			Get();

-		} else SynErr(180);

+		} else SynErr(181);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  MatchCaseExpr/*!*/ c;

 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();

 		

-		Expect(65);

+		Expect(66);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 61) {

+		while (la.kind == 62) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2533,7 +2567,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 103 || la.kind == 104) {

 			Exists();

 			x = t; 

-		} else SynErr(181);

+		} else SynErr(182);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

@@ -2553,7 +2587,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ range;

 		Expression body = null;

 		

-		Expect(39);

+		Expect(40);

 		x = t; 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv); 

@@ -2579,10 +2613,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(61);

+		Expect(62);

 		x = t; 

 		Ident(out id);

-		if (la.kind == 34) {

+		if (la.kind == 23) {

 			Get();

 			IdentTypeOptional(out bv);

 			arguments.Add(bv); 

@@ -2591,9 +2625,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				IdentTypeOptional(out bv);

 				arguments.Add(bv); 

 			}

-			Expect(35);

+			Expect(25);

 		}

-		Expect(62);

+		Expect(63);

 		Expression(out body);

 		c = new MatchCaseExpr(x, id.val, arguments, body); 

 	}

@@ -2603,7 +2637,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 102) {

 			Get();

-		} else SynErr(182);

+		} else SynErr(183);

 	}

 

 	void Exists() {

@@ -2611,7 +2645,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 104) {

 			Get();

-		} else SynErr(183);

+		} else SynErr(184);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2647,26 +2681,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	static readonly bool[,]/*!*/ set = {

-		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,x, x,T,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,T,T,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

-		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

-		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

+		{T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,T, x,x,x,x, T,T,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,x,T,x, T,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, T,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},

+		{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

+		{x,x,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},

+		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}

 

 	};

 } // end Parser

@@ -2714,61 +2748,61 @@ public class Errors {
 			case 20: s = "\"var\" expected"; break;

 			case 21: s = "\",\" expected"; break;

 			case 22: s = "\"type\" expected"; break;

-			case 23: s = "\"<\" expected"; break;

-			case 24: s = "\">\" expected"; break;

-			case 25: s = "\"method\" expected"; break;

-			case 26: s = "\"constructor\" expected"; break;

-			case 27: s = "\"returns\" expected"; break;

-			case 28: s = "\"...\" expected"; break;

-			case 29: s = "\"modifies\" expected"; break;

-			case 30: s = "\"free\" expected"; break;

-			case 31: s = "\"requires\" expected"; break;

-			case 32: s = "\"ensures\" expected"; break;

-			case 33: s = "\"decreases\" expected"; break;

-			case 34: s = "\"(\" expected"; break;

-			case 35: s = "\")\" expected"; break;

-			case 36: s = "\"bool\" expected"; break;

-			case 37: s = "\"nat\" expected"; break;

-			case 38: s = "\"int\" expected"; break;

-			case 39: s = "\"set\" expected"; break;

-			case 40: s = "\"multiset\" expected"; break;

-			case 41: s = "\"seq\" expected"; break;

-			case 42: s = "\"map\" expected"; break;

-			case 43: s = "\"object\" expected"; break;

-			case 44: s = "\"function\" expected"; break;

-			case 45: s = "\"predicate\" expected"; break;

-			case 46: s = "\"reads\" expected"; break;

-			case 47: s = "\"*\" expected"; break;

-			case 48: s = "\"`\" expected"; break;

-			case 49: s = "\"label\" expected"; break;

-			case 50: s = "\"break\" expected"; break;

-			case 51: s = "\"return\" expected"; break;

-			case 52: s = "\":=\" expected"; break;

-			case 53: s = "\":|\" expected"; break;

-			case 54: s = "\"assume\" expected"; break;

-			case 55: s = "\"new\" expected"; break;

-			case 56: s = "\"[\" expected"; break;

-			case 57: s = "\"]\" expected"; break;

-			case 58: s = "\"choose\" expected"; break;

-			case 59: s = "\"if\" expected"; break;

-			case 60: s = "\"else\" expected"; break;

-			case 61: s = "\"case\" expected"; break;

-			case 62: s = "\"=>\" expected"; break;

-			case 63: s = "\"while\" expected"; break;

-			case 64: s = "\"invariant\" expected"; break;

-			case 65: s = "\"match\" expected"; break;

-			case 66: s = "\"assert\" expected"; break;

-			case 67: s = "\"print\" expected"; break;

-			case 68: s = "\"parallel\" expected"; break;

-			case 69: s = "\"<==>\" expected"; break;

-			case 70: s = "\"\\u21d4\" expected"; break;

-			case 71: s = "\"==>\" expected"; break;

-			case 72: s = "\"\\u21d2\" expected"; break;

-			case 73: s = "\"&&\" expected"; break;

-			case 74: s = "\"\\u2227\" expected"; break;

-			case 75: s = "\"||\" expected"; break;

-			case 76: s = "\"\\u2228\" expected"; break;

-			case 77: s = "\"==\" expected"; break;

+			case 23: s = "\"(\" expected"; break;

+			case 24: s = "\"==\" expected"; break;

+			case 25: s = "\")\" expected"; break;

+			case 26: s = "\"<\" expected"; break;

+			case 27: s = "\">\" expected"; break;

+			case 28: s = "\"method\" expected"; break;

+			case 29: s = "\"constructor\" expected"; break;

+			case 30: s = "\"returns\" expected"; break;

+			case 31: s = "\"...\" expected"; break;

+			case 32: s = "\"modifies\" expected"; break;

+			case 33: s = "\"free\" expected"; break;

+			case 34: s = "\"requires\" expected"; break;

+			case 35: s = "\"ensures\" expected"; break;

+			case 36: s = "\"decreases\" expected"; break;

+			case 37: s = "\"bool\" expected"; break;

+			case 38: s = "\"nat\" expected"; break;

+			case 39: s = "\"int\" expected"; break;

+			case 40: s = "\"set\" expected"; break;

+			case 41: s = "\"multiset\" expected"; break;

+			case 42: s = "\"seq\" expected"; break;

+			case 43: s = "\"map\" expected"; break;

+			case 44: s = "\"object\" expected"; break;

+			case 45: s = "\"function\" expected"; break;

+			case 46: s = "\"predicate\" expected"; break;

+			case 47: s = "\"reads\" expected"; break;

+			case 48: s = "\"*\" expected"; break;

+			case 49: s = "\"`\" expected"; break;

+			case 50: s = "\"label\" expected"; break;

+			case 51: s = "\"break\" expected"; break;

+			case 52: s = "\"return\" expected"; break;

+			case 53: s = "\":=\" expected"; break;

+			case 54: s = "\":|\" expected"; break;

+			case 55: s = "\"assume\" expected"; break;

+			case 56: s = "\"new\" expected"; break;

+			case 57: s = "\"[\" expected"; break;

+			case 58: s = "\"]\" expected"; break;

+			case 59: s = "\"choose\" expected"; break;

+			case 60: s = "\"if\" expected"; break;

+			case 61: s = "\"else\" expected"; break;

+			case 62: s = "\"case\" expected"; break;

+			case 63: s = "\"=>\" expected"; break;

+			case 64: s = "\"while\" expected"; break;

+			case 65: s = "\"invariant\" expected"; break;

+			case 66: s = "\"match\" expected"; break;

+			case 67: s = "\"assert\" expected"; break;

+			case 68: s = "\"print\" expected"; break;

+			case 69: s = "\"parallel\" expected"; break;

+			case 70: s = "\"<==>\" expected"; break;

+			case 71: s = "\"\\u21d4\" expected"; break;

+			case 72: s = "\"==>\" expected"; break;

+			case 73: s = "\"\\u21d2\" expected"; break;

+			case 74: s = "\"&&\" expected"; break;

+			case 75: s = "\"\\u2227\" expected"; break;

+			case 76: s = "\"||\" expected"; break;

+			case 77: s = "\"\\u2228\" expected"; break;

 			case 78: s = "\"<=\" expected"; break;

 			case 79: s = "\">=\" expected"; break;

 			case 80: s = "\"!=\" expected"; break;

@@ -2838,43 +2872,44 @@ public class Errors {
 			case 144: s = "this symbol not expected in OneStmt"; break;

 			case 145: s = "invalid OneStmt"; break;

 			case 146: s = "invalid AssertStmt"; break;

-			case 147: s = "invalid UpdateStmt"; break;

+			case 147: s = "invalid AssumeStmt"; break;

 			case 148: s = "invalid UpdateStmt"; break;

-			case 149: s = "invalid IfStmt"; break;

+			case 149: s = "invalid UpdateStmt"; break;

 			case 150: s = "invalid IfStmt"; break;

-			case 151: s = "invalid WhileStmt"; break;

+			case 151: s = "invalid IfStmt"; break;

 			case 152: s = "invalid WhileStmt"; break;

-			case 153: s = "invalid Rhs"; break;

-			case 154: s = "invalid Lhs"; break;

-			case 155: s = "invalid Guard"; break;

-			case 156: s = "this symbol not expected in LoopSpec"; break;

+			case 153: s = "invalid WhileStmt"; break;

+			case 154: s = "invalid Rhs"; break;

+			case 155: s = "invalid Lhs"; break;

+			case 156: s = "invalid Guard"; break;

 			case 157: s = "this symbol not expected in LoopSpec"; break;

 			case 158: s = "this symbol not expected in LoopSpec"; break;

 			case 159: s = "this symbol not expected in LoopSpec"; break;

 			case 160: s = "this symbol not expected in LoopSpec"; break;

-			case 161: s = "this symbol not expected in Invariant"; break;

-			case 162: s = "invalid AttributeArg"; break;

-			case 163: s = "invalid EquivOp"; break;

-			case 164: s = "invalid ImpliesOp"; break;

-			case 165: s = "invalid AndOp"; break;

-			case 166: s = "invalid OrOp"; break;

-			case 167: s = "invalid RelOp"; break;

-			case 168: s = "invalid AddOp"; break;

-			case 169: s = "invalid UnaryExpression"; break;

-			case 170: s = "invalid MulOp"; break;

-			case 171: s = "invalid NegOp"; break;

-			case 172: s = "invalid EndlessExpression"; break;

-			case 173: s = "invalid Suffix"; break;

+			case 161: s = "this symbol not expected in LoopSpec"; break;

+			case 162: s = "this symbol not expected in Invariant"; break;

+			case 163: s = "invalid AttributeArg"; break;

+			case 164: s = "invalid EquivOp"; break;

+			case 165: s = "invalid ImpliesOp"; break;

+			case 166: s = "invalid AndOp"; break;

+			case 167: s = "invalid OrOp"; break;

+			case 168: s = "invalid RelOp"; break;

+			case 169: s = "invalid AddOp"; break;

+			case 170: s = "invalid UnaryExpression"; break;

+			case 171: s = "invalid MulOp"; break;

+			case 172: s = "invalid NegOp"; break;

+			case 173: s = "invalid EndlessExpression"; break;

 			case 174: s = "invalid Suffix"; break;

 			case 175: s = "invalid Suffix"; break;

-			case 176: s = "invalid DisplayExpr"; break;

-			case 177: s = "invalid MultiSetExpr"; break;

-			case 178: s = "invalid MapExpr"; break;

-			case 179: s = "invalid ConstAtomExpression"; break;

-			case 180: s = "invalid QSep"; break;

-			case 181: s = "invalid QuantifierGuts"; break;

-			case 182: s = "invalid Forall"; break;

-			case 183: s = "invalid Exists"; break;

+			case 176: s = "invalid Suffix"; break;

+			case 177: s = "invalid DisplayExpr"; break;

+			case 178: s = "invalid MultiSetExpr"; break;

+			case 179: s = "invalid MapExpr"; break;

+			case 180: s = "invalid ConstAtomExpression"; break;

+			case 181: s = "invalid QSep"; break;

+			case 182: s = "invalid QuantifierGuts"; break;

+			case 183: s = "invalid Forall"; break;

+			case 184: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 36b5f791..4b0b6ec1 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -45,6 +45,9 @@ namespace Microsoft.Dafny {
           if (i++ != 0) { wr.WriteLine(); }

           Indent(indent);

           PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());

+          if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {

+            wr.Write("(==)");

+          }

           wr.WriteLine(";");

         } else if (d is DatatypeDecl) {

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

@@ -146,7 +149,10 @@ namespace Microsoft.Dafny {
 

       wr.Write(" {0}", name);

       if (typeArgs.Count != 0) {

-        wr.Write("<" + Util.Comma(", ", typeArgs, tp => tp.Name) + ">");

+        wr.Write("<" +

+                 Util.Comma(", ", typeArgs,

+                   tp => tp.Name + (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Required? "(==)": ""))

+                 + ">");

       }

     }

 

@@ -422,24 +428,14 @@ namespace Microsoft.Dafny {
         }

       }

 

-      if (stmt is AssertStmt) {

-        Expression expr = ((AssertStmt)stmt).Expr;

-

-        wr.Write("assert");

-

-        if (stmt.HasAttributes())

-        {

+      if (stmt is PredicateStmt) {

+        Expression expr = ((PredicateStmt)stmt).Expr;

+        wr.Write(stmt is AssertStmt ? "assert" : "assume");

+        if (stmt.HasAttributes()) {

           PrintAttributes(stmt.Attributes);

         }

-

         wr.Write(" ");

         PrintExpression(expr);

-

-        wr.Write(";");

-

-      } else if (stmt is AssumeStmt) {

-        wr.Write("assume ");

-        PrintExpression(((AssumeStmt)stmt).Expr);

         wr.Write(";");

 

       } else if (stmt is PrintStmt) {

@@ -624,6 +620,9 @@ namespace Microsoft.Dafny {
         } else if (s.S is AssertStmt) {

           Contract.Assert(s.ConditionOmitted);

           wr.Write("assert ...;");

+        } else if (s.S is AssumeStmt) {

+          Contract.Assert(s.ConditionOmitted);

+          wr.Write("assume ...;");

         } else if (s.S is IfStmt) {

           PrintIfStatement(indent, (IfStmt)s.S, s.ConditionOmitted);

         } else if (s.S is WhileStmt) {

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index 04550c3e..0d32e24e 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -50,7 +50,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class RefinementTransformer

+  public class RefinementTransformer : IRewriter

   {

     ResolutionErrorReporter reporter;

     public RefinementTransformer(ResolutionErrorReporter reporter) {

@@ -59,15 +59,19 @@ namespace Microsoft.Dafny {
     }

 

     private ModuleDefinition moduleUnderConstruction;  // non-null for the duration of Construct calls

+    private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

 

-    public void Construct(ModuleDefinition m) {

+    public void PreResolve(ModuleDefinition m) {

       Contract.Requires(m != null);

       Contract.Requires(m.RefinementBase != null);

 

-      Contract.Assert(moduleUnderConstruction == null);

-      moduleUnderConstruction = m;

-      var prev = m.RefinementBase;

+      if (moduleUnderConstruction != null) {

+        postTasks.Clear();

+      }

       

+      moduleUnderConstruction = m;

+      var prev = m.RefinementBase;     

+

       // Create a simple name-to-decl dictionary.  Ignore any duplicates at this time.

       var declaredNames = new Dictionary<string, int>();

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

@@ -112,11 +116,39 @@ namespace Microsoft.Dafny {
               }

             }

           } else if (d is ArbitraryTypeDecl) {

-            // this is allowed to be refined by any type declaration, so just keep the new one

-            // of course, the new thing has to be a type. Everything is a type except for a module

-            // declaration

             if (nw is ModuleDecl) {

               reporter.Error(nw, "a module ({0}) must refine another module", nw.Name);

+            } else {

+              bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;

+              if (nw is ArbitraryTypeDecl) {

+                if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {

+                  reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);

+                }

+              } else if (dDemandsEqualitySupport) {

+                if (nw is ClassDecl) {

+                  // fine, as long as "nw" does not take any type parameters

+                  if (nw.TypeArgs.Count != 0) {

+                    reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);

+                  }

+                } else if (nw is CoDatatypeDecl) {

+                  reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

+                } else {

+                  Contract.Assert(nw is IndDatatypeDecl);

+                  if (nw.TypeArgs.Count != 0) {

+                    reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);

+                  } else {

+                    // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

+                    // taken place, so we defer it until the PostResolve phase.

+                    var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());

+                    postTasks.Enqueue(delegate()

+                    {

+                      if (!udt.SupportsEquality) {

+                        reporter.Error(udt.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", udt.Name);

+                      }

+                    });

+                  }

+                }

+              }

             }

           } else if (nw is ArbitraryTypeDecl) {

             reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);

@@ -133,7 +165,18 @@ namespace Microsoft.Dafny {
         }

       }

 

-      Contract.Assert(moduleUnderConstruction == m);

+      Contract.Assert(moduleUnderConstruction == m);  // this should be as it was set earlier in this method

+    }

+

+    public void PostResolve(ModuleDefinition m) {

+      if (m == moduleUnderConstruction) {

+        while (this.postTasks.Count != 0) {

+          var a = postTasks.Dequeue();

+          a();

+        }

+      } else {

+        postTasks.Clear();

+      }

       moduleUnderConstruction = null;

     }

 

@@ -154,7 +197,7 @@ namespace Microsoft.Dafny {
 

       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

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

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

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

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

@@ -203,7 +246,7 @@ namespace Microsoft.Dafny {
     }

 

     TypeParameter CloneTypeParam(TypeParameter tp) {

-      return new TypeParameter(Tok(tp.tok), tp.Name);

+      return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);

     }

 

     MemberDecl CloneMember(MemberDecl member) {

@@ -467,11 +510,11 @@ namespace Microsoft.Dafny {
       Statement r;

       if (stmt is AssertStmt) {

         var s = (AssertStmt)stmt;

-        r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr));

+        r = new AssertStmt(Tok(s.Tok), CloneExpr(s.Expr), null);

 

       } else if (stmt is AssumeStmt) {

         var s = (AssumeStmt)stmt;

-        r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr));

+        r = new AssumeStmt(Tok(s.Tok), CloneExpr(s.Expr), null);

 

       } else if (stmt is PrintStmt) {

         var s = (PrintStmt)stmt;

@@ -636,6 +679,8 @@ namespace Microsoft.Dafny {
     // -------------------------------------------------- Merging ---------------------------------------------------------------

 

     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {

+      CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "class");

+

       // Create a simple name-to-member dictionary.  Ignore any duplicates at this time.

       var declaredNames = new Dictionary<string, int>();

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

@@ -769,6 +814,27 @@ namespace Microsoft.Dafny {
           var n = nw[i];

           if (o.Name != n.Name) {

             reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being refined (expected '{1}', found '{2}')", thing, o.Name, n.Name);

+          } else {

+            // This explains what we want to do and why:

+            // switch (o.EqualitySupport) {

+            //   case TypeParameter.EqualitySupportValue.Required:

+            //     // here, we will insist that the new type-parameter also explicitly requires equality support (because we don't want

+            //     // to wait for the inference to run on the new module)

+            //     good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Required;

+            //     break;

+            //   case TypeParameter.EqualitySupportValue.InferredRequired:

+            //     // here, we can allow anything, because even with an Unspecified value, the inference will come up with InferredRequired, like before

+            //     good = true;

+            //     break;

+            //   case TypeParameter.EqualitySupportValue.Unspecified:

+            //     // inference didn't come up with anything on the previous module, so the only value we'll allow here is Unspecified as well

+            //     good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified;

+            //     break;

+            // }

+            // Here's how we actually compute it:

+            if (o.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.EqualitySupport != n.EqualitySupport) {

+              reporter.Error(n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name);

+            }

           }

         }

       }

@@ -832,6 +898,8 @@ namespace Microsoft.Dafny {
            *   assert ...;                 assert E;                    assert E;

            *   assert E;                                                assert E;

            *   

+           *   assume ...;                 assume E;                    assume E;

+           *   

            *   var x := E;                 var x;                       var x := E;

            *   var x := E;                 var x := *;                  var x := E;

            *   var x := E1;                var x :| E0;                 var x := E1; assert E0;

@@ -893,6 +961,19 @@ namespace Microsoft.Dafny {
                 i++; j++;

               }

 

+            } else if (S is AssumeStmt) {

+              var skel = (AssumeStmt)S;

+              Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);

+              var oldAssume = oldS as AssumeStmt;

+              if (oldAssume == null) {

+                reporter.Error(cur.Tok, "assume template does not match inherited statement");

+                i++;

+              } else {

+                var e = CloneExpr(oldAssume.Expr);

+                body.Add(new AssumeStmt(skel.Tok, e, null));

+                i++; j++;

+              }

+

             } else if (S is IfStmt) {

               var skel = (IfStmt)S;

               Contract.Assert(((SkeletonStatement)cur).ConditionOmitted);

@@ -903,7 +984,7 @@ namespace Microsoft.Dafny {
               } else {

                 var resultingThen = MergeBlockStmt(skel.Thn, oldIf.Thn);

                 var resultingElse = MergeElse(skel.Els, oldIf.Els);

-                var r = new IfStmt(skel.Tok, skel.Guard, resultingThen, resultingElse);

+                var r = new IfStmt(skel.Tok, CloneExpr(oldIf.Guard), resultingThen, resultingElse);

                 body.Add(r);

                 i++; j++;

               }

@@ -966,7 +1047,7 @@ namespace Microsoft.Dafny {
               body.Add(cNew);

               i++; j++;

               if (addedAssert != null) {

-                body.Add(new AssertStmt(addedAssert.tok, addedAssert));

+                body.Add(new AssertStmt(addedAssert.tok, addedAssert, null));

               }

             } else {

               MergeAddStatement(cur, body);

@@ -1044,6 +1125,8 @@ namespace Microsoft.Dafny {
         var S = ((SkeletonStatement)nxt).S;

         if (S is AssertStmt) {

           return other is PredicateStmt;

+        } else if (S is AssumeStmt) {

+          return other is AssumeStmt;

         } else if (S is IfStmt) {

           return other is IfStmt;

         } else if (S is WhileStmt) {

@@ -1070,22 +1153,35 @@ namespace Microsoft.Dafny {
 

       // Note, the parser produces errors if there are any decreases or modifies clauses (and it creates

       // the Specification structures with a null list).

-      Contract.Assume(cNew.Decreases.Expressions == null);

       Contract.Assume(cNew.Mod.Expressions == null);

 

+      // If the previous loop was not specified with "decreases *", then the new loop is not allowed to provide any "decreases" clause.

+      // Any "decreases *" clause is not inherited, so if the previous loop was specified with "decreases *", then the new loop needs

+      // to either redeclare "decreases *", provided a termination-checking "decreases" clause, or give no "decreases" clause and thus

+      // get a default "decreases" loop.

+      Specification<Expression> decr;

+      if (Contract.Exists(cOld.Decreases.Expressions, e => e is WildcardExpr)) {

+        decr = cNew.Decreases;  // take the new decreases clauses, whatever they may be (including nothing at all)

+      } else {

+        if (cNew.Decreases.Expressions.Count != 0) {

+          reporter.Error(cNew.Decreases.Expressions[0].tok, "a refining loop can provide a decreases clause only if the loop being refined was declared with 'decreases *'");

+        }

+        decr = CloneSpecExpr(cOld.Decreases);

+      }

+

       var invs = cOld.Invariants.ConvertAll(CloneMayBeFreeExpr);

       invs.AddRange(cNew.Invariants);

-      var r = new WhileStmt(cNew.Tok, guard, invs, CloneSpecExpr(cOld.Decreases), CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body));

+      var r = new RefinedWhileStmt(cNew.Tok, guard, invs, decr, CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body));

       return r;

     }

 

     Statement MergeElse(Statement skeleton, Statement oldStmt) {

-      Contract.Requires(skeleton == null || skeleton is BlockStmt || skeleton is IfStmt);

-      Contract.Requires(oldStmt == null || oldStmt is BlockStmt || oldStmt is IfStmt);

+      Contract.Requires(skeleton == null || skeleton is BlockStmt || skeleton is IfStmt || skeleton is SkeletonStatement);

+      Contract.Requires(oldStmt == null || oldStmt is BlockStmt || oldStmt is IfStmt || oldStmt is SkeletonStatement);

 

       if (skeleton == null) {

         return CloneStmt(oldStmt);

-      } else if (skeleton is IfStmt) {

+      } else if (skeleton is IfStmt || skeleton is SkeletonStatement) {

         // wrap a block statement around the if statement

         skeleton = new BlockStmt(skeleton.Tok, new List<Statement>() { skeleton });

       }

@@ -1093,7 +1189,7 @@ namespace Microsoft.Dafny {
       if (oldStmt == null) {

         // make it into an empty block statement

         oldStmt = new BlockStmt(skeleton.Tok, new List<Statement>());

-      } else if (oldStmt is IfStmt) {

+      } else if (oldStmt is IfStmt || oldStmt is SkeletonStatement) {

         // wrap a block statement around the if statement

         oldStmt = new BlockStmt(oldStmt.Tok, new List<Statement>() { oldStmt });

       }

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index f6c77934..098bcc2e 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -138,7 +138,8 @@ namespace Microsoft.Dafny {
         }

         h++;

       }

-      // register top-level declarations

+

+      var refinementTransformer = new RefinementTransformer(this);

       

       //Rewriter rewriter = new AutoContractsRewriter();

       var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);

@@ -160,8 +161,7 @@ namespace Microsoft.Dafny {
             if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out refinedSig)) {

               if (refinedSig.ModuleDef != null) {

                 m.RefinementBase = refinedSig.ModuleDef;

-                var transformer = new RefinementTransformer(this);

-                transformer.Construct(m);

+                refinementTransformer.PreResolve(m);

               } else {

                 Error(m.RefinementBaseName[0], "module ({0}) named as refinement base is not a literal module or simple reference to a literal module", Util.Comma(".", m.RefinementBaseName, x => x.val));

               }

@@ -175,8 +175,12 @@ namespace Microsoft.Dafny {
           moduleInfo = MergeSignature(literalDecl.Signature, systemNameInfo);

           // resolve

           var datatypeDependencies = new Graph<IndDatatypeDecl>();

+          int prevErrorCount = ErrorCount;

           ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

+          if (ErrorCount == prevErrorCount)

           ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+

+          refinementTransformer.PostResolve(m);

           // give rewriter a chance to do processing

           //rewriter.PostResolve(m);

         } else if (decl is AliasModuleDecl) {

@@ -472,7 +476,7 @@ namespace Microsoft.Dafny {
 

       if (d is ArbitraryTypeDecl) {

         var dd = (ArbitraryTypeDecl)d;

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

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

       } else if (d is IndDatatypeDecl) {

         var dd = (IndDatatypeDecl)d;

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

@@ -817,15 +821,16 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

 

-      // Perform the stratosphere check on inductive datatypes

+      // Perform the stratosphere check on inductive datatypes, and compute to what extent the inductive datatypes require equality support

       foreach (var dtd in datatypeDependencies.TopologicallySortedComponents()) {

         if (datatypeDependencies.GetSCCRepresentative(dtd) == dtd) {

           // do the following check once per SCC, so call it on each SCC representative

           SccStratosphereCheck(dtd, datatypeDependencies);

+          DetermineEqualitySupport(dtd, datatypeDependencies);

         }

       }

-      // Perform the guardedness check on co-datatypes

       if (ErrorCount == prevErrorCount) {  // because CheckCoCalls requires the given expression to have been successfully resolved

+        // Perform the guardedness check on co-datatypes

         foreach (var decl in declarations) {

           var cl = decl as ClassDecl;

           if (cl != null) {

@@ -849,9 +854,398 @@ namespace Microsoft.Dafny {
             }

           }

         }

+        // Inferred required equality support for datatypes and for Function and Method signatures

+        // First, do datatypes until a fixpoint is reached

+        bool inferredSomething;

+        do {

+          inferredSomething = false;

+          foreach (var d in declarations) {

+            if (d is DatatypeDecl) {

+              var dt = (DatatypeDecl)d;

+              foreach (var tp in dt.TypeArgs) {

+                if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                  // here's our chance to infer the need for equality support

+                  foreach (var ctor in dt.Ctors) {

+                    foreach (var arg in ctor.Formals) {

+                      if (InferRequiredEqualitySupport(tp, arg.Type)) {

+                        tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                        inferredSomething = true;

+                        goto DONE_DT;  // break out of the doubly-nested loop

+                      }

+                    }

+                  }

+                DONE_DT: ;

+                }

+              }

+            }

+          }

+        } while (inferredSomething);

+        // Now do it for Function and Method signatures

+        foreach (var d in declarations) {

+          if (d is ClassDecl) {

+            var cl = (ClassDecl)d;

+            foreach (var member in cl.Members) {

+              if (!member.IsGhost) {

+                if (member is Function) {

+                  var f = (Function)member;

+                  foreach (var tp in f.TypeArgs) {

+                    if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                      // here's our chance to infer the need for equality support

+                      if (InferRequiredEqualitySupport(tp, f.ResultType)) {

+                        tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                      } else {

+                        foreach (var p in f.Formals) {

+                          if (InferRequiredEqualitySupport(tp, p.Type)) {

+                            tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                            break;

+                          }

+                        }

+                      }

+                    }

+                  }

+                } else if (member is Method) {

+                  var m = (Method)member;

+                  foreach (var tp in m.TypeArgs) {

+                    if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {

+                      // here's our chance to infer the need for equality support

+                      foreach (var p in m.Ins) {

+                        if (InferRequiredEqualitySupport(tp, p.Type)) {

+                          tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                          goto DONE;

+                        }

+                      }

+                      foreach (var p in m.Outs) {

+                        if (InferRequiredEqualitySupport(tp, p.Type)) {

+                          tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;

+                          goto DONE;

+                        }

+                      }

+                    DONE: ;

+                    }

+                  }

+                }

+              }

+            }

+          }

+        }

+        // Check that all == and != operators in non-ghost contexts are applied to equality-supporting types.

+        // Note that this check can only be done after determining which expressions are ghosts.

+        foreach (var d in declarations) {

+          if (d is ClassDecl) {

+            var cl = (ClassDecl)d;

+            foreach (var member in cl.Members) {

+              if (!member.IsGhost) {

+                if (member is Field) {

+                  var f = (Field)member;

+                  CheckEqualityTypes_Type(f.tok, f.Type);

+                } else if (member is Function) {

+                  var f = (Function)member;

+                  foreach (var p in f.Formals) {

+                    if (!p.IsGhost) {

+                      CheckEqualityTypes_Type(p.tok, p.Type);

+                    }

+                  }

+                  CheckEqualityTypes_Type(f.tok, f.ResultType);

+                  if (f.Body != null) {

+                    CheckEqualityTypes(f.Body);

+                  }

+                } else if (member is Method) {

+                  var m = (Method)member;

+                  foreach (var p in m.Ins) {

+                    if (!p.IsGhost) {

+                      CheckEqualityTypes_Type(p.tok, p.Type);

+                    }

+                  }

+                  foreach (var p in m.Outs) {

+                    if (!p.IsGhost) {

+                      CheckEqualityTypes_Type(p.tok, p.Type);

+                    }

+                  }

+                  if (m.Body != null) {

+                    CheckEqualityTypes_Stmt(m.Body);

+                  }

+                }

+              }

+            }

+          } else if (d is DatatypeDecl) {

+            var dt = (DatatypeDecl)d;

+            foreach (var ctor in dt.Ctors) {

+              foreach (var p in ctor.Formals) {

+                if (!p.IsGhost) {

+                  CheckEqualityTypes_Type(p.tok, p.Type);

+                }

+              }

+            }

+          }

+        }

+      }

+    }

+

+    void CheckEqualityTypes_Stmt(Statement stmt) {

+      Contract.Requires(stmt != null);

+      if (stmt.IsGhost) {

+        return;

+      } else if (stmt is PrintStmt) {

+        var s = (PrintStmt)stmt;

+        foreach (var arg in s.Args) {

+          if (arg.E != null) {

+            CheckEqualityTypes(arg.E);

+          }

+        }

+      } else if (stmt is BreakStmt) {

+      } else if (stmt is ReturnStmt) {

+        var s = (ReturnStmt)stmt;

+        if (s.rhss != null) {

+          s.rhss.Iter(CheckEqualityTypes_Rhs);

+        }

+      } else if (stmt is AssignStmt) {

+        AssignStmt s = (AssignStmt)stmt;

+        CheckEqualityTypes(s.Lhs);

+        CheckEqualityTypes_Rhs(s.Rhs);

+      } else if (stmt is VarDecl) {

+        var s = (VarDecl)stmt;

+        s.SubStatements.Iter(CheckEqualityTypes_Stmt);

+      } else if (stmt is CallStmt) {

+        var s = (CallStmt)stmt;

+        CheckEqualityTypes(s.Receiver);

+        s.Args.Iter(CheckEqualityTypes);

+        s.Lhs.Iter(CheckEqualityTypes);

+

+        Contract.Assert(s.Method.TypeArgs.Count <= s.TypeArgumentSubstitutions.Count);

+        var i = 0;

+        foreach (var formalTypeArg in s.Method.TypeArgs) {

+          var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg];

+          if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {

+            Error(s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));

+          }

+          i++;

+        }

+      } else if (stmt is BlockStmt) {

+        var s = (BlockStmt)stmt;

+        s.Body.Iter(CheckEqualityTypes_Stmt);

+      } else if (stmt is IfStmt) {

+        var s = (IfStmt)stmt;

+        if (s.Guard != null) {

+          CheckEqualityTypes(s.Guard);

+        }

+        s.SubStatements.Iter(CheckEqualityTypes_Stmt);

+      } else if (stmt is AlternativeStmt) {

+        var s = (AlternativeStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          CheckEqualityTypes(alt.Guard);

+          alt.Body.Iter(CheckEqualityTypes_Stmt);

+        }

+      } else if (stmt is WhileStmt) {

+        var s = (WhileStmt)stmt;

+        if (s.Guard != null) {

+          CheckEqualityTypes(s.Guard);

+        }

+        CheckEqualityTypes_Stmt(s.Body);

+      } else if (stmt is AlternativeLoopStmt) {

+        var s = (AlternativeLoopStmt)stmt;

+        foreach (var alt in s.Alternatives) {

+          CheckEqualityTypes(alt.Guard);

+          alt.Body.Iter(CheckEqualityTypes_Stmt);

+        }

+      } else if (stmt is ParallelStmt) {

+        var s = (ParallelStmt)stmt;

+        CheckEqualityTypes(s.Range);

+        CheckEqualityTypes_Stmt(s.Body);

+      } else if (stmt is MatchStmt) {

+        var s = (MatchStmt)stmt;

+        CheckEqualityTypes(s.Source);

+        foreach (MatchCaseStmt mc in s.Cases) {

+          mc.Body.Iter(CheckEqualityTypes_Stmt);

+        }

+      } else if (stmt is ConcreteSyntaxStatement) {

+        var s = (ConcreteSyntaxStatement)stmt;

+        s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);

+      } else {

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

       }

     }

 

+    void CheckEqualityTypes_Rhs(AssignmentRhs rhs) {

+      Contract.Requires(rhs != null);

+      rhs.SubExpressions.Iter(CheckEqualityTypes);

+      rhs.SubStatements.Iter(CheckEqualityTypes_Stmt);

+    }

+

+    void CheckEqualityTypes(Expression expr) {

+      Contract.Requires(expr != null);

+      if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

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

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

+        switch (e.Op) {

+          case BinaryExpr.Opcode.Eq:

+          case BinaryExpr.Opcode.Neq:

+            // First, check a special case:  a datatype value (like Nil) that takes no parameters

+            var e0 = e.E0.Resolved as DatatypeValue;

+            var e1 = e.E1.Resolved as DatatypeValue;

+            if (e0 != null && e0.Arguments.Count == 0) {

+              // that's cool

+            } else if (e1 != null && e1.Arguments.Count == 0) {

+              // oh yeah!

+            } else if (!t0.SupportsEquality) {

+              Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

+            } else if (!t1.SupportsEquality) {

+              Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));

+            }

+            break;

+          default:

+            switch (e.ResolvedOp) {

+              // Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how

+              // these types are instantiated.  (Except: This guarantee does not apply to equality on maps, because the Range type

+              // of maps is not restricted, only the Domain type.  However, the equality operator is checked above.)

+              case BinaryExpr.ResolvedOpcode.InSeq:

+              case BinaryExpr.ResolvedOpcode.NotInSeq:

+              case BinaryExpr.ResolvedOpcode.Prefix:

+              case BinaryExpr.ResolvedOpcode.ProperPrefix:

+                if (!t1.SupportsEquality) {

+                  Error(e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));

+                } else if (!t0.SupportsEquality) {

+                  if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) {

+                    Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

+                  } else {

+                    Error(e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));

+                  }

+                }

+                break;

+              default:

+                break;

+            }

+            break;

+        }

+      } else if (expr is ComprehensionExpr) {

+        var e = (ComprehensionExpr)expr;

+        foreach (var bv in e.BoundVars) {

+          CheckEqualityTypes_Type(bv.tok, bv.Type);

+        }

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        foreach (var bv in e.Vars) {

+          CheckEqualityTypes_Type(bv.tok, bv.Type);

+        }

+      } else if (expr is FunctionCallExpr) {

+        var e = (FunctionCallExpr)expr;

+        Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count);

+        var i = 0;

+        foreach (var formalTypeArg in e.Function.TypeArgs) {

+          var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg];

+          if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {

+            Error(e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));

+          }

+          i++;

+        }

+      }

+

+      foreach (var ee in expr.SubExpressions) {

+        CheckEqualityTypes(ee);

+      }

+    }

+

+    void CheckEqualityTypes_Type(IToken tok, Type type) {

+      Contract.Requires(tok != null);

+      Contract.Requires(type != null);

+      type = type.Normalize();

+      if (type is BasicType) {

+        // fine

+      } else if (type is SetType) {

+        var argType = ((SetType)type).Arg;

+        if (!argType.SupportsEquality) {

+          Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));

+        }

+        CheckEqualityTypes_Type(tok, argType);

+

+      } else if (type is MultiSetType) {

+        var argType = ((MultiSetType)type).Arg;

+        if (!argType.SupportsEquality) {

+          Error(tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));

+        }

+        CheckEqualityTypes_Type(tok, argType);

+

+      } else if (type is MapType) {

+        var mt = (MapType)type;

+        if (!mt.Domain.SupportsEquality) {

+          Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain));

+        }

+        CheckEqualityTypes_Type(tok, mt.Domain);

+        CheckEqualityTypes_Type(tok, mt.Range);

+

+      } else if (type is SeqType) {

+        Type argType = ((SeqType)type).Arg;

+        CheckEqualityTypes_Type(tok, argType);

+

+      } else if (type is UserDefinedType) {

+        var udt = (UserDefinedType)type;

+        if (udt.ResolvedClass != null) {

+          Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);

+          var i = 0;

+          foreach (var argType in udt.TypeArgs) {

+            var formalTypeArg = udt.ResolvedClass.TypeArgs[i];

+            if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {

+              Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));

+            }

+            CheckEqualityTypes_Type(tok, argType);

+            i++;

+          }

+        } else {

+          Contract.Assert(udt.TypeArgs.Count == 0);  // TypeParameters have no type arguments

+        }

+

+      } else {

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

+      }

+    }

+

+    string TypeEqualityErrorMessageHint(Type argType) {

+      Contract.Requires(argType != null);

+      var tp = argType.AsTypeParameter;

+      if (tp != null) {

+        return string.Format(" (perhaps try declaring type parameter '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line);

+      }

+      return "";

+    }

+

+    bool InferRequiredEqualitySupport(TypeParameter tp, Type type) {

+      Contract.Requires(tp != null);

+      Contract.Requires(type != null);

+

+      type = type.Normalize();

+      if (type is BasicType) {

+      } else  if (type is SetType) {

+        var st = (SetType)type;

+        return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg);

+      } else if (type is MultiSetType) {

+        var ms = (MultiSetType)type;

+        return ms.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, ms.Arg);

+      } else if (type is MapType) {

+        var mt = (MapType)type;

+        return mt.Domain.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, mt.Domain) || InferRequiredEqualitySupport(tp, mt.Range);

+      } else if (type is SeqType) {

+        var sq = (SeqType)type;

+        return InferRequiredEqualitySupport(tp, sq.Arg);

+      } else if (type is UserDefinedType) {

+        var udt = (UserDefinedType)type;

+        if (udt.ResolvedClass != null) {

+          var i = 0;

+          foreach (var argType in udt.TypeArgs) {

+            var formalTypeArg = udt.ResolvedClass.TypeArgs[i];

+            if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) {

+              return true;

+            }

+            i++;

+          }

+        } else {

+          Contract.Assert(udt.TypeArgs.Count == 0);  // TypeParameters have no type arguments

+        }

+      } else {

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

+      }

+      return false;

+    }

+

     ClassDecl currentClass;

     Function currentFunction;

     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();

@@ -1079,6 +1473,99 @@ namespace Microsoft.Dafny {
       return true;

     }

 

+    void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph<IndDatatypeDecl/*!*/>/*!*/ dependencies) {

+      Contract.Requires(startingPoint != null);

+      Contract.Requires(dependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(dependencies));

+

+      var scc = dependencies.GetSCC(startingPoint);

+      // First, the simple case:  If any parameter of any inductive datatype in the SCC is of a codatatype type, then

+      // the whole SCC is incapable of providing the equality operation.

+      foreach (var dt in scc) {

+        Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);

+        foreach (var ctor in dt.Ctors) {

+          foreach (var arg in ctor.Formals) {

+            var anotherIndDt = arg.Type.AsIndDatatype;

+            if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {

+              // arg.Type is known never to support equality

+              // So, go around the entire SCC and record what we learnt

+              foreach (var ddtt in scc) {

+                ddtt.EqualitySupport = IndDatatypeDecl.ES.Never;

+              }

+              return;  // we are done

+            }

+          }

+        }

+      }

+

+      // Now for the more involved case:  we need to determine which type parameters determine equality support for each datatype in the SCC

+      // We start by seeing where each datatype's type parameters are used in a place known to determine equality support.

+      bool thingsChanged = false;

+      foreach (var dt in scc) {

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

+          // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors

+          continue;

+        }

+        foreach (var ctor in dt.Ctors) {

+          foreach (var arg in ctor.Formals) {

+            var typeArg = arg.Type.AsTypeParameter;

+            if (typeArg != null) {

+              typeArg.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;

+              thingsChanged = true;

+            } 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 i = 0;

+                foreach (var otherTp in otherDt.TypeArgs) {

+                  if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

+                    var tp = otherUdt.TypeArgs[i].AsTypeParameter;

+                    if (tp != null) {

+                      tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;

+                      thingsChanged = true;

+                    }

+                  }

+                }

+              }

+            }

+          }

+        }

+      }

+      // Then we propagate this information up through the SCC

+      while (thingsChanged) {

+        thingsChanged = false;

+        foreach (var dt in scc) {

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

+            // if the datatype has no type parameters, we certainly won't find any type parameters being used in the arguments types to the constructors

+            continue;

+          }

+          foreach (var ctor in dt.Ctors) {

+            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 i = 0;

+                foreach (var otherTp in otherDt.TypeArgs) {

+                  if (otherTp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

+                    var tp = otherUdt.TypeArgs[i].AsTypeParameter;

+                    if (tp != null && !tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype) {

+                      tp.NecessaryForEqualitySupportOfSurroundingInductiveDatatype = true;

+                      thingsChanged = true;

+                    }

+                  }

+                  i++;

+                }

+              }

+            }

+          }

+        }

+      }

+      // Now that we have computed the .NecessaryForEqualitySupportOfSurroundingInductiveDatatype values, mark the datatypes as ones

+      // where equality support should be checked by looking at the type arguments.

+      foreach (var dt in scc) {

+        dt.EqualitySupport = IndDatatypeDecl.ES.ConsultTypeArguments;

+      }

+    }

+

     void ResolveAttributes(Attributes attrs, bool twoState) {

       // order does not matter much for resolution, so resolve them in reverse order

       for (; attrs != null; attrs = attrs.Prev) {

@@ -1549,7 +2036,7 @@ namespace Microsoft.Dafny {
 

       // In the remaining cases, proxy is a restricted proxy and t is a non-proxy

       } else if (proxy is DatatypeProxy) {

-        if (t.IsDatatype) {

+        if (t.IsIndDatatype) {

           // all is fine, proxy can be redirected to t

         } else {

           return false;

@@ -1562,14 +2049,6 @@ namespace Microsoft.Dafny {
           return false;

         }

 

-      } else if (proxy is ObjectsTypeProxy) {

-        if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

-          // all is good

-        } else if (t is CollectionType) {

-          proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());

-          return UnifyTypes(proxy.T, t);

-        }

-

       } else if (proxy is CollectionTypeProxy) {

         CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;

         if (t is CollectionType) {

@@ -1651,10 +2130,6 @@ namespace Microsoft.Dafny {
           // all is fine

           a.T = b;

           return true;

-        } else if (b is ObjectsTypeProxy) {

-          // unify a and b by redirecting b to a, since a gives the stronger requirement

-          b.T = a;

-          return true;

         } else if (b is IndexableTypeProxy) {

           // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type

           a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg);

@@ -1664,37 +2139,6 @@ namespace Microsoft.Dafny {
           return false;

         }

 

-      } else if (a is ObjectsTypeProxy) {

-        if (b is ObjectsTypeProxy) {

-          // fine

-          a.T = b;

-          return true;

-        } else if (b is CollectionTypeProxy) {

-          // fine provided b's collection-element-type can be unified with object or a class type

-          a.T = b;

-          return UnifyTypes(((CollectionTypeProxy)b).Arg, new ObjectTypeProxy());

-        } else if (b is OperationTypeProxy) {

-          // fine; restrict a to sets of object/class, and restrict b to set/seq of object/class

-          if (((OperationTypeProxy)b).AllowSeq) {

-            a.T = new CollectionTypeProxy(new ObjectTypeProxy());

-            b.T = a.T;

-          } else {

-            a.T = new SetType(new ObjectTypeProxy());

-            b.T = a.T;

-          }

-          return true;

-        } else if (b is IndexableTypeProxy) {

-          IndexableTypeProxy pb = (IndexableTypeProxy)b;

-          // the intersection of ObjectsTypeProxy and IndexableTypeProxy is

-          // EITHER a sequence of ObjectTypeProxy OR an array of anything OR map of ObjectTypeProxy in either domain or range.

-          // TODO: here, only the first of the three cases is supported

-          b.T = new SeqType(pb.Arg);

-          a.T = b.T;

-          return UnifyTypes(pb.Arg, new ObjectTypeProxy());

-        } else {

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

-        }

-

       } else if (a is CollectionTypeProxy) {

         if (b is CollectionTypeProxy) {

           a.T = b;

@@ -2538,22 +2982,22 @@ namespace Microsoft.Dafny {
         UserDefinedType ctype = (UserDefinedType)nptype;  // TODO: get rid of this statement, make this code handle any non-proxy type

 #endif

         // build the type substitution map

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

+        s.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

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

-          subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

+          s.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

         }

         foreach (TypeParameter p in callee.TypeArgs) {

-          subst.Add(p, new ParamTypeProxy(p));

+          s.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));

         }

         // type check the arguments

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

-          Type st = SubstType(callee.Ins[i].Type, subst);

+          Type st = SubstType(callee.Ins[i].Type, s.TypeArgumentSubstitutions);

           if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {

             Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);

           }

         }

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

-          Type st = SubstType(callee.Outs[i].Type, subst);

+          Type st = SubstType(callee.Outs[i].Type, s.TypeArgumentSubstitutions);

           var lhs = s.Lhs[i];

           if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {

             Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);

@@ -3342,12 +3786,12 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Le:

           case BinaryExpr.Opcode.Add:

             {

-              if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsDatatype) {

+              if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {

                 if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {

                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

                 }

                 expr.Type = Type.Bool;

-              } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsDatatype) {

+              } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {

                 if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {

                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);

                 }

@@ -3376,7 +3820,7 @@ namespace Microsoft.Dafny {
           case BinaryExpr.Opcode.Gt:

           case BinaryExpr.Opcode.Ge:

             {

-              if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsDatatype) {

+              if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {

                 if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {

                   Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);

                 }

@@ -3909,24 +4353,24 @@ namespace Microsoft.Dafny {
             }

           }

           // build the type substitution map

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

+          e.TypeArgumentSubstitutions =  new Dictionary<TypeParameter, Type>();

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

-            subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

+            e.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);

           }

           foreach (TypeParameter p in function.TypeArgs) {

-            subst.Add(p, new ParamTypeProxy(p));

+            e.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));

           }

           // type check the arguments

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

             Expression farg = e.Args[i];

             ResolveExpression(farg, twoState);

             Contract.Assert(farg.Type != null);  // follows from postcondition of ResolveExpression

-            Type s = SubstType(function.Formals[i].Type, subst);

+            Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);

             if (!UnifyTypes(farg.Type, s)) {

               Error(e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);

             }

           }

-          e.Type = SubstType(function.ResultType, subst);

+          e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);

         }

 

         // Resolution termination check

@@ -4615,6 +5059,7 @@ namespace Microsoft.Dafny {
       Contract.Assert(e.Seq.Type != null);  // follows from postcondition of ResolveExpression

       Type elementType = new InferredTypeProxy();

       Type domainType = new InferredTypeProxy();

+      

       IndexableTypeProxy expectedType = new IndexableTypeProxy(elementType, domainType);

       if (!UnifyTypes(e.Seq.Type, expectedType)) {

         Error(e, "sequence/array/map selection requires a sequence, array or map (got {0})", e.Seq.Type);

@@ -4700,7 +5145,7 @@ namespace Microsoft.Dafny {
             return BinaryExpr.ResolvedOpcode.Disjoint;

           }

         case BinaryExpr.Opcode.Lt:

-          if (operandType.IsDatatype || operandType is DatatypeProxy) {

+          if (operandType.IsIndDatatype || operandType is DatatypeProxy) {

             return BinaryExpr.ResolvedOpcode.RankLt;

           } else if (operandType is SetType) {

             return BinaryExpr.ResolvedOpcode.ProperSubset;

diff --git a/Dafny/Rewriter.cs b/Dafny/Rewriter.cs
index 45e4f50c..af41a679 100644
--- a/Dafny/Rewriter.cs
+++ b/Dafny/Rewriter.cs
@@ -4,11 +4,22 @@ using System.Diagnostics.Contracts;
 

 namespace Microsoft.Dafny

 {

-  public interface Rewriter

+  [ContractClass(typeof(IRewriterContracts))]

+  public interface IRewriter

   {

     void PreResolve(ModuleDefinition m);

     void PostResolve(ModuleDefinition m);

   }

+  [ContractClassFor(typeof(IRewriter))]

+  abstract class IRewriterContracts : IRewriter

+  {

+    public void PreResolve(ModuleDefinition m) {

+      Contract.Requires(m != null);

+    }

+    public void PostResolve(ModuleDefinition m) {

+      Contract.Requires(m != null);

+    }

+  }

 

   /// <summary>

   /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate

@@ -48,7 +59,7 @@ namespace Microsoft.Dafny
   ///    if (A != null) { Repr := Repr + {A}; }

   ///    if (F != null) { Repr := Repr + {F} + F.Repr; }

   /// </summary>

-  public class AutoContractsRewriter : Rewriter

+  public class AutoContractsRewriter : IRewriter

   {

     public void PreResolve(ModuleDefinition m) {

       foreach (var d in m.TopLevelDecls) {

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 307fa321..32c92a8b 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -266,10 +266,10 @@ public class Scanner {
 		start[46] = 58; 

 		start[124] = 59; 

 		start[44] = 20; 

+		start[40] = 21; 

+		start[41] = 22; 

 		start[60] = 60; 

 		start[62] = 61; 

-		start[40] = 22; 

-		start[41] = 23; 

 		start[42] = 24; 

 		start[96] = 25; 

 		start[91] = 28; 

@@ -498,40 +498,40 @@ public class Scanner {
 			case "codatatype": t.kind = 18; break;

 			case "var": t.kind = 20; break;

 			case "type": t.kind = 22; break;

-			case "method": t.kind = 25; break;

-			case "constructor": t.kind = 26; break;

-			case "returns": t.kind = 27; break;

-			case "modifies": t.kind = 29; break;

-			case "free": t.kind = 30; break;

-			case "requires": t.kind = 31; break;

-			case "ensures": t.kind = 32; break;

-			case "decreases": t.kind = 33; break;

-			case "bool": t.kind = 36; break;

-			case "nat": t.kind = 37; break;

-			case "int": t.kind = 38; break;

-			case "set": t.kind = 39; break;

-			case "multiset": t.kind = 40; break;

-			case "seq": t.kind = 41; break;

-			case "map": t.kind = 42; break;

-			case "object": t.kind = 43; break;

-			case "function": t.kind = 44; break;

-			case "predicate": t.kind = 45; break;

-			case "reads": t.kind = 46; break;

-			case "label": t.kind = 49; break;

-			case "break": t.kind = 50; break;

-			case "return": t.kind = 51; break;

-			case "assume": t.kind = 54; break;

-			case "new": t.kind = 55; break;

-			case "choose": t.kind = 58; break;

-			case "if": t.kind = 59; break;

-			case "else": t.kind = 60; break;

-			case "case": t.kind = 61; break;

-			case "while": t.kind = 63; break;

-			case "invariant": t.kind = 64; break;

-			case "match": t.kind = 65; break;

-			case "assert": t.kind = 66; break;

-			case "print": t.kind = 67; break;

-			case "parallel": t.kind = 68; break;

+			case "method": t.kind = 28; break;

+			case "constructor": t.kind = 29; break;

+			case "returns": t.kind = 30; break;

+			case "modifies": t.kind = 32; break;

+			case "free": t.kind = 33; break;

+			case "requires": t.kind = 34; break;

+			case "ensures": t.kind = 35; break;

+			case "decreases": t.kind = 36; break;

+			case "bool": t.kind = 37; break;

+			case "nat": t.kind = 38; break;

+			case "int": t.kind = 39; break;

+			case "set": t.kind = 40; break;

+			case "multiset": t.kind = 41; break;

+			case "seq": t.kind = 42; break;

+			case "map": t.kind = 43; break;

+			case "object": t.kind = 44; break;

+			case "function": t.kind = 45; break;

+			case "predicate": t.kind = 46; break;

+			case "reads": t.kind = 47; break;

+			case "label": t.kind = 50; break;

+			case "break": t.kind = 51; break;

+			case "return": t.kind = 52; break;

+			case "assume": t.kind = 55; break;

+			case "new": t.kind = 56; break;

+			case "choose": t.kind = 59; break;

+			case "if": t.kind = 60; break;

+			case "else": t.kind = 61; break;

+			case "case": t.kind = 62; break;

+			case "while": t.kind = 64; break;

+			case "invariant": t.kind = 65; break;

+			case "match": t.kind = 66; break;

+			case "assert": t.kind = 67; break;

+			case "print": t.kind = 68; break;

+			case "parallel": t.kind = 69; break;

 			case "in": t.kind = 82; break;

 			case "false": t.kind = 92; break;

 			case "true": t.kind = 93; break;

@@ -652,47 +652,47 @@ public class Scanner {
 			case 20:

 				{t.kind = 21; break;}

 			case 21:

-				{t.kind = 28; break;}

+				{t.kind = 23; break;}

 			case 22:

-				{t.kind = 34; break;}

+				{t.kind = 25; break;}

 			case 23:

-				{t.kind = 35; break;}

+				{t.kind = 31; break;}

 			case 24:

-				{t.kind = 47; break;}

-			case 25:

 				{t.kind = 48; break;}

+			case 25:

+				{t.kind = 49; break;}

 			case 26:

-				{t.kind = 52; break;}

-			case 27:

 				{t.kind = 53; break;}

+			case 27:

+				{t.kind = 54; break;}

 			case 28:

-				{t.kind = 56; break;}

-			case 29:

 				{t.kind = 57; break;}

+			case 29:

+				{t.kind = 58; break;}

 			case 30:

-				{t.kind = 62; break;}

+				{t.kind = 63; break;}

 			case 31:

 				if (ch == '>') {AddCh(); goto case 32;}

 				else {goto case 0;}

 			case 32:

-				{t.kind = 69; break;}

-			case 33:

 				{t.kind = 70; break;}

-			case 34:

+			case 33:

 				{t.kind = 71; break;}

-			case 35:

+			case 34:

 				{t.kind = 72; break;}

+			case 35:

+				{t.kind = 73; break;}

 			case 36:

 				if (ch == '&') {AddCh(); goto case 37;}

 				else {goto case 0;}

 			case 37:

-				{t.kind = 73; break;}

-			case 38:

 				{t.kind = 74; break;}

-			case 39:

+			case 38:

 				{t.kind = 75; break;}

-			case 40:

+			case 39:

 				{t.kind = 76; break;}

+			case 40:

+				{t.kind = 77; break;}

 			case 41:

 				{t.kind = 79; break;}

 			case 42:

@@ -731,8 +731,8 @@ public class Scanner {
 				else {t.kind = 5; break;}

 			case 57:

 				recEnd = pos; recKind = 11;

-				if (ch == '>') {AddCh(); goto case 30;}

-				else if (ch == '=') {AddCh(); goto case 63;}

+				if (ch == '=') {AddCh(); goto case 63;}

+				else if (ch == '>') {AddCh(); goto case 30;}

 				else {t.kind = 11; break;}

 			case 58:

 				recEnd = pos; recKind = 14;

@@ -743,25 +743,25 @@ public class Scanner {
 				if (ch == '|') {AddCh(); goto case 39;}

 				else {t.kind = 19; break;}

 			case 60:

-				recEnd = pos; recKind = 23;

+				recEnd = pos; recKind = 26;

 				if (ch == '=') {AddCh(); goto case 65;}

-				else {t.kind = 23; break;}

+				else {t.kind = 26; break;}

 			case 61:

-				recEnd = pos; recKind = 24;

+				recEnd = pos; recKind = 27;

 				if (ch == '=') {AddCh(); goto case 41;}

-				else {t.kind = 24; break;}

+				else {t.kind = 27; break;}

 			case 62:

 				recEnd = pos; recKind = 83;

 				if (ch == '=') {AddCh(); goto case 42;}

 				else if (ch == '!') {AddCh(); goto case 43;}

 				else {t.kind = 83; break;}

 			case 63:

-				recEnd = pos; recKind = 77;

+				recEnd = pos; recKind = 24;

 				if (ch == '>') {AddCh(); goto case 34;}

-				else {t.kind = 77; break;}

+				else {t.kind = 24; break;}

 			case 64:

 				recEnd = pos; recKind = 100;

-				if (ch == '.') {AddCh(); goto case 21;}

+				if (ch == '.') {AddCh(); goto case 23;}

 				else {t.kind = 100; break;}

 			case 65:

 				recEnd = pos; recKind = 78;

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 7a841a3b..86b0afc6 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -4247,7 +4247,16 @@ namespace Microsoft.Dafny {
           decrs.Add(etran.TrExpr(e));

         }

         Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, etran, loopBodyBuilder, " at end of loop iteration", false, false);

-        loopBodyBuilder.Add(Assert(s.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease"));

+        string msg;

+        if (inferredDecreases) {

+          msg = "cannot prove termination; try supplying a decreases clause for the loop";

+          if (s is RefinedWhileStmt) {

+            msg += " (note that a refined loop does not inherit 'decreases *' from the refined loop)";

+          }

+        } else {

+          msg = "decreases expression might not decrease";

+        }

+        loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg));

       }

       // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check

       // of invariant-maintenance can use the appropriate canCall predicates.

@@ -4625,7 +4634,7 @@ namespace Microsoft.Dafny {
       if (allowance != null) {

         decrExpr = Bpl.Expr.Or(allowance, decrExpr);

       }

-      var msg = inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure";

+      string msg = inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure";

       if (hint != null) {

         msg += " (" + hint + ")";

       }

diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy
index b70ff4d0..76e1ffa7 100644
--- a/Test/VSI-Benchmarks/b4.dfy
+++ b/Test/VSI-Benchmarks/b4.dfy
@@ -14,7 +14,7 @@
 // that the specification can use mathematical sequences while the

 // implementation uses a linked list.

 

-class Map<Key,Value> {

+class Map<Key(==),Value> {

   ghost var Keys: seq<Key>;

   ghost var Values: seq<Value>;

   ghost var Repr: set<object>;

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 383bccfd..2149df25 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -250,7 +250,7 @@ class WriterStream {
   

   

   

-class Map<Key,Value> {

+class Map<Key(==),Value> {

   var keys: seq<Key>;

   var values: seq<Value>;

   

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5f80df86..7510363a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -58,7 +58,6 @@ class C {
 Dafny program verifier finished with 0 verified, 0 errors

 

 -------------------- TypeTests.dfy --------------------

-TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

 TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

@@ -88,11 +87,12 @@ TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)

 TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

 TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type

+TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context

-TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

 36 resolution/type errors detected in TypeTests.dfy

 

@@ -719,33 +719,32 @@ Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of th
 Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

-Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)

-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

-Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)

-Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

-Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

-Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

-Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

-Modules0.dfy(250,15): Error: unresolved identifier: X

-Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(294,16): Error: member R does not exist in class B

-Modules0.dfy(294,6): Error: expected method call, found expression

-Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

-Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

-Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)

-Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)

-Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp

-Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

-Modules0.dfy(327,30): Error: member Create does not exist in class Klassy

-Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts

-Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts

-Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts

-Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context

-Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context

-37 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(52,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(52,12): Error: new can be applied only to reference types (got T)

+Modules0.dfy(57,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

+Modules0.dfy(73,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

+Modules0.dfy(74,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

+Modules0.dfy(84,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

+Modules0.dfy(108,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

+Modules0.dfy(247,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

+Modules0.dfy(256,13): Error: unresolved identifier: X

+Modules0.dfy(257,15): Error: member DoesNotExist does not exist in class X

+Modules0.dfy(299,16): Error: member R does not exist in class B

+Modules0.dfy(299,6): Error: expected method call, found expression

+Modules0.dfy(322,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

+Modules0.dfy(326,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

+Modules0.dfy(327,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)

+Modules0.dfy(328,11): Error: Undeclared module name: Wazzup (did you forget a module import?)

+Modules0.dfy(329,17): Error: Undeclared class name Edon in module Q_Imp

+Modules0.dfy(331,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

+Modules0.dfy(332,30): Error: member Create does not exist in class Klassy

+Modules0.dfy(143,11): Error: ghost variables are allowed only in specification contexts

+Modules0.dfy(157,11): Error: old expressions are allowed only in specification and ghost contexts

+Modules0.dfy(158,11): Error: fresh expressions are allowed only in specification and ghost contexts

+Modules0.dfy(159,11): Error: allocated expressions are allowed only in specification and ghost contexts

+Modules0.dfy(175,10): Error: match source expression 'tree' has already been used as a match source expression in this context

+Modules0.dfy(214,12): Error: match source expression 'l' has already been used as a match source expression in this context

+36 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(74,16): Error: assertion violation

@@ -1328,6 +1327,17 @@ Dafny program verifier finished with 12 verified, 3 errors
 

 Dafny program verifier finished with 12 verified, 0 errors

 

+-------------------- EqualityTypes.dfy --------------------

+EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype

+EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

+EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters

+EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters

+EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality

+EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

+EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)

+EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)

+8 resolution/type errors detected in EqualityTypes.dfy

+

 -------------------- SplitExpr.dfy --------------------

 

 Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index cc66c3c1..80ac7eef 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -45,9 +45,12 @@ module A imports N, M {  // Note, this has the effect of importing two different
     { x }

     method M(x: T)  // error: use of the ambiguous name T

       returns (y: T)  // error: use of the ambiguous name T

-    { var g := new T; }  // error: use of the ambiguous name T

   }

 }

+module A' imports N, M {

+  method M()

+    { var g := new T; }  // error: use of the ambiguous name T

+}

 

 module B0 imports A {

   class BadUse {

@@ -241,15 +244,17 @@ module BTr imports ATr {
 module CTr imports BTr {

   class Z {

     var b: Y;  // fine

-    var a: X;  // error: imports don't reach name name X explicitly

-    method P() {

-      var y := new Y;

-      var x := y.N();  // this is allowed and will correctly infer the type of x to

-                       // be X, but X could not have been mentioned explicitly

-      var q := x.M();

-      var r := X.Q();  // error: X is not in scope

-      var s := x.DoesNotExist();  // error: method not declared in class X

-    }

+    var a: X;  // error: imports don't reach name X explicitly

+  }

+}

+module CTs imports BTr {

+  method P() {

+    var y := new Y;

+    var x := y.N();  // this is allowed and will correctly infer the type of x to

+                     // be X, but X could not have been mentioned explicitly

+    var q := x.M();

+    var r := X.Q();  // error: X is not in scope

+    var s := x.DoesNotExist();  // error: method not declared in class X

   }

 }

 

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index e8b618d7..40df1135 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -294,7 +294,7 @@ method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)
   assert x != y;

 }

 

-method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)

+method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)

   requires 0 <= N && N <= |a|;

   requires exists k | 0 <= k && k < N :: a[k] == y;

   ensures forall k | 0 <= k && k < N :: a[k] == y;  // error

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 1482dc24..bf3702ae 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -92,8 +92,8 @@ class Termination {
     ensures a == List.Cons(val, b);

   {

     match a {

-	  case Cons(v, r) => val := v; b := r;

-	}

+      case Cons(v, r) => val := v; b := r;

+    }

   }

 }

 

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index d6804661..cb9b5660 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -1,11 +1,11 @@
-class C<U> {

+class C<U(==)> {

   method M<T>(x: T, u: U) returns (y: T)

     ensures x == y && u == u;

   {

     y := x;

   }

 

-  function method F<X>(x: X, u: U): bool

+  function method F<X(==)>(x: X, u: U): bool

   {

     x == x && u == u

   }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 8434f06c..2dea7a52 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -86,7 +86,8 @@ method ArrayRangeAssignments(a: array<C>, c: C)
 

 // --------------------- tests of restrictions on subranges (nat)

 

-method K(s: set<nat>) {  // error: not allowed to instantiate 'set' with 'nat'

+method K() {

+  var s: set<nat>;  // error: not allowed to instantiate 'set' with 'nat'

   var d: MutuallyRecursiveDataType<nat>;  // error: not allowed to instantiate with 'nat'

   var a := new nat[100];  // error: not allowed the type array<nat>

   var b := new nat[100,200];  // error: not allowed the type array2<nat>

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index ac7c8aed..d352cf44 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

             TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy

-            TypeAntecedents.dfy NoTypeArgs.dfy SplitExpr.dfy

+            TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy

             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 7c7719ee..06cac03b 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -51,6 +51,10 @@ Dafny program verifier finished with 8 verified, 0 errors
 

 Dafny program verifier finished with 10 verified, 0 errors

 

+-------------------- SchorrWaite-stages.dfy --------------------

+

+Dafny program verifier finished with 16 verified, 0 errors

+

 -------------------- Cubes.dfy --------------------

 

 Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 21b895aa..4c761671 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
 }

 

 method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

-  requires (exists c :: IsCelebrity(c, people));

+  requires exists c :: IsCelebrity(c, people);

   ensures r == c;

 {

   var cc; assume cc == c;  // this line essentially converts ghost c to non-ghost cc

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c8419890..c78d5e81 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,6 +1,6 @@
 // ultra filter

 

-class UltraFilter<G> {

+class UltraFilter<G(==)> {

   static function IsFilter(f: set<set<G>>, S: set<G>): bool

   {

     (forall A, B :: A in f && A <= B ==> B in f) &&

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index d098d753..fa7f7c70 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy
             SeparationLogicList.dfy

             ListCopy.dfy ListReverse.dfy ListContents.dfy

             MatrixFun.dfy pow2.dfy

-            SchorrWaite.dfy

+            SchorrWaite.dfy SchorrWaite-stages.dfy

             Cubes.dfy SumOfCubes.dfy FindZero.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

             Induction.dfy Rippling.dfy MoreInduction.dfy

diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy
index a7512486..af67ee92 100644
--- a/Test/dafny2/MajorityVote.dfy
+++ b/Test/dafny2/MajorityVote.dfy
@@ -31,6 +31,10 @@
 // choice, if there is such a choice, and then passes in that choice as the ghost parameter K

 // to the main algorithm.  Neat, huh?

 

+// Language comment:

+// The "(==)" that sits after some type parameters in this program says that the actual

+// type argument must support equality.

+

 // Advanced remark:

 // There is a subtle situation in the verification of DetermineElection.  Suppose the type

 // parameter Candidate denotes some type whose instances depend on which object are

@@ -47,7 +51,7 @@
 // to the Count function.  Alternatively, one could have added the antecedent "c in a" or

 // "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.

 

-function method Count<T>(a: seq<T>, s: int, t: int, x: T): int

+function method Count<T(==)>(a: seq<T>, s: int, t: int, x: T): int

   requires 0 <= s <= t <= |a|;

   ensures Count(a, s, t, x) == 0 || x in a;

 {

@@ -57,7 +61,7 @@ function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
 

 // Here is the first version of the algorithm, the one that assumes there is a majority choice.

 

-method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

+method FindWinner<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)

   requires 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

   ensures k == K;  // find K

 {

@@ -93,7 +97,7 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k:
 // Here is the second version of the program, the one that also computes whether or not

 // there is a majority choice.

 

-method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)

+method DetermineElection<Candidate(==)>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)

   ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;

   ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;

 {

@@ -107,7 +111,7 @@ method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool,
 // antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"

 // statement.

 

-method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)

+method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)

   requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|;  // K has a (strict) majority of the votes

   ensures hasWinner ==> k == K;  // find K

 {

diff --git a/Test/vacid0/AnswerRuntimeChecking b/Test/vacid0/AnswerRuntimeChecking
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/Test/vacid0/AnswerRuntimeChecking
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index 5153b053..4373136b 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -1,4 +1,4 @@
-class BreadthFirstSearch<Vertex>

+class BreadthFirstSearch<Vertex(==)>

 {

   // The following function is left uninterpreted (for the purpose of the 

   // verification problem, it can be thought of as a parameter to the class)

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 051d60f4..af789102 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -42,6 +42,7 @@
     % the following isn't actually Dafny, but it gives the option to produce nicer latex

     {<<}{$\langle$}1

     {>>}{$\rangle$}1

+    {(==)}{${}^{(=)}$}2

     {...}{$\ldots$}1

     {\\alpha}{$\alpha$}1

     {\\beta}{$\beta$}1