Merge

10 files changed, 2838 insertions, 2612 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 032e30a0..c94c697d 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -40,7 +40,7 @@ namespace Microsoft.Dafny
       } else if (d is TypeSynonymDecl) {

         var dd = (TypeSynonymDecl)d;

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

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

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

       } else if (d is NewtypeDecl) {

         var dd = (NewtypeDecl)d;

         if (dd.Var == null) {

@@ -61,7 +61,7 @@ namespace Microsoft.Dafny
         var dd = (CoDatatypeDecl)d;

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

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

-        var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));

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

         return dt;

       } else if (d is IteratorDecl) {

         var dd = (IteratorDecl)d;

@@ -97,7 +97,7 @@ namespace Microsoft.Dafny
               var dd = (TraitDecl)d;

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

               var mm = dd.Members.ConvertAll(CloneMember);

-              var cl = new TraitDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));

+              var cl = new TraitDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd);

               return cl;

           }

       }

@@ -106,7 +106,7 @@ namespace Microsoft.Dafny
         var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

         var mm = dd.Members.ConvertAll(CloneMember);

         if (d is DefaultClassDecl) {

-          return new DefaultClassDecl(m, mm);

+          return new DefaultClassDecl(m, mm, ((DefaultClassDecl)d));

         } else {

           return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd);

         }

@@ -137,7 +137,7 @@ namespace Microsoft.Dafny
     }

 

     public DatatypeCtor CloneCtor(DatatypeCtor ct) {

-      return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes));

+      return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes), ct);

     }

 

     public TypeParameter CloneTypeParam(TypeParameter tp) {

@@ -649,16 +649,16 @@ namespace Microsoft.Dafny
 

       if (f is Predicate) {

         return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, f.IsGhost, tps, formals,

-          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null);

+          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null, f);

       } else if (f is InductivePredicate) {

         return new InductivePredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,

-          req, reads, ens, body, CloneAttributes(f.Attributes), null);

+          req, reads, ens, body, CloneAttributes(f.Attributes), null, f);

       } else if (f is CoPredicate) {

         return new CoPredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,

-          req, reads, ens, body, CloneAttributes(f.Attributes), null);

+          req, reads, ens, body, CloneAttributes(f.Attributes), null, f);

       } else {

         return new Function(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, f.IsGhost, tps, formals, CloneType(f.ResultType),

-          req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);

+          req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null, f);

       }

     }

 

@@ -676,19 +676,19 @@ namespace Microsoft.Dafny
       var body = CloneBlockStmt(m.Body);

       if (m is Constructor) {

         return new Constructor(Tok(m.tok), m.Name, tps, ins,

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else if (m is InductiveLemma) {

         return new InductiveLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else if (m is CoLemma) {

         return new CoLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else if (m is Lemma) {

         return new Lemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       } else {

         return new Method(Tok(m.tok), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

+          req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m);

       }

     }

     public virtual IToken Tok(IToken tok) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index cdd968cf..13381cc7 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -102,7 +102,11 @@ namespace Microsoft.Dafny {
         }

         int indent = 0;

         if (!m.IsDefaultModule) {

-          wr.WriteLine("namespace @{0} {{", m.CompileName);

+          var m_prime = m;

+          while (DafnyOptions.O.IronDafny && m_prime.ClonedFrom != null) {

+            m_prime = m.ClonedFrom;

+          }

+          wr.WriteLine("namespace @{0} {{", m_prime.CompileName);

           indent += IndentAmount;

         }

         foreach (TopLevelDecl d in m.TopLevelDecls) {

@@ -687,11 +691,18 @@ namespace Microsoft.Dafny {
       return formal.HasName ? formal.CompileName : "_a" + i;

     }

 

+    string DtName(DatatypeDecl decl) {

+        var d = (TopLevelDecl)decl;

+        while (DafnyOptions.O.IronDafny && d.ClonedFrom != null) {

+          d = (TopLevelDecl)d.ClonedFrom;

+        }

+      return d.Module.IsDefaultModule ? d.CompileName : d.FullCompileName;

+    }

     string DtCtorName(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

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

 

-      return ctor.EnclosingDatatype.FullCompileName + "_" + ctor.CompileName;

+      return DtName(ctor.EnclosingDatatype) + "_" + ctor.CompileName;

     }

     string DtCtorDeclartionName(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

@@ -1123,61 +1134,78 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

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

 

-      type = type.NormalizeExpand();

-      if (type is TypeProxy) {

+      var xType = type.NormalizeExpand();

+      if (xType is TypeProxy) {

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

         return "object";

       }

 

-      if (type is BoolType) {

+      if (xType is BoolType) {

         return "bool";

-      } else if (type is CharType) {

+      } else if (xType is CharType) {

         return "char";

-      } else if (type is IntType) {

+      } else if (xType is IntType) {

         return "BigInteger";

-      } else if (type is RealType) {

+      } else if (xType is RealType) {

         return "Dafny.BigRational";

-      } else if (type.AsNewtype != null) {

-        NativeType nativeType = type.AsNewtype.NativeType;

+      } else if (xType.AsNewtype != null) {

+        NativeType nativeType = xType.AsNewtype.NativeType;

         if (nativeType != null) {

           return nativeType.Name;

         }

-        return TypeName(type.AsNewtype.BaseType);

-      } else if (type is ObjectType) {

+        return TypeName(xType.AsNewtype.BaseType);

+      } else if (xType is ObjectType) {

         return "object";

-      } else if (type.IsArrayType) {

-        ArrayClassDecl at = type.AsArrayType;

+      } else if (xType.IsArrayType) {

+        ArrayClassDecl at = xType.AsArrayType;

         Contract.Assert(at != null);  // follows from type.IsArrayType

-        Type elType = UserDefinedType.ArrayElementType(type);

+        Type elType = UserDefinedType.ArrayElementType(xType);

         string name = TypeName(elType) + "[";

         for (int i = 1; i < at.Dims; i++) {

           name += ",";

         }

         return name + "]";

-      } else if (type is UserDefinedType) {

-        var udt = (UserDefinedType)type;

-        return TypeName_UDT(udt.FullCompileName, udt.TypeArgs);

-      } else if (type is SetType) {

-        Type argType = ((SetType)type).Arg;

+      } else if (xType is UserDefinedType) {

+        var udt = (UserDefinedType)xType;

+        var s = udt.FullCompileName;

+        var rc = udt.ResolvedClass;

+        if (DafnyOptions.O.IronDafny && 

+            !(xType is ArrowType) &&

+            rc != null &&

+            rc.Module != null &&

+            !rc.Module.IsDefaultModule) {

+          while (rc.ClonedFrom != null || rc.ExclusiveRefinement != null) {

+            if (rc.ClonedFrom != null) {

+              rc = (TopLevelDecl)rc.ClonedFrom;

+            } else {

+              Contract.Assert(rc.ExclusiveRefinement != null);

+              rc = rc.ExclusiveRefinement;

+            }

+          }

+          s = rc.FullCompileName;

+        }

+        return TypeName_UDT(s, udt.TypeArgs);

+      } else if (xType is SetType) {

+        Type argType = ((SetType)xType).Arg;

         if (argType is ObjectType) {

           Error("compilation of set<object> is not supported; consider introducing a ghost");

         }

         return DafnySetClass + "<" + TypeName(argType) + ">";

-      } else if (type is SeqType) {

-        Type argType = ((SeqType)type).Arg;

+      } else if (xType is SeqType) {

+        Type argType = ((SeqType)xType).Arg;

         if (argType is ObjectType) {

           Error("compilation of seq<object> is not supported; consider introducing a ghost");

         }

         return DafnySeqClass + "<" + TypeName(argType) + ">";

-      } else if (type is MultiSetType) {

-        Type argType = ((MultiSetType)type).Arg;

+      } else if (xType is MultiSetType) {

+        Type argType = ((MultiSetType)xType).Arg;

         if (argType is ObjectType) {

           Error("compilation of seq<object> is not supported; consider introducing a ghost");

         }

         return DafnyMultiSetClass + "<" + TypeName(argType) + ">";

-      } else if (type is MapType) {

-        Type domType = ((MapType)type).Domain;

-        Type ranType = ((MapType)type).Range;

+      } else if (xType is MapType) {

+        Type domType = ((MapType)xType).Domain;

+        Type ranType = ((MapType)xType).Range;

         if (domType is ObjectType || ranType is ObjectType) {

           Error("compilation of map<object, _> or map<_, object> is not supported; consider introducing a ghost");

         }

@@ -1218,36 +1246,52 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

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

 

-      type = type.NormalizeExpand();

-      if (type is TypeProxy) {

+      var xType = type.NormalizeExpand();

+      if (xType is TypeProxy) {

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

         return "null";

       }

 

-      if (type is BoolType) {

+      if (xType is BoolType) {

         return "false";

-      } else if (type is CharType) {

+      } else if (xType is CharType) {

         return "'D'";

-      } else if (type is IntType) {

+      } else if (xType is IntType) {

         return "BigInteger.Zero";

-      } else if (type is RealType) {

+      } else if (xType is RealType) {

         return "Dafny.BigRational.ZERO";

-      } else if (type.AsNewtype != null) {

-        if (type.AsNewtype.NativeType != null) {

+      } else if (xType.AsNewtype != null) {

+        if (xType.AsNewtype.NativeType != null) {

           return "0";

         }

-        return DefaultValue(type.AsNewtype.BaseType);

-      } else if (type.IsRefType) {

-        return string.Format("({0})null", TypeName(type));

-      } else if (type.IsDatatype) {

-        UserDefinedType udt = (UserDefinedType)type;

-        string s = "@" + udt.FullCompileName;

+        return DefaultValue(xType.AsNewtype.BaseType);

+      } else if (xType.IsRefType) {

+        return string.Format("({0})null", TypeName(xType));

+      } else if (xType.IsDatatype) {

+        var udt = (UserDefinedType)xType;

+        var s = "@" + udt.FullCompileName;

+        var rc = udt.ResolvedClass;

+        if (DafnyOptions.O.IronDafny && 

+            !(xType is ArrowType) &&

+            rc != null &&

+            rc.Module != null &&

+            !rc.Module.IsDefaultModule) {

+          while (rc.ClonedFrom != null || rc.ExclusiveRefinement != null) {

+            if (rc.ClonedFrom != null) {

+              rc = (TopLevelDecl)rc.ClonedFrom;

+            } else {

+              Contract.Assert(rc.ExclusiveRefinement != null);

+              rc = rc.ExclusiveRefinement;

+            }

+          }

+          s = "@" + rc.FullCompileName;

+        }

         if (udt.TypeArgs.Count != 0) {

           s += "<" + TypeNames(udt.TypeArgs) + ">";

         }

         return string.Format("new {0}()", s);

-      } else if (type.IsTypeParameter) {

-        var udt = (UserDefinedType)type;

+      } else if (xType.IsTypeParameter) {

+        var udt = (UserDefinedType)xType;

         string s = "default(@" + udt.FullCompileName;

         if (udt.TypeArgs.Count != 0)

         {

@@ -1255,15 +1299,15 @@ namespace Microsoft.Dafny {
         }

         s += ")";

         return s;

-      } else if (type is SetType) {

-        return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";

-      } else if (type is MultiSetType) {

-        return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)type).Arg) + ">.Empty";

-      } else if (type is SeqType) {

-        return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";

-      } else if (type is MapType) {

-        return TypeName(type)+".Empty";

-      } else if (type is ArrowType) {

+      } else if (xType is SetType) {

+        return DafnySetClass + "<" + TypeName(((SetType)xType).Arg) + ">.Empty";

+      } else if (xType is MultiSetType) {

+        return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)xType).Arg) + ">.Empty";

+      } else if (xType is SeqType) {

+        return DafnySeqClass + "<" + TypeName(((SeqType)xType).Arg) + ">.Empty";

+      } else if (xType is MapType) {

+        return TypeName(xType)+".Empty";

+      } else if (xType is ArrowType) {

         return "null";

       } else {

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

@@ -2392,7 +2436,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

         var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs));

 

-        wr.Write("new {0}{1}(", dtv.Ctor.EnclosingDatatype.FullCompileName, typeParams);

+        wr.Write("new {0}{1}(", DtName(dtv.Ctor.EnclosingDatatype), typeParams);

         if (!dtv.IsCoCall) {

           // For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:

           //   new Dt_Cons<T>( args )

@@ -2864,7 +2908,7 @@ namespace Microsoft.Dafny {
             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

             wr.Write("Dafny.Helpers.QuantDatatype(");

 

-            wr.Write("{0}.AllSingletonConstructors, ", b.Decl.FullCompileName);

+            wr.Write("{0}.AllSingletonConstructors, ", DtName(b.Decl));

           } else {

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

           }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b460d9b4..4fc48f2f 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -183,7 +183,7 @@ namespace Microsoft.Dafny {
           null, null, null);

         readsIS.Function = reads;  // just so we can really claim the member declarations are resolved

         readsIS.TypeArgumentSubstitutions = Util.Dict(tps, tys);  // ditto

-        var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule, DontCompile());

+        var arrowDecl = new ArrowTypeDecl(tps, req, reads, SystemModule, DontCompile(), null);

         arrowTypeDecls.Add(arity, arrowDecl);

         SystemModule.TopLevelDecls.Add(arrowDecl);

       }

@@ -431,16 +431,33 @@ namespace Microsoft.Dafny {
         var pt = type as TypeProxy;

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

           type = pt.T;

-        } else {

+          continue;

+        }

           var syn = type.AsTypeSynonym;

           if (syn != null) {

             var udt = (UserDefinedType)type;  // correctness of cast follows from the AsTypeSynonym != null test.

             // Instantiate with the actual type arguments

             type = syn.RhsWithArgument(udt.TypeArgs);

+          continue;

+        }

+        if (DafnyOptions.O.IronDafny && type is UserDefinedType) {

+          var rc = ((UserDefinedType)type).ResolvedClass;

+          if (rc != null) {

+            while (rc.ClonedFrom != null || rc.ExclusiveRefinement != null) {

+              if (rc.ClonedFrom != null) {

+                rc = (TopLevelDecl)rc.ClonedFrom;

           } else {

-            return type;

+                Contract.Assert(rc.ExclusiveRefinement != null);

+                rc = rc.ExclusiveRefinement;

+              }

+            }

+          }

+          if (rc is TypeSynonymDecl) {

+            type = ((TypeSynonymDecl)rc).Rhs;

+            continue;

           }

         }

+        return type;

       }

     }

 

@@ -1051,7 +1068,11 @@ namespace Microsoft.Dafny {
     public string FullCompanionCompileName {

       get {

         Contract.Requires(ResolvedClass is TraitDecl);

-        var s = ResolvedClass.Module.IsDefaultModule ? "" : ResolvedClass.Module.CompileName + ".";

+          var m = ResolvedClass.Module;

+          while (DafnyOptions.O.IronDafny && m.ClonedFrom != null) {

+            m = m.ClonedFrom;

+          }

+        var s = m.IsDefaultModule ? "" : m.CompileName + ".";

         return s + "@_Companion_" + CompileName;

       }

     }

@@ -1823,6 +1844,16 @@ namespace Microsoft.Dafny {
       }

     }

 

+    public string RefinementCompileName {

+      get {

+        if (ExclusiveRefinement != null) {

+          return this.ExclusiveRefinement.RefinementCompileName;

+        } else {

+          return this.CompileName;

+        }

+      }

+    }

+

     /// <summary>

     /// Determines if "a" and "b" are in the same strongly connected component of the call graph, that is,

     /// if "a" and "b" are mutually recursive.

@@ -1967,6 +1998,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(typeArgs));

       Module = module;

       TypeArgs = typeArgs;

+      ExclusiveRefinement = null;

     }

 

     public string FullName {

@@ -1979,6 +2011,13 @@ namespace Microsoft.Dafny {
         return Module.CompileName + "." + CompileName;

       }

     }

+

+    public string FullSanitizedRefinementName {

+      get {

+        return Module.RefinementCompileName + "." + CompileName;

+      }

+    }

+

     public string FullNameInContext(ModuleDefinition context) {

       if (Module == context) {

         return Name;

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

       }

     }

+    public TopLevelDecl ExclusiveRefinement { get; set; }

   }

 

   public class TraitDecl : ClassDecl

@@ -2002,8 +2042,8 @@ namespace Microsoft.Dafny {
     public override string WhatKind { get { return "trait"; } }

     public bool IsParent { set; get; }

     public TraitDecl(IToken tok, string name, ModuleDefinition module,

-      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes)

-      : base(tok, name, module, typeArgs, members, attributes, null) { }

+      List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, TraitDecl clonedFrom = null)

+      : base(tok, name, module, typeArgs, members, attributes, null, clonedFrom) { }

   }

 

   public class ClassDecl : TopLevelDecl {

@@ -2045,8 +2085,8 @@ namespace Microsoft.Dafny {
   }

 

   public class DefaultClassDecl : ClassDecl {

-    public DefaultClassDecl(ModuleDefinition module, [Captured] List<MemberDecl> members)

-      : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null, null) {

+    public DefaultClassDecl(ModuleDefinition module, [Captured] List<MemberDecl> members, DefaultClassDecl clonedFrom = null)

+      : base(Token.NoToken, "_default", module, new List<TypeParameter>(), members, null, null, clonedFrom) {

       Contract.Requires(module != null);

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

     }

@@ -2079,9 +2119,9 @@ namespace Microsoft.Dafny {
     public readonly Function Requires;

     public readonly Function Reads;

 

-    public ArrowTypeDecl(List<TypeParameter> tps, Function req, Function reads, ModuleDefinition module, Attributes attributes)

+    public ArrowTypeDecl(List<TypeParameter> tps, Function req, Function reads, ModuleDefinition module, Attributes attributes, ArrowTypeDecl clonedFrom)

       : base(Token.NoToken, ArrowType.ArrowTypeName(tps.Count - 1), module, tps,

-             new List<MemberDecl> { req, reads }, attributes, null) {

+             new List<MemberDecl> { req, reads }, attributes, null, clonedFrom) {

       Contract.Requires(tps != null && 1 <= tps.Count);

       Contract.Requires(req != null);

       Contract.Requires(reads != null);

@@ -2207,8 +2247,8 @@ namespace Microsoft.Dafny {
     public CoDatatypeDecl SscRepr;  // filled in during resolution

 

     public CoDatatypeDecl(IToken tok, string name, ModuleDefinition module, List<TypeParameter> typeArgs,

-      [Captured] List<DatatypeCtor> ctors, Attributes attributes)

-      : base(tok, name, module, typeArgs, ctors, attributes) {

+      [Captured] List<DatatypeCtor> ctors, Attributes attributes, CoDatatypeDecl clonedFrom = null)

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

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(module != null);

@@ -2235,8 +2275,8 @@ namespace Microsoft.Dafny {
     public SpecialField QueryField;  // filled in during resolution

     public List<DatatypeDestructor> Destructors = new List<DatatypeDestructor>();  // contents filled in during resolution; includes both implicit (not mentionable in source) and explicit destructors

 

-    public DatatypeCtor(IToken tok, string name, [Captured] List<Formal> formals, Attributes attributes)

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

+    public DatatypeCtor(IToken tok, string name, [Captured] List<Formal> formals, Attributes attributes, DatatypeCtor clonedFrom = null)

+      : base(tok, name, attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

@@ -2489,8 +2529,8 @@ namespace Microsoft.Dafny {
     public readonly bool IsGhost;

     public TopLevelDecl EnclosingClass;  // filled in during resolution

     public MemberDecl RefinementBase;  // filled in during the pre-resolution refinement transformation; null if the member is new here

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

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

+    public MemberDecl(IToken tok, string name, bool hasStaticKeyword, bool isGhost, Attributes attributes, Declaration clonedFrom = null)

+      : base(tok, name, attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       HasStaticKeyword = hasStaticKeyword;

@@ -2515,6 +2555,14 @@ namespace Microsoft.Dafny {
         return EnclosingClass.FullSanitizedName + "." + CompileName;

       }

     }

+    public string FullSanitizedRefinementName {

+      get {

+        Contract.Requires(EnclosingClass != null);

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

+

+        return EnclosingClass.FullSanitizedRefinementName + "." + CompileName;

+      }

+    }

     public string FullNameInContext(ModuleDefinition context) {

       Contract.Requires(EnclosingClass != null);

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

@@ -2726,8 +2774,8 @@ namespace Microsoft.Dafny {
   {

     public override string WhatKind { get { return "type synonym"; } }

     public readonly Type Rhs;

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

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

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

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

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

       Contract.Requires(typeArgs != null);

@@ -3131,8 +3179,8 @@ namespace Microsoft.Dafny {
     public Function(IToken tok, string name, bool hasStaticKeyword, bool isProtected, bool isGhost,

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

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

-                    Expression body, Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, isGhost, attributes) {

+                    Expression body, Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, hasStaticKeyword, isGhost, attributes, clonedFrom) {

 

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -3187,8 +3235,8 @@ namespace Microsoft.Dafny {
     public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected, bool isGhost,

                      List<TypeParameter> typeArgs, List<Formal> formals,

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

-                     Expression body, BodyOriginKind bodyOrigin, Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, isProtected, isGhost, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {

+                     Expression body, BodyOriginKind bodyOrigin, Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, hasStaticKeyword, isProtected, isGhost, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis, clonedFrom) {

       Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);

       BodyOrigin = bodyOrigin;

     }

@@ -3206,7 +3254,7 @@ namespace Microsoft.Dafny {
                      List<TypeParameter> typeArgs, Formal k, List<Formal> formals,

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

                      Expression body, Attributes attributes, FixpointPredicate fixpointPred)

-      : base(tok, name, hasStaticKeyword, isProtected, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {

+      : base(tok, name, hasStaticKeyword, isProtected, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null, null) {

       Contract.Requires(k != null);

       Contract.Requires(fixpointPred != null);

       Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k);

@@ -3223,9 +3271,9 @@ namespace Microsoft.Dafny {
     public FixpointPredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,

                              List<TypeParameter> typeArgs, List<Formal> formals,

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

-                             Expression body, Attributes attributes, IToken signatureEllipsis)

+                             Expression body, Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

       : base(tok, name, hasStaticKeyword, isProtected, true, typeArgs, formals, new BoolType(),

-             req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureEllipsis) {

+             req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureEllipsis, clonedFrom) {

     }

 

     /// <summary>

@@ -3264,9 +3312,9 @@ namespace Microsoft.Dafny {
     public InductivePredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,

                               List<TypeParameter> typeArgs, List<Formal> formals,

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

-                              Expression body, Attributes attributes, IToken signatureEllipsis)

+                              Expression body, Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

       : base(tok, name, hasStaticKeyword, isProtected, typeArgs, formals,

-             req, reads, ens, body, attributes, signatureEllipsis) {

+             req, reads, ens, body, attributes, signatureEllipsis, clonedFrom) {

     }

   }

 

@@ -3276,9 +3324,9 @@ namespace Microsoft.Dafny {
     public CoPredicate(IToken tok, string name, bool hasStaticKeyword, bool isProtected,

                        List<TypeParameter> typeArgs, List<Formal> formals,

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

-                       Expression body, Attributes attributes, IToken signatureEllipsis)

+                       Expression body, Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

       : base(tok, name, hasStaticKeyword, isProtected, typeArgs, formals,

-             req, reads, ens, body, attributes, signatureEllipsis) {

+             req, reads, ens, body, attributes, signatureEllipsis, clonedFrom) {

     }

   }

 

@@ -3338,8 +3386,8 @@ namespace Microsoft.Dafny {
                   [Captured] List<MaybeFreeExpression> ens,

                   [Captured] Specification<Expression> decreases,

                   [Captured] BlockStmt body,

-                  Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, isGhost, attributes) {

+                  Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, hasStaticKeyword, isGhost, attributes, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

@@ -3411,8 +3459,8 @@ namespace Microsoft.Dafny {
                  [Captured] List<MaybeFreeExpression> ens,

                  [Captured] Specification<Expression> decreases,

                  [Captured] BlockStmt body,

-                 Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {

+                 Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis, clonedFrom) {

     }

   }

 

@@ -3426,8 +3474,8 @@ namespace Microsoft.Dafny {
                   [Captured] List<MaybeFreeExpression> ens,

                   [Captured] Specification<Expression> decreases,

                   [Captured] BlockStmt body,

-                  Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, false, false, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis) {

+                  Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, false, false, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

@@ -3478,8 +3526,8 @@ namespace Microsoft.Dafny {
                          List<MaybeFreeExpression> ens,

                          Specification<Expression> decreases,

                          BlockStmt body,

-                         Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {

+                         Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom)

+      : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

@@ -3504,8 +3552,8 @@ namespace Microsoft.Dafny {
                           List<MaybeFreeExpression> ens,

                           Specification<Expression> decreases,

                           BlockStmt body,

-                          Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {

+                          Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, hasStaticKeyword, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

@@ -3530,8 +3578,8 @@ namespace Microsoft.Dafny {
                    List<MaybeFreeExpression> ens,

                    Specification<Expression> decreases,

                    BlockStmt body,

-                   Attributes attributes, IToken signatureEllipsis)

-      : base(tok, name, hasStaticKeyword, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {

+                   Attributes attributes, IToken signatureEllipsis, Declaration clonedFrom = null)

+      : base(tok, name, hasStaticKeyword, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis, clonedFrom) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

@@ -5319,7 +5367,9 @@ namespace Microsoft.Dafny {
     public static Expression CreateAdd(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

+      Contract.Requires(

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Add, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;  // resolve here

@@ -5361,8 +5411,12 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateSubtract(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

+      Contract.Requires(e0.Type != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

+      Contract.Requires(e1.Type != null);

+      Contract.Requires(

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Sub, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here

@@ -5375,7 +5429,8 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateIncrement(Expression e, int n) {

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.IsIntegerType);

+      Contract.Requires(e.Type != null);

+      Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuation.Int));

       Contract.Requires(0 <= n);

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

       if (n == 0) {

@@ -5390,7 +5445,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     public static Expression CreateDecrement(Expression e, int n) {

       Contract.Requires(e != null);

-      Contract.Requires(e.Type.IsIntegerType);

+      Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuation.Int));

       Contract.Requires(0 <= n);

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

       if (n == 0) {

@@ -5449,7 +5504,7 @@ namespace Microsoft.Dafny {
     public static Expression CreateLess(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires(e0.Type.IsIntegerType && e1.Type.IsIntegerType);

+      Contract.Requires(e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Lt, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Lt;  // resolve here

@@ -5463,7 +5518,9 @@ namespace Microsoft.Dafny {
     public static Expression CreateAtMost(Expression e0, Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      Contract.Requires((e0.Type.IsIntegerType && e1.Type.IsIntegerType) || (e0.Type.IsRealType && e1.Type.IsRealType));

+      Contract.Requires(

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Int) && e1.Type.IsNumericBased(Type.NumericPersuation.Int)) ||

+        (e0.Type.IsNumericBased(Type.NumericPersuation.Real) && e1.Type.IsNumericBased(Type.NumericPersuation.Real)));

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

       var s = new BinaryExpr(e0.tok, BinaryExpr.Opcode.Le, e0, e1);

       s.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 08e53d5c..59d0eb2c 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -1,392 +1,393 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics.Contracts;

-using Bpl = Microsoft.Boogie;

-

-namespace Microsoft.Dafny

-{

-  public class DafnyOptions : Bpl.CommandLineOptions

-  {

-    private ErrorReporter errorReporter;

-

-    public DafnyOptions(ErrorReporter errorReporter = null)

-      : base("Dafny", "Dafny program verifier") {

-        this.errorReporter = errorReporter;

-        SetZ3ExecutableName();

-    }

-

-    public override string VersionNumber {

-      get {

-        return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion

-#if ENABLE_IRONDAFNY

-          + "[IronDafny]"

-#endif

-          ;

-      }

-    }

-    public override string VersionSuffix {

-      get {

-        return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft.";

-      }

-    }

-

-    private static DafnyOptions clo;

-    public static DafnyOptions O {

-      get { return clo; }

-    }

-

-    public static void Install(DafnyOptions options) {

-      Contract.Requires(options != null);

-      clo = options;

-      Bpl.CommandLineOptions.Install(options);

-    }

-

-    public bool UnicodeOutput = false;

-    public bool DisallowSoundnessCheating = false;

-    public bool Dafnycc = false;

-    public int Induction = 3;

-    public int InductionHeuristic = 6;

-    public string DafnyPrelude = null;

-    public string DafnyPrintFile = null;

-    public enum PrintModes { Everything, NoIncludes, NoGhost };

-    public PrintModes PrintMode;

-    public bool DafnyVerify = true;

-    public string DafnyPrintResolvedFile = null;

-    public bool Compile = true;

-    public bool ForceCompile = false;

-    public bool RunAfterCompile = false;

-    public bool SpillTargetCode = false;

-    public bool DisallowIncludes = false;

-    public bool DisableNLarith = false;

-    public string AutoReqPrintFile = null;

-    public bool ignoreAutoReq = false;

-    public bool AllowGlobals = false;

-    public bool CountVerificationErrors = true;

-    public bool Optimize = false;

-    public bool AutoTriggers = false;

-    public bool PrintTooltips = false;

-    public bool PrintStats = false;

-    public bool PrintFunctionCallGraph = false;

-    public bool WarnShadowing = false;

-    public bool IronDafny = 

-#if ENABLE_IRONDAFNY 

-      true

-#else

-      false

-#endif

-    ;

-

-    protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

-      var args = ps.args;  // convenient synonym

-

-      switch (name) {

-        case "dprelude":

-          if (ps.ConfirmArgumentCount(1)) {

-            DafnyPrelude = args[ps.i];

-          }

-          return true;

-

-        case "dprint":

-          if (ps.ConfirmArgumentCount(1)) {

-            DafnyPrintFile = args[ps.i];

-          }

-          return true;

-

-        case "printMode":

-          if (ps.ConfirmArgumentCount(1)) {

-            if (args[ps.i].Equals("Everything")) {

-              PrintMode = PrintModes.Everything;

-            }

-            else if (args[ps.i].Equals("NoIncludes"))

-            {

-                PrintMode = PrintModes.NoIncludes;

-            }

-            else if (args[ps.i].Equals("NoGhost"))

-            {

-                PrintMode = PrintModes.NoGhost;

-            }

-            else

-            {

-                throw new Exception("Invalid value for printMode");

-            }

-          }

-          return true;

-

-        case "rprint":

-          if (ps.ConfirmArgumentCount(1)) {

-            DafnyPrintResolvedFile = args[ps.i];

-          }

-          return true;

-

-        case "compile": {

-            int compile = 0;

-            if (ps.GetNumericArgument(ref compile, 4)) {

-              // convert option to two booleans

-              Compile = compile != 0;

-              ForceCompile = compile == 2;

-              RunAfterCompile = compile == 3;

-            }

-            return true;

-          }

-

-        case "dafnyVerify":

-            {

-                int verify = 0;

-                if (ps.GetNumericArgument(ref verify, 2)) {

-                    DafnyVerify = verify != 0; // convert to boolean

-                }

-                return true;

-            }

-

-        case "spillTargetCode": {

-            int spill = 0;

-            if (ps.GetNumericArgument(ref spill, 2)) {

-              SpillTargetCode = spill != 0;  // convert to a boolean

-            }

-            return true;

-          }

-

-        case "dafnycc":

-          Dafnycc = true;

-          Induction = 0;

-          Compile = false;

-          UseAbstractInterpretation = false; // /noinfer

-          return true;

-

-        case "noCheating": {

-            int cheat = 0; // 0 is default, allows cheating

-            if (ps.GetNumericArgument(ref cheat, 2)) {

-              DisallowSoundnessCheating = cheat == 1;

-            }

-            return true;

-          }

-

-        case "induction":

-          ps.GetNumericArgument(ref Induction, 4);

-          return true;

-

-        case "inductionHeuristic":

-          ps.GetNumericArgument(ref InductionHeuristic, 7);

-          return true;

-

-        case "noIncludes":

-          DisallowIncludes = true;

-          return true;

-

-        case "noNLarith":

-          DisableNLarith = true;

-          this.AddZ3Option("NL_ARITH=false");

-          return true;

-

-        case "autoReqPrint":

-          if (ps.ConfirmArgumentCount(1)) {

-              AutoReqPrintFile = args[ps.i];

-          }

-          return true;

-

-        case "noAutoReq":

-          ignoreAutoReq = true;

-          return true;

-

-        case "allowGlobals":

-          AllowGlobals = true;

-          return true;

-        

-        case "stats":

-          PrintStats = true;

-          return true;

-

-        case "funcCallGraph":

-          PrintFunctionCallGraph = true;

-          return true;

-

-        case "warnShadowing":

-          WarnShadowing = true;

-          return true;

-

-        case "countVerificationErrors": {

-          int countErrors = 1; // defaults to reporting verification errors

-          if (ps.GetNumericArgument(ref countErrors, 2)) {

-            CountVerificationErrors = countErrors == 1;

-          }

-          return true;

-        }

-

-        case "printTooltips":

-          PrintTooltips = true;

-          return true;

-

-        case "autoTriggers": {

-            int autoTriggers = 0;

-            if (ps.GetNumericArgument(ref autoTriggers, 2)) {

-              AutoTriggers = autoTriggers == 1;

-            }

-            return true;

-          }

-

-        case "optimize": {

-            Optimize = true;

-            return true;

-        }

-

-        case "noIronDafny": {

-            IronDafny = false;

-            return true;

-        }

-

-        case "ironDafny": {

-            IronDafny = true;

-            return true;

-        }

-

-        default:

-          break;

-      }

-      // not a Dafny-specific option, so defer to superclass

-      return base.ParseOption(name, ps);

-    }

-

-    public override void ApplyDefaultOptions() {

-      base.ApplyDefaultOptions();

-

-      // expand macros in filenames, now that LogPrefix is fully determined

-      ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp);

-      ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp);

-    }

-

-    public override void AttributeUsage() {

-      // TODO: provide attribute help here

-    }

-

-    

-    /// <summary>

-    /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. 

-    /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.

-    /// For developers though (and people getting this from source), it's convenient to be able to run right away, 

-    /// so we vendor a Windows version.

-    /// </summary>

-    private void SetZ3ExecutableName() {

-      var platform = (int)System.Environment.OSVersion.Platform;

-

-      // http://www.mono-project.com/docs/faq/technical/

-      var isUnix = platform == 4 || platform == 128;

-      

-      var z3binName = isUnix ? "z3" : "z3.exe";

-      var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

-      var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");

-      var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);

-

-      if (!System.IO.File.Exists(z3BinPath) && !isUnix) {

-        // This is most likely a Windows user running from source without downloading z3 

-        // separately; this is ok, since we vendor z3.exe.

-        z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);

-      }

-      

-      if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {

-        var tok = new Bpl.Token(1, 1) { filename = "*** " };

-        errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", 

-          z3binName, z3BinDir, System.Environment.NewLine);

-      } else {

-        Z3ExecutablePath = z3BinPath;

-      }

-    }

-

-    public override void Usage() {

-      Console.WriteLine(@"  ---- Dafny options ---------------------------------------------------------

-

-  Multiple .dfy files supplied on the command line are concatenated into one

-  Dafny program.

-

-  /dprelude:<file>

-                choose Dafny prelude file

-  /dprint:<file>

-                print Dafny program after parsing it

-                (use - as <file> to print to console)

-  /printMode:<Everything|NoIncludes|NoGhost>

-                NoIncludes disables printing of {:verify false} methods incorporated via the

-                include mechanism, as well as datatypes and fields included from other files.

-                NoGhost disables printing of functions, ghost methods, and proof statements in

-                implementation methods.  It also disables anything NoIncludes disables.

-  /rprint:<file>

-                print Dafny program after resolving it

-                (use - as <file> to print to console)

-  /dafnyVerify:<n>

-                0 - stop after typechecking

-                1 - continue on to translation, verification, and compilation

-  /compile:<n>  0 - do not compile Dafny program

-                1 (default) - upon successful verification of the Dafny

-                    program, compile Dafny program to .NET assembly

-                    Program.exe (if the program has a Main method) or

-                    Program.dll (othewise), where Program.dfy is the name

-                    of the last .dfy file on the command line

-                2 - always attempt to compile Dafny program to C# program

-                    out.cs, regardless of verification outcome

-                3 - if there is a Main method and there are no verification

-                    errors, compiles program in memory (i.e., does not write

-                    an output file) and runs it

-  /spillTargetCode:<n>

-                0 (default) - don't write the compiled Dafny program (but

-                    still compile it, if /compile indicates to do so)

-                1 - write the compiled Dafny program as a .cs file

-  /dafnycc      Disable features not supported by DafnyCC

-  /noCheating:<n>

-                0 (default) - allow assume statements and free invariants

-                1 - treat all assumptions as asserts, and drop free.

-  /induction:<n>

-                0 - never do induction, not even when attributes request it

-                1 - only apply induction when attributes request it

-                2 - apply induction as requested (by attributes) and also

-                    for heuristically chosen quantifiers

-                3 (default) - apply induction as requested, and for

-                    heuristically chosen quantifiers and lemmas

-  /inductionHeuristic:<n>

-                0 - least discriminating induction heuristic (that is, lean

-                    toward applying induction more often)

-                1,2,3,4,5 - levels in between, ordered as follows as far as

-                    how discriminating they are:  0 < 1 < 2 < (3,4) < 5 < 6

-                6 (default) - most discriminating

-  /noIncludes   Ignore include directives

-  /noNLarith    Reduce Z3's knowledge of non-linear arithmetic (*,/,%).

-                Results in more manual work, but also produces more predictable behavior.

-  /autoReqPrint:<file>

-                Print out requirements that were automatically generated by autoReq.

-  /noAutoReq    Ignore autoReq attributes

-  /allowGlobals Allow the implicit class '_default' to contain fields, instance functions,

-                and instance methods.  These class members are declared at the module scope,

-                outside of explicit classes.  This command-line option is provided to simplify

-                a transition from the behavior in the language prior to version 1.9.3, from

-                which point onward all functions and methods declared at the module scope are

-                implicitly static and fields declarations are not allowed at the module scope.

-  /countVerificationErrors:<n>

-                0 - If preprocessing succeeds, set exit code to 0 regardless of the number

-                    of verification errors.

-                1 (default) - If preprocessing succeeds, set exit code to the number of

-                              verification errors.

-  /autoTriggers:<n>

-                0 (default) - Do not generate {:trigger} annotations for user-level quantifiers.

-                1 - Add a {:trigger} to each user-level quantifier. Existing

-                              annotations are preserved.

-  /optimize     Produce optimized C# code, meaning:

-                  - selects optimized C# prelude by passing 

-                    /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires 

-                    System.Collections.Immutable.dll in the source directory to successfully 

-                    compile).

-                  - passes /optimize flag to csc.exe.

-  /stats        Print interesting statistics about the Dafny files supplied.

-  /funcCallGraph Print out the function call graph.  Format is: func,mod=callee*

-  /warnShadowing  Emits a warning if the name of a declared variable caused another variable

-                to be shadowed

-  /ironDafny    Enable experimental features needed to support Ironclad/Ironfleet. Use of

-                these features may cause your code to become incompatible with future

-                releases of Dafny.

-  /noIronDafny  Disable Ironclad/Ironfleet features, if enabled by default.

-  /printTooltips    

-                Dump additional positional information (displayed as mouse-over tooltips by 

-                the VS plugin) to stdout as 'Info' messages.

-");

-      base.Usage();  // also print the Boogie options

-    }

-  }

-}

+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using Bpl = Microsoft.Boogie;
+
+namespace Microsoft.Dafny
+{
+  public class DafnyOptions : Bpl.CommandLineOptions
+  {
+    private ErrorReporter errorReporter;
+
+    public DafnyOptions(ErrorReporter errorReporter = null)
+      : base("Dafny", "Dafny program verifier") {
+        this.errorReporter = errorReporter;
+        SetZ3ExecutableName();
+    }
+
+    public override string VersionNumber {
+      get {
+        return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion
+#if ENABLE_IRONDAFNY
+          + "[IronDafny]"
+#endif
+          ;
+      }
+    }
+    public override string VersionSuffix {
+      get {
+        return " version " + VersionNumber + ", Copyright (c) 2003-2015, Microsoft.";
+      }
+    }
+
+    private static DafnyOptions clo;
+    public static DafnyOptions O {
+      get { return clo; }
+    }
+
+    public static void Install(DafnyOptions options) {
+      Contract.Requires(options != null);
+      clo = options;
+      Bpl.CommandLineOptions.Install(options);
+    }
+
+    public bool UnicodeOutput = false;
+    public bool DisallowSoundnessCheating = false;
+    public bool Dafnycc = false;
+    public int Induction = 3;
+    public int InductionHeuristic = 6;
+    public string DafnyPrelude = null;
+    public string DafnyPrintFile = null;
+    public enum PrintModes { Everything, NoIncludes, NoGhost };
+    public PrintModes PrintMode = PrintModes.Everything;  // Default to printing everything
+    public bool DafnyVerify = true;
+    public string DafnyPrintResolvedFile = null;
+    public bool Compile = true;
+    public bool ForceCompile = false;
+    public bool RunAfterCompile = false;
+    public bool SpillTargetCode = false;
+    public bool DisallowIncludes = false;
+    public bool DisableNLarith = false;
+    public string AutoReqPrintFile = null;
+    public bool ignoreAutoReq = false;
+    public bool AllowGlobals = false;
+    public bool CountVerificationErrors = true;
+    public bool Optimize = false;
+    public bool AutoTriggers = false;
+    public bool PrintTooltips = false;
+    public bool PrintStats = false;
+    public bool PrintFunctionCallGraph = false;
+    public bool WarnShadowing = false;
+    public bool IronDafny = 
+#if ENABLE_IRONDAFNY 
+      true
+#else
+      false
+#endif
+    ;
+
+    protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
+      var args = ps.args;  // convenient synonym
+
+      switch (name) {
+        case "dprelude":
+          if (ps.ConfirmArgumentCount(1)) {
+            DafnyPrelude = args[ps.i];
+          }
+          return true;
+
+        case "dprint":
+          if (ps.ConfirmArgumentCount(1)) {
+            DafnyPrintFile = args[ps.i];
+          }
+          return true;
+
+        case "printMode":
+          if (ps.ConfirmArgumentCount(1)) {
+            if (args[ps.i].Equals("Everything")) {
+              PrintMode = PrintModes.Everything;
+            }
+            else if (args[ps.i].Equals("NoIncludes"))
+            {
+                PrintMode = PrintModes.NoIncludes;
+            }
+            else if (args[ps.i].Equals("NoGhost"))
+            {
+                PrintMode = PrintModes.NoGhost;
+            }
+            else
+            {
+                throw new Exception("Invalid value for printMode");
+            }
+          }
+          return true;
+
+        case "rprint":
+          if (ps.ConfirmArgumentCount(1)) {
+            DafnyPrintResolvedFile = args[ps.i];
+          }
+          return true;
+
+        case "compile": {
+            int compile = 0;
+            if (ps.GetNumericArgument(ref compile, 4)) {
+              // convert option to two booleans
+              Compile = compile != 0;
+              ForceCompile = compile == 2;
+              RunAfterCompile = compile == 3;
+            }
+            return true;
+          }
+
+        case "dafnyVerify":
+            {
+                int verify = 0;
+                if (ps.GetNumericArgument(ref verify, 2)) {
+                    DafnyVerify = verify != 0; // convert to boolean
+                }
+                return true;
+            }
+
+        case "spillTargetCode": {
+            int spill = 0;
+            if (ps.GetNumericArgument(ref spill, 2)) {
+              SpillTargetCode = spill != 0;  // convert to a boolean
+            }
+            return true;
+          }
+
+        case "dafnycc":
+          Dafnycc = true;
+          Induction = 0;
+          Compile = false;
+          UseAbstractInterpretation = false; // /noinfer
+          return true;
+
+        case "noCheating": {
+            int cheat = 0; // 0 is default, allows cheating
+            if (ps.GetNumericArgument(ref cheat, 2)) {
+              DisallowSoundnessCheating = cheat == 1;
+            }
+            return true;
+          }
+
+        case "induction":
+          ps.GetNumericArgument(ref Induction, 4);
+          return true;
+
+        case "inductionHeuristic":
+          ps.GetNumericArgument(ref InductionHeuristic, 7);
+          return true;
+
+        case "noIncludes":
+          DisallowIncludes = true;
+          return true;
+
+        case "noNLarith":
+          DisableNLarith = true;
+          this.AddZ3Option("smt.arith.nl=false");
+          return true;
+
+        case "autoReqPrint":
+          if (ps.ConfirmArgumentCount(1)) {
+              AutoReqPrintFile = args[ps.i];
+          }
+          return true;
+
+        case "noAutoReq":
+          ignoreAutoReq = true;
+          return true;
+
+        case "allowGlobals":
+          AllowGlobals = true;
+          return true;
+        
+        case "stats":
+          PrintStats = true;
+          return true;
+
+        case "funcCallGraph":
+          PrintFunctionCallGraph = true;
+          return true;
+
+        case "warnShadowing":
+          WarnShadowing = true;
+          return true;
+
+        case "countVerificationErrors": {
+          int countErrors = 1; // defaults to reporting verification errors
+          if (ps.GetNumericArgument(ref countErrors, 2)) {
+            CountVerificationErrors = countErrors == 1;
+          }
+          return true;
+        }
+
+        case "printTooltips":
+          PrintTooltips = true;
+          return true;
+
+        case "autoTriggers": {
+            int autoTriggers = 0;
+            if (ps.GetNumericArgument(ref autoTriggers, 2)) {
+              AutoTriggers = autoTriggers == 1;
+            }
+            return true;
+          }
+
+        case "optimize": {
+            Optimize = true;
+            return true;
+        }
+
+        case "noIronDafny": {
+            IronDafny = false;
+            return true;
+        }
+
+        case "ironDafny": {
+            IronDafny = true;
+            return true;
+        }
+
+        default:
+          break;
+      }
+      // not a Dafny-specific option, so defer to superclass
+      return base.ParseOption(name, ps);
+    }
+
+    public override void ApplyDefaultOptions() {
+      base.ApplyDefaultOptions();
+
+      // expand macros in filenames, now that LogPrefix is fully determined
+      ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp);
+      ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp);
+    }
+
+    public override void AttributeUsage() {
+      // TODO: provide attribute help here
+    }
+
+    
+    /// <summary>
+    /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. 
+    /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script.
+    /// For developers though (and people getting this from source), it's convenient to be able to run right away, 
+    /// so we vendor a Windows version.
+    /// </summary>
+    private void SetZ3ExecutableName() {
+      var platform = (int)System.Environment.OSVersion.Platform;
+
+      // http://www.mono-project.com/docs/faq/technical/
+      var isUnix = platform == 4 || platform == 128;
+      
+      var z3binName = isUnix ? "z3" : "z3.exe";
+      var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
+      var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin");
+      var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName);
+
+      if (!System.IO.File.Exists(z3BinPath) && !isUnix) {
+        // This is most likely a Windows user running from source without downloading z3 
+        // separately; this is ok, since we vendor z3.exe.
+        z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName);
+      }
+      
+      if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) {
+        var tok = new Bpl.Token(1, 1) { filename = "*** " };
+        errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", 
+          z3binName, z3BinDir, System.Environment.NewLine);
+      } else {
+        Z3ExecutablePath = z3BinPath;
+      }
+    }
+
+    public override void Usage() {
+      Console.WriteLine(@"  ---- Dafny options ---------------------------------------------------------
+
+  Multiple .dfy files supplied on the command line are concatenated into one
+  Dafny program.
+
+  /dprelude:<file>
+                choose Dafny prelude file
+  /dprint:<file>
+                print Dafny program after parsing it
+                (use - as <file> to print to console)
+  /printMode:<Everything|NoIncludes|NoGhost>
+                Everything is the default.
+                NoIncludes disables printing of {:verify false} methods incorporated via the
+                include mechanism, as well as datatypes and fields included from other files.
+                NoGhost disables printing of functions, ghost methods, and proof statements in
+                implementation methods.  It also disables anything NoIncludes disables.
+  /rprint:<file>
+                print Dafny program after resolving it
+                (use - as <file> to print to console)
+  /dafnyVerify:<n>
+                0 - stop after typechecking
+                1 - continue on to translation, verification, and compilation
+  /compile:<n>  0 - do not compile Dafny program
+                1 (default) - upon successful verification of the Dafny
+                    program, compile Dafny program to .NET assembly
+                    Program.exe (if the program has a Main method) or
+                    Program.dll (othewise), where Program.dfy is the name
+                    of the last .dfy file on the command line
+                2 - always attempt to compile Dafny program to C# program
+                    out.cs, regardless of verification outcome
+                3 - if there is a Main method and there are no verification
+                    errors, compiles program in memory (i.e., does not write
+                    an output file) and runs it
+  /spillTargetCode:<n>
+                0 (default) - don't write the compiled Dafny program (but
+                    still compile it, if /compile indicates to do so)
+                1 - write the compiled Dafny program as a .cs file
+  /dafnycc      Disable features not supported by DafnyCC
+  /noCheating:<n>
+                0 (default) - allow assume statements and free invariants
+                1 - treat all assumptions as asserts, and drop free.
+  /induction:<n>
+                0 - never do induction, not even when attributes request it
+                1 - only apply induction when attributes request it
+                2 - apply induction as requested (by attributes) and also
+                    for heuristically chosen quantifiers
+                3 (default) - apply induction as requested, and for
+                    heuristically chosen quantifiers and lemmas
+  /inductionHeuristic:<n>
+                0 - least discriminating induction heuristic (that is, lean
+                    toward applying induction more often)
+                1,2,3,4,5 - levels in between, ordered as follows as far as
+                    how discriminating they are:  0 < 1 < 2 < (3,4) < 5 < 6
+                6 (default) - most discriminating
+  /noIncludes   Ignore include directives
+  /noNLarith    Reduce Z3's knowledge of non-linear arithmetic (*,/,%).
+                Results in more manual work, but also produces more predictable behavior.
+  /autoReqPrint:<file>
+                Print out requirements that were automatically generated by autoReq.
+  /noAutoReq    Ignore autoReq attributes
+  /allowGlobals Allow the implicit class '_default' to contain fields, instance functions,
+                and instance methods.  These class members are declared at the module scope,
+                outside of explicit classes.  This command-line option is provided to simplify
+                a transition from the behavior in the language prior to version 1.9.3, from
+                which point onward all functions and methods declared at the module scope are
+                implicitly static and fields declarations are not allowed at the module scope.
+  /countVerificationErrors:<n>
+                0 - If preprocessing succeeds, set exit code to 0 regardless of the number
+                    of verification errors.
+                1 (default) - If preprocessing succeeds, set exit code to the number of
+                              verification errors.
+  /autoTriggers:<n>
+                0 (default) - Do not generate {:trigger} annotations for user-level quantifiers.
+                1 - Add a {:trigger} to each user-level quantifier. Existing
+                              annotations are preserved.
+  /optimize     Produce optimized C# code, meaning:
+                  - selects optimized C# prelude by passing 
+                    /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires 
+                    System.Collections.Immutable.dll in the source directory to successfully 
+                    compile).
+                  - passes /optimize flag to csc.exe.
+  /stats        Print interesting statistics about the Dafny files supplied.
+  /funcCallGraph Print out the function call graph.  Format is: func,mod=callee*
+  /warnShadowing  Emits a warning if the name of a declared variable caused another variable
+                to be shadowed
+  /ironDafny    Enable experimental features needed to support Ironclad/Ironfleet. Use of
+                these features may cause your code to become incompatible with future
+                releases of Dafny.
+  /noIronDafny  Disable Ironclad/Ironfleet features, if enabled by default.
+  /printTooltips    
+                Dump additional positional information (displayed as mouse-over tooltips by 
+                the VS plugin) to stdout as 'Info' messages.
+");
+      base.Usage();  // also print the Boogie options
+    }
+  }
+}
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 13a1e53e..501a624c 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -41,7 +41,7 @@
     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

     <OutputPath>bin\Debug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DefineConstants>TRACE;DEBUG;NO_ENABLE_IRONDAFNY</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

     <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

@@ -83,7 +83,7 @@
     <DebugType>pdbonly</DebugType>

     <Optimize>true</Optimize>

     <OutputPath>bin\Release\</OutputPath>

-    <DefineConstants>TRACE</DefineConstants>

+    <DefineConstants>TRACE;NO_ENABLE_IRONDAFNY</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

@@ -91,7 +91,7 @@
   <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

     <DebugSymbols>true</DebugSymbols>

     <OutputPath>bin\Checked\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DefineConstants>TRACE;DEBUG;NO_ENABLE_IRONDAFNY</DefineConstants>

     <DebugType>full</DebugType>

     <PlatformTarget>AnyCPU</PlatformTarget>

     <ErrorReport>prompt</ErrorReport>

@@ -199,4 +199,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index ce8b54bb..e242c8bb 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1,2010 +1,2010 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.IO;

-using System.Collections.Generic;

-using System.Diagnostics.Contracts;

-using System.Numerics;

-using System.Linq;

-using Bpl = Microsoft.Boogie;

-

-namespace Microsoft.Dafny {

-  public class Printer {

-    TextWriter wr;

-    DafnyOptions.PrintModes printMode;

-

-    [ContractInvariantMethod]

-    void ObjectInvariant()

-    {

-      Contract.Invariant(wr!=null);

-    }

-

-    public Printer(TextWriter wr, DafnyOptions.PrintModes printMode = DafnyOptions.PrintModes.Everything) {

-      Contract.Requires(wr != null);

-      this.wr = wr;

-      this.printMode = printMode;

-    }

-

-    public static string ExprToString(Expression expr)

-    {

-      Contract.Requires(expr != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintExpression(expr, false);

-        return wr.ToString();

-      }

-    }

-

-    public static string GuardToString(Expression expr) {

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintGuard(expr);

-        return wr.ToString();

-      }

-    }

-

-    public static string ExtendedExprToString(Expression expr) {

-      Contract.Requires(expr != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintExtendedExpr(expr, 0, true, false);

-        return wr.ToString();

-      }

-    }

-

-    public static string FrameExprListToString(List<FrameExpression> fexprs) {

-      Contract.Requires(fexprs != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintFrameExpressionList(fexprs);

-        return wr.ToString();

-      }

-    }

-

-    public static string StatementToString(Statement stmt) {

-      Contract.Requires(stmt != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintStatement(stmt, 0);

-        return ToStringWithoutNewline(wr);

-      }

-    }

-

-    public static string IteratorClassToString(IteratorDecl iter) {

-      Contract.Requires(iter != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintIteratorClass(iter, 0, null);

-        return ToStringWithoutNewline(wr);

-      }

-    }

-

-    public static string IteratorSignatureToString(IteratorDecl iter) {

-      Contract.Requires(iter != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintIteratorSignature(iter, 0);

-        return ToStringWithoutNewline(wr);

-      }

-    }

-

-    public static string FunctionSignatureToString(Function f) {

-      Contract.Requires(f != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintFunction(f, 0, true);

-        return ToStringWithoutNewline(wr);

-      }

-    }

-

-    public static string MethodSignatureToString(Method m) {

-      Contract.Requires(m != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintMethod(m, 0, true);

-        return ToStringWithoutNewline(wr);

-      }

-    }

-

-    public static string OneAttributeToString(Attributes a, string nameSubstitution = null) {

-      Contract.Requires(a != null);

-      using (var wr = new System.IO.StringWriter()) {

-        var pr = new Printer(wr);

-        pr.PrintOneAttribute(a, nameSubstitution);

-        return ToStringWithoutNewline(wr);

-      }

-    }

-

-    public static string ToStringWithoutNewline(System.IO.StringWriter wr) {

-      Contract.Requires(wr != null);

-      var sb = wr.GetStringBuilder();

-      var len = sb.Length;

-      while (len > 0 && (sb[len - 1] == '\n' || sb[len - 1] == '\r')) {

-        len--;

-      }

-      return sb.ToString(0, len);

-    }

-

-    public void PrintProgram(Program prog) {

-      Contract.Requires(prog != null);

-      if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) {

-        wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Version);

-        wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);

-      }

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

-      if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

-        wr.WriteLine();

-        wr.WriteLine("/*");

-        PrintModuleDefinition(prog.BuiltIns.SystemModule, 0, Path.GetFullPath(DafnyOptions.O.DafnyPrintResolvedFile));

-        wr.WriteLine("*/");

-      }

-      wr.WriteLine();

-      PrintCallGraph(prog.DefaultModuleDef, 0);

-      PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, Path.GetFullPath(prog.FullName));

-      wr.Flush();

-    }

-

-    public void PrintCallGraph(ModuleDefinition module, int indent) {

-      Contract.Requires(module != null);

-      Contract.Requires(0 <= indent);

-      if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

-        // print call graph

-        Indent(indent); wr.WriteLine("/* CALL GRAPH for module {0}:", module.Name);

-        var SCCs = module.CallGraph.TopologicallySortedComponents();

-        SCCs.Reverse();

-        foreach (var clbl in SCCs) {

-          Indent(indent); wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativeId(clbl));

-          var r = module.CallGraph.GetSCC(clbl);

-          foreach (var m in r) {

-            Indent(indent); wr.WriteLine(" *   {0}", m.NameRelativeToModule);

-          }

-        }

-        Indent(indent); wr.WriteLine(" */");

-      }

-    }

-

-    public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, string fileBeingPrinted) {

-      Contract.Requires(decls!= null);

-      int i = 0;

-      foreach (TopLevelDecl d in decls) {

-        Contract.Assert(d != null);

-        if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }

-        if (d is OpaqueTypeDecl) {

-          var at = (OpaqueTypeDecl)d;

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

-          Indent(indent);

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

-          wr.Write(EqualitySupportSuffix(at.EqualitySupport));

-          wr.WriteLine();

-        } else if (d is NewtypeDecl) {

-          var dd = (NewtypeDecl)d;

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

-          Indent(indent);

-          PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List<TypeParameter>());

-          wr.Write(" = ");

-          if (dd.Var == null) {

-            PrintType(dd.BaseType);

-          } else {

-            wr.Write(dd.Var.DisplayName);

-            if (!(dd.Var.Type is TypeProxy) || DafnyOptions.O.DafnyPrintResolvedFile != null) {

-              wr.Write(": ");

-              PrintType(dd.BaseType);

-            }

-            wr.Write(" | ");

-            PrintExpression(dd.Constraint, true);

-          }

-          wr.WriteLine();

-        } else if (d is TypeSynonymDecl) {

-          var syn = (TypeSynonymDecl)d;

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

-          Indent(indent);

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

-          wr.Write(" = ");

-          PrintType(syn.Rhs);

-          wr.WriteLine();

-        } else if (d is DatatypeDecl) {

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

-          PrintDatatype((DatatypeDecl)d, indent);

-        } else if (d is IteratorDecl) {

-          var iter = (IteratorDecl)d;

-          PrintIteratorSignature(iter, indent);

-

-          if (iter.Body != null) {

-            Indent(indent);

-            PrintStatement(iter.Body, indent);

-            wr.WriteLine();

-          }

-

-          if (DafnyOptions.O.DafnyPrintResolvedFile != null) {

-            // also print the members that were created as part of the interpretation of the iterator

-            Contract.Assert(iter.Members.Count != 0);  // filled in during resolution

-            wr.WriteLine("/*---------- iterator members ----------");

-            PrintIteratorClass(iter, indent, fileBeingPrinted);

-            wr.WriteLine("---------- iterator members ----------*/");

-          }

-

-        } else if (d is ClassDecl) {

-          ClassDecl cl = (ClassDecl)d;

-          if (!cl.IsDefaultClass) {

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

-            PrintClass(cl, indent, fileBeingPrinted);

-          } else if (cl.Members.Count == 0) {

-            // print nothing

-          } else {

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

-            PrintMembers(cl.Members, indent, fileBeingPrinted);

-          }

-

-        } else if (d is ModuleDecl) {

-          wr.WriteLine();

-          Indent(indent);

-          if (d is LiteralModuleDecl) {

-            ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef;

-            PrintModuleDefinition(module, indent, fileBeingPrinted);

-          } else if (d is AliasModuleDecl) {

-            wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened");

-            wr.Write(" {0} ", ((AliasModuleDecl)d).Name);

-            wr.WriteLine("= {0}", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val));

-          } else if (d is ModuleFacadeDecl) {

-            wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened");

-            wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name);

-            wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val));

-          }

-

-        } else {

-          Contract.Assert(false);  // unexpected TopLevelDecl

-        }

-      }

-    }

-

-    void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) {

-      Contract.Requires(module != null);

-      Contract.Requires(0 <= indent);

-      if (module.IsAbstract) {

-        wr.Write("abstract ");

-      }

-      wr.Write("module");

-      PrintAttributes(module.Attributes);

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

-      if (module.RefinementBaseName != null) {

-        wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val));

-      }

-      if (module.TopLevelDecls.Count == 0) {

-        wr.WriteLine("{ }");

-      } else {

-        wr.WriteLine("{");

-        PrintCallGraph(module, indent + IndentAmount);

-        PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted);

-        Indent(indent);

-        wr.WriteLine("}");

-      }

-    }

-

-    void PrintIteratorSignature(IteratorDecl iter, int indent) {

-      Indent(indent);

-      PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs);

-      if (iter.SignatureIsOmitted) {

-        wr.WriteLine(" ...");

-      } else {

-        PrintFormals(iter.Ins);

-        if (iter.Outs.Count != 0) {

-          if (iter.Ins.Count + iter.Outs.Count <= 3) {

-            wr.Write(" yields ");

-          } else {

-            wr.WriteLine();

-            Indent(indent + 2 * IndentAmount);

-            wr.Write("yields ");

-          }

-          PrintFormals(iter.Outs);

-        }

-        wr.WriteLine();

-      }

-

-      int ind = indent + IndentAmount;

-      PrintSpec("requires", iter.Requires, ind);

-      if (iter.Reads.Expressions != null) {

-        PrintFrameSpecLine("reads", iter.Reads.Expressions, ind, iter.Reads.HasAttributes() ? iter.Reads.Attributes : null);

-      }

-      if (iter.Modifies.Expressions != null) {

-        PrintFrameSpecLine("modifies", iter.Modifies.Expressions, ind, iter.Modifies.HasAttributes() ? iter.Modifies.Attributes : null);

-      }

-      PrintSpec("yield requires", iter.YieldRequires, ind);

-      PrintSpec("yield ensures", iter.YieldEnsures, ind);

-      PrintSpec("ensures", iter.Ensures, ind);

-      PrintDecreasesSpec(iter.Decreases, ind);

-    }

-

-    private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) {

-      PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);

-      wr.WriteLine(" {");

-      PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted);

-      Indent(indent); wr.WriteLine("}");

-    }

-

-    public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) {

-      Contract.Requires(c != null);

-      Indent(indent);

-      PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);

-      string sep = " extends ";

-      foreach (var trait in c.TraitsTyp) {

-        wr.Write(sep);

-        PrintType(trait);

-        sep = ", ";

-      }

-      if (c.Members.Count == 0) {

-        wr.WriteLine(" { }");

-      } else {

-        wr.WriteLine(" {");

-        PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted);

-        Indent(indent);

-        wr.WriteLine("}");

-      }

-    }

-

-    public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted)

-    {

-      Contract.Requires(members != null);

-

-      int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

-      foreach (MemberDecl m in members) {

-        if (PrintModeSkipGeneral(m.tok, fileBeingPrinted)) { continue; }

-        if (m is Method) {

-          if (state != 0) { wr.WriteLine(); }

-          PrintMethod((Method)m, indent, false);

-          var com = m as FixpointLemma;

-          if (com != null && com.PrefixLemma != null) {

-            Indent(indent); wr.WriteLine("/***");

-            PrintMethod(com.PrefixLemma, indent, false);

-            Indent(indent); wr.WriteLine("***/");

-          }

-          state = 2;

-        } else if (m is Field) {

-          if (state == 2) { wr.WriteLine(); }

-          PrintField((Field)m, indent);

-          state = 1;

-        } else if (m is Function) {

-          if (state != 0) { wr.WriteLine(); }

-          PrintFunction((Function)m, indent, false);

-          var fixp = m as FixpointPredicate;

-          if (fixp != null && fixp.PrefixPredicate != null) {

-            Indent(indent); wr.WriteLine("/***");

-            PrintFunction(fixp.PrefixPredicate, indent, false);

-            Indent(indent); wr.WriteLine("***/");

-          }

-          state = 2;

-        } else {

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

-        }

-      }

-    }

-

-    /// <summary>

-    /// Prints no space before "kind", but does print a space before "attrs" and "name".

-    /// </summary>

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

-      Contract.Requires(kind != null);

-      Contract.Requires(name != null);

-      Contract.Requires(typeArgs != null);

-      if (kind.Length != 0) {

-        wr.Write(kind);

-      }

-

-      PrintAttributes(attrs);

-

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

-      PrintTypeParams(typeArgs);

-    }

-

-    private void PrintTypeParams(List<TypeParameter> typeArgs) {

-      Contract.Requires(typeArgs != null);

-      if (typeArgs.Count != 0) {

-        wr.Write("<" +

-                 Util.Comma(", ", typeArgs,

-                   tp => tp.Name + EqualitySupportSuffix(tp.EqualitySupport))

-                 + ">");

-      }

-    }

-

-    private void PrintTypeInstantiation(List<Type> typeArgs) {

-      Contract.Requires(typeArgs == null || typeArgs.Count != 0);

-      if (typeArgs != null) {

-        wr.Write("<{0}>", Util.Comma(",", typeArgs, ty => ty.ToString()));

-      }

-    }

-

-    public void PrintDatatype(DatatypeDecl dt, int indent) {

-      Contract.Requires(dt != null);

-      Indent(indent);

-      PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);

-      wr.Write(" =");

-      string sep = "";

-      foreach (DatatypeCtor ctor in dt.Ctors) {

-        wr.Write(sep);

-        PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List<TypeParameter>());

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

-          PrintFormals(ctor.Formals);

-        }

-        sep = " |";

-      }

-      wr.WriteLine();

-    }

-

-    /// <summary>

-    /// Prints a space before each attribute.

-    /// </summary>

-    public void PrintAttributes(Attributes a) {

-      if (a != null) {

-        PrintAttributes(a.Prev);

-        wr.Write(" ");

-        PrintOneAttribute(a);

-      }

-    }

-    public void PrintOneAttribute(Attributes a, string nameSubstitution = null) {

-      Contract.Requires(a != null);

-      var name = nameSubstitution ?? a.Name;

-      var usAttribute = name.StartsWith("_");

-      wr.Write("{1}{{:{0}", name, usAttribute ? "/*" : "");

-      if (a.Args != null) {

-        PrintAttributeArgs(a.Args, false);

-      }

-      wr.Write("}}{0}", usAttribute ? "*/" : "");

-    }

-

-    public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {

-      Contract.Requires(args != null);

-      string prefix = " ";

-      foreach (var arg in args) {

-        Contract.Assert(arg != null);

-        wr.Write(prefix);

-        prefix = ", ";

-        PrintExpression(arg, isFollowedBySemicolon);

-      }

-    }

-

-    public void PrintField(Field field, int indent) {

-      Contract.Requires(field != null);

-      Indent(indent);

-      if (field.IsGhost) {

-        wr.Write("ghost ");

-      }

-      wr.Write("var");

-      PrintAttributes(field.Attributes);

-      wr.Write(" {0}: ", field.Name);

-      PrintType(field.Type);

-      if (field.IsUserMutable) {

-        // nothing more to say

-      } else if (field.IsMutable) {

-        wr.Write("  // non-assignable");

-      } else {

-        wr.Write("  // immutable");

-      }

-      wr.WriteLine();

-    }

-

-    public void PrintFunction(Function f, int indent, bool printSignatureOnly) {

-      Contract.Requires(f != null);

-

-      if (PrintModeSkipFunctionOrMethod(f.IsGhost, f.Attributes, f.Name)) { return; }

-      var isPredicate = f is Predicate || f is PrefixPredicate;

-      Indent(indent);

-      string k = isPredicate ? "predicate" : f is InductivePredicate ? "inductive predicate" : f is CoPredicate ? "copredicate" : "function";

-      if (f.IsProtected) { k = "protected " + k; }

-      if (f.HasStaticKeyword) { k = "static " + k; }

-      if (!f.IsGhost) { k += " method"; }

-      PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);

-      if (f.SignatureIsOmitted) {

-        wr.WriteLine(" ...");

-      } else {

-        PrintFormals(f.Formals, f.Name);

-        if (!isPredicate) {

-          wr.Write(": ");

-          PrintType(f.ResultType);

-        }

-        wr.WriteLine();

-      }

-

-      int ind = indent + IndentAmount;

-      PrintSpec("requires", f.Req, ind);

-      PrintFrameSpecLine("reads", f.Reads, ind, null);

-      PrintSpec("ensures", f.Ens, ind);

-      PrintDecreasesSpec(f.Decreases, ind);

-      if (f.Body != null && !printSignatureOnly) {

-        Indent(indent);

-        wr.WriteLine("{");

-        PrintExtendedExpr(f.Body, ind, true, false);

-        Indent(indent);

-        wr.WriteLine("}");

-      }

-    }

-

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

-

-    const int IndentAmount = 2; // The amount of indent for each new scope

-    const string BunchaSpaces = "                                ";

-    void Indent(int amount)

-    {

-      Contract.Requires(0 <= amount);

-

-      while (0 < amount) {

-        wr.Write(BunchaSpaces.Substring(0, amount));

-        amount -= BunchaSpaces.Length;

-      }

-    }

-

-    private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name)

-    {

-      if (printMode == DafnyOptions.PrintModes.NoGhost && IsGhost)

-          { return true; }

-      if (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)

-      {

-          bool verify = true;

-          if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify)

-          { return true; }

-          if (name.Contains("INTERNAL") || name.StartsWith("reveal_"))

-          { return true; }

-      }

-      return false;

-    }

-

-    private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted)

-    {

-        return (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)

-               && (tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted);

-    }

-

-    public void PrintMethod(Method method, int indent, bool printSignatureOnly) {

-      Contract.Requires(method != null);

-

-      if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; }

-      Indent(indent);

-      string k = method is Constructor ? "constructor" :

-        method is InductiveLemma ? "inductive lemma" :

-        method is CoLemma ? "colemma" :

-        method is Lemma ? "lemma" :

-        "method";

-      if (method.HasStaticKeyword) { k = "static " + k; }

-      if (method.IsGhost && !(method is Lemma) && !(method is FixpointLemma)) { k = "ghost " + k; }

-      string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;

-      PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs);

-      if (method.SignatureIsOmitted) {

-        wr.WriteLine(" ...");

-      } else {

-        PrintFormals(method.Ins, method.Name);

-        if (method.Outs.Count != 0) {

-          if (method.Ins.Count + method.Outs.Count <= 3) {

-            wr.Write(" returns ");

-          } else {

-            wr.WriteLine();

-            Indent(indent + 2 * IndentAmount);

-            wr.Write("returns ");

-          }

-          PrintFormals(method.Outs);

-        }

-        wr.WriteLine();

-      }

-

-      int ind = indent + IndentAmount;

-      PrintSpec("requires", method.Req, ind);

-      if (method.Mod.Expressions != null)

-      {

-        PrintFrameSpecLine("modifies", method.Mod.Expressions, ind, method.Mod.HasAttributes() ? method.Mod.Attributes : null);

-      }

-      PrintSpec("ensures", method.Ens, ind);

-      PrintDecreasesSpec(method.Decreases, ind);

-

-      if (method.Body != null && !printSignatureOnly) {

-        Indent(indent);

-        PrintStatement(method.Body, indent);

-        wr.WriteLine();

-      }

-    }

-

-    internal void PrintFormals(List<Formal> ff, string name = null) {

-      Contract.Requires(ff != null);

-      if (name != null && name.EndsWith("#")) {

-        wr.Write("[");

-        PrintFormal(ff[0]);

-        wr.Write("]");

-        ff = new List<Formal>(ff.Skip(1));

-      }

-      wr.Write("(");

-      string sep = "";

-      foreach (Formal f in ff) {

-        Contract.Assert(f != null);

-        wr.Write(sep);

-        sep = ", ";

-        PrintFormal(f);

-      }

-      wr.Write(")");

-    }

-

-    void PrintFormal(Formal f) {

-      Contract.Requires(f != null);

-      if (f.IsGhost) {

-        wr.Write("ghost ");

-      }

-      if (f.HasName) {

-        wr.Write("{0}: ", f.DisplayName);

-      }

-      PrintType(f.Type);

-    }

-

-    internal void PrintSpec(string kind, List<Expression> ee, int indent) {

-      Contract.Requires(kind != null);

-      Contract.Requires(ee != null);

-      foreach (Expression e in ee) {

-        Contract.Assert(e != null);

-        Indent(indent);

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

-        PrintExpression(e, true);

-        wr.WriteLine();

-      }

-    }

-

-    internal void PrintDecreasesSpec(Specification<Expression> decs, int indent, bool newLine = true) {

-      Contract.Requires(decs != null);

-      if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

-      if (decs.Expressions != null && decs.Expressions.Count != 0) {

-        Indent(indent);

-        wr.Write("decreases");

-        if (decs.HasAttributes())

-        {

-          PrintAttributes(decs.Attributes);

-        }

-        wr.Write(" ");

-        PrintExpressionList(decs.Expressions, true);

-        if (newLine) {

-          wr.WriteLine();

-        } else {

-          wr.Write(" ");

-        }

-      }

-    }

-

-    internal void PrintFrameSpecLine(string kind, List<FrameExpression/*!*/> ee, int indent, Attributes attrs, bool newLine = true) {

-      Contract.Requires(kind != null);

-      Contract.Requires(cce.NonNullElements(ee));

-      if (ee != null && ee.Count != 0) {

-        Indent(indent);

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

-        if (attrs != null) {

-          PrintAttributes(attrs);

-        }

-        wr.Write(" ");

-        PrintFrameExpressionList(ee);

-        if (newLine) {

-          wr.WriteLine();

-        } else {

-          wr.Write(" ");

-        }

-      }

-    }

-

-    internal void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent, bool newLine = true) {

-      Contract.Requires(kind != null);

-      Contract.Requires(ee != null);

-      if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

-      foreach (MaybeFreeExpression e in ee)

-      {

-        Contract.Assert(e != null);

-        Indent(indent);

-        wr.Write("{0}{1}", e.IsFree ? "free " : "", kind);

-

-        if (e.HasAttributes())

-        {

-          PrintAttributes(e.Attributes);

-        }

-

-        wr.Write(" ");

-        PrintExpression(e.E, true);

-        if (newLine) {

-          wr.WriteLine();

-        } else {

-          wr.Write(" ");

-        }

-      }

-    }

-

-    // ----------------------------- PrintType -----------------------------

-

-    public void PrintType(Type ty) {

-      Contract.Requires(ty != null);

-      wr.Write(ty.ToString());

-    }

-

-    public void PrintType(string prefix, Type ty) {

-      Contract.Requires(prefix != null);

-      Contract.Requires(ty != null);

-      string s = ty.ToString();

-      if (s != "?") {

-        wr.Write("{0}{1}", prefix, s);

-      }

-    }

-

-    string EqualitySupportSuffix(TypeParameter.EqualitySupportValue es) {

-      if (es == TypeParameter.EqualitySupportValue.Required ||

-        (es == TypeParameter.EqualitySupportValue.InferredRequired && DafnyOptions.O.DafnyPrintResolvedFile != null)) {

-        return "(==)";

-      } else {

-        return "";

-      }

-    }

-

-    // ----------------------------- PrintStatement -----------------------------

-

-    /// <summary>

-    /// Prints from the current position of the current line.

-    /// If the statement requires several lines, subsequent lines are indented at "indent".

-    /// No newline is printed after the statement.

-    /// </summary>

-    public void PrintStatement(Statement stmt, int indent) {

-      Contract.Requires(stmt != null);

-

-      if (stmt.IsGhost && printMode == DafnyOptions.PrintModes.NoGhost) { return; }

-      for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {

-        if (label.Data.Name != null) {

-          wr.WriteLine("label {0}:", label.Data.Name);

-          Indent(indent);

-        }

-      }

-

-      if (stmt is PredicateStmt) {

-        if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }

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

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

-        if (stmt.Attributes != null) {

-          PrintAttributes(stmt.Attributes);

-        }

-        wr.Write(" ");

-        PrintExpression(expr, true);

-        wr.Write(";");

-

-      } else if (stmt is PrintStmt) {

-        PrintStmt s = (PrintStmt)stmt;

-        wr.Write("print");

-        PrintAttributeArgs(s.Args, true);

-        wr.Write(";");

-

-      } else if (stmt is BreakStmt) {

-        BreakStmt s = (BreakStmt)stmt;

-        if (s.TargetLabel != null) {

-          wr.Write("break {0};", s.TargetLabel);

-        } else {

-          string sep = "";

-          for (int i = 0; i < s.BreakCount; i++) {

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

-            sep = " ";

-          }

-          wr.Write(";");

-        }

-

-      } else if (stmt is ProduceStmt) {

-        var s = (ProduceStmt) stmt;

-        wr.Write(s is YieldStmt ? "yield" : "return");

-        if (s.rhss != null) {

-          var sep = " ";

-          foreach (var rhs in s.rhss) {

-            wr.Write(sep);

-            PrintRhs(rhs);

-            sep = ", ";

-          }

-        }

-          wr.Write(";");

-

-      } else if (stmt is AssignStmt) {

-        AssignStmt s = (AssignStmt)stmt;

-        PrintExpression(s.Lhs, true);

-        wr.Write(" := ");

-        PrintRhs(s.Rhs);

-        wr.Write(";");

-

-      } else if (stmt is BlockStmt) {

-        wr.WriteLine("{");

-        int ind = indent + IndentAmount;

-        foreach (Statement s in ((BlockStmt)stmt).Body) {

-          Indent(ind);

-          PrintStatement(s, ind);

-          wr.WriteLine();

-        }

-        Indent(indent);

-        wr.Write("}");

-

-      } else if (stmt is IfStmt) {

-        IfStmt s = (IfStmt)stmt;

-        PrintIfStatement(indent, s, false);

-

-      } else if (stmt is AlternativeStmt) {

-        var s = (AlternativeStmt)stmt;

-        wr.WriteLine("if {");

-        PrintAlternatives(indent, s.Alternatives);

-        Indent(indent);

-        wr.Write("}");

-

-      } else if (stmt is WhileStmt) {

-        WhileStmt s = (WhileStmt)stmt;

-        PrintWhileStatement(indent, s, false, false);

-

-      } else if (stmt is AlternativeLoopStmt) {

-        var s = (AlternativeLoopStmt)stmt;

-        wr.WriteLine("while");

-        PrintSpec("invariant", s.Invariants, indent + IndentAmount);

-        PrintDecreasesSpec(s.Decreases, indent + IndentAmount);

-

-        Indent(indent);

-        wr.WriteLine("{");

-        PrintAlternatives(indent, s.Alternatives);

-        Indent(indent);

-        wr.Write("}");

-

-      } else if (stmt is ForallStmt) {

-        var s = (ForallStmt)stmt;

-        wr.Write("forall");

-        if (s.BoundVars.Count != 0) {

-          wr.Write(" ");

-          PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);

-        }

-        if (s.Ens.Count == 0) {

-          wr.Write(" ");

-        } else {

-          wr.WriteLine();

-          PrintSpec("ensures", s.Ens, indent + IndentAmount, s.Body != null);

-          Indent(indent);

-        }

-        if (s.Body != null) {

-          PrintStatement(s.Body, indent);

-        }

-

-      } else if (stmt is ModifyStmt) {

-        var s = (ModifyStmt)stmt;

-        PrintModifyStmt(indent, s, false);

-

-      } else if (stmt is CalcStmt) {

-        CalcStmt s = (CalcStmt)stmt;

-        if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }   // Calcs don't get a "ghost" attribute, but they are.

-        wr.Write("calc ");

-        if (!s.Op.Equals(CalcStmt.DefaultOp)) {

-          PrintCalcOp(s.Op);

-          wr.Write(" ");

-        }

-        wr.WriteLine("{");

-        int lineInd = indent + IndentAmount;

-        int lineCount = s.Lines.Count == 0 ? 0 : s.Lines.Count - 1;  // if nonempty, .Lines always contains a duplicated last line

-        // The number of op/hints is commonly one less than the number of lines, but

-        // it can also equal the number of lines for empty calc's and for calc's with

-        // a dangling hint.

-        int hintCount = s.Lines.Count != 0 && s.Hints.Last().Body.Count == 0 ? lineCount - 1 : lineCount;

-        for (var i = 0; i < lineCount; i++) {

-          var e = s.Lines[i];

-          var op = s.StepOps[i];

-          var h = s.Hints[i];

-          // print the line

-          Indent(lineInd);

-          PrintExpression(e, true, lineInd);

-          wr.WriteLine(";");

-          if (i == hintCount) {

-            break;

-          }

-          // print the operator, if any

-          if (!s.Op.Equals(op)) {

-            Indent(indent);  // this lines up with the "calc"

-            PrintCalcOp(op);

-            wr.WriteLine();

-          }

-          // print the hints

-          foreach (var st in h.Body) {

-            Indent(lineInd);

-            PrintStatement(st, lineInd);

-            wr.WriteLine();

-          }

-        }

-        Indent(indent);

-        wr.Write("}");

-

-      } else if (stmt is MatchStmt) {

-        MatchStmt s = (MatchStmt)stmt;

-        wr.Write("match ");

-        PrintExpression(s.Source, false);

-        if (s.UsesOptionalBraces) {

-          wr.Write(" {");

-        }

-        int caseInd = indent + (s.UsesOptionalBraces ? IndentAmount : 0);

-        foreach (MatchCaseStmt mc in s.Cases) {

-          wr.WriteLine();

-          Indent(caseInd);

-          wr.Write("case {0}", mc.Id);

-          PrintMatchCaseArgument(mc);

-          wr.Write(" =>");

-          foreach (Statement bs in mc.Body) {

-            wr.WriteLine();

-            Indent(caseInd + IndentAmount);

-            PrintStatement(bs, caseInd + IndentAmount);

-          }

-        }

-        if (s.UsesOptionalBraces) {

-          wr.WriteLine();

-          Indent(indent);

-          wr.Write("}");

-        }

-

-      } else if (stmt is ConcreteUpdateStatement) {

-        var s = (ConcreteUpdateStatement)stmt;

-        string sep = "";

-        foreach (var lhs in s.Lhss) {

-          wr.Write(sep);

-          PrintExpression(lhs, true);

-          sep = ", ";

-        }

-        PrintUpdateRHS(s);

-        wr.Write(";");

-

-      } else if (stmt is VarDeclStmt) {

-        var s = (VarDeclStmt)stmt;

-        if (s.Locals.Exists(v => v.IsGhost) && printMode == DafnyOptions.PrintModes.NoGhost) { return; }

-        if (s.Locals.Exists(v => v.IsGhost)) {

-          wr.Write("ghost ");

-        }

-        wr.Write("var");

-        string sep = "";

-        foreach (var local in s.Locals) {

-          wr.Write(sep);

-          if (local.Attributes != null) {

-            PrintAttributes(local.Attributes);

-          }

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

-          PrintType(": ", local.OptionalType);

-          sep = ",";

-        }

-        if (s.Update != null) {

-          PrintUpdateRHS(s.Update);

-        }

-        wr.Write(";");

-

-      } else if (stmt is SkeletonStatement) {

-        var s = (SkeletonStatement)stmt;

-        if (s.S == null) {

-          wr.Write("...;");

-        } 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) {

-          PrintWhileStatement(indent, (WhileStmt)s.S, s.ConditionOmitted, s.BodyOmitted);

-        } else if (s.S is ModifyStmt) {

-          PrintModifyStmt(indent, (ModifyStmt)s.S, true);

-        } else {

-          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected skeleton statement

-        }

-

-      } else {

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

-      }

-    }

-

-    private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {

-      Contract.Requires(0 <= indent);

-      Contract.Requires(s != null);

-      Contract.Requires(!omitFrame || s.Mod.Expressions.Count == 0);

-

-      wr.Write("modify");

-      PrintAttributes(s.Mod.Attributes);

-      wr.Write(" ");

-      if (omitFrame) {

-        wr.Write("...");

-      } else {

-        PrintFrameExpressionList(s.Mod.Expressions);

-      }

-      if (s.Body != null) {

-        // There's a possible syntactic ambiguity, namely if the frame is empty (more precisely,

-        // if s.Mod.Expressions.Count is 0).  Since the statement was parsed at some point, this

-        // situation can occur only if the modify statement inherited its frame by refinement

-        // and we're printing the post-resolve AST.  In this special case, print an explicit

-        // empty set as the frame.

-        if (s.Mod.Expressions.Count == 0) {

-          wr.Write(" {}");

-        }

-        wr.Write(" ");

-        PrintStatement(s.Body, indent);

-      } else {

-        wr.Write(";");

-      }

-    }

-

-    /// <summary>

-    /// Does not print LHS

-    /// </summary>

-    void PrintUpdateRHS(ConcreteUpdateStatement s) {

-      Contract.Requires(s != null);

-      if (s is UpdateStmt) {

-        var update = (UpdateStmt)s;

-        if (update.Lhss.Count != 0) {

-          wr.Write(" := ");

-        }

-        var sep = "";

-        foreach (var rhs in update.Rhss) {

-          wr.Write(sep);

-          PrintRhs(rhs);

-          sep = ", ";

-        }

-      } else if (s is AssignSuchThatStmt) {

-        var update = (AssignSuchThatStmt)s;

-        wr.Write(" :| ");

-        if (update.AssumeToken != null) {

-          wr.Write("assume ");

-        }

-        PrintExpression(update.Expr, true);

-      } else {

-        Contract.Assert(s == null);  // otherwise, unknown type

-      }

-    }

-

-    void PrintIfStatement(int indent, IfStmt s, bool omitGuard) {

-      while (true) {

-        if (omitGuard) {

-          wr.Write("if ... ");

-        } else {

-          wr.Write("if ");

-          PrintGuard(s.Guard);

-          wr.Write(" ");

-        }

-        PrintStatement(s.Thn, indent);

-        if (s.Els == null) {

-          break;

-        }

-        wr.Write(" else ");

-        if (s.Els is IfStmt) {

-          s = (IfStmt)s.Els;

-        } else {

-          PrintStatement(s.Els, indent);

-          break;

-        }

-      }

-    }

-

-    void PrintWhileStatement(int indent, WhileStmt s, bool omitGuard, bool omitBody) {

-      Contract.Requires(0 <= indent);

-      if (omitGuard) {

-        wr.WriteLine("while ...");

-      } else {

-        wr.Write("while ");

-        PrintGuard(s.Guard);

-        wr.WriteLine();

-      }

-

-      PrintSpec("invariant", s.Invariants, indent + IndentAmount, s.Body != null || omitBody || (s.Decreases.Expressions != null && s.Decreases.Expressions.Count != 0) || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0));

-      PrintDecreasesSpec(s.Decreases, indent + IndentAmount, s.Body != null || omitBody || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0));

-      if (s.Mod.Expressions != null) {

-        PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null, s.Body != null || omitBody);

-      }

-      Indent(indent);

-      if (omitBody) {

-        wr.WriteLine("...;");

-      } else if (s.Body != null) {

-        PrintStatement(s.Body, indent);

-      }

-    }

-

-    void PrintAlternatives(int indent, List<GuardedAlternative> alternatives) {

-      int caseInd = indent + IndentAmount;

-      foreach (var alternative in alternatives) {

-        Indent(caseInd);

-        wr.Write("case ");

-        PrintExpression(alternative.Guard, false);

-        wr.WriteLine(" =>");

-        foreach (Statement s in alternative.Body) {

-          Indent(caseInd + IndentAmount);

-          PrintStatement(s, caseInd + IndentAmount);

-          wr.WriteLine();

-        }

-      }

-    }

-

-    void PrintRhs(AssignmentRhs rhs) {

-      Contract.Requires(rhs != null);

-      if (rhs is ExprRhs) {

-        PrintExpression(((ExprRhs)rhs).Expr, true);

-      } else if (rhs is HavocRhs) {

-        wr.Write("*");

-      } else if (rhs is TypeRhs) {

-        TypeRhs t = (TypeRhs)rhs;

-        wr.Write("new ");

-        if (t.ArrayDimensions != null) {

-          PrintType(t.EType);

-          string s = "[";

-          foreach (Expression dim in t.ArrayDimensions) {

-            Contract.Assume(dim != null);

-            wr.Write(s);

-            PrintExpression(dim, false);

-            s = ", ";

-          }

-          wr.Write("]");

-        } else if (t.Arguments == null) {

-          PrintType(t.EType);

-        } else {

-          PrintType(t.Path);

-          wr.Write("(");

-          PrintExpressionList(t.Arguments, false);

-          wr.Write(")");

-        }

-      } else {

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

-      }

-

-      if (rhs.HasAttributes())

-      {

-        PrintAttributes(rhs.Attributes);

-      }

-    }

-

-    void PrintGuard(Expression guard) {

-      if (guard == null) {

-        wr.Write("*");

-      } else {

-        PrintExpression(guard, false);

-      }

-    }

-

-    void PrintCalcOp(CalcStmt.CalcOp op) {

-      Contract.Requires(op != null);

-      wr.Write(op.ToString());

-      if (op is CalcStmt.TernaryCalcOp) {

-        wr.Write("[");

-        PrintExpression(((CalcStmt.TernaryCalcOp) op).Index, false);

-        wr.Write("]");

-      }

-    }

-

-    // ----------------------------- PrintExpression -----------------------------

-

-    /// <summary>

-    /// PrintExtendedExpr prints an expression, but formats top-level if-then-else and match expressions across several lines.

-    /// Its intended use is thus to print the body of a function.

-    /// </summary>

-    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {

-      Contract.Requires(expr != null);

-      if (expr is ITEExpr) {

-        Indent(indent);

-        while (true) {

-          var ite = (ITEExpr)expr;

-          wr.Write("if ");

-          PrintExpression(ite.Test, false);

-          wr.WriteLine(" then");

-          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);

-          expr = ite.Els;

-          if (expr is ITEExpr) {

-            Indent(indent);  wr.Write("else ");

-          } else {

-            Indent(indent);  wr.WriteLine("else");

-            Indent(indent + IndentAmount);

-            PrintExpression(expr, isRightmost, false);

-            wr.WriteLine(endWithCloseParen ? ")" : "");

-            return;

-          }

-        }

-      } else if (expr is MatchExpr) {

-        var e = (MatchExpr)expr;

-        Indent(indent);

-        var parensNeeded = !isRightmost && !e.UsesOptionalBraces;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write("match ");

-        PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, false);

-        if (e.UsesOptionalBraces) { wr.WriteLine(" {"); }

-        else if (parensNeeded && e.Cases.Count == 0) { wr.WriteLine(")"); }

-        else { wr.WriteLine(); }

-        int i = 0;

-        int ind = indent + (e.UsesOptionalBraces ? IndentAmount : 0);

-        foreach (var mc in e.Cases) {

-          bool isLastCase = i == e.Cases.Count - 1;

-          Indent(ind);

-          wr.Write("case {0}", mc.Id);

-          PrintMatchCaseArgument(mc);          

-          wr.WriteLine(" =>");

-          PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));

-          i++;

-        }

-        if (e.UsesOptionalBraces) {

-          Indent(indent);

-          wr.WriteLine("}");

-        }

-      } else if (expr is LetExpr) {

-        var e = (LetExpr)expr;

-        Indent(indent);

-        wr.Write("var ");

-        string sep = "";

-        foreach (var lhs in e.LHSs) {

-          wr.Write(sep);

-          PrintCasePattern(lhs);

-          sep = ", ";

-        }

-        if (e.Exact) {

-          wr.Write(" := ");

-        } else {

-          wr.Write(" :| ");

-        }

-        PrintExpressionList(e.RHSs, true);

-        wr.WriteLine(";");

-        PrintExtendedExpr(e.Body, indent, isRightmost, endWithCloseParen);

-

-      } else if (expr is ParensExpression) {

-        PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen);

-      } else {

-        Indent(indent);

-        PrintExpression(expr, false, indent);

-        wr.WriteLine(endWithCloseParen ? ")" : "");

-      }

-    }

-

-    public void PrintMatchCaseArgument(MatchCase mc) {

-      if (mc.Arguments != null) {

-        if (mc.Arguments.Count != 0) {

-          string sep = "(";

-          foreach (BoundVar bv in mc.Arguments) {

-            wr.Write("{0}{1}", sep, bv.DisplayName);

-            if (bv.Type is NonProxyType) {

-              wr.Write(": {0}", bv.Type);

-            }

-            sep = ", ";

-          }

-          wr.Write(")");

-        }

-      } else {

-        Contract.Assert(mc.CasePatterns != null);

-        if (mc.CasePatterns.Count != 0) {

-          string sep = "(";

-          foreach (var cp in mc.CasePatterns) {

-            wr.Write(sep);

-            PrintCasePattern(cp);

-            sep = ", ";

-          }

-          wr.Write(")");

-        }

-      }

-    }

-

-    public void PrintExpression(Expression expr, bool isFollowedBySemicolon) {

-      Contract.Requires(expr != null);

-      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1);

-    }

-

-    public void PrintExpression(Expression expr, bool isRightmost, bool isFollowedBySemicolon) {

-      Contract.Requires(expr != null);

-      PrintExpr(expr, 0, false, isRightmost, isFollowedBySemicolon, -1);

-    }

-

-    /// <summary>

-    /// An indent of -1 means print the entire expression on one line.

-    /// </summary>

-    public void PrintExpression(Expression expr, bool isFollowedBySemicolon, int indent) {

-      Contract.Requires(expr != null);

-      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, indent);

-    }

-

-    private bool ParensNeeded(int opBindingStrength, int contextBindingStrength, bool fragileContext) {

-      return opBindingStrength < contextBindingStrength ||

-             (fragileContext && opBindingStrength == contextBindingStrength);

-    }

-

-    /// <summary>

-    /// An indent of -1 means print the entire expression on one line.

-    /// </summary>

-    void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, bool isRightmost, bool isFollowedBySemicolon, int indent, int resolv_count = 2)

-    {

-      Contract.Requires(-1 <= indent);

-      Contract.Requires(expr != null);

-

-      /* When debugging:

-      if (resolv_count > 0 && expr.Resolved != null) {

-        PrintExpr(expr.Resolved, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count - 1);

-        return;

-      }

-      */

-

-      if (expr is StaticReceiverExpr) {

-        StaticReceiverExpr e = (StaticReceiverExpr)expr;

-        wr.Write(e.Type);

-      } else if (expr is LiteralExpr) {

-        LiteralExpr e = (LiteralExpr)expr;

-        if (e.Value == null) {

-          wr.Write("null");

-        } else if (e.Value is bool) {

-          wr.Write((bool)e.Value ? "true" : "false");

-        } else if (e is CharLiteralExpr) {

-          wr.Write("'{0}'", (string)e.Value);

-        } else if (e is StringLiteralExpr) {

-          var str = (StringLiteralExpr)e;

-          wr.Write("{0}\"{1}\"", str.IsVerbatim ? "@" : "", (string)e.Value);

-        } else if (e.Value is Basetypes.BigDec) {

-          Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;

-          wr.Write((dec.Mantissa >= 0) ? "" : "-");

-          string s = BigInteger.Abs(dec.Mantissa).ToString();

-          int digits = s.Length;

-          if (dec.Exponent >= 0) {

-            wr.Write("{0}{1}.0", s, new string('0', dec.Exponent));

-          } else {

-            int exp = -dec.Exponent;

-            if (exp < digits) {

-              int intDigits = digits - exp;

-              int fracDigits = digits - intDigits;

-              wr.Write("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));

-            } else {

-              int fracDigits = digits;

-              wr.Write("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));

-            }

-          }

-        } else {

-          wr.Write((BigInteger)e.Value);

-        }

-

-      } else if (expr is ThisExpr) {

-        wr.Write("this");

-

-      } else if (expr is IdentifierExpr) {

-        wr.Write(((IdentifierExpr)expr).Name);

-

-      } else if (expr is DatatypeValue) {

-        var dtv = (DatatypeValue)expr;

-        bool printParens;

-        if (dtv.MemberName == BuiltIns.TupleTypeCtorName) {

-          // we're looking at a tuple, whose printed constructor name is essentially the empty string

-          printParens = true;

-        } else {

-          wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName);

-          printParens = dtv.Arguments.Count != 0;

-        }

-        if (printParens) {

-          wr.Write("(");

-          PrintExpressionList(dtv.Arguments, false);

-          wr.Write(")");

-        }

-

-      } else if (expr is DisplayExpression) {

-        DisplayExpression e = (DisplayExpression)expr;

-        if (e is MultiSetDisplayExpr) {

-          wr.Write("multiset");

-        } else if (e is SetDisplayExpr && !((SetDisplayExpr)e).Finite) {

-          wr.Write("iset");

-        }

-        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");

-        PrintExpressionList(e.Elements, false);

-        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");

-

-      } else if (expr is MapDisplayExpr) {

-        MapDisplayExpr e = (MapDisplayExpr)expr;

-        wr.Write(e.Finite ? "map" : "imap");

-        wr.Write("[");

-        PrintExpressionPairList(e.Elements);

-        wr.Write("]");

-

-      } else if (expr is NameSegment) {

-        var e = (NameSegment)expr;

-        wr.Write(e.Name);

-        PrintTypeInstantiation(e.OptTypeArguments);

-

-      } else if (expr is ExprDotName) {

-        var e = (ExprDotName)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = !e.Lhs.IsImplicit && // KRML: I think that this never holds

-          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-        if (!e.Lhs.IsImplicit) {

-          PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

-          wr.Write(".");

-        }

-        wr.Write(e.SuffixName);

-        PrintTypeInstantiation(e.OptTypeArguments);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is ApplySuffix) {

-        var e = (ApplySuffix)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = !e.Lhs.IsImplicit &&  // KRML: I think that this never holds

-          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-        if (ParensMayMatter(e.Lhs)) {

-          wr.Write("(");

-          PrintExpression(e.Lhs, false);

-          wr.Write(")");

-        } else {

-          PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

-        }

-        wr.Write("(");

-        PrintExpressionList(e.Args, false);

-        wr.Write(")");

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is MemberSelectExpr) {

-        MemberSelectExpr e = (MemberSelectExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = !e.Obj.IsImplicit &&

-          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-        if (!(e.Obj.IsImplicit)) {

-          PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

-          wr.Write(".");

-        }

-        wr.Write(e.MemberName);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is SeqSelectExpr) {

-        SeqSelectExpr e = (SeqSelectExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

-        wr.Write("[");

-        if (e.SelectOne) {

-          Contract.Assert( e.E0 != null);

-          PrintExpression(e.E0, false);

-        } else {

-          if (e.E0 != null) {

-            PrintExpression(e.E0, false);

-          }

-          wr.Write(e.E0 != null && e.E1 != null ? " .. " : "..");

-          if (e.E1 != null) {

-            PrintExpression(e.E1, false);

-          }

-        }

-        wr.Write("]");

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is MultiSelectExpr) {

-        MultiSelectExpr e = (MultiSelectExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-        PrintExpr(e.Array, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

-        string prefix = "[";

-        foreach (Expression idx in e.Indices) {

-          Contract.Assert(idx != null);

-          wr.Write(prefix);

-          PrintExpression(idx, false);

-          prefix = ", ";

-        }

-        wr.Write("]");

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is SeqUpdateExpr) {

-        SeqUpdateExpr e = (SeqUpdateExpr)expr;

-        if (e.ResolvedUpdateExpr != null)

-        {

-          PrintExpr(e.ResolvedUpdateExpr, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);

-        }

-        else

-        {

-          // determine if parens are needed

-          int opBindingStrength = 0x70;

-          bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-          if (parensNeeded) { wr.Write("("); }

-          PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

-          wr.Write("[");

-          PrintExpression(e.Index, false);

-          wr.Write(" := ");

-          PrintExpression(e.Value, false);

-          wr.Write("]");

-          if (parensNeeded) { wr.Write(")"); }

-        }

-      } else if (expr is ApplyExpr) {

-        var e = (ApplyExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-

-        PrintExpr(e.Function, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

-        wr.Write("(");

-        PrintExpressionList(e.Args, false);

-        wr.Write(")");

-

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is FunctionCallExpr) {

-        var e = (FunctionCallExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x70;

-        bool parensNeeded = !(e.Receiver.IsImplicit) &&

-          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        if (parensNeeded) { wr.Write("("); }

-        if (!e.Receiver.IsImplicit) {

-          PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);

-          wr.Write(".");

-        }

-        wr.Write(e.Name);

-        /* When debugging, this is nice to have:

-        if (e.TypeArgumentSubstitutions.Count > 0) {

-          wr.Write("[");

-          wr.Write(Util.Comma(",", e.TypeArgumentSubstitutions, kv => kv.Key.FullName() + "->" + kv.Value));

-          wr.Write("]");

-        }

-        */

-        if (e.OpenParen == null && e.Args.Count == 0) {

-        } else {

-          PrintActualArguments(e.Args, e.Name);

-        }

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is OldExpr) {

-        wr.Write("old(");

-        PrintExpression(((OldExpr)expr).E, false);

-        wr.Write(")");

-

-      } else if (expr is MultiSetFormingExpr) {

-        wr.Write("multiset(");

-        PrintExpression(((MultiSetFormingExpr)expr).E, false);

-        wr.Write(")");

-

-      } else if (expr is UnaryOpExpr) {

-        var e = (UnaryOpExpr)expr;

-        if (e.Op == UnaryOpExpr.Opcode.Cardinality) {

-          wr.Write("|");

-          PrintExpression(e.E, false);

-          wr.Write("|");

-        } else if (e.Op == UnaryOpExpr.Opcode.Fresh) {

-          wr.Write("fresh(");

-          PrintExpression(e.E, false);

-          wr.Write(")");

-        } else {

-          // Prefix operator.

-          // determine if parens are needed

-          string op;

-          int opBindingStrength;

-          switch (e.Op) {

-            case UnaryOpExpr.Opcode.Not:

-              op = "!";  opBindingStrength = 0x60;  break;

-            default:

-              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary opcode

-          }

-          bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-          bool containsNestedNot = e.E is ParensExpression &&

-                                ((ParensExpression)e.E).E is UnaryExpr &&

-                                ((UnaryOpExpr)((ParensExpression)e.E).E).Op == UnaryOpExpr.Opcode.Not;

-

-          if (parensNeeded) { wr.Write("("); }

-          wr.Write(op);

-          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);

-          if (parensNeeded) { wr.Write(")"); }

-        }

-

-      } else if (expr is ConversionExpr) {

-        var e = (ConversionExpr)expr;

-        PrintType(e.ToType);

-        wr.Write("(");

-        PrintExpression(e.E, false);

-        wr.Write(")");

-

-      } else if (expr is BinaryExpr) {

-        BinaryExpr e = (BinaryExpr)expr;

-        // determine if parens are needed

-        int opBindingStrength;

-        bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"

-        bool fragileRightContext = false;  // false means "allow same binding power on right without parens"

-        switch (e.Op)

-        {

-          case BinaryExpr.Opcode.Add:

-            opBindingStrength = 0x40; break;

-          case BinaryExpr.Opcode.Sub:

-            opBindingStrength = 0x40; fragileRightContext = true; break;

-          case BinaryExpr.Opcode.Mul:

-            opBindingStrength = 0x50; break;

-          case BinaryExpr.Opcode.Div:

-          case BinaryExpr.Opcode.Mod:

-            opBindingStrength = 0x50; fragileRightContext = true; break;

-          case BinaryExpr.Opcode.Eq:

-          case BinaryExpr.Opcode.Neq:

-          case BinaryExpr.Opcode.Gt:

-          case BinaryExpr.Opcode.Ge:

-          case BinaryExpr.Opcode.Lt:

-          case BinaryExpr.Opcode.Le:

-          case BinaryExpr.Opcode.Disjoint:

-          case BinaryExpr.Opcode.In:

-          case BinaryExpr.Opcode.NotIn:

-            opBindingStrength = 0x30; fragileLeftContext = fragileRightContext = true; break;

-          case BinaryExpr.Opcode.And:

-            opBindingStrength = 0x20; break;

-          case BinaryExpr.Opcode.Or:

-            opBindingStrength = 0x21; break;

-          case BinaryExpr.Opcode.Imp:

-            opBindingStrength = 0x10; fragileLeftContext = true; break;

-          case BinaryExpr.Opcode.Exp:

-            opBindingStrength = 0x11; fragileRightContext = true; break;

-          case BinaryExpr.Opcode.Iff:

-            opBindingStrength = 0x08; break;

-          default:

-            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary operator

-        }

-        int opBS = opBindingStrength & 0xF8;

-        int ctxtBS = contextBindingStrength & 0xF8;

-        bool parensNeeded = opBS < ctxtBS ||

-          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

-

-        string op = BinaryExpr.OpcodeString(e.Op);

-        if (parensNeeded) { wr.Write("("); }

-        var sem = !parensNeeded && isFollowedBySemicolon;

-        if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);

-          wr.WriteLine(" {0}", op);

-          Indent(indent);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, indent);

-        } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);

-          wr.WriteLine(" {0}", op);

-          int ind = indent + IndentAmount;

-          Indent(ind);

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);

-        } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Exp) {

-          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, indent);

-          wr.WriteLine(" {0}", op);

-          int ind = indent + IndentAmount;

-          Indent(ind);

-          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);

-        } else if (e.Op == BinaryExpr.Opcode.Exp) {

-          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);

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

-          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);

-        } else {

-          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, -1);

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

-          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);

-        }

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is TernaryExpr) {

-        var e = (TernaryExpr)expr;

-        switch (e.Op) {

-          case TernaryExpr.Opcode.PrefixEqOp:

-          case TernaryExpr.Opcode.PrefixNeqOp:

-            var opBindingStrength = 0x30;

-            var fragileLeftContext = true;

-            var fragileRightContext = true;

-

-            int opBS = opBindingStrength & 0xF8;

-            int ctxtBS = contextBindingStrength & 0xF8;

-            bool parensNeeded = opBS < ctxtBS ||

-              (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

-

-            if (parensNeeded) { wr.Write("("); }

-            var sem = !parensNeeded && isFollowedBySemicolon;

-            PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);

-            wr.Write(" {0}#[", e.Op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=");

-            PrintExpression(e.E0, false);

-            wr.Write("] ");

-            PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);

-            if (parensNeeded) { wr.Write(")"); }

-            break;

-          default:

-            Contract.Assert(false);  // unexpected ternary operator

-            break;

-        }

-

-      } else if (expr is ChainingExpression) {

-        var e = (ChainingExpression)expr;

-        // determine if parens are needed

-        int opBindingStrength = 0x30;

-        int opBS = opBindingStrength & 0xF8;

-        int ctxtBS = contextBindingStrength & 0xF8;

-        bool parensNeeded = opBS < ctxtBS ||

-          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));

-

-        if (parensNeeded) { wr.Write("("); }

-        var sem = !parensNeeded && isFollowedBySemicolon;

-        PrintExpr(e.Operands[0], opBindingStrength, true, false, sem, -1);

-        for (int i = 0; i < e.Operators.Count; i++) {

-          string op = BinaryExpr.OpcodeString(e.Operators[i]);

-          if (e.PrefixLimits[i] == null) {

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

-          } else {

-            wr.Write(" {0}#[", op);

-            PrintExpression(e.PrefixLimits[i], false);

-            wr.Write("] ");

-          }

-          PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), sem, -1);

-        }

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is LetExpr) {

-        var e = (LetExpr)expr;

-        bool parensNeeded = !isRightmost;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write("var ");

-        string sep = "";

-        foreach (var lhs in e.LHSs) {

-          wr.Write(sep);

-          PrintCasePattern(lhs);

-          sep = ", ";

-        }

-        if (e.Exact) {

-          wr.Write(" := ");

-        } else {

-          wr.Write(" :| ");

-        }

-        PrintExpressionList(e.RHSs, true);

-        wr.Write("; ");

-        PrintExpression(e.Body, !parensNeeded && isFollowedBySemicolon);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is QuantifierExpr) {

-        QuantifierExpr e = (QuantifierExpr)expr;

-

-        if (DafnyOptions.O.DafnyPrintResolvedFile != null && e.SplitQuantifier != null) {

-          PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count);

-          return;

-        }

-

-        bool parensNeeded = !isRightmost;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write(e is ForallExpr ? "forall" : "exists");

-        PrintTypeParams(e.TypeArgs); // new!

-        wr.Write(" ");

-        PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);

-        wr.Write(" :: ");

-        if (0 <= indent) {

-          int ind = indent + IndentAmount;

-          wr.WriteLine();

-          Indent(ind);

-          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon, ind);

-        } else {

-          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

-        }

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is NamedExpr) {

-        var e = (NamedExpr)expr;

-        wr.Write("expr {0}: ", e.Name);

-        PrintExpression(e.Body, isFollowedBySemicolon);

-

-       } else if (expr is SetComprehension) {

-        var e = (SetComprehension)expr;

-        bool parensNeeded = !isRightmost;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write("set ");

-        string sep = "";

-        foreach (BoundVar bv in e.BoundVars) {

-          wr.Write("{0}{1}", sep, bv.DisplayName);

-          sep = ", ";

-          PrintType(": ", bv.Type);

-        }

-        PrintAttributes(e.Attributes);

-        wr.Write(" | ");

-        PrintExpression(e.Range, !parensNeeded && isFollowedBySemicolon);

-        if (!e.TermIsImplicit) {

-          wr.Write(" :: ");

-          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

-        }

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is MapComprehension) {

-        var e = (MapComprehension)expr;

-        bool parensNeeded = !isRightmost;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write(e.Finite ? "map " : "imap ");

-        string sep = "";

-        foreach (BoundVar bv in e.BoundVars) {

-          wr.Write("{0}{1}", sep, bv.DisplayName);

-          sep = ", ";

-          PrintType(": ", bv.Type);

-        }

-        PrintAttributes(e.Attributes);

-        wr.Write(" | ");

-        PrintExpression(e.Range, !parensNeeded && isFollowedBySemicolon);

-        wr.Write(" :: ");

-        PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is LambdaExpr) {

-        var e = (LambdaExpr)expr;

-        bool parensNeeded = !isRightmost;

-        if (parensNeeded) { wr.Write("("); }

-        var skipSignatureParens = e.BoundVars.Count == 1 && e.BoundVars[0].Type is InferredTypeProxy;

-        if (!skipSignatureParens) { wr.Write("("); }

-        wr.Write(Util.Comma(", ", e.BoundVars, bv => bv.DisplayName + (bv.Type is InferredTypeProxy ? "" : ": " + bv.Type)));

-        if (!skipSignatureParens) { wr.Write(")"); }

-        if (e.Range != null) {

-          wr.Write(" requires ");

-          PrintExpression(e.Range, false);

-        }

-        foreach (var read in e.Reads) {

-          wr.Write(" reads ");

-          PrintExpression(read.E, false);

-        }

-        wr.Write(e.OneShot ? " -> " : " => ");

-        PrintExpression(e.Body, isFollowedBySemicolon);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is WildcardExpr) {

-        wr.Write("*");

-

-      } else if (expr is StmtExpr) {

-        var e = (StmtExpr)expr;

-        bool parensNeeded;

-        if (e.S is AssertStmt || e.S is AssumeStmt || e.S is CalcStmt) {

-          parensNeeded = !isRightmost;

-        } else {

-          parensNeeded = !isRightmost || isFollowedBySemicolon;

-        }

-        if (parensNeeded) { wr.Write("("); }

-        int ind = indent < 0 ? IndentAmount : indent;  // if the expression was to be printed on one line, instead print the .S part at indentation IndentAmount (not pretty, but something)

-        PrintStatement(e.S, ind);

-        wr.Write(" ");

-        PrintExpression(e.E, !parensNeeded && isFollowedBySemicolon);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is ITEExpr) {

-        ITEExpr ite = (ITEExpr)expr;

-        bool parensNeeded = !isRightmost;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write("if ");

-        PrintExpression(ite.Test, false);

-        wr.Write(" then ");

-        PrintExpression(ite.Thn, false);

-        wr.Write(" else ");

-        PrintExpression(ite.Els, !parensNeeded && isFollowedBySemicolon);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is ParensExpression) {

-        var e = (ParensExpression)expr;

-        // printing of parentheses is done optimally, not according to the parentheses in the given program

-        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);

-

-      } else if (expr is NegationExpression) {

-        var e = (NegationExpression)expr;

-        string op = "-";

-        int opBindingStrength = 0x60;

-        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

-

-        bool containsNestedNegation = e.E is ParensExpression && ((ParensExpression)e.E).E is NegationExpression;

-

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write(op);

-        PrintExpr(e.E, opBindingStrength, containsNestedNegation, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);

-        if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is MatchExpr) {

-        var e = (MatchExpr)expr;

-        var parensNeeded = !isRightmost && !e.UsesOptionalBraces;

-        if (parensNeeded) { wr.Write("("); }

-        wr.Write("match ");

-        PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, !parensNeeded && isFollowedBySemicolon);

-        if (e.UsesOptionalBraces) { wr.Write(" {"); }

-        int i = 0;

-        foreach (var mc in e.Cases) {

-          bool isLastCase = i == e.Cases.Count - 1;

-          wr.Write(" case {0}", mc.Id);

-          PrintMatchCaseArgument(mc);

-          wr.Write(" => ");

-          PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);

-          i++;

-        }

-        if (e.UsesOptionalBraces) { wr.Write(" }"); }

-        else if (parensNeeded) { wr.Write(")"); }

-

-      } else if (expr is BoxingCastExpr) {

-        // this is not expected for a parsed program, but we may be called for /trace purposes in the translator

-        var e = (BoxingCastExpr)expr;

-        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);

-      } else if (expr is Translator.BoogieWrapper) {

-        wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here

-      } else {

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

-      }

-    }

-

-    bool ParensMayMatter(Expression expr) {

-      Contract.Requires(expr != null);

-      int parenPairs = 0;

-      for (; expr is ParensExpression; parenPairs++) {

-        expr = ((ParensExpression)expr).E;

-      }

-      // If the program were resolved, we could be more precise than the following (in particular, looking

-      // to see if expr denotes a MemberSelectExpr of a member that is a Function.

-      return parenPairs != 0 && (expr is NameSegment || expr is ExprDotName);

-    }

-

-    void PrintCasePattern(CasePattern pat) {

-      Contract.Requires(pat != null);

-      var v = pat.Var;

-      if (v != null) {

-        wr.Write(v.DisplayName);

-        if (v.Type is NonProxyType || DafnyOptions.O.DafnyPrintResolvedFile != null) {

-          PrintType(": ", v.Type);

-        }

-      } else {

-        wr.Write(pat.Id);

-        if (pat.Arguments != null) {

-          wr.Write("(");

-          var sep = "";

-          foreach (var arg in pat.Arguments) {

-            wr.Write(sep);

-            PrintCasePattern(arg);

-            sep = ", ";

-          }

-          wr.Write(")");

-        }

-      }

-    }

-

-    private void PrintQuantifierDomain(List<BoundVar> boundVars, Attributes attrs, Expression range) {

-      Contract.Requires(boundVars != null);

-      string sep = "";

-      foreach (BoundVar bv in boundVars) {

-        wr.Write("{0}{1}", sep, bv.DisplayName);

-        PrintType(": ", bv.Type);

-        sep = ", ";

-      }

-      PrintAttributes(attrs);

-      if (range != null) {

-        wr.Write(" | ");

-        PrintExpression(range, false);

-      }

-    }

-

-    void PrintActualArguments(List<Expression> args, string name) {

-      Contract.Requires(args != null);

-      Contract.Requires(name != null);

-      if (name.EndsWith("#")) {

-        wr.Write("[");

-        PrintExpression(args[0], false);

-        wr.Write("]");

-        args = new List<Expression>(args.Skip(1));

-      }

-      wr.Write("(");

-      PrintExpressionList(args, false);

-      wr.Write(")");

-    }

-

-    void PrintExpressionList(List<Expression> exprs, bool isFollowedBySemicolon) {

-      Contract.Requires(exprs != null);

-      string sep = "";

-      foreach (Expression e in exprs) {

-        Contract.Assert(e != null);

-        wr.Write(sep);

-        sep = ", ";

-        PrintExpression(e, isFollowedBySemicolon);

-      }

-    }

-    void PrintExpressionPairList(List<ExpressionPair> exprs) {

-      Contract.Requires(exprs != null);

-      string sep = "";

-      foreach (ExpressionPair p in exprs) {

-        Contract.Assert(p != null);

-        wr.Write(sep);

-        sep = ", ";

-        PrintExpression(p.A, false);

-        wr.Write(":=");

-        PrintExpression(p.B, false);

-      }

-    }

-

-    void PrintFrameExpressionList(List<FrameExpression/*!*/>/*!*/ fexprs) {

-      Contract.Requires(fexprs != null);

-      string sep = "";

-      foreach (FrameExpression fe in fexprs) {

-        Contract.Assert(fe != null);

-        wr.Write(sep);

-        sep = ", ";

-        PrintExpression(fe.E, true);

-        if (fe.FieldName != null) {

-          wr.Write("`{0}", fe.FieldName);

-        }

-      }

-    }

-  }

-}

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Numerics;
+using System.Linq;
+using Bpl = Microsoft.Boogie;
+
+namespace Microsoft.Dafny {
+  public class Printer {
+    TextWriter wr;
+    DafnyOptions.PrintModes printMode;
+
+    [ContractInvariantMethod]
+    void ObjectInvariant()
+    {
+      Contract.Invariant(wr!=null);
+    }
+
+    public Printer(TextWriter wr, DafnyOptions.PrintModes printMode = DafnyOptions.PrintModes.Everything) {
+      Contract.Requires(wr != null);
+      this.wr = wr;
+      this.printMode = printMode;
+    }
+
+    public static string ExprToString(Expression expr)
+    {
+      Contract.Requires(expr != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintExpression(expr, false);
+        return wr.ToString();
+      }
+    }
+
+    public static string GuardToString(Expression expr) {
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintGuard(expr);
+        return wr.ToString();
+      }
+    }
+
+    public static string ExtendedExprToString(Expression expr) {
+      Contract.Requires(expr != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintExtendedExpr(expr, 0, true, false);
+        return wr.ToString();
+      }
+    }
+
+    public static string FrameExprListToString(List<FrameExpression> fexprs) {
+      Contract.Requires(fexprs != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintFrameExpressionList(fexprs);
+        return wr.ToString();
+      }
+    }
+
+    public static string StatementToString(Statement stmt) {
+      Contract.Requires(stmt != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintStatement(stmt, 0);
+        return ToStringWithoutNewline(wr);
+      }
+    }
+
+    public static string IteratorClassToString(IteratorDecl iter) {
+      Contract.Requires(iter != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintIteratorClass(iter, 0, null);
+        return ToStringWithoutNewline(wr);
+      }
+    }
+
+    public static string IteratorSignatureToString(IteratorDecl iter) {
+      Contract.Requires(iter != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintIteratorSignature(iter, 0);
+        return ToStringWithoutNewline(wr);
+      }
+    }
+
+    public static string FunctionSignatureToString(Function f) {
+      Contract.Requires(f != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintFunction(f, 0, true);
+        return ToStringWithoutNewline(wr);
+      }
+    }
+
+    public static string MethodSignatureToString(Method m) {
+      Contract.Requires(m != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintMethod(m, 0, true);
+        return ToStringWithoutNewline(wr);
+      }
+    }
+
+    public static string OneAttributeToString(Attributes a, string nameSubstitution = null) {
+      Contract.Requires(a != null);
+      using (var wr = new System.IO.StringWriter()) {
+        var pr = new Printer(wr);
+        pr.PrintOneAttribute(a, nameSubstitution);
+        return ToStringWithoutNewline(wr);
+      }
+    }
+
+    public static string ToStringWithoutNewline(System.IO.StringWriter wr) {
+      Contract.Requires(wr != null);
+      var sb = wr.GetStringBuilder();
+      var len = sb.Length;
+      while (len > 0 && (sb[len - 1] == '\n' || sb[len - 1] == '\r')) {
+        len--;
+      }
+      return sb.ToString(0, len);
+    }
+
+    public void PrintProgram(Program prog) {
+      Contract.Requires(prog != null);
+      if (Bpl.CommandLineOptions.Clo.ShowEnv != Bpl.CommandLineOptions.ShowEnvironment.Never) {
+        wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Version);
+        wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);
+      }
+      wr.WriteLine("// {0}", prog.Name);
+      if (DafnyOptions.O.DafnyPrintResolvedFile != null && DafnyOptions.O.PrintMode == DafnyOptions.PrintModes.Everything) {
+        wr.WriteLine();
+        wr.WriteLine("/*");
+        PrintModuleDefinition(prog.BuiltIns.SystemModule, 0, Path.GetFullPath(DafnyOptions.O.DafnyPrintResolvedFile));
+        wr.WriteLine("*/");
+      }
+      wr.WriteLine();
+      PrintCallGraph(prog.DefaultModuleDef, 0);
+      PrintTopLevelDecls(prog.DefaultModuleDef.TopLevelDecls, 0, Path.GetFullPath(prog.FullName));
+      wr.Flush();
+    }
+
+    public void PrintCallGraph(ModuleDefinition module, int indent) {
+      Contract.Requires(module != null);
+      Contract.Requires(0 <= indent);
+      if (DafnyOptions.O.DafnyPrintResolvedFile != null && DafnyOptions.O.PrintMode == DafnyOptions.PrintModes.Everything) {
+         // print call graph
+        Indent(indent); wr.WriteLine("/* CALL GRAPH for module {0}:", module.Name);
+        var SCCs = module.CallGraph.TopologicallySortedComponents();
+        SCCs.Reverse();
+        foreach (var clbl in SCCs) {
+          Indent(indent); wr.WriteLine(" * SCC at height {0}:", module.CallGraph.GetSCCRepresentativeId(clbl));
+          var r = module.CallGraph.GetSCC(clbl);
+          foreach (var m in r) {
+            Indent(indent); wr.WriteLine(" *   {0}", m.NameRelativeToModule);
+          }
+        }
+        Indent(indent); wr.WriteLine(" */");
+      }
+    }
+
+    public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, string fileBeingPrinted) {
+      Contract.Requires(decls!= null);
+      int i = 0;
+      foreach (TopLevelDecl d in decls) {
+        Contract.Assert(d != null);
+        if (PrintModeSkipGeneral(d.tok, fileBeingPrinted)) { continue; }
+        if (d is OpaqueTypeDecl) {
+          var at = (OpaqueTypeDecl)d;
+          if (i++ != 0) { wr.WriteLine(); }
+          Indent(indent);
+          PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());
+          wr.Write(EqualitySupportSuffix(at.EqualitySupport));
+          wr.WriteLine();
+        } else if (d is NewtypeDecl) {
+          var dd = (NewtypeDecl)d;
+          if (i++ != 0) { wr.WriteLine(); }
+          Indent(indent);
+          PrintClassMethodHelper("newtype", dd.Attributes, dd.Name, new List<TypeParameter>());
+          wr.Write(" = ");
+          if (dd.Var == null) {
+            PrintType(dd.BaseType);
+          } else {
+            wr.Write(dd.Var.DisplayName);
+            if (!(dd.Var.Type is TypeProxy) || DafnyOptions.O.DafnyPrintResolvedFile != null) {
+              wr.Write(": ");
+              PrintType(dd.BaseType);
+            }
+            wr.Write(" | ");
+            PrintExpression(dd.Constraint, true);
+          }
+          wr.WriteLine();
+        } else if (d is TypeSynonymDecl) {
+          var syn = (TypeSynonymDecl)d;
+          if (i++ != 0) { wr.WriteLine(); }
+          Indent(indent);
+          PrintClassMethodHelper("type", syn.Attributes, syn.Name, syn.TypeArgs);
+          wr.Write(" = ");
+          PrintType(syn.Rhs);
+          wr.WriteLine();
+        } else if (d is DatatypeDecl) {
+          if (i++ != 0) { wr.WriteLine(); }
+          PrintDatatype((DatatypeDecl)d, indent);
+        } else if (d is IteratorDecl) {
+          var iter = (IteratorDecl)d;
+          PrintIteratorSignature(iter, indent);
+
+          if (iter.Body != null) {
+            Indent(indent);
+            PrintStatement(iter.Body, indent);
+            wr.WriteLine();
+          }
+
+          if (DafnyOptions.O.DafnyPrintResolvedFile != null) {
+            // also print the members that were created as part of the interpretation of the iterator
+            Contract.Assert(iter.Members.Count != 0);  // filled in during resolution
+            wr.WriteLine("/*---------- iterator members ----------");
+            PrintIteratorClass(iter, indent, fileBeingPrinted);
+            wr.WriteLine("---------- iterator members ----------*/");
+          }
+
+        } else if (d is ClassDecl) {
+          ClassDecl cl = (ClassDecl)d;
+          if (!cl.IsDefaultClass) {
+            if (i++ != 0) { wr.WriteLine(); }
+            PrintClass(cl, indent, fileBeingPrinted);
+          } else if (cl.Members.Count == 0) {
+            // print nothing
+          } else {
+            if (i++ != 0) { wr.WriteLine(); }
+            PrintMembers(cl.Members, indent, fileBeingPrinted);
+          }
+
+        } else if (d is ModuleDecl) {
+          wr.WriteLine();
+          Indent(indent);
+          if (d is LiteralModuleDecl) {
+            ModuleDefinition module = ((LiteralModuleDecl)d).ModuleDef;
+            PrintModuleDefinition(module, indent, fileBeingPrinted);
+          } else if (d is AliasModuleDecl) {
+            wr.Write("import"); if (((AliasModuleDecl)d).Opened) wr.Write(" opened");
+            wr.Write(" {0} ", ((AliasModuleDecl)d).Name);
+            wr.WriteLine("= {0}", Util.Comma(".", ((AliasModuleDecl)d).Path, id => id.val));
+          } else if (d is ModuleFacadeDecl) {
+            wr.Write("import"); if (((ModuleFacadeDecl)d).Opened) wr.Write(" opened");
+            wr.Write(" {0} ", ((ModuleFacadeDecl)d).Name);
+            wr.WriteLine("as {0}", Util.Comma(".", ((ModuleFacadeDecl)d).Path, id => id.val));
+          }
+
+        } else {
+          Contract.Assert(false);  // unexpected TopLevelDecl
+        }
+      }
+    }
+
+    void PrintModuleDefinition(ModuleDefinition module, int indent, string fileBeingPrinted) {
+      Contract.Requires(module != null);
+      Contract.Requires(0 <= indent);
+      if (module.IsAbstract) {
+        wr.Write("abstract ");
+      }
+      wr.Write("module");
+      PrintAttributes(module.Attributes);
+      wr.Write(" {0} ", module.Name);
+      if (module.RefinementBaseName != null) {
+        wr.Write("refines {0} ", Util.Comma(".", module.RefinementBaseName, id => id.val));
+      }
+      if (module.TopLevelDecls.Count == 0) {
+        wr.WriteLine("{ }");
+      } else {
+        wr.WriteLine("{");
+        PrintCallGraph(module, indent + IndentAmount);
+        PrintTopLevelDecls(module.TopLevelDecls, indent + IndentAmount, fileBeingPrinted);
+        Indent(indent);
+        wr.WriteLine("}");
+      }
+    }
+
+    void PrintIteratorSignature(IteratorDecl iter, int indent) {
+      Indent(indent);
+      PrintClassMethodHelper("iterator", iter.Attributes, iter.Name, iter.TypeArgs);
+      if (iter.SignatureIsOmitted) {
+        wr.WriteLine(" ...");
+      } else {
+        PrintFormals(iter.Ins);
+        if (iter.Outs.Count != 0) {
+          if (iter.Ins.Count + iter.Outs.Count <= 3) {
+            wr.Write(" yields ");
+          } else {
+            wr.WriteLine();
+            Indent(indent + 2 * IndentAmount);
+            wr.Write("yields ");
+          }
+          PrintFormals(iter.Outs);
+        }
+        wr.WriteLine();
+      }
+
+      int ind = indent + IndentAmount;
+      PrintSpec("requires", iter.Requires, ind);
+      if (iter.Reads.Expressions != null) {
+        PrintFrameSpecLine("reads", iter.Reads.Expressions, ind, iter.Reads.HasAttributes() ? iter.Reads.Attributes : null);
+      }
+      if (iter.Modifies.Expressions != null) {
+        PrintFrameSpecLine("modifies", iter.Modifies.Expressions, ind, iter.Modifies.HasAttributes() ? iter.Modifies.Attributes : null);
+      }
+      PrintSpec("yield requires", iter.YieldRequires, ind);
+      PrintSpec("yield ensures", iter.YieldEnsures, ind);
+      PrintSpec("ensures", iter.Ensures, ind);
+      PrintDecreasesSpec(iter.Decreases, ind);
+    }
+
+    private void PrintIteratorClass(IteratorDecl iter, int indent, string fileBeingPrinted) {
+      PrintClassMethodHelper("class", null, iter.Name, iter.TypeArgs);
+      wr.WriteLine(" {");
+      PrintMembers(iter.Members, indent + IndentAmount, fileBeingPrinted);
+      Indent(indent); wr.WriteLine("}");
+    }
+
+    public void PrintClass(ClassDecl c, int indent, string fileBeingPrinted) {
+      Contract.Requires(c != null);
+      Indent(indent);
+      PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
+      string sep = " extends ";
+      foreach (var trait in c.TraitsTyp) {
+        wr.Write(sep);
+        PrintType(trait);
+        sep = ", ";
+      }
+      if (c.Members.Count == 0) {
+        wr.WriteLine(" { }");
+      } else {
+        wr.WriteLine(" {");
+        PrintMembers(c.Members, indent + IndentAmount, fileBeingPrinted);
+        Indent(indent);
+        wr.WriteLine("}");
+      }
+    }
+
+    public void PrintMembers(List<MemberDecl> members, int indent, string fileBeingPrinted)
+    {
+      Contract.Requires(members != null);
+
+      int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
+      foreach (MemberDecl m in members) {
+        if (PrintModeSkipGeneral(m.tok, fileBeingPrinted)) { continue; }
+        if (m is Method) {
+          if (state != 0) { wr.WriteLine(); }
+          PrintMethod((Method)m, indent, false);
+          var com = m as FixpointLemma;
+          if (com != null && com.PrefixLemma != null) {
+            Indent(indent); wr.WriteLine("/***");
+            PrintMethod(com.PrefixLemma, indent, false);
+            Indent(indent); wr.WriteLine("***/");
+          }
+          state = 2;
+        } else if (m is Field) {
+          if (state == 2) { wr.WriteLine(); }
+          PrintField((Field)m, indent);
+          state = 1;
+        } else if (m is Function) {
+          if (state != 0) { wr.WriteLine(); }
+          PrintFunction((Function)m, indent, false);
+          var fixp = m as FixpointPredicate;
+          if (fixp != null && fixp.PrefixPredicate != null) {
+            Indent(indent); wr.WriteLine("/***");
+            PrintFunction(fixp.PrefixPredicate, indent, false);
+            Indent(indent); wr.WriteLine("***/");
+          }
+          state = 2;
+        } else {
+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member
+        }
+      }
+    }
+
+    /// <summary>
+    /// Prints no space before "kind", but does print a space before "attrs" and "name".
+    /// </summary>
+    void PrintClassMethodHelper(string kind, Attributes attrs, string name, List<TypeParameter> typeArgs) {
+      Contract.Requires(kind != null);
+      Contract.Requires(name != null);
+      Contract.Requires(typeArgs != null);
+      if (kind.Length != 0) {
+        wr.Write(kind);
+      }
+
+      PrintAttributes(attrs);
+
+      wr.Write(" {0}", name);
+      PrintTypeParams(typeArgs);
+    }
+
+    private void PrintTypeParams(List<TypeParameter> typeArgs) {
+      Contract.Requires(typeArgs != null);
+      if (typeArgs.Count != 0) {
+        wr.Write("<" +
+                 Util.Comma(", ", typeArgs,
+                   tp => tp.Name + EqualitySupportSuffix(tp.EqualitySupport))
+                 + ">");
+      }
+    }
+
+    private void PrintTypeInstantiation(List<Type> typeArgs) {
+      Contract.Requires(typeArgs == null || typeArgs.Count != 0);
+      if (typeArgs != null) {
+        wr.Write("<{0}>", Util.Comma(",", typeArgs, ty => ty.ToString()));
+      }
+    }
+
+    public void PrintDatatype(DatatypeDecl dt, int indent) {
+      Contract.Requires(dt != null);
+      Indent(indent);
+      PrintClassMethodHelper(dt is IndDatatypeDecl ? "datatype" : "codatatype", dt.Attributes, dt.Name, dt.TypeArgs);
+      wr.Write(" =");
+      string sep = "";
+      foreach (DatatypeCtor ctor in dt.Ctors) {
+        wr.Write(sep);
+        PrintClassMethodHelper("", ctor.Attributes, ctor.Name, new List<TypeParameter>());
+        if (ctor.Formals.Count != 0) {
+          PrintFormals(ctor.Formals);
+        }
+        sep = " |";
+      }
+      wr.WriteLine();
+    }
+
+    /// <summary>
+    /// Prints a space before each attribute.
+    /// </summary>
+    public void PrintAttributes(Attributes a) {
+      if (a != null) {
+        PrintAttributes(a.Prev);
+        wr.Write(" ");
+        PrintOneAttribute(a);
+      }
+    }
+    public void PrintOneAttribute(Attributes a, string nameSubstitution = null) {
+      Contract.Requires(a != null);
+      var name = nameSubstitution ?? a.Name;
+      var usAttribute = name.StartsWith("_");
+      wr.Write("{1}{{:{0}", name, usAttribute ? "/*" : "");
+      if (a.Args != null) {
+        PrintAttributeArgs(a.Args, false);
+      }
+      wr.Write("}}{0}", usAttribute ? "*/" : "");
+    }
+
+    public void PrintAttributeArgs(List<Expression> args, bool isFollowedBySemicolon) {
+      Contract.Requires(args != null);
+      string prefix = " ";
+      foreach (var arg in args) {
+        Contract.Assert(arg != null);
+        wr.Write(prefix);
+        prefix = ", ";
+        PrintExpression(arg, isFollowedBySemicolon);
+      }
+    }
+
+    public void PrintField(Field field, int indent) {
+      Contract.Requires(field != null);
+      Indent(indent);
+      if (field.IsGhost) {
+        wr.Write("ghost ");
+      }
+      wr.Write("var");
+      PrintAttributes(field.Attributes);
+      wr.Write(" {0}: ", field.Name);
+      PrintType(field.Type);
+      if (field.IsUserMutable) {
+        // nothing more to say
+      } else if (field.IsMutable) {
+        wr.Write("  // non-assignable");
+      } else {
+        wr.Write("  // immutable");
+      }
+      wr.WriteLine();
+    }
+
+    public void PrintFunction(Function f, int indent, bool printSignatureOnly) {
+      Contract.Requires(f != null);
+
+      if (PrintModeSkipFunctionOrMethod(f.IsGhost, f.Attributes, f.Name)) { return; }
+      var isPredicate = f is Predicate || f is PrefixPredicate;
+      Indent(indent);
+      string k = isPredicate ? "predicate" : f is InductivePredicate ? "inductive predicate" : f is CoPredicate ? "copredicate" : "function";
+      if (f.IsProtected) { k = "protected " + k; }
+      if (f.HasStaticKeyword) { k = "static " + k; }
+      if (!f.IsGhost) { k += " method"; }
+      PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);
+      if (f.SignatureIsOmitted) {
+        wr.WriteLine(" ...");
+      } else {
+        PrintFormals(f.Formals, f.Name);
+        if (!isPredicate) {
+          wr.Write(": ");
+          PrintType(f.ResultType);
+        }
+        wr.WriteLine();
+      }
+
+      int ind = indent + IndentAmount;
+      PrintSpec("requires", f.Req, ind);
+      PrintFrameSpecLine("reads", f.Reads, ind, null);
+      PrintSpec("ensures", f.Ens, ind);
+      PrintDecreasesSpec(f.Decreases, ind);
+      if (f.Body != null && !printSignatureOnly) {
+        Indent(indent);
+        wr.WriteLine("{");
+        PrintExtendedExpr(f.Body, ind, true, false);
+        Indent(indent);
+        wr.WriteLine("}");
+      }
+    }
+
+    // ----------------------------- PrintMethod -----------------------------
+
+    const int IndentAmount = 2; // The amount of indent for each new scope
+    const string BunchaSpaces = "                                ";
+    void Indent(int amount)
+    {
+      Contract.Requires(0 <= amount);
+
+      while (0 < amount) {
+        wr.Write(BunchaSpaces.Substring(0, amount));
+        amount -= BunchaSpaces.Length;
+      }
+    }
+
+    private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, string name)
+    {
+      if (printMode == DafnyOptions.PrintModes.NoGhost && IsGhost)
+          { return true; }
+      if (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)
+      {
+          bool verify = true;
+          if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify)
+          { return true; }
+          if (name.Contains("INTERNAL") || name.StartsWith("reveal_"))
+          { return true; }
+      }
+      return false;
+    }
+
+    private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted)
+    {
+        return (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)
+               && (tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted);
+    }
+
+    public void PrintMethod(Method method, int indent, bool printSignatureOnly) {
+      Contract.Requires(method != null);
+
+      if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; }
+      Indent(indent);
+      string k = method is Constructor ? "constructor" :
+        method is InductiveLemma ? "inductive lemma" :
+        method is CoLemma ? "colemma" :
+        method is Lemma ? "lemma" :
+        "method";
+      if (method.HasStaticKeyword) { k = "static " + k; }
+      if (method.IsGhost && !(method is Lemma) && !(method is FixpointLemma)) { k = "ghost " + k; }
+      string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;
+      PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs);
+      if (method.SignatureIsOmitted) {
+        wr.WriteLine(" ...");
+      } else {
+        PrintFormals(method.Ins, method.Name);
+        if (method.Outs.Count != 0) {
+          if (method.Ins.Count + method.Outs.Count <= 3) {
+            wr.Write(" returns ");
+          } else {
+            wr.WriteLine();
+            Indent(indent + 2 * IndentAmount);
+            wr.Write("returns ");
+          }
+          PrintFormals(method.Outs);
+        }
+        wr.WriteLine();
+      }
+
+      int ind = indent + IndentAmount;
+      PrintSpec("requires", method.Req, ind);
+      if (method.Mod.Expressions != null)
+      {
+        PrintFrameSpecLine("modifies", method.Mod.Expressions, ind, method.Mod.HasAttributes() ? method.Mod.Attributes : null);
+      }
+      PrintSpec("ensures", method.Ens, ind);
+      PrintDecreasesSpec(method.Decreases, ind);
+
+      if (method.Body != null && !printSignatureOnly) {
+        Indent(indent);
+        PrintStatement(method.Body, indent);
+        wr.WriteLine();
+      }
+    }
+
+    internal void PrintFormals(List<Formal> ff, string name = null) {
+      Contract.Requires(ff != null);
+      if (name != null && name.EndsWith("#")) {
+        wr.Write("[");
+        PrintFormal(ff[0]);
+        wr.Write("]");
+        ff = new List<Formal>(ff.Skip(1));
+      }
+      wr.Write("(");
+      string sep = "";
+      foreach (Formal f in ff) {
+        Contract.Assert(f != null);
+        wr.Write(sep);
+        sep = ", ";
+        PrintFormal(f);
+      }
+      wr.Write(")");
+    }
+
+    void PrintFormal(Formal f) {
+      Contract.Requires(f != null);
+      if (f.IsGhost) {
+        wr.Write("ghost ");
+      }
+      if (f.HasName) {
+        wr.Write("{0}: ", f.DisplayName);
+      }
+      PrintType(f.Type);
+    }
+
+    internal void PrintSpec(string kind, List<Expression> ee, int indent) {
+      Contract.Requires(kind != null);
+      Contract.Requires(ee != null);
+      foreach (Expression e in ee) {
+        Contract.Assert(e != null);
+        Indent(indent);
+        wr.Write("{0} ", kind);
+        PrintExpression(e, true);
+        wr.WriteLine();
+      }
+    }
+
+    internal void PrintDecreasesSpec(Specification<Expression> decs, int indent, bool newLine = true) {
+      Contract.Requires(decs != null);
+      if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }
+      if (decs.Expressions != null && decs.Expressions.Count != 0) {
+        Indent(indent);
+        wr.Write("decreases");
+        if (decs.HasAttributes())
+        {
+          PrintAttributes(decs.Attributes);
+        }
+        wr.Write(" ");
+        PrintExpressionList(decs.Expressions, true);
+        if (newLine) {
+          wr.WriteLine();
+        } else {
+          wr.Write(" ");
+        }
+      }
+    }
+
+    internal void PrintFrameSpecLine(string kind, List<FrameExpression/*!*/> ee, int indent, Attributes attrs, bool newLine = true) {
+      Contract.Requires(kind != null);
+      Contract.Requires(cce.NonNullElements(ee));
+      if (ee != null && ee.Count != 0) {
+        Indent(indent);
+        wr.Write("{0}", kind);
+        if (attrs != null) {
+          PrintAttributes(attrs);
+        }
+        wr.Write(" ");
+        PrintFrameExpressionList(ee);
+        if (newLine) {
+          wr.WriteLine();
+        } else {
+          wr.Write(" ");
+        }
+      }
+    }
+
+    internal void PrintSpec(string kind, List<MaybeFreeExpression> ee, int indent, bool newLine = true) {
+      Contract.Requires(kind != null);
+      Contract.Requires(ee != null);
+      if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }
+      foreach (MaybeFreeExpression e in ee)
+      {
+        Contract.Assert(e != null);
+        Indent(indent);
+        wr.Write("{0}{1}", e.IsFree ? "free " : "", kind);
+
+        if (e.HasAttributes())
+        {
+          PrintAttributes(e.Attributes);
+        }
+
+        wr.Write(" ");
+        PrintExpression(e.E, true);
+        if (newLine) {
+          wr.WriteLine();
+        } else {
+          wr.Write(" ");
+        }
+      }
+    }
+
+    // ----------------------------- PrintType -----------------------------
+
+    public void PrintType(Type ty) {
+      Contract.Requires(ty != null);
+      wr.Write(ty.ToString());
+    }
+
+    public void PrintType(string prefix, Type ty) {
+      Contract.Requires(prefix != null);
+      Contract.Requires(ty != null);
+      string s = ty.ToString();
+      if (s != "?") {
+        wr.Write("{0}{1}", prefix, s);
+      }
+    }
+
+    string EqualitySupportSuffix(TypeParameter.EqualitySupportValue es) {
+      if (es == TypeParameter.EqualitySupportValue.Required ||
+        (es == TypeParameter.EqualitySupportValue.InferredRequired && DafnyOptions.O.DafnyPrintResolvedFile != null)) {
+        return "(==)";
+      } else {
+        return "";
+      }
+    }
+
+    // ----------------------------- PrintStatement -----------------------------
+
+    /// <summary>
+    /// Prints from the current position of the current line.
+    /// If the statement requires several lines, subsequent lines are indented at "indent".
+    /// No newline is printed after the statement.
+    /// </summary>
+    public void PrintStatement(Statement stmt, int indent) {
+      Contract.Requires(stmt != null);
+
+      if (stmt.IsGhost && printMode == DafnyOptions.PrintModes.NoGhost) { return; }
+      for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {
+        if (label.Data.Name != null) {
+          wr.WriteLine("label {0}:", label.Data.Name);
+          Indent(indent);
+        }
+      }
+
+      if (stmt is PredicateStmt) {
+        if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }
+        Expression expr = ((PredicateStmt)stmt).Expr;
+        wr.Write(stmt is AssertStmt ? "assert" : "assume");
+        if (stmt.Attributes != null) {
+          PrintAttributes(stmt.Attributes);
+        }
+        wr.Write(" ");
+        PrintExpression(expr, true);
+        wr.Write(";");
+
+      } else if (stmt is PrintStmt) {
+        PrintStmt s = (PrintStmt)stmt;
+        wr.Write("print");
+        PrintAttributeArgs(s.Args, true);
+        wr.Write(";");
+
+      } else if (stmt is BreakStmt) {
+        BreakStmt s = (BreakStmt)stmt;
+        if (s.TargetLabel != null) {
+          wr.Write("break {0};", s.TargetLabel);
+        } else {
+          string sep = "";
+          for (int i = 0; i < s.BreakCount; i++) {
+            wr.Write("{0}break", sep);
+            sep = " ";
+          }
+          wr.Write(";");
+        }
+
+      } else if (stmt is ProduceStmt) {
+        var s = (ProduceStmt) stmt;
+        wr.Write(s is YieldStmt ? "yield" : "return");
+        if (s.rhss != null) {
+          var sep = " ";
+          foreach (var rhs in s.rhss) {
+            wr.Write(sep);
+            PrintRhs(rhs);
+            sep = ", ";
+          }
+        }
+          wr.Write(";");
+
+      } else if (stmt is AssignStmt) {
+        AssignStmt s = (AssignStmt)stmt;
+        PrintExpression(s.Lhs, true);
+        wr.Write(" := ");
+        PrintRhs(s.Rhs);
+        wr.Write(";");
+
+      } else if (stmt is BlockStmt) {
+        wr.WriteLine("{");
+        int ind = indent + IndentAmount;
+        foreach (Statement s in ((BlockStmt)stmt).Body) {
+          Indent(ind);
+          PrintStatement(s, ind);
+          wr.WriteLine();
+        }
+        Indent(indent);
+        wr.Write("}");
+
+      } else if (stmt is IfStmt) {
+        IfStmt s = (IfStmt)stmt;
+        PrintIfStatement(indent, s, false);
+
+      } else if (stmt is AlternativeStmt) {
+        var s = (AlternativeStmt)stmt;
+        wr.WriteLine("if {");
+        PrintAlternatives(indent, s.Alternatives);
+        Indent(indent);
+        wr.Write("}");
+
+      } else if (stmt is WhileStmt) {
+        WhileStmt s = (WhileStmt)stmt;
+        PrintWhileStatement(indent, s, false, false);
+
+      } else if (stmt is AlternativeLoopStmt) {
+        var s = (AlternativeLoopStmt)stmt;
+        wr.WriteLine("while");
+        PrintSpec("invariant", s.Invariants, indent + IndentAmount);
+        PrintDecreasesSpec(s.Decreases, indent + IndentAmount);
+
+        Indent(indent);
+        wr.WriteLine("{");
+        PrintAlternatives(indent, s.Alternatives);
+        Indent(indent);
+        wr.Write("}");
+
+      } else if (stmt is ForallStmt) {
+        var s = (ForallStmt)stmt;
+        wr.Write("forall");
+        if (s.BoundVars.Count != 0) {
+          wr.Write(" ");
+          PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
+        }
+        if (s.Ens.Count == 0) {
+          wr.Write(" ");
+        } else {
+          wr.WriteLine();
+          PrintSpec("ensures", s.Ens, indent + IndentAmount, s.Body != null);
+          Indent(indent);
+        }
+        if (s.Body != null) {
+          PrintStatement(s.Body, indent);
+        }
+
+      } else if (stmt is ModifyStmt) {
+        var s = (ModifyStmt)stmt;
+        PrintModifyStmt(indent, s, false);
+
+      } else if (stmt is CalcStmt) {
+        CalcStmt s = (CalcStmt)stmt;
+        if (printMode == DafnyOptions.PrintModes.NoGhost) { return; }   // Calcs don't get a "ghost" attribute, but they are.
+        wr.Write("calc ");
+        if (!s.Op.Equals(CalcStmt.DefaultOp)) {
+          PrintCalcOp(s.Op);
+          wr.Write(" ");
+        }
+        wr.WriteLine("{");
+        int lineInd = indent + IndentAmount;
+        int lineCount = s.Lines.Count == 0 ? 0 : s.Lines.Count - 1;  // if nonempty, .Lines always contains a duplicated last line
+        // The number of op/hints is commonly one less than the number of lines, but
+        // it can also equal the number of lines for empty calc's and for calc's with
+        // a dangling hint.
+        int hintCount = s.Lines.Count != 0 && s.Hints.Last().Body.Count == 0 ? lineCount - 1 : lineCount;
+        for (var i = 0; i < lineCount; i++) {
+          var e = s.Lines[i];
+          var op = s.StepOps[i];
+          var h = s.Hints[i];
+          // print the line
+          Indent(lineInd);
+          PrintExpression(e, true, lineInd);
+          wr.WriteLine(";");
+          if (i == hintCount) {
+            break;
+          }
+          // print the operator, if any
+          if (!s.Op.Equals(op)) {
+            Indent(indent);  // this lines up with the "calc"
+            PrintCalcOp(op);
+            wr.WriteLine();
+          }
+          // print the hints
+          foreach (var st in h.Body) {
+            Indent(lineInd);
+            PrintStatement(st, lineInd);
+            wr.WriteLine();
+          }
+        }
+        Indent(indent);
+        wr.Write("}");
+
+      } else if (stmt is MatchStmt) {
+        MatchStmt s = (MatchStmt)stmt;
+        wr.Write("match ");
+        PrintExpression(s.Source, false);
+        if (s.UsesOptionalBraces) {
+          wr.Write(" {");
+        }
+        int caseInd = indent + (s.UsesOptionalBraces ? IndentAmount : 0);
+        foreach (MatchCaseStmt mc in s.Cases) {
+          wr.WriteLine();
+          Indent(caseInd);
+          wr.Write("case {0}", mc.Id);
+          PrintMatchCaseArgument(mc);
+          wr.Write(" =>");
+          foreach (Statement bs in mc.Body) {
+            wr.WriteLine();
+            Indent(caseInd + IndentAmount);
+            PrintStatement(bs, caseInd + IndentAmount);
+          }
+        }
+        if (s.UsesOptionalBraces) {
+          wr.WriteLine();
+          Indent(indent);
+          wr.Write("}");
+        }
+
+      } else if (stmt is ConcreteUpdateStatement) {
+        var s = (ConcreteUpdateStatement)stmt;
+        string sep = "";
+        foreach (var lhs in s.Lhss) {
+          wr.Write(sep);
+          PrintExpression(lhs, true);
+          sep = ", ";
+        }
+        PrintUpdateRHS(s);
+        wr.Write(";");
+
+      } else if (stmt is VarDeclStmt) {
+        var s = (VarDeclStmt)stmt;
+        if (s.Locals.Exists(v => v.IsGhost) && printMode == DafnyOptions.PrintModes.NoGhost) { return; }
+        if (s.Locals.Exists(v => v.IsGhost)) {
+          wr.Write("ghost ");
+        }
+        wr.Write("var");
+        string sep = "";
+        foreach (var local in s.Locals) {
+          wr.Write(sep);
+          if (local.Attributes != null) {
+            PrintAttributes(local.Attributes);
+          }
+          wr.Write(" {0}", local.DisplayName);
+          PrintType(": ", local.OptionalType);
+          sep = ",";
+        }
+        if (s.Update != null) {
+          PrintUpdateRHS(s.Update);
+        }
+        wr.Write(";");
+
+      } else if (stmt is SkeletonStatement) {
+        var s = (SkeletonStatement)stmt;
+        if (s.S == null) {
+          wr.Write("...;");
+        } 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) {
+          PrintWhileStatement(indent, (WhileStmt)s.S, s.ConditionOmitted, s.BodyOmitted);
+        } else if (s.S is ModifyStmt) {
+          PrintModifyStmt(indent, (ModifyStmt)s.S, true);
+        } else {
+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected skeleton statement
+        }
+
+      } else {
+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
+      }
+    }
+
+    private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {
+      Contract.Requires(0 <= indent);
+      Contract.Requires(s != null);
+      Contract.Requires(!omitFrame || s.Mod.Expressions.Count == 0);
+
+      wr.Write("modify");
+      PrintAttributes(s.Mod.Attributes);
+      wr.Write(" ");
+      if (omitFrame) {
+        wr.Write("...");
+      } else {
+        PrintFrameExpressionList(s.Mod.Expressions);
+      }
+      if (s.Body != null) {
+        // There's a possible syntactic ambiguity, namely if the frame is empty (more precisely,
+        // if s.Mod.Expressions.Count is 0).  Since the statement was parsed at some point, this
+        // situation can occur only if the modify statement inherited its frame by refinement
+        // and we're printing the post-resolve AST.  In this special case, print an explicit
+        // empty set as the frame.
+        if (s.Mod.Expressions.Count == 0) {
+          wr.Write(" {}");
+        }
+        wr.Write(" ");
+        PrintStatement(s.Body, indent);
+      } else {
+        wr.Write(";");
+      }
+    }
+
+    /// <summary>
+    /// Does not print LHS
+    /// </summary>
+    void PrintUpdateRHS(ConcreteUpdateStatement s) {
+      Contract.Requires(s != null);
+      if (s is UpdateStmt) {
+        var update = (UpdateStmt)s;
+        if (update.Lhss.Count != 0) {
+          wr.Write(" := ");
+        }
+        var sep = "";
+        foreach (var rhs in update.Rhss) {
+          wr.Write(sep);
+          PrintRhs(rhs);
+          sep = ", ";
+        }
+      } else if (s is AssignSuchThatStmt) {
+        var update = (AssignSuchThatStmt)s;
+        wr.Write(" :| ");
+        if (update.AssumeToken != null) {
+          wr.Write("assume ");
+        }
+        PrintExpression(update.Expr, true);
+      } else {
+        Contract.Assert(s == null);  // otherwise, unknown type
+      }
+    }
+
+    void PrintIfStatement(int indent, IfStmt s, bool omitGuard) {
+      while (true) {
+        if (omitGuard) {
+          wr.Write("if ... ");
+        } else {
+          wr.Write("if ");
+          PrintGuard(s.Guard);
+          wr.Write(" ");
+        }
+        PrintStatement(s.Thn, indent);
+        if (s.Els == null) {
+          break;
+        }
+        wr.Write(" else ");
+        if (s.Els is IfStmt) {
+          s = (IfStmt)s.Els;
+        } else {
+          PrintStatement(s.Els, indent);
+          break;
+        }
+      }
+    }
+
+    void PrintWhileStatement(int indent, WhileStmt s, bool omitGuard, bool omitBody) {
+      Contract.Requires(0 <= indent);
+      if (omitGuard) {
+        wr.WriteLine("while ...");
+      } else {
+        wr.Write("while ");
+        PrintGuard(s.Guard);
+        wr.WriteLine();
+      }
+
+      PrintSpec("invariant", s.Invariants, indent + IndentAmount, s.Body != null || omitBody || (s.Decreases.Expressions != null && s.Decreases.Expressions.Count != 0) || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0));
+      PrintDecreasesSpec(s.Decreases, indent + IndentAmount, s.Body != null || omitBody || (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0));
+      if (s.Mod.Expressions != null) {
+        PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null, s.Body != null || omitBody);
+      }
+      Indent(indent);
+      if (omitBody) {
+        wr.WriteLine("...;");
+      } else if (s.Body != null) {
+        PrintStatement(s.Body, indent);
+      }
+    }
+
+    void PrintAlternatives(int indent, List<GuardedAlternative> alternatives) {
+      int caseInd = indent + IndentAmount;
+      foreach (var alternative in alternatives) {
+        Indent(caseInd);
+        wr.Write("case ");
+        PrintExpression(alternative.Guard, false);
+        wr.WriteLine(" =>");
+        foreach (Statement s in alternative.Body) {
+          Indent(caseInd + IndentAmount);
+          PrintStatement(s, caseInd + IndentAmount);
+          wr.WriteLine();
+        }
+      }
+    }
+
+    void PrintRhs(AssignmentRhs rhs) {
+      Contract.Requires(rhs != null);
+      if (rhs is ExprRhs) {
+        PrintExpression(((ExprRhs)rhs).Expr, true);
+      } else if (rhs is HavocRhs) {
+        wr.Write("*");
+      } else if (rhs is TypeRhs) {
+        TypeRhs t = (TypeRhs)rhs;
+        wr.Write("new ");
+        if (t.ArrayDimensions != null) {
+          PrintType(t.EType);
+          string s = "[";
+          foreach (Expression dim in t.ArrayDimensions) {
+            Contract.Assume(dim != null);
+            wr.Write(s);
+            PrintExpression(dim, false);
+            s = ", ";
+          }
+          wr.Write("]");
+        } else if (t.Arguments == null) {
+          PrintType(t.EType);
+        } else {
+          PrintType(t.Path);
+          wr.Write("(");
+          PrintExpressionList(t.Arguments, false);
+          wr.Write(")");
+        }
+      } else {
+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS
+      }
+
+      if (rhs.HasAttributes())
+      {
+        PrintAttributes(rhs.Attributes);
+      }
+    }
+
+    void PrintGuard(Expression guard) {
+      if (guard == null) {
+        wr.Write("*");
+      } else {
+        PrintExpression(guard, false);
+      }
+    }
+
+    void PrintCalcOp(CalcStmt.CalcOp op) {
+      Contract.Requires(op != null);
+      wr.Write(op.ToString());
+      if (op is CalcStmt.TernaryCalcOp) {
+        wr.Write("[");
+        PrintExpression(((CalcStmt.TernaryCalcOp) op).Index, false);
+        wr.Write("]");
+      }
+    }
+
+    // ----------------------------- PrintExpression -----------------------------
+
+    /// <summary>
+    /// PrintExtendedExpr prints an expression, but formats top-level if-then-else and match expressions across several lines.
+    /// Its intended use is thus to print the body of a function.
+    /// </summary>
+    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {
+      Contract.Requires(expr != null);
+      if (expr is ITEExpr) {
+        Indent(indent);
+        while (true) {
+          var ite = (ITEExpr)expr;
+          wr.Write("if ");
+          PrintExpression(ite.Test, false);
+          wr.WriteLine(" then");
+          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);
+          expr = ite.Els;
+          if (expr is ITEExpr) {
+            Indent(indent);  wr.Write("else ");
+          } else {
+            Indent(indent);  wr.WriteLine("else");
+            Indent(indent + IndentAmount);
+            PrintExpression(expr, isRightmost, false);
+            wr.WriteLine(endWithCloseParen ? ")" : "");
+            return;
+          }
+        }
+      } else if (expr is MatchExpr) {
+        var e = (MatchExpr)expr;
+        Indent(indent);
+        var parensNeeded = !isRightmost && !e.UsesOptionalBraces;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write("match ");
+        PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, false);
+        if (e.UsesOptionalBraces) { wr.WriteLine(" {"); }
+        else if (parensNeeded && e.Cases.Count == 0) { wr.WriteLine(")"); }
+        else { wr.WriteLine(); }
+        int i = 0;
+        int ind = indent + (e.UsesOptionalBraces ? IndentAmount : 0);
+        foreach (var mc in e.Cases) {
+          bool isLastCase = i == e.Cases.Count - 1;
+          Indent(ind);
+          wr.Write("case {0}", mc.Id);
+          PrintMatchCaseArgument(mc);          
+          wr.WriteLine(" =>");
+          PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));
+          i++;
+        }
+        if (e.UsesOptionalBraces) {
+          Indent(indent);
+          wr.WriteLine("}");
+        }
+      } else if (expr is LetExpr) {
+        var e = (LetExpr)expr;
+        Indent(indent);
+        wr.Write("var ");
+        string sep = "";
+        foreach (var lhs in e.LHSs) {
+          wr.Write(sep);
+          PrintCasePattern(lhs);
+          sep = ", ";
+        }
+        if (e.Exact) {
+          wr.Write(" := ");
+        } else {
+          wr.Write(" :| ");
+        }
+        PrintExpressionList(e.RHSs, true);
+        wr.WriteLine(";");
+        PrintExtendedExpr(e.Body, indent, isRightmost, endWithCloseParen);
+
+      } else if (expr is ParensExpression) {
+        PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen);
+      } else {
+        Indent(indent);
+        PrintExpression(expr, false, indent);
+        wr.WriteLine(endWithCloseParen ? ")" : "");
+      }
+    }
+
+    public void PrintMatchCaseArgument(MatchCase mc) {
+      if (mc.Arguments != null) {
+        if (mc.Arguments.Count != 0) {
+          string sep = "(";
+          foreach (BoundVar bv in mc.Arguments) {
+            wr.Write("{0}{1}", sep, bv.DisplayName);
+            if (bv.Type is NonProxyType) {
+              wr.Write(": {0}", bv.Type);
+            }
+            sep = ", ";
+          }
+          wr.Write(")");
+        }
+      } else {
+        Contract.Assert(mc.CasePatterns != null);
+        if (mc.CasePatterns.Count != 0) {
+          string sep = "(";
+          foreach (var cp in mc.CasePatterns) {
+            wr.Write(sep);
+            PrintCasePattern(cp);
+            sep = ", ";
+          }
+          wr.Write(")");
+        }
+      }
+    }
+
+    public void PrintExpression(Expression expr, bool isFollowedBySemicolon) {
+      Contract.Requires(expr != null);
+      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1);
+    }
+
+    public void PrintExpression(Expression expr, bool isRightmost, bool isFollowedBySemicolon) {
+      Contract.Requires(expr != null);
+      PrintExpr(expr, 0, false, isRightmost, isFollowedBySemicolon, -1);
+    }
+
+    /// <summary>
+    /// An indent of -1 means print the entire expression on one line.
+    /// </summary>
+    public void PrintExpression(Expression expr, bool isFollowedBySemicolon, int indent) {
+      Contract.Requires(expr != null);
+      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, indent);
+    }
+
+    private bool ParensNeeded(int opBindingStrength, int contextBindingStrength, bool fragileContext) {
+      return opBindingStrength < contextBindingStrength ||
+             (fragileContext && opBindingStrength == contextBindingStrength);
+    }
+
+    /// <summary>
+    /// An indent of -1 means print the entire expression on one line.
+    /// </summary>
+    void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, bool isRightmost, bool isFollowedBySemicolon, int indent, int resolv_count = 2)
+    {
+      Contract.Requires(-1 <= indent);
+      Contract.Requires(expr != null);
+
+      /* When debugging:
+      if (resolv_count > 0 && expr.Resolved != null) {
+        PrintExpr(expr.Resolved, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count - 1);
+        return;
+      }
+      */
+
+      if (expr is StaticReceiverExpr) {
+        StaticReceiverExpr e = (StaticReceiverExpr)expr;
+        wr.Write(e.Type);
+      } else if (expr is LiteralExpr) {
+        LiteralExpr e = (LiteralExpr)expr;
+        if (e.Value == null) {
+          wr.Write("null");
+        } else if (e.Value is bool) {
+          wr.Write((bool)e.Value ? "true" : "false");
+        } else if (e is CharLiteralExpr) {
+          wr.Write("'{0}'", (string)e.Value);
+        } else if (e is StringLiteralExpr) {
+          var str = (StringLiteralExpr)e;
+          wr.Write("{0}\"{1}\"", str.IsVerbatim ? "@" : "", (string)e.Value);
+        } else if (e.Value is Basetypes.BigDec) {
+          Basetypes.BigDec dec = (Basetypes.BigDec)e.Value;
+          wr.Write((dec.Mantissa >= 0) ? "" : "-");
+          string s = BigInteger.Abs(dec.Mantissa).ToString();
+          int digits = s.Length;
+          if (dec.Exponent >= 0) {
+            wr.Write("{0}{1}.0", s, new string('0', dec.Exponent));
+          } else {
+            int exp = -dec.Exponent;
+            if (exp < digits) {
+              int intDigits = digits - exp;
+              int fracDigits = digits - intDigits;
+              wr.Write("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
+            } else {
+              int fracDigits = digits;
+              wr.Write("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
+            }
+          }
+        } else {
+          wr.Write((BigInteger)e.Value);
+        }
+
+      } else if (expr is ThisExpr) {
+        wr.Write("this");
+
+      } else if (expr is IdentifierExpr) {
+        wr.Write(((IdentifierExpr)expr).Name);
+
+      } else if (expr is DatatypeValue) {
+        var dtv = (DatatypeValue)expr;
+        bool printParens;
+        if (dtv.MemberName == BuiltIns.TupleTypeCtorName) {
+          // we're looking at a tuple, whose printed constructor name is essentially the empty string
+          printParens = true;
+        } else {
+          wr.Write("{0}.{1}", dtv.DatatypeName, dtv.MemberName);
+          printParens = dtv.Arguments.Count != 0;
+        }
+        if (printParens) {
+          wr.Write("(");
+          PrintExpressionList(dtv.Arguments, false);
+          wr.Write(")");
+        }
+
+      } else if (expr is DisplayExpression) {
+        DisplayExpression e = (DisplayExpression)expr;
+        if (e is MultiSetDisplayExpr) {
+          wr.Write("multiset");
+        } else if (e is SetDisplayExpr && !((SetDisplayExpr)e).Finite) {
+          wr.Write("iset");
+        }
+        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "{" : "[");
+        PrintExpressionList(e.Elements, false);
+        wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");
+
+      } else if (expr is MapDisplayExpr) {
+        MapDisplayExpr e = (MapDisplayExpr)expr;
+        wr.Write(e.Finite ? "map" : "imap");
+        wr.Write("[");
+        PrintExpressionPairList(e.Elements);
+        wr.Write("]");
+
+      } else if (expr is NameSegment) {
+        var e = (NameSegment)expr;
+        wr.Write(e.Name);
+        PrintTypeInstantiation(e.OptTypeArguments);
+
+      } else if (expr is ExprDotName) {
+        var e = (ExprDotName)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = !e.Lhs.IsImplicit && // KRML: I think that this never holds
+          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        if (!e.Lhs.IsImplicit) {
+          PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+          wr.Write(".");
+        }
+        wr.Write(e.SuffixName);
+        PrintTypeInstantiation(e.OptTypeArguments);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is ApplySuffix) {
+        var e = (ApplySuffix)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = !e.Lhs.IsImplicit &&  // KRML: I think that this never holds
+          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        if (ParensMayMatter(e.Lhs)) {
+          wr.Write("(");
+          PrintExpression(e.Lhs, false);
+          wr.Write(")");
+        } else {
+          PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+        }
+        wr.Write("(");
+        PrintExpressionList(e.Args, false);
+        wr.Write(")");
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is MemberSelectExpr) {
+        MemberSelectExpr e = (MemberSelectExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = !e.Obj.IsImplicit &&
+          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        if (!(e.Obj.IsImplicit)) {
+          PrintExpr(e.Obj, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+          wr.Write(".");
+        }
+        wr.Write(e.MemberName);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is SeqSelectExpr) {
+        SeqSelectExpr e = (SeqSelectExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+        wr.Write("[");
+        if (e.SelectOne) {
+          Contract.Assert( e.E0 != null);
+          PrintExpression(e.E0, false);
+        } else {
+          if (e.E0 != null) {
+            PrintExpression(e.E0, false);
+          }
+          wr.Write(e.E0 != null && e.E1 != null ? " .. " : "..");
+          if (e.E1 != null) {
+            PrintExpression(e.E1, false);
+          }
+        }
+        wr.Write("]");
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is MultiSelectExpr) {
+        MultiSelectExpr e = (MultiSelectExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        PrintExpr(e.Array, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+        string prefix = "[";
+        foreach (Expression idx in e.Indices) {
+          Contract.Assert(idx != null);
+          wr.Write(prefix);
+          PrintExpression(idx, false);
+          prefix = ", ";
+        }
+        wr.Write("]");
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is SeqUpdateExpr) {
+        SeqUpdateExpr e = (SeqUpdateExpr)expr;
+        if (e.ResolvedUpdateExpr != null)
+        {
+          PrintExpr(e.ResolvedUpdateExpr, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+        }
+        else
+        {
+          // determine if parens are needed
+          int opBindingStrength = 0x70;
+          bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+          if (parensNeeded) { wr.Write("("); }
+          PrintExpr(e.Seq, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);
+          wr.Write("[");
+          PrintExpression(e.Index, false);
+          wr.Write(" := ");
+          PrintExpression(e.Value, false);
+          wr.Write("]");
+          if (parensNeeded) { wr.Write(")"); }
+        }
+      } else if (expr is ApplyExpr) {
+        var e = (ApplyExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+
+        PrintExpr(e.Function, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+        wr.Write("(");
+        PrintExpressionList(e.Args, false);
+        wr.Write(")");
+
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is FunctionCallExpr) {
+        var e = (FunctionCallExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x70;
+        bool parensNeeded = !(e.Receiver.IsImplicit) &&
+          ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        if (parensNeeded) { wr.Write("("); }
+        if (!e.Receiver.IsImplicit) {
+          PrintExpr(e.Receiver, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1);
+          wr.Write(".");
+        }
+        wr.Write(e.Name);
+        /* When debugging, this is nice to have:
+        if (e.TypeArgumentSubstitutions.Count > 0) {
+          wr.Write("[");
+          wr.Write(Util.Comma(",", e.TypeArgumentSubstitutions, kv => kv.Key.FullName() + "->" + kv.Value));
+          wr.Write("]");
+        }
+        */
+        if (e.OpenParen == null && e.Args.Count == 0) {
+        } else {
+          PrintActualArguments(e.Args, e.Name);
+        }
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is OldExpr) {
+        wr.Write("old(");
+        PrintExpression(((OldExpr)expr).E, false);
+        wr.Write(")");
+
+      } else if (expr is MultiSetFormingExpr) {
+        wr.Write("multiset(");
+        PrintExpression(((MultiSetFormingExpr)expr).E, false);
+        wr.Write(")");
+
+      } else if (expr is UnaryOpExpr) {
+        var e = (UnaryOpExpr)expr;
+        if (e.Op == UnaryOpExpr.Opcode.Cardinality) {
+          wr.Write("|");
+          PrintExpression(e.E, false);
+          wr.Write("|");
+        } else if (e.Op == UnaryOpExpr.Opcode.Fresh) {
+          wr.Write("fresh(");
+          PrintExpression(e.E, false);
+          wr.Write(")");
+        } else {
+          // Prefix operator.
+          // determine if parens are needed
+          string op;
+          int opBindingStrength;
+          switch (e.Op) {
+            case UnaryOpExpr.Opcode.Not:
+              op = "!";  opBindingStrength = 0x60;  break;
+            default:
+              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary opcode
+          }
+          bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+          bool containsNestedNot = e.E is ParensExpression &&
+                                ((ParensExpression)e.E).E is UnaryExpr &&
+                                ((UnaryOpExpr)((ParensExpression)e.E).E).Op == UnaryOpExpr.Opcode.Not;
+
+          if (parensNeeded) { wr.Write("("); }
+          wr.Write(op);
+          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);
+          if (parensNeeded) { wr.Write(")"); }
+        }
+
+      } else if (expr is ConversionExpr) {
+        var e = (ConversionExpr)expr;
+        PrintType(e.ToType);
+        wr.Write("(");
+        PrintExpression(e.E, false);
+        wr.Write(")");
+
+      } else if (expr is BinaryExpr) {
+        BinaryExpr e = (BinaryExpr)expr;
+        // determine if parens are needed
+        int opBindingStrength;
+        bool fragileLeftContext = false;  // false means "allow same binding power on left without parens"
+        bool fragileRightContext = false;  // false means "allow same binding power on right without parens"
+        switch (e.Op)
+        {
+          case BinaryExpr.Opcode.Add:
+            opBindingStrength = 0x40; break;
+          case BinaryExpr.Opcode.Sub:
+            opBindingStrength = 0x40; fragileRightContext = true; break;
+          case BinaryExpr.Opcode.Mul:
+            opBindingStrength = 0x50; break;
+          case BinaryExpr.Opcode.Div:
+          case BinaryExpr.Opcode.Mod:
+            opBindingStrength = 0x50; fragileRightContext = true; break;
+          case BinaryExpr.Opcode.Eq:
+          case BinaryExpr.Opcode.Neq:
+          case BinaryExpr.Opcode.Gt:
+          case BinaryExpr.Opcode.Ge:
+          case BinaryExpr.Opcode.Lt:
+          case BinaryExpr.Opcode.Le:
+          case BinaryExpr.Opcode.Disjoint:
+          case BinaryExpr.Opcode.In:
+          case BinaryExpr.Opcode.NotIn:
+            opBindingStrength = 0x30; fragileLeftContext = fragileRightContext = true; break;
+          case BinaryExpr.Opcode.And:
+            opBindingStrength = 0x20; break;
+          case BinaryExpr.Opcode.Or:
+            opBindingStrength = 0x21; break;
+          case BinaryExpr.Opcode.Imp:
+            opBindingStrength = 0x10; fragileLeftContext = true; break;
+          case BinaryExpr.Opcode.Exp:
+            opBindingStrength = 0x11; fragileRightContext = true; break;
+          case BinaryExpr.Opcode.Iff:
+            opBindingStrength = 0x08; break;
+          default:
+            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary operator
+        }
+        int opBS = opBindingStrength & 0xF8;
+        int ctxtBS = contextBindingStrength & 0xF8;
+        bool parensNeeded = opBS < ctxtBS ||
+          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
+
+        string op = BinaryExpr.OpcodeString(e.Op);
+        if (parensNeeded) { wr.Write("("); }
+        var sem = !parensNeeded && isFollowedBySemicolon;
+        if (0 <= indent && e.Op == BinaryExpr.Opcode.And) {
+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);
+          wr.WriteLine(" {0}", op);
+          Indent(indent);
+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, indent);
+        } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Imp) {
+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, indent);
+          wr.WriteLine(" {0}", op);
+          int ind = indent + IndentAmount;
+          Indent(ind);
+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);
+        } else if (0 <= indent && e.Op == BinaryExpr.Opcode.Exp) {
+          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, indent);
+          wr.WriteLine(" {0}", op);
+          int ind = indent + IndentAmount;
+          Indent(ind);
+          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, ind);
+        } else if (e.Op == BinaryExpr.Opcode.Exp) {
+          PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);
+          wr.Write(" {0} ", op);
+          PrintExpr(e.E0, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);
+        } else {
+          PrintExpr(e.E0, opBindingStrength, fragileLeftContext, false, sem, -1);
+          wr.Write(" {0} ", op);
+          PrintExpr(e.E1, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);
+        }
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is TernaryExpr) {
+        var e = (TernaryExpr)expr;
+        switch (e.Op) {
+          case TernaryExpr.Opcode.PrefixEqOp:
+          case TernaryExpr.Opcode.PrefixNeqOp:
+            var opBindingStrength = 0x30;
+            var fragileLeftContext = true;
+            var fragileRightContext = true;
+
+            int opBS = opBindingStrength & 0xF8;
+            int ctxtBS = contextBindingStrength & 0xF8;
+            bool parensNeeded = opBS < ctxtBS ||
+              (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
+
+            if (parensNeeded) { wr.Write("("); }
+            var sem = !parensNeeded && isFollowedBySemicolon;
+            PrintExpr(e.E1, opBindingStrength, fragileLeftContext, false, sem, -1);
+            wr.Write(" {0}#[", e.Op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=");
+            PrintExpression(e.E0, false);
+            wr.Write("] ");
+            PrintExpr(e.E2, opBindingStrength, fragileRightContext, parensNeeded || isRightmost, sem, -1);
+            if (parensNeeded) { wr.Write(")"); }
+            break;
+          default:
+            Contract.Assert(false);  // unexpected ternary operator
+            break;
+        }
+
+      } else if (expr is ChainingExpression) {
+        var e = (ChainingExpression)expr;
+        // determine if parens are needed
+        int opBindingStrength = 0x30;
+        int opBS = opBindingStrength & 0xF8;
+        int ctxtBS = contextBindingStrength & 0xF8;
+        bool parensNeeded = opBS < ctxtBS ||
+          (opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
+
+        if (parensNeeded) { wr.Write("("); }
+        var sem = !parensNeeded && isFollowedBySemicolon;
+        PrintExpr(e.Operands[0], opBindingStrength, true, false, sem, -1);
+        for (int i = 0; i < e.Operators.Count; i++) {
+          string op = BinaryExpr.OpcodeString(e.Operators[i]);
+          if (e.PrefixLimits[i] == null) {
+            wr.Write(" {0} ", op);
+          } else {
+            wr.Write(" {0}#[", op);
+            PrintExpression(e.PrefixLimits[i], false);
+            wr.Write("] ");
+          }
+          PrintExpr(e.Operands[i+1], opBindingStrength, true, i == e.Operators.Count - 1 && (parensNeeded || isRightmost), sem, -1);
+        }
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is LetExpr) {
+        var e = (LetExpr)expr;
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write("var ");
+        string sep = "";
+        foreach (var lhs in e.LHSs) {
+          wr.Write(sep);
+          PrintCasePattern(lhs);
+          sep = ", ";
+        }
+        if (e.Exact) {
+          wr.Write(" := ");
+        } else {
+          wr.Write(" :| ");
+        }
+        PrintExpressionList(e.RHSs, true);
+        wr.Write("; ");
+        PrintExpression(e.Body, !parensNeeded && isFollowedBySemicolon);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is QuantifierExpr) {
+        QuantifierExpr e = (QuantifierExpr)expr;
+
+        if (DafnyOptions.O.DafnyPrintResolvedFile != null && e.SplitQuantifier != null) {
+          PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count);
+          return;
+        }
+
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write(e is ForallExpr ? "forall" : "exists");
+        PrintTypeParams(e.TypeArgs); // new!
+        wr.Write(" ");
+        PrintQuantifierDomain(e.BoundVars, e.Attributes, e.Range);
+        wr.Write(" :: ");
+        if (0 <= indent) {
+          int ind = indent + IndentAmount;
+          wr.WriteLine();
+          Indent(ind);
+          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon, ind);
+        } else {
+          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);
+        }
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is NamedExpr) {
+        var e = (NamedExpr)expr;
+        wr.Write("expr {0}: ", e.Name);
+        PrintExpression(e.Body, isFollowedBySemicolon);
+
+       } else if (expr is SetComprehension) {
+        var e = (SetComprehension)expr;
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write("set ");
+        string sep = "";
+        foreach (BoundVar bv in e.BoundVars) {
+          wr.Write("{0}{1}", sep, bv.DisplayName);
+          sep = ", ";
+          PrintType(": ", bv.Type);
+        }
+        PrintAttributes(e.Attributes);
+        wr.Write(" | ");
+        PrintExpression(e.Range, !parensNeeded && isFollowedBySemicolon);
+        if (!e.TermIsImplicit) {
+          wr.Write(" :: ");
+          PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);
+        }
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is MapComprehension) {
+        var e = (MapComprehension)expr;
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write(e.Finite ? "map " : "imap ");
+        string sep = "";
+        foreach (BoundVar bv in e.BoundVars) {
+          wr.Write("{0}{1}", sep, bv.DisplayName);
+          sep = ", ";
+          PrintType(": ", bv.Type);
+        }
+        PrintAttributes(e.Attributes);
+        wr.Write(" | ");
+        PrintExpression(e.Range, !parensNeeded && isFollowedBySemicolon);
+        wr.Write(" :: ");
+        PrintExpression(e.Term, !parensNeeded && isFollowedBySemicolon);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is LambdaExpr) {
+        var e = (LambdaExpr)expr;
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        var skipSignatureParens = e.BoundVars.Count == 1 && e.BoundVars[0].Type is InferredTypeProxy;
+        if (!skipSignatureParens) { wr.Write("("); }
+        wr.Write(Util.Comma(", ", e.BoundVars, bv => bv.DisplayName + (bv.Type is InferredTypeProxy ? "" : ": " + bv.Type)));
+        if (!skipSignatureParens) { wr.Write(")"); }
+        if (e.Range != null) {
+          wr.Write(" requires ");
+          PrintExpression(e.Range, false);
+        }
+        foreach (var read in e.Reads) {
+          wr.Write(" reads ");
+          PrintExpression(read.E, false);
+        }
+        wr.Write(e.OneShot ? " -> " : " => ");
+        PrintExpression(e.Body, isFollowedBySemicolon);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is WildcardExpr) {
+        wr.Write("*");
+
+      } else if (expr is StmtExpr) {
+        var e = (StmtExpr)expr;
+        bool parensNeeded;
+        if (e.S is AssertStmt || e.S is AssumeStmt || e.S is CalcStmt) {
+          parensNeeded = !isRightmost;
+        } else {
+          parensNeeded = !isRightmost || isFollowedBySemicolon;
+        }
+        if (parensNeeded) { wr.Write("("); }
+        int ind = indent < 0 ? IndentAmount : indent;  // if the expression was to be printed on one line, instead print the .S part at indentation IndentAmount (not pretty, but something)
+        PrintStatement(e.S, ind);
+        wr.Write(" ");
+        PrintExpression(e.E, !parensNeeded && isFollowedBySemicolon);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is ITEExpr) {
+        ITEExpr ite = (ITEExpr)expr;
+        bool parensNeeded = !isRightmost;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write("if ");
+        PrintExpression(ite.Test, false);
+        wr.Write(" then ");
+        PrintExpression(ite.Thn, false);
+        wr.Write(" else ");
+        PrintExpression(ite.Els, !parensNeeded && isFollowedBySemicolon);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is ParensExpression) {
+        var e = (ParensExpression)expr;
+        // printing of parentheses is done optimally, not according to the parentheses in the given program
+        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+
+      } else if (expr is NegationExpression) {
+        var e = (NegationExpression)expr;
+        string op = "-";
+        int opBindingStrength = 0x60;
+        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);
+
+        bool containsNestedNegation = e.E is ParensExpression && ((ParensExpression)e.E).E is NegationExpression;
+
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write(op);
+        PrintExpr(e.E, opBindingStrength, containsNestedNegation, parensNeeded || isRightmost, !parensNeeded && isFollowedBySemicolon, -1);
+        if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is MatchExpr) {
+        var e = (MatchExpr)expr;
+        var parensNeeded = !isRightmost && !e.UsesOptionalBraces;
+        if (parensNeeded) { wr.Write("("); }
+        wr.Write("match ");
+        PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, !parensNeeded && isFollowedBySemicolon);
+        if (e.UsesOptionalBraces) { wr.Write(" {"); }
+        int i = 0;
+        foreach (var mc in e.Cases) {
+          bool isLastCase = i == e.Cases.Count - 1;
+          wr.Write(" case {0}", mc.Id);
+          PrintMatchCaseArgument(mc);
+          wr.Write(" => ");
+          PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);
+          i++;
+        }
+        if (e.UsesOptionalBraces) { wr.Write(" }"); }
+        else if (parensNeeded) { wr.Write(")"); }
+
+      } else if (expr is BoxingCastExpr) {
+        // this is not expected for a parsed program, but we may be called for /trace purposes in the translator
+        var e = (BoxingCastExpr)expr;
+        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent);
+      } else if (expr is Translator.BoogieWrapper) {
+        wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here
+      } else {
+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
+      }
+    }
+
+    bool ParensMayMatter(Expression expr) {
+      Contract.Requires(expr != null);
+      int parenPairs = 0;
+      for (; expr is ParensExpression; parenPairs++) {
+        expr = ((ParensExpression)expr).E;
+      }
+      // If the program were resolved, we could be more precise than the following (in particular, looking
+      // to see if expr denotes a MemberSelectExpr of a member that is a Function.
+      return parenPairs != 0 && (expr is NameSegment || expr is ExprDotName);
+    }
+
+    void PrintCasePattern(CasePattern pat) {
+      Contract.Requires(pat != null);
+      var v = pat.Var;
+      if (v != null) {
+        wr.Write(v.DisplayName);
+        if (v.Type is NonProxyType || DafnyOptions.O.DafnyPrintResolvedFile != null) {
+          PrintType(": ", v.Type);
+        }
+      } else {
+        wr.Write(pat.Id);
+        if (pat.Arguments != null) {
+          wr.Write("(");
+          var sep = "";
+          foreach (var arg in pat.Arguments) {
+            wr.Write(sep);
+            PrintCasePattern(arg);
+            sep = ", ";
+          }
+          wr.Write(")");
+        }
+      }
+    }
+
+    private void PrintQuantifierDomain(List<BoundVar> boundVars, Attributes attrs, Expression range) {
+      Contract.Requires(boundVars != null);
+      string sep = "";
+      foreach (BoundVar bv in boundVars) {
+        wr.Write("{0}{1}", sep, bv.DisplayName);
+        PrintType(": ", bv.Type);
+        sep = ", ";
+      }
+      PrintAttributes(attrs);
+      if (range != null) {
+        wr.Write(" | ");
+        PrintExpression(range, false);
+      }
+    }
+
+    void PrintActualArguments(List<Expression> args, string name) {
+      Contract.Requires(args != null);
+      Contract.Requires(name != null);
+      if (name.EndsWith("#")) {
+        wr.Write("[");
+        PrintExpression(args[0], false);
+        wr.Write("]");
+        args = new List<Expression>(args.Skip(1));
+      }
+      wr.Write("(");
+      PrintExpressionList(args, false);
+      wr.Write(")");
+    }
+
+    void PrintExpressionList(List<Expression> exprs, bool isFollowedBySemicolon) {
+      Contract.Requires(exprs != null);
+      string sep = "";
+      foreach (Expression e in exprs) {
+        Contract.Assert(e != null);
+        wr.Write(sep);
+        sep = ", ";
+        PrintExpression(e, isFollowedBySemicolon);
+      }
+    }
+    void PrintExpressionPairList(List<ExpressionPair> exprs) {
+      Contract.Requires(exprs != null);
+      string sep = "";
+      foreach (ExpressionPair p in exprs) {
+        Contract.Assert(p != null);
+        wr.Write(sep);
+        sep = ", ";
+        PrintExpression(p.A, false);
+        wr.Write(":=");
+        PrintExpression(p.B, false);
+      }
+    }
+
+    void PrintFrameExpressionList(List<FrameExpression/*!*/>/*!*/ fexprs) {
+      Contract.Requires(fexprs != null);
+      string sep = "";
+      foreach (FrameExpression fe in fexprs) {
+        Contract.Assert(fe != null);
+        wr.Write(sep);
+        sep = ", ";
+        PrintExpression(fe.E, true);
+        if (fe.FieldName != null) {
+          wr.Write("`{0}", fe.FieldName);
+        }
+      }
+    }
+  }
+}
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index ba558ea6..24d1126f 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -547,16 +547,16 @@ namespace Microsoft.Dafny
 

       if (f is Predicate) {

         return new Predicate(tok, f.Name, f.HasStaticKeyword, f.IsProtected, isGhost, tps, formals,

-          req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

+          req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);

       } else if (f is InductivePredicate) {

         return new InductivePredicate(tok, f.Name, f.HasStaticKeyword, f.IsProtected, tps, formals,

-          req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

+          req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);

       } else if (f is CoPredicate) {

         return new CoPredicate(tok, f.Name, f.HasStaticKeyword, f.IsProtected, tps, formals,

-          req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

+          req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);

       } else {

         return new Function(tok, f.Name, f.HasStaticKeyword, f.IsProtected, isGhost, tps, formals, refinementCloner.CloneType(f.ResultType),

-          req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);

+          req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null, f);

       }

     }

 

@@ -581,19 +581,19 @@ namespace Microsoft.Dafny
       var body = newBody ?? refinementCloner.CloneBlockStmt(m.Body);

       if (m is Constructor) {

         return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,

-          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

+          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);

       } else if (m is InductiveLemma) {

         return new InductiveLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

-          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

+          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);

       } else if (m is CoLemma) {

         return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

-          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

+          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);

       } else if (m is Lemma) {

         return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

-          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

+          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);

       } else {

         return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

-          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

+          req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null, m);

       }

     }

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1c376c49..0b0bbf26 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -857,9 +857,34 @@ namespace Microsoft.Dafny
               if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) {

                 TopLevelDecl d;

                 if (sig.TopLevels.TryGetValue(kv.Key, out d)) {

-                  if (DafnyOptions.O.IronDafny && kv.Value.ClonedFrom == d) {

+                  bool resolved = false;

+                  if (DafnyOptions.O.IronDafny) {

+                    // sometimes, we need to compare two type synonyms in order to come up with a decision regarding substitution.

+                    var aliased1 = Object.ReferenceEquals(kv.Value, d);

+                    if (!aliased1) {

+                      var a = d;

+                      while (a.ExclusiveRefinement != null) {

+                        a = a.ExclusiveRefinement;

+                      }

+                      var b = kv.Value;

+                      while (b.ExclusiveRefinement != null) {

+                        b = b.ExclusiveRefinement;

+                      }

+                      if (a is TypeSynonymDecl && b is TypeSynonymDecl) {

+                        aliased1 = UnifyTypes(((TypeSynonymDecl)a).Rhs, ((TypeSynonymDecl)b).Rhs);

+                      } else {

+                        aliased1 = Object.ReferenceEquals(a, b);

+                      }

+                    }

+                    if (aliased1 ||

+                      Object.ReferenceEquals(kv.Value.ClonedFrom, d) ||

+                      Object.ReferenceEquals(d.ClonedFrom, kv.Value) ||

+                      Object.ReferenceEquals(kv.Value.ExclusiveRefinement, d)) {

                     sig.TopLevels[kv.Key] = kv.Value;

-                  } else {

+                      resolved = true;

+                    }

+                  }

+                  if (!resolved) {

                     sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value);

                   }

                 } else {

@@ -876,7 +901,10 @@ namespace Microsoft.Dafny
               if (sig.Ctors.TryGetValue(kv.Key, out pair)) {

                 // The same ctor can be imported from two different imports (e.g "diamond" imports), in which case, 

                 // they are not duplicates.

-                if (kv.Value.Item1 != pair.Item1) {

+                if (!Object.ReferenceEquals(kv.Value.Item1, pair.Item1) &&

+                    (!DafnyOptions.O.IronDafny ||

+                        (!Object.ReferenceEquals(kv.Value.Item1.ClonedFrom, pair.Item1) &&

+                        !Object.ReferenceEquals(kv.Value.Item1, pair.Item1.ClonedFrom)))) {

                   // mark it as a duplicate

                   sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);

                 }

@@ -892,7 +920,48 @@ namespace Microsoft.Dafny
             foreach (var kv in s.StaticMembers) {

               MemberDecl md;

               if (sig.StaticMembers.TryGetValue(kv.Key, out md)) {

+                var resolved = false;

+                if (DafnyOptions.O.IronDafny) {

+                  var aliased0 = Object.ReferenceEquals(kv.Value, md) || Object.ReferenceEquals(kv.Value.ClonedFrom, md) || Object.ReferenceEquals(md.ClonedFrom, kv.Value);

+                  var aliased1 = aliased0;

+                  if (!aliased0) {

+                    var a = kv.Value.EnclosingClass;

+                    while (a != null && 

+                        (a.ExclusiveRefinement != null || a.ClonedFrom != null)) {

+                      if (a.ClonedFrom != null) {

+                        a = (TopLevelDecl)a.ClonedFrom;

+                      } else {

+                        Contract.Assert(a.ExclusiveRefinement != null);

+                        a = a.ExclusiveRefinement;

+                      }

+                    }

+                    var b = md.EnclosingClass;

+                    while (b != null && 

+                            (b.ExclusiveRefinement != null || b.ClonedFrom != null)) {

+                      if (b.ClonedFrom != null) {

+                        b = (TopLevelDecl)b.ClonedFrom;

+                      } else {

+                        Contract.Assert(b.ExclusiveRefinement != null);

+                        b = b.ExclusiveRefinement;

+                      }

+                    }

+                    aliased1 = Object.ReferenceEquals(a, b);

+                  }

+                  if (aliased0 || aliased1) {

+                    if (kv.Value.EnclosingClass != null && 

+                        md.EnclosingClass != null &&

+                        md.EnclosingClass.ExclusiveRefinement != null &&

+                        !Object.ReferenceEquals(

+                            kv.Value.EnclosingClass.ExclusiveRefinement, 

+                            md.EnclosingClass)) {

+                      sig.StaticMembers[kv.Key] = kv.Value;

+                    }

+                    resolved = true;

+                  }

+                }

+                if (!resolved) {

                 sig.StaticMembers[kv.Key] = AmbiguousMemberDecl.Create(moduleDef, md, kv.Value);

+                }

               } else {

                 // add new

                 sig.StaticMembers.Add(kv.Key, kv.Value);

@@ -1249,6 +1318,14 @@ namespace Microsoft.Dafny
 

       var typeRedirectionDependencies = new Graph<RedirectingTypeDecl>();

       foreach (TopLevelDecl d in declarations) {

+        if (DafnyOptions.O.IronDafny && d.Module.IsExclusiveRefinement) {

+          var refinementOf =

+            def.RefinementBase.TopLevelDecls.Find(

+              i => String.Equals(i.Name, d.Name, StringComparison.InvariantCulture));

+          if (refinementOf != null && refinementOf.ExclusiveRefinement == null) {

+            refinementOf.ExclusiveRefinement = d;

+          }      

+        }

         Contract.Assert(d != null);

         allTypeParameters.PushMarker();

         ResolveTypeParameters(d.TypeArgs, true, d);

@@ -1281,9 +1358,13 @@ namespace Microsoft.Dafny
           if (!def.IsAbstract) {

             if (decl.Signature.IsAbstract)

               {

-                if (!(def.IsDefaultModule)) // _module is allowed to contain abstract modules, but not be abstract itself. Note this presents a challenge to

+                if (// _module is allowed to contain abstract modules, but not be abstract itself. Note this presents a challenge to

                                             // trusted verification, as toplevels can't be trusted if they invoke abstract module members.

-                  reporter.Error(MessageSource.Resolver, d.tok, "an abstract module can only be imported into other abstract modules, not a concrete one.");

+                    !def.IsDefaultModule 

+                    // [IronDafny] it's possbile for an abstract module to have an exclusive refinement, so it no longer makes sense to disallow this.

+                    && !DafnyOptions.O.IronDafny) 

+                                            

+                reporter.Error(MessageSource.Resolver, d.tok, "an abstract module can only be imported into other abstract modules, not a concrete one.");

               } else {

                 // physical modules are allowed everywhere

               }

@@ -4784,6 +4865,11 @@ namespace Microsoft.Dafny
               }

             } else if (d is NewtypeDecl) {

               var dd = (NewtypeDecl)d;

+              if (DafnyOptions.O.IronDafny) {

+                while (dd.ClonedFrom != null) {

+                  dd = (NewtypeDecl)d.ClonedFrom;

+                }

+              }

               var caller = context as ICallable;

               if (caller != null) {

                 caller.EnclosingModule.CallGraph.AddEdge(caller, dd);

@@ -4899,28 +4985,60 @@ namespace Microsoft.Dafny
                UnifyTypes(((MapType)a).Domain, ((MapType)b).Domain) && UnifyTypes(((MapType)a).Range, ((MapType)b).Range);

       } else if (a is SeqType) {

         return b is SeqType && UnifyTypes(((SeqType)a).Arg, ((SeqType)b).Arg);

-      } else if (a is UserDefinedType) {

-        if (!(b is UserDefinedType)) {

-          return false;

+      } else if (a is UserDefinedType || b is UserDefinedType) {

+        if (!(a is UserDefinedType) && b is UserDefinedType) {

+          var x = a;

+          a = b;

+          b = x;

         }

+

         var aa = (UserDefinedType)a;

         var rca = aa.ResolvedClass;

+        // traits are currently unfriendly to irondafny features.

+        if (DafnyOptions.O.IronDafny && !(rca is TraitDecl)) { 

+          if (rca != null) {

+            while (rca.ClonedFrom != null || rca.ExclusiveRefinement != null) {

+              if (rca.ClonedFrom != null) {

+                rca = (TopLevelDecl)rca.ClonedFrom;                

+              } else {

+                Contract.Assert(rca.ExclusiveRefinement != null);

+                rca = rca.ExclusiveRefinement;

+              }

+            }

+          }

+        }

+

+        if (!(b is UserDefinedType)) {

+          return DafnyOptions.O.IronDafny && rca is TypeSynonymDecl && UnifyTypes(((TypeSynonymDecl)rca).Rhs, b);

+        }

+

         var bb = (UserDefinedType)b;

         var rcb = bb.ResolvedClass;

-        if (DafnyOptions.O.IronDafny)

-        {

-          while (rca != null && rca.Module.IsAbstract && rca.ClonedFrom != null)

-          {

-            // todo: should ClonedFrom be a TopLevelDecl?

-            // todo: should ClonedFrom be moved to TopLevelDecl?

-            rca = (TopLevelDecl)rca.ClonedFrom;

+        // traits are currently unfriendly to irondafny features.

+        if (DafnyOptions.O.IronDafny && !(rca is TraitDecl) && !(rcb is TraitDecl)) {

+          if (rcb != null) {

+            while (rcb.ClonedFrom != null || rcb.ExclusiveRefinement != null) {

+              if (rcb.ClonedFrom != null) {

+                rcb = (TopLevelDecl)rcb.ClonedFrom;                

+              } else {

+                Contract.Assert(rcb.ExclusiveRefinement != null);

+                rcb = rcb.ExclusiveRefinement;

+              }

+            }

           }

-          while (rcb != null && rcb.Module.IsAbstract && rcb.ClonedFrom != null)

-          {

-            rcb = (TopLevelDecl)rcb.ClonedFrom;

+          if (rca is TypeSynonymDecl || rcb is TypeSynonymDecl) {

+            var aaa = a;

+            var bbb = b;

+            if (rca is TypeSynonymDecl) {

+              aaa = ((TypeSynonymDecl)rca).Rhs;

+            }

+            if (rcb is TypeSynonymDecl) {

+              bbb = ((TypeSynonymDecl)rcb).Rhs;

+          }

+            return UnifyTypes(aaa, bbb);

           }

         }

-        if (rca != null && rca == rcb) {

+        if (rca != null && Object.ReferenceEquals(rca, rcb)) {

           // these are both resolved class/datatype types

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

           bool successSoFar = true;

@@ -7513,41 +7631,43 @@ namespace Microsoft.Dafny
             }

             eIter = ei.Seq;

           }

-          var e0 = eIter;

-

-          // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)"

-          // Wrapping it in a let expr avoids exponential growth in the size of the expression

-          // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" to

-          //   "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)"

-

-          // Create a unique name for d', the variable we introduce in the let expression

-          string tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext);

-          IdentifierExpr tmpVarIdExpr = new IdentifierExpr(e0.tok, tmpName);

-          BoundVar tmpVarBv = new BoundVar(e0.tok, tmpName, e0.Type);

-

-          // Build the arguments to the datatype constructor, using the updated value in the appropriate slot

-          List<Expression> ctor_args = new List<Expression>();

-          foreach (Formal d in ctor.Formals) {

-            Expression v = null;

-            foreach (var dvPair in IndexToValue.Values) {

-              var destructor = dvPair.Item1;

-              if (d == destructor.CorrespondingFormal) {

-                Contract.Assert(v == null);

-                v = dvPair.Item2;

+          if (ctor != null) {

+            var e0 = eIter;

+

+            // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)"

+            // Wrapping it in a let expr avoids exponential growth in the size of the expression

+            // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" to

+            //   "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)"

+

+            // Create a unique name for d', the variable we introduce in the let expression

+            string tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext);

+            IdentifierExpr tmpVarIdExpr = new IdentifierExpr(e0.tok, tmpName);

+            BoundVar tmpVarBv = new BoundVar(e0.tok, tmpName, e0.Type);

+

+            // Build the arguments to the datatype constructor, using the updated value in the appropriate slot

+            List<Expression> ctor_args = new List<Expression>();

+            foreach (Formal d in ctor.Formals) {

+              Expression v = null;

+              foreach (var dvPair in IndexToValue.Values) {

+                var destructor = dvPair.Item1;

+                if (d == destructor.CorrespondingFormal) {

+                  Contract.Assert(v == null);

+                  v = dvPair.Item2;

+                }

               }

+              ctor_args.Add(v ?? new ExprDotName(expr.tok, tmpVarIdExpr, d.Name, null));

             }

-            ctor_args.Add(v ?? new ExprDotName(expr.tok, tmpVarIdExpr, d.Name, null));

-          }

 

-          DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args);

+            DatatypeValue ctor_call = new DatatypeValue(expr.tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args);

 

-          CasePattern tmpVarPat = new CasePattern(e0.tok, tmpVarBv);

-          LetExpr let = new LetExpr(e0.tok, new List<CasePattern>() { tmpVarPat }, new List<Expression>() { e0 }, ctor_call, true);

+            CasePattern tmpVarPat = new CasePattern(e0.tok, tmpVarBv);

+            LetExpr let = new LetExpr(e0.tok, new List<CasePattern>() { tmpVarPat }, new List<Expression>() { e0 }, ctor_call, true);

 

-          ResolveExpression(let, opts);

-          e.ResolvedUpdateExpr = let;

+            ResolveExpression(let, opts);

+            e.ResolvedUpdateExpr = let;

 

-          expr.Type = e0.Type;

+            expr.Type = e0.Type;

+          }

         } else {

           reporter.Error(MessageSource.Resolver, expr, "update requires a sequence, map, or datatype (got {0})", e.Seq.Type);

         }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 09ca32e0..af8225da 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -9246,41 +9246,41 @@ namespace Microsoft.Dafny {
       Contract.Requires(type != null);

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

 

-      type = type.NormalizeExpand();

-

-      if (type is SetType) {

-        bool finite = ((SetType)type).Finite;

-        return FunctionCall(Token.NoToken, finite ? "TSet" : "TISet", predef.Ty, TypeToTy(((CollectionType)type).Arg));

-      } else if (type is MultiSetType) {

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

-      } else if (type is SeqType) {

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

-      } else if (type is MapType) {

-        bool finite = ((MapType)type).Finite;

+      var normType = type.NormalizeExpand();

+

+      if (normType is SetType) {

+        bool finite = ((SetType)normType).Finite;

+        return FunctionCall(Token.NoToken, finite ? "TSet" : "TISet", predef.Ty, TypeToTy(((CollectionType)normType).Arg));

+      } else if (normType is MultiSetType) {

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

+      } else if (normType is SeqType) {

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

+      } else if (normType is MapType) {

+        bool finite = ((MapType)normType).Finite;

         return FunctionCall(Token.NoToken, finite ? "TMap" : "TIMap", predef.Ty,

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

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

-      } else if (type is BoolType) {

+          TypeToTy(((MapType)normType).Domain),

+          TypeToTy(((MapType)normType).Range));

+      } else if (normType is BoolType) {

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

-      } else if (type is CharType) {

+      } else if (normType is CharType) {

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

-      } else if (type is RealType) {

+      } else if (normType is RealType) {

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

-      } else if (type is NatType) {

+      } else if (normType is NatType) {

         // (Nat needs to come before Int)

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

-      } else if (type is IntType) {

+      } else if (normType is IntType) {

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

-      } else if (type.IsTypeParameter) {

-        return trTypeParam(type.AsTypeParameter, type.TypeArgs);

-      } else if (type is ObjectType) {

+      } else if (normType.IsTypeParameter) {

+        return trTypeParam(normType.AsTypeParameter, normType.TypeArgs);

+      } else if (normType is ObjectType) {

         return ClassTyCon(program.BuiltIns.ObjectDecl, new List<Bpl.Expr>());

-      } else if (type is UserDefinedType) {

+      } else if (normType is UserDefinedType) {

         // Classes, (co-)datatypes

-        var args = type.TypeArgs.ConvertAll(TypeToTy);

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

-      } else if (type is ParamTypeProxy) {

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

+        var args = normType.TypeArgs.ConvertAll(TypeToTy);

+        return ClassTyCon(((UserDefinedType)normType), args);

+      } else if (normType is ParamTypeProxy) {

+        return trTypeParam(((ParamTypeProxy)normType).orig, null);

       } else {

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

       }

@@ -9383,19 +9383,19 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

 

-      type = type.NormalizeExpand();

-      if (type is TypeProxy) {

+      var normType = type.NormalizeExpand();

+      if (normType is TypeProxy) {

         // Unresolved proxy

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

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

         return null;

       }

 

-      if (type is NatType) {

+      if (normType is NatType) {

         // nat:

         // 0 <= x

         return Bpl.Expr.Le(Bpl.Expr.Literal(0), x);

-      } else if (type is BoolType || type is IntType || type is RealType) {

+      } else if (normType is BoolType || normType is IntType || normType is RealType) {

         // nothing to do

         return null;

       /* } else if (type is ArrowType) {

@@ -9403,7 +9403,7 @@ namespace Microsoft.Dafny {
         return null;

         */

       } else {

-        return BplAnd(MkIs(x, type), MkIsAlloc(x, type, etran.HeapExpr));

+        return BplAnd(MkIs(x, normType), MkIsAlloc(x, normType, etran.HeapExpr));

       }

     }

 

@@ -11029,7 +11029,11 @@ namespace Microsoft.Dafny {
           }

 

           var ty = translator.TrType(e.Type);

-          var id = new Bpl.IdentifierExpr(e.tok, e.Function.FullSanitizedName, ty);

+          var name = e.Function.FullSanitizedName;

+          if (DafnyOptions.O.IronDafny) {

+            name = e.Function.FullSanitizedRefinementName;

+          }

+          var id = new Bpl.IdentifierExpr(e.tok, name, ty);

 

           bool argsAreLit;

           var args = FunctionInvocationArguments(e, layerArgument, out argsAreLit);

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 5b70329d..d638cb6c 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -77,7 +77,7 @@ namespace DafnyLanguage
       int start = entire.Start;

       int end = entire.End;

       foreach (var r in _regions) {

-        if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {

+        if (0 <= r.Length && r.Start >= start && r.Start + r.Length <= end) {

           DafnyTokenKind kind;

           switch (r.Kind) {

             case IdRegion.OccurrenceKind.Use: