Fix issue89. Copy the out param to a local before use it in an anonymous

method that is generated by LetExpr. Change the compiler so that each stmt
writes to its own buffer before add it to the program's buffer so that we can
insert the above mentioned copy instruction before the stmt.

2 files changed, 589 insertions, 566 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index aa4ca3ec..f992d6c0 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -14,18 +14,11 @@ using System.Text;
 

 namespace Microsoft.Dafny {

   public class Compiler {

-    public Compiler(TextWriter wr) {

-      Contract.Requires(wr != null);

-      this.wr = wr;

+    public Compiler() {

+  

     }

 

-    [ContractInvariantMethod]

-    void ObjectInvariant()

-    {

-      Contract.Invariant(wr!=null);

-    }

-

-    TextWriter wr;

+    StringBuilder copyInstrWriter = new StringBuilder(); // a buffer that stores copy instructions generated by letExpr that uses out param.

     Method enclosingMethod;  // non-null when a method body is being translated

 

     FreshIdGenerator idGenerator = new FreshIdGenerator();

@@ -50,7 +43,7 @@ namespace Microsoft.Dafny {
     public int ErrorCount;

     public TextWriter ErrorWriter = Console.Out;

 

-    void Error(string msg, params object[] args) {

+    void Error(string msg, TextWriter wr, params object[] args) {

       Contract.Requires(msg != null);

       Contract.Requires(args != null);

 

@@ -60,7 +53,7 @@ namespace Microsoft.Dafny {
       ErrorCount++;

     }

 

-    void ReadRuntimeSystem() {

+    void ReadRuntimeSystem(TextWriter wr) {

       string codebase = cce.NonNull( System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));

       string path = System.IO.Path.Combine(codebase, "DafnyRuntime.cs");

       using (TextReader rd = new StreamReader(new FileStream(path, System.IO.FileMode.Open, System.IO.FileAccess.Read)))

@@ -75,16 +68,16 @@ namespace Microsoft.Dafny {
     }

 

     readonly int IndentAmount = 2;

-    void Indent(int ind) {

+    void Indent(int ind, TextWriter wr) {

       Contract.Requires(0 <= ind);

       string spaces = "          ";

       for (; spaces.Length < ind; ind -= spaces.Length) {

         wr.Write(spaces);

       }

-      wr.Write(spaces.Substring(0, ind));

+     wr.Write(spaces.Substring(0, ind));

     }

 

-    public void Compile(Program program) {

+    public void Compile(Program program, TextWriter wr) {

       Contract.Requires(program != null);

       wr.WriteLine("// Dafny program {0} compiled into C#", program.Name);

       wr.WriteLine("// To recompile, use 'csc' with: /r:System.Numerics.dll");

@@ -92,8 +85,8 @@ namespace Microsoft.Dafny {
       wr.WriteLine("// You might also want to include compiler switches like:");

       wr.WriteLine("//     /debug /nowarn:0164 /nowarn:0219");

       wr.WriteLine();

-      ReadRuntimeSystem();

-      CompileBuiltIns(program.BuiltIns);

+      ReadRuntimeSystem(wr);

+      CompileBuiltIns(program.BuiltIns, wr);

 

       foreach (ModuleDefinition m in program.CompileModules) {

         if (m.IsAbstract) {

@@ -117,33 +110,33 @@ namespace Microsoft.Dafny {
           wr.WriteLine();

           if (d is OpaqueTypeDecl) {

             var at = (OpaqueTypeDecl)d;

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

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

           } else if (d is TypeSynonymDecl) {

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

           } else if (d is NewtypeDecl) {

             var nt = (NewtypeDecl)d;

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("public class @{0} {{", nt.CompileName);

             if (nt.NativeType != null) {

-              Indent(indent + IndentAmount);

+              Indent(indent + IndentAmount, wr);

               wr.WriteLine("public static System.Collections.Generic.IEnumerable<{0}> IntegerRange(BigInteger lo, BigInteger hi) {{", nt.NativeType.Name);

-              Indent(indent + 2 * IndentAmount);

+              Indent(indent + 2 * IndentAmount, wr);

               wr.WriteLine("for (var j = lo; j < hi; j++) {{ yield return ({0})j; }}", nt.NativeType.Name);

-              Indent(indent + IndentAmount);

+              Indent(indent + IndentAmount, wr);

               wr.WriteLine("}");

             }

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("}");

           } else if (d is DatatypeDecl) {

             var dt = (DatatypeDecl)d;

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("public abstract class Base_{0}", dt.CompileName);

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

               wr.Write("<{0}>", TypeParameters(dt.TypeArgs));

             }

             wr.WriteLine(" { }");

-            CompileDatatypeConstructors(dt, indent);

-            CompileDatatypeStruct(dt, indent);

+            CompileDatatypeConstructors(dt, indent, wr);

+            CompileDatatypeStruct(dt, indent, wr);

           } else if (d is IteratorDecl) {

             var iter = (IteratorDecl)d;

             // An iterator is compiled as follows:

@@ -169,7 +162,7 @@ namespace Microsoft.Dafny {
             //     }

             //   }

 

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("public class @{0}", iter.CompileName);

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

               wr.Write("<{0}>", TypeParameters(iter.TypeArgs));

@@ -181,58 +174,58 @@ namespace Microsoft.Dafny {
             foreach (var member in iter.Members) {

               var f = member as Field;

               if (f != null && !f.IsGhost) {

-                Indent(ind);

-                wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));

+                Indent(ind, wr);

+                wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type, wr), f.CompileName, DefaultValue(f.Type, wr));

               } else if (member is Constructor) {

                 Contract.Assert(ct == null);  // we're expecting just one constructor

                 ct = (Constructor)member;

               }

             }

             Contract.Assert(ct != null);  // we do expect a constructor

-            Indent(ind); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");

+            Indent(ind, wr); wr.WriteLine("System.Collections.Generic.IEnumerator<object> __iter;");

 

             // here's the initializer method

-            Indent(ind); wr.Write("public void @{0}(", ct.CompileName);

+            Indent(ind, wr); wr.Write("public void @{0}(", ct.CompileName);

             string sep = "";

             foreach (var p in ct.Ins) {

               if (!p.IsGhost) {

                 // here we rely on the parameters and the corresponding fields having the same names

-                wr.Write("{0}{1} @{2}", sep, TypeName(p.Type), p.CompileName);

+                wr.Write("{0}{1} @{2}", sep, TypeName(p.Type, wr), p.CompileName);

                 sep = ", ";

               }

             }

             wr.WriteLine(") {");

             foreach (var p in ct.Ins) {

               if (!p.IsGhost) {

-                Indent(ind + IndentAmount);

+                Indent(ind + IndentAmount, wr);

                 wr.WriteLine("this.@{0} = @{0};", p.CompileName);

               }

             }

-            Indent(ind + IndentAmount); wr.WriteLine("__iter = TheIterator();");

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

+            Indent(ind + IndentAmount, wr); wr.WriteLine("__iter = TheIterator();");

+            Indent(ind, wr);  wr.WriteLine("}");

             // here are the enumerator methods

-            Indent(ind); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");

-            Indent(ind); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");

+            Indent(ind, wr); wr.WriteLine("public void MoveNext(out bool more) { more = __iter.MoveNext(); }");

+            Indent(ind, wr); wr.WriteLine("private System.Collections.Generic.IEnumerator<object> TheIterator() {");

             if (iter.Body == null) {

-              Error("Iterator {0} has no body", iter.FullName);

+              Error("Iterator {0} has no body", wr, iter.FullName);

             } else {

-              TrStmt(iter.Body, ind + IndentAmount);

+              wr.Write(TrStmt(iter.Body, ind + IndentAmount).ToString());

             }

-            Indent(ind + IndentAmount); wr.WriteLine("yield break;");

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

+            Indent(ind + IndentAmount, wr); wr.WriteLine("yield break;");

+            Indent(ind, wr); wr.WriteLine("}");

             // end of the class

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

+            Indent(indent, wr); wr.WriteLine("}");

 

           }

           else if (d is TraitDecl)

           {

               //writing the trait

               var trait = (TraitDecl)d;

-              Indent(indent);

+              Indent(indent, wr);

               wr.Write("public interface @{0}", trait.CompileName);

               wr.WriteLine(" {");

-              CompileClassMembers(trait, false, indent + IndentAmount);

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

+              CompileClassMembers(trait, false, indent + IndentAmount, wr);

+              Indent(indent, wr); wr.WriteLine("}");

 

               //writing the _Companion class

               List<MemberDecl> members = new List<MemberDecl>();

@@ -252,27 +245,27 @@ namespace Microsoft.Dafny {
                       }

                   }

               }

-              Indent(indent);

+              Indent(indent, wr);

               wr.Write("public class @_Companion_{0}", trait.CompileName);

               wr.WriteLine(" {");

-              CompileClassMembers(trait, true, indent + IndentAmount);

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

+              CompileClassMembers(trait, true, indent + IndentAmount, wr);

+              Indent(indent, wr); wr.WriteLine("}");

           }

           else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("public class @{0}", cl.CompileName);

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

               wr.Write("<{0}>", TypeParameters(cl.TypeArgs));

             }

             string sep = " : ";

             foreach (var trait in cl.TraitsTyp) {

-              wr.Write("{0}{1}", sep, TypeName(trait));

+              wr.Write("{0}{1}", sep, TypeName(trait, wr));

               sep = ", ";

             }

             wr.WriteLine(" {");

-            CompileClassMembers(cl, false, indent+IndentAmount);

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

+            CompileClassMembers(cl, false, indent+IndentAmount, wr);

+            Indent(indent, wr);  wr.WriteLine("}");

           } else if (d is ModuleDecl) {

             // nop

           } else { Contract.Assert(false); }

@@ -283,15 +276,15 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CompileBuiltIns(BuiltIns builtIns) {

+    void CompileBuiltIns(BuiltIns builtIns, TextWriter wr) {

       wr.WriteLine("namespace Dafny {");

-      Indent(IndentAmount);

+      Indent(IndentAmount, wr);

       wr.WriteLine("public partial class Helpers {");

       foreach (var decl in builtIns.SystemModule.TopLevelDecls) {

         if (decl is ArrayClassDecl) {

           int dims = ((ArrayClassDecl)decl).Dims;

           // public static T[,] InitNewArray2<T>(BigInteger size0, BigInteger size1) {

-          Indent(3 * IndentAmount);

+          Indent(3 * IndentAmount, wr);

           wr.Write("public static T[");

           RepeatWrite(wr, dims, "", ",");

           wr.Write("] InitNewArray{0}<T>(", dims);

@@ -299,52 +292,52 @@ namespace Microsoft.Dafny {
           wr.WriteLine(") {");

           // int s0 = (int)size0;

           for (int i = 0; i < dims; i++) {

-            Indent(4 * IndentAmount);

+            Indent(4 * IndentAmount, wr);

             wr.WriteLine("int s{0} = (int)size{0};", i);

           }

           // T[,] a = new T[s0, s1];

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.Write("T[");

           RepeatWrite(wr, dims, "", ",");

           wr.Write("] a = new T[");

           RepeatWrite(wr, dims, "s{0}", ",");

           wr.WriteLine("];");

           // BigInteger[,] b = a as BigInteger[,];

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.Write("BigInteger[");

           RepeatWrite(wr, dims, "", ",");

           wr.Write("] b = a as BigInteger[");

           RepeatWrite(wr, dims, "", ",");

           wr.WriteLine("];");

           // if (b != null) {

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.WriteLine("if (b != null) {");

           // BigInteger z = new BigInteger(0);

-          Indent(5 * IndentAmount);

+          Indent(5 * IndentAmount, wr);

           wr.WriteLine("BigInteger z = new BigInteger(0);");

           // for (int i0 = 0; i0 < s0; i0++)

           //   for (int i1 = 0; i1 < s1; i1++)

           for (int i = 0; i < dims; i++) {

-            Indent((5+i) * IndentAmount);

+            Indent((5+i) * IndentAmount, wr);

             wr.WriteLine("for (int i{0} = 0; i{0} < s{0}; i{0}++)", i);

           }

           // b[i0,i1] = z;

-          Indent((5+dims) * IndentAmount);

+          Indent((5+dims) * IndentAmount, wr);

           wr.Write("b[");

           RepeatWrite(wr, dims, "i{0}", ",");

           wr.WriteLine("] = z;");

           // }

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.WriteLine("}");

           // return a;

-          Indent(4 * IndentAmount);

+          Indent(4 * IndentAmount, wr);

           wr.WriteLine("return a;");

           // }

-          Indent(3 * IndentAmount);

+          Indent(3 * IndentAmount, wr);

           wr.WriteLine("}");  // end of method

         }

       }

-      Indent(IndentAmount);

+      Indent(IndentAmount, wr);

       wr.WriteLine("}");  // end of class Helpers

       wr.WriteLine("}");  // end of namespace

     }

@@ -359,7 +352,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CompileDatatypeConstructors(DatatypeDecl dt, int indent)

+    void CompileDatatypeConstructors(DatatypeDecl dt, int indent, TextWriter wr)

     {

       Contract.Requires(dt != null);

 

@@ -372,20 +365,20 @@ namespace Microsoft.Dafny {
         //   public Dt__Lazy(Computer c) { this.c = c; }

         //   public Base_Dt<T> Get() { return c(); }

         // }

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("public class {0}__Lazy{1} : Base_{0}{1} {{", dt.CompileName, typeParams);

         int ind = indent + IndentAmount;

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public delegate Base_{0}{1} Computer();", dt.CompileName, typeParams);

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public delegate Computer ComputerComputer();");

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("Computer c;");

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public {0}__Lazy(Computer c) {{ this.c = c; }}", dt.CompileName);

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public Base_{0}{1} Get() {{ return c(); }}", dt.CompileName, typeParams);

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("}");

       }

 

@@ -407,7 +400,7 @@ namespace Microsoft.Dafny {
         //     // ...

         //   }

         // }

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("public class {0}", DtCtorDeclarationName(ctor, dt.TypeArgs));

         wr.WriteLine(" : Base_{0}{1} {{", dt.CompileName, typeParams);

         int ind = indent + IndentAmount;

@@ -415,32 +408,32 @@ namespace Microsoft.Dafny {
         int i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

-            Indent(ind);

-            wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type), FormalName(arg, i));

+            Indent(ind, wr);

+            wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type, wr), FormalName(arg, i));

             i++;

           }

         }

 

-        Indent(ind);

+        Indent(ind, wr);

         wr.Write("public {0}(", DtCtorDeclartionName(ctor));

-        WriteFormals("", ctor.Formals);

+        WriteFormals("", ctor.Formals, wr);

         wr.WriteLine(") {");

         i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

-            Indent(ind + IndentAmount);

+            Indent(ind + IndentAmount, wr);

             wr.WriteLine("this.@{0} = @{0};", FormalName(arg, i));

             i++;

           }

         }

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

+        Indent(ind, wr);  wr.WriteLine("}");

 

         // Equals method

-        Indent(ind); wr.WriteLine("public override bool Equals(object other) {");

-        Indent(ind + IndentAmount);

+        Indent(ind, wr); wr.WriteLine("public override bool Equals(object other) {");

+        Indent(ind + IndentAmount, wr);

         wr.Write("var oth = other as {0}", DtCtorName(ctor, dt.TypeArgs));

         wr.WriteLine(";");

-        Indent(ind + IndentAmount);

+        Indent(ind + IndentAmount, wr);

         wr.Write("return oth != null");

         i = 0;

         foreach (Formal arg in ctor.Formals) {

@@ -455,56 +448,56 @@ namespace Microsoft.Dafny {
           }

         }

         wr.WriteLine(";");

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

+        Indent(ind, wr); wr.WriteLine("}");

 

         // GetHashCode method (Uses the djb2 algorithm)

-        Indent(ind); wr.WriteLine("public override int GetHashCode() {");

-        Indent(ind + IndentAmount); wr.WriteLine("ulong hash = 5381;");

-        Indent(ind + IndentAmount); wr.WriteLine("hash = ((hash << 5) + hash) + {0};", constructorIndex);

+        Indent(ind, wr); wr.WriteLine("public override int GetHashCode() {");

+        Indent(ind + IndentAmount, wr); wr.WriteLine("ulong hash = 5381;");

+        Indent(ind + IndentAmount, wr); wr.WriteLine("hash = ((hash << 5) + hash) + {0};", constructorIndex);

         i = 0;

         foreach (Formal arg in ctor.Formals) {

           if (!arg.IsGhost) {

             string nm = FormalName(arg, i);

-            Indent(ind + IndentAmount); wr.WriteLine("hash = ((hash << 5) + hash) + ((ulong)this.@{0}.GetHashCode());", nm);

+            Indent(ind + IndentAmount, wr); wr.WriteLine("hash = ((hash << 5) + hash) + ((ulong)this.@{0}.GetHashCode());", nm);

             i++;

           }

         }

-        Indent(ind + IndentAmount); wr.WriteLine("return (int) hash;");

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

+        Indent(ind + IndentAmount, wr); wr.WriteLine("return (int) hash;");

+        Indent(ind, wr); wr.WriteLine("}");

 

         if (dt is IndDatatypeDecl) {

-          Indent(ind); wr.WriteLine("public override string ToString() {");

+          Indent(ind, wr); wr.WriteLine("public override string ToString() {");

           string nm;

           if (dt is TupleTypeDecl) {

             nm = "";

           } else {

             nm = (dt.Module.IsDefaultModule ? "" : dt.Module.CompileName + ".") + dt.CompileName + "." + ctor.CompileName;

           }

-          Indent(ind + IndentAmount); wr.WriteLine("string s = \"{0}\";", nm);

+          Indent(ind + IndentAmount, wr); wr.WriteLine("string s = \"{0}\";", nm);

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

-            Indent(ind + IndentAmount); wr.WriteLine("s += \"(\";");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("s += \"(\";");

             i = 0;

             foreach (var arg in ctor.Formals) {

               if (!arg.IsGhost) {

                 if (i != 0) {

-                  Indent(ind + IndentAmount); wr.WriteLine("s += \", \";");

+                  Indent(ind + IndentAmount, wr); wr.WriteLine("s += \", \";");

                 }

-                Indent(ind + IndentAmount); wr.WriteLine("s += @{0}.ToString();", FormalName(arg, i));

+                Indent(ind + IndentAmount, wr); wr.WriteLine("s += @{0}.ToString();", FormalName(arg, i));

                 i++;

               }

             }

-            Indent(ind + IndentAmount); wr.WriteLine("s += \")\";");

+            Indent(ind + IndentAmount, wr); wr.WriteLine("s += \")\";");

           }

-          Indent(ind + IndentAmount); wr.WriteLine("return s;");

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

+          Indent(ind + IndentAmount, wr); wr.WriteLine("return s;");

+          Indent(ind, wr); wr.WriteLine("}");

         }

 

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

+        Indent(indent, wr); wr.WriteLine("}");

       }

       constructorIndex++;

     }

 

-    void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

+    void CompileDatatypeStruct(DatatypeDecl dt, int indent, TextWriter wr) {

       Contract.Requires(dt != null);

 

       // public struct Dt<T> : IDatatype{

@@ -548,46 +541,46 @@ namespace Microsoft.Dafny {
         DtT += DtT_TypeArgs;

       }

 

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("public struct @{0} {{", DtT);

       int ind = indent + IndentAmount;

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("Base_{0} _d;", DtT);

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public Base_{0} _D {{", DtT);

-      Indent(ind + IndentAmount);

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("get {");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("if (_d == null) {");

-      Indent(ind + 3 * IndentAmount);

+      Indent(ind + 3 * IndentAmount, wr);

       wr.WriteLine("_d = Default;");

       if (dt is CoDatatypeDecl) {

         string typeParams = dt.TypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeParameters(dt.TypeArgs));

-        Indent(ind + 2 * IndentAmount);

+        Indent(ind + 2 * IndentAmount, wr);

         wr.WriteLine("}} else if (_d is {0}__Lazy{1}) {{", dt.CompileName, typeParams);

-        Indent(ind + 3 * IndentAmount);

+        Indent(ind + 3 * IndentAmount, wr);

         wr.WriteLine("_d = (({0}__Lazy{1})_d).Get();", dt.CompileName, typeParams);

       }

-      Indent(ind + 2 * IndentAmount);  wr.WriteLine("}");

-      Indent(ind + 2 * IndentAmount);  wr.WriteLine("return _d;");

-      Indent(ind + IndentAmount);  wr.WriteLine("}");

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

+      Indent(ind + 2 * IndentAmount, wr); wr.WriteLine("}");

+      Indent(ind + 2 * IndentAmount, wr); wr.WriteLine("return _d;");

+      Indent(ind + IndentAmount, wr); wr.WriteLine("}");

+      Indent(ind, wr); wr.WriteLine("}");

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public @{0}(Base_{1} d) {{ this._d = d; }}", dt.CompileName, DtT);

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("static Base_{0} theDefault;", DtT);

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public static Base_{0} Default {{", DtT);

-      Indent(ind + IndentAmount);

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("get {");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("if (theDefault == null) {");

-      Indent(ind + 3 * IndentAmount);

+      Indent(ind + 3 * IndentAmount, wr);

       wr.Write("theDefault = ");

 

       DatatypeCtor defaultCtor;

@@ -601,55 +594,55 @@ namespace Microsoft.Dafny {
       string sep = "";

       foreach (Formal f in defaultCtor.Formals) {

         if (!f.IsGhost) {

-          wr.Write("{0}{1}", sep, DefaultValue(f.Type));

+          wr.Write("{0}{1}", sep, DefaultValue(f.Type, wr));

           sep = ", ";

         }

       }

       wr.Write(")");

 

       wr.WriteLine(";");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("}");

-      Indent(ind + 2 * IndentAmount);

+      Indent(ind + 2 * IndentAmount, wr);

       wr.WriteLine("return theDefault;");

-      Indent(ind + IndentAmount); wr.WriteLine("}");

+      Indent(ind + IndentAmount, wr); wr.WriteLine("}");

 

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

+      Indent(ind, wr); wr.WriteLine("}");

 

-      Indent(ind);  wr.WriteLine("public override bool Equals(object other) {");

-      Indent(ind + IndentAmount);

+      Indent(ind, wr); wr.WriteLine("public override bool Equals(object other) {");

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("return other is @{0} && _D.Equals(((@{0})other)._D);", DtT);

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

+      Indent(ind, wr); wr.WriteLine("}");

 

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("public override int GetHashCode() { return _D.GetHashCode(); }");

       if (dt is IndDatatypeDecl) {

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public override string ToString() { return _D.ToString(); }");

       }

 

       // query properties

       foreach (var ctor in dt.Ctors) {

         //   public bool is_Ctor0 { get { return _D is Dt_Ctor0; } }

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public bool is_{0} {{ get {{ return _D is {1}_{0}{2}; }} }}", ctor.CompileName, dt.CompileName, DtT_TypeArgs);

       }

       if (dt.HasFinitePossibleValues) {

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("public static System.Collections.Generic.IEnumerable<@{0}> AllSingletonConstructors {{", DtT);

-        Indent(ind + IndentAmount);

+        Indent(ind + IndentAmount, wr);

         wr.WriteLine("get {");

         foreach (var ctr in dt.Ctors) {

           if (ctr.Formals.Count == 0) {

-            Indent(ind + IndentAmount + IndentAmount);

+            Indent(ind + IndentAmount + IndentAmount, wr);

             wr.WriteLine("yield return new @{0}(new {2}_{1}());", DtT, ctr.CompileName, dt.CompileName);

           }

         }

-        Indent(ind + IndentAmount + IndentAmount);

+        Indent(ind + IndentAmount + IndentAmount, wr);

         wr.WriteLine("yield break;");

-        Indent(ind + IndentAmount);

+        Indent(ind + IndentAmount, wr);

         wr.WriteLine("}");

-        Indent(ind);

+        Indent(ind, wr);

         wr.WriteLine("}");

       }

 

@@ -658,17 +651,17 @@ namespace Microsoft.Dafny {
         foreach (var arg in ctor.Formals) {

           if (!arg.IsGhost && arg.HasName) {

             //   public T0 @Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }

-            Indent(ind);

-            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);

+            Indent(ind, wr);

+            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type, wr), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);

           }

         }

       }

 

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("}");

     }

 

-    int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals)

+    int WriteFormals(string sep, List<Formal/*!*/>/*!*/ formals, TextWriter wr)

     {

       Contract.Requires(sep != null);

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

@@ -676,7 +669,7 @@ namespace Microsoft.Dafny {
       foreach (Formal arg in formals) {

         if (!arg.IsGhost) {

           string name = FormalName(arg, i);

-          wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);

+          wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type, wr), name);

           sep = ", ";

           i++;

         }

@@ -732,13 +725,13 @@ namespace Microsoft.Dafny {
       return s;

     }

 

-    string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs) {

+    string DtCtorName(DatatypeCtor ctor, List<Type> typeArgs, TextWriter wr) {

       Contract.Requires(ctor != null);

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

 

       var s = DtCtorName(ctor);

       if (typeArgs != null && typeArgs.Count != 0) {

-        s += "<" + TypeNames(typeArgs) + ">";

+        s += "<" + TypeNames(typeArgs, wr) + ">";

       }

       return s;

     }

@@ -776,7 +769,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent) {

+    void CompileClassMembers(ClassDecl c, bool forCompanionClass, int indent, TextWriter wr) {

       Contract.Requires(c != null);

       Contract.Requires(!forCompanionClass || c is TraitDecl);

       Contract.Requires(0 <= indent);

@@ -785,9 +778,9 @@ namespace Microsoft.Dafny {
         if (member is Field) {

           var f = (Field)member;

           // every field is inherited

-          Indent(indent);

-          wr.WriteLine("public {0} @_{1};", TypeName(f.Type), f.CompileName);

-          wr.Write("public {0} @{1}", TypeName(f.Type), f.CompileName);

+          Indent(indent, wr);

+          wr.WriteLine("public {0} @_{1};", TypeName(f.Type, wr), f.CompileName);

+          wr.Write("public {0} @{1}", TypeName(f.Type, wr), f.CompileName);

           wr.WriteLine(" {");

           wr.WriteLine(" get { ");

           wr.Write("return this.@_{0};", f.CompileName);

@@ -799,11 +792,11 @@ namespace Microsoft.Dafny {
         } else if (member is Function) {

           var f = (Function)member;

           Contract.Assert(f.Body != null);

-          CompileFunction(indent, f);

+          CompileFunction(indent, f, wr);

         } else if (member is Method) {

           var method = (Method)member;

           Contract.Assert(method.Body != null);

-          CompileMethod(c, indent, method);

+          CompileMethod(c, indent, method, wr);

         } else {

           Contract.Assert(false);  // unexpected member

         }

@@ -814,12 +807,12 @@ namespace Microsoft.Dafny {
           if (f.IsGhost || forCompanionClass) {

             // emit nothing

           } else if (c is TraitDecl) {

-            Indent(indent);

-            wr.Write("{0} @{1}", TypeName(f.Type), f.CompileName);

+            Indent(indent, wr);

+            wr.Write("{0} @{1}", TypeName(f.Type, wr), f.CompileName);

             wr.WriteLine(" { get; set; }");

           } else {

-            Indent(indent);

-            wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.CompileName, DefaultValue(f.Type));

+            Indent(indent, wr);

+            wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type, wr), f.CompileName, DefaultValue(f.Type, wr));

           }

         } else if (member is Function) {

           var f = (Function)member;

@@ -828,29 +821,29 @@ namespace Microsoft.Dafny {
             if (forCompanionClass || Attributes.Contains(f.Attributes, "axiom")) {

               // suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)

             } else {

-              Error("Function {0} has no body", f.FullName);

+              Error("Function {0} has no body", wr, f.FullName);

             }

           } else if (f.IsGhost) {

             // nothing to compile, but we do check for assumes

             if (f.Body == null) {

               Contract.Assert(c is TraitDecl && !f.IsStatic);

             } else {

-              var v = new CheckHasNoAssumes_Visitor(this);

+              var v = new CheckHasNoAssumes_Visitor(this, wr);

               v.Visit(f.Body);

             }

           } else if (c is TraitDecl && !forCompanionClass) {

             // include it, unless it's static

             if (!f.IsStatic) {

-              Indent(indent);

-              wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);

+              Indent(indent, wr);

+              wr.Write("{0} @{1}", TypeName(f.ResultType, wr), f.CompileName);

               wr.Write("(");

-              WriteFormals("", f.Formals);

+              WriteFormals("", f.Formals, wr);

               wr.WriteLine(");");

             }

           } else if (forCompanionClass && !f.IsStatic) {

             // companion classes only has static members

           } else {

-            CompileFunction(indent, f);

+            CompileFunction(indent, f, wr);

           }

         } else if (member is Method) {

           var m = (Method)member;

@@ -859,30 +852,30 @@ namespace Microsoft.Dafny {
             if (forCompanionClass || Attributes.Contains(m.Attributes, "axiom")) {

               // suppress error message (in the case of "forCompanionClass", the non-forCompanionClass call will produce the error message)

             } else {

-              Error("Method {0} has no body", m.FullName);

+              Error("Method {0} has no body", wr, m.FullName);

             }

           } else if (m.IsGhost) {

             // nothing to compile, but we do check for assumes

             if (m.Body == null) {

               Contract.Assert(c is TraitDecl && !m.IsStatic);

             } else {

-              var v = new CheckHasNoAssumes_Visitor(this);

+              var v = new CheckHasNoAssumes_Visitor(this, wr);

               v.Visit(m.Body);

             }

           } else if (c is TraitDecl && !forCompanionClass) {

             // include it, unless it's static

             if (!m.IsStatic) {

-              Indent(indent);

+              Indent(indent, wr);

               wr.Write("void @{0}", m.CompileName);

               wr.Write("(");

-              int nIns = WriteFormals("", m.Ins);

-              WriteFormals(nIns == 0 ? "" : ", ", m.Outs);

+              int nIns = WriteFormals("", m.Ins, wr);

+              WriteFormals(nIns == 0 ? "" : ", ", m.Outs, wr);

               wr.WriteLine(");");

             }

           } else if (forCompanionClass && !m.IsStatic) {

             // companion classes only has static members

           } else {

-            CompileMethod(c, indent, m);

+            CompileMethod(c, indent, m, wr);

           }

         } else {

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

@@ -890,59 +883,59 @@ namespace Microsoft.Dafny {
       }

     }

 

-    private void CompileFunction(int indent, Function f) {

-      Indent(indent);

-      wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);

+    private void CompileFunction(int indent, Function f, TextWriter wr) {

+      Indent(indent, wr);

+      wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType, wr), f.CompileName);

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

         wr.Write("<{0}>", TypeParameters(f.TypeArgs));

       }

       wr.Write("(");

-      WriteFormals("", f.Formals);

+      WriteFormals("", f.Formals, wr);

       wr.WriteLine(") {");

-      CompileReturnBody(f.Body, indent + IndentAmount);

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

+      CompileReturnBody(f.Body, indent + IndentAmount, wr);

+      Indent(indent, wr); wr.WriteLine("}");

     }

 

-    private void CompileMethod(ClassDecl c, int indent, Method m) {

-      Indent(indent);

+    private void CompileMethod(ClassDecl c, int indent, Method m, TextWriter wr) {

+      Indent(indent, wr);

       wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);

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

         wr.Write("<{0}>", TypeParameters(m.TypeArgs));

       }

       wr.Write("(");

-      int nIns = WriteFormals("", m.Ins);

-      WriteFormals(nIns == 0 ? "" : ", ", m.Outs);

+      int nIns = WriteFormals("", m.Ins, wr);

+      WriteFormals(nIns == 0 ? "" : ", ", m.Outs, wr);

       wr.WriteLine(")");

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

+      Indent(indent, wr); wr.WriteLine("{");

       foreach (Formal p in m.Outs) {

         if (!p.IsGhost) {

-          Indent(indent + IndentAmount);

-          wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type));

+          Indent(indent + IndentAmount, wr);

+          wr.WriteLine("@{0} = {1};", p.CompileName, DefaultValue(p.Type, wr));

         }

       }

       if (m.Body == null) {

-        Error("Method {0} has no body", m.FullName);

+        Error("Method {0} has no body", wr, m.FullName);

       } else {

         if (m.IsTailRecursive) {

-          Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");

+          Indent(indent, wr); wr.WriteLine("TAIL_CALL_START: ;");

           if (!m.IsStatic) {

-            Indent(indent + IndentAmount); wr.WriteLine("var _this = this;");

+            Indent(indent + IndentAmount, wr); wr.WriteLine("var _this = this;");

           }

         }

         Contract.Assert(enclosingMethod == null);

         enclosingMethod = m;

-        TrStmtList(m.Body.Body, indent);

+        TrStmtList(m.Body.Body, indent, wr);

         Contract.Assert(enclosingMethod == m);

         enclosingMethod = null;

       }

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

+      Indent(indent, wr); wr.WriteLine("}");

 

       // allow the Main method to be an instance method

       if (!m.IsStatic && IsMain(m)) {

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("public static void Main(string[] args) {");

         Contract.Assert(m.EnclosingClass == c);

-        Indent(indent + IndentAmount);

+        Indent(indent + IndentAmount, wr);

         wr.Write("@{0} b = new @{0}", c.CompileName);

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

           // instantiate every parameter, it doesn't particularly matter how

@@ -955,12 +948,12 @@ namespace Microsoft.Dafny {
           wr.Write(">");

         }

         wr.WriteLine("();");

-        Indent(indent + IndentAmount); wr.WriteLine("b.@Main();");

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

+        Indent(indent + IndentAmount, wr); wr.WriteLine("b.@Main();");

+        Indent(indent, wr); wr.WriteLine("}");

       }

     }

 

-    void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string, int indent) {

+    void TrCasePatternOpt(CasePattern pat, Expression rhs, string rhs_string, int indent, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(pat != null);

       Contract.Requires(pat.Var != null || rhs != null);

       if (pat.Var != null) {

@@ -970,10 +963,10 @@ namespace Microsoft.Dafny {
         // var x := G;

         var bv = pat.Var;

         if (!bv.IsGhost) {

-          Indent(indent);

-          wr.Write("{0} {1} = ", TypeName(bv.Type), "@" + bv.CompileName);

+          Indent(indent, wr);

+          wr.Write("{0} {1} = ", TypeName(bv.Type, wr), "@" + bv.CompileName);

           if (rhs != null) {

-            TrExpr(rhs);

+            TrExpr(rhs, wr, inLetExprBody);

           } else {

             wr.Write(rhs_string);

           }

@@ -992,9 +985,9 @@ namespace Microsoft.Dafny {
 

         // Create the temporary variable to hold G

         var tmp_name = idGenerator.FreshId("_let_tmp_rhs");

-        Indent(indent);

-        wr.Write("{0} {1} = ", TypeName(rhs.Type), tmp_name);

-        TrExpr(rhs);

+        Indent(indent, wr);

+        wr.Write("{0} {1} = ", TypeName(rhs.Type, wr), tmp_name);

+        TrExpr(rhs, wr, inLetExprBody);

         wr.WriteLine(";");

 

         var k = 0;  // number of non-ghost formals processed

@@ -1005,21 +998,21 @@ namespace Microsoft.Dafny {
             // nothing to compile, but do a sanity check

             Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));

           } else {            

-            TrCasePatternOpt(arg, null, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), tmp_name, FormalName(formal, k)), indent);

+            TrCasePatternOpt(arg, null, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs, wr), tmp_name, FormalName(formal, k)), indent, wr, inLetExprBody);

             k++;

           }

         }

       }

     }

 

-    void ReturnExpr(Expression expr, int indent) {

-      Indent(indent);

+    void ReturnExpr(Expression expr, int indent, TextWriter wr, bool inLetExprBody) {

+      Indent(indent, wr);

       wr.Write("return ");

-      TrExpr(expr);

+      TrExpr(expr, wr, inLetExprBody);

       wr.WriteLine(";");

     }

 

-    void TrExprOpt(Expression expr, int indent) {

+    void TrExprOpt(Expression expr, int indent, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(expr != null);

       if (expr is LetExpr) {

         var e = (LetExpr)expr;

@@ -1027,25 +1020,25 @@ namespace Microsoft.Dafny {
           for (int i = 0; i < e.LHSs.Count; i++) {

             var lhs = e.LHSs[i];

             if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {

-              TrCasePatternOpt(lhs, e.RHSs[i], null, indent);

+              TrCasePatternOpt(lhs, e.RHSs[i], null, indent, wr, inLetExprBody);

             }            

           }

-          TrExprOpt(e.Body, indent);

+          TrExprOpt(e.Body, indent, wr, inLetExprBody);

         } else {

           // We haven't optimized the other cases, so fallback to normal compilation

-          ReturnExpr(e, indent);

+          ReturnExpr(e, indent, wr, inLetExprBody);

         }

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("if (");

-        TrExpr(e.Test);

+        TrExpr(e.Test, wr, inLetExprBody);

         wr.Write(") {\n");

-        TrExprOpt(e.Thn, indent + IndentAmount);

-        Indent(indent);

+        TrExprOpt(e.Thn, indent + IndentAmount, wr, inLetExprBody);

+        Indent(indent, wr);

         wr.WriteLine("} else {");

-        TrExprOpt(e.Els, indent + IndentAmount);

-        Indent(indent);

+        TrExprOpt(e.Els, indent + IndentAmount, wr, inLetExprBody);

+        Indent(indent, wr);

         wr.WriteLine("}");

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;   

@@ -1060,9 +1053,9 @@ namespace Microsoft.Dafny {
         //     ...

         //   }

         string source = idGenerator.FreshId("_source");

-        Indent(indent);

-        wr.Write("{0} {1} = ", TypeName(e.Source.Type), source);

-        TrExpr(e.Source);

+        Indent(indent, wr);

+        wr.Write("{0} {1} = ", TypeName(e.Source.Type, wr), source);

+        TrExpr(e.Source, wr, inLetExprBody);

         wr.WriteLine(";");        

 

         if (e.Cases.Count == 0) {

@@ -1073,28 +1066,28 @@ namespace Microsoft.Dafny {
           var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();

           foreach (MatchCaseExpr mc in e.Cases) {

             //Indent(indent);

-            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, indent);

-            TrExprOpt(mc.Body, indent + IndentAmount);

+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, indent, wr);

+            TrExprOpt(mc.Body, indent + IndentAmount, wr, inLetExprBody);

             i++;

           }

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("}");

         }        

       }  else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

-        TrExprOpt(e.E, indent);

+        TrExprOpt(e.E, indent, wr, inLetExprBody);

       } else {

         // We haven't optimized any other cases, so fallback to normal compilation

-        ReturnExpr(expr, indent);

+        ReturnExpr(expr, indent, wr, inLetExprBody);

       }

     }

 

-    void CompileReturnBody(Expression body, int indent) {

+    void CompileReturnBody(Expression body, int indent, TextWriter wr) {

       Contract.Requires(0 <= indent);

       body = body.Resolved;

       //Indent(indent);

       //wr.Write("return ");

-      TrExprOpt(body, indent);

+      TrExprOpt(body, indent, wr, false);

       //wr.WriteLine(";");

     }

 

@@ -1113,23 +1106,23 @@ namespace Microsoft.Dafny {
       return null;

     }

 

-    string TypeName_Companion(Type type) {

+    string TypeName_Companion(Type type, TextWriter wr) {

       Contract.Requires(type != null);

       var udt = type as UserDefinedType;

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

         string s = udt.FullCompanionCompileName;

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

           if (udt.TypeArgs.Exists(argType => argType is ObjectType)) {

-            Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

+            Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost", wr);

           }

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

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

         }

         return s;

       } else {

-        return TypeName(type);

+        return TypeName(type, wr);

       }

     }

-    string TypeName(Type type)

+    string TypeName(Type type, TextWriter wr)

     {

       Contract.Requires(type != null);

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

@@ -1153,14 +1146,14 @@ namespace Microsoft.Dafny {
         if (nativeType != null) {

           return nativeType.Name;

         }

-        return TypeName(xType.AsNewtype.BaseType);

+        return TypeName(xType.AsNewtype.BaseType, wr);

       } else if (xType is ObjectType) {

         return "object";

       } else if (xType.IsArrayType) {

         ArrayClassDecl at = xType.AsArrayType;

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

         Type elType = UserDefinedType.ArrayElementType(xType);

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

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

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

           name += ",";

         }

@@ -1184,54 +1177,60 @@ namespace Microsoft.Dafny {
           }

           s = rc.FullCompileName;

         }

-        return TypeName_UDT(s, udt.TypeArgs);

+        return TypeName_UDT(s, udt.TypeArgs, wr);

       } 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");

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

         }

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

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

       } 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");

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

         }

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

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

       } 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");

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

         }

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

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

       } 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");

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

         }

-        return DafnyMapClass + "<" + TypeName(domType) + "," + TypeName(ranType) + ">";

+        return DafnyMapClass + "<" + TypeName(domType, wr) + "," + TypeName(ranType, wr) + ">";

       } else {

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

       }

     }

 

-    string TypeName_UDT(string fullCompileName, List<Type> typeArgs) {

+    string TypeName_UDT(string fullCompileName, List<Type> typeArgs, TextWriter wr) {

       Contract.Requires(fullCompileName != null);

       Contract.Requires(typeArgs != null);

       string s = "@" + fullCompileName;

       if (typeArgs.Count != 0) {

         if (typeArgs.Exists(argType => argType is ObjectType)) {

-          Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");

+          Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost", wr);

         }

-        s += "<" + TypeNames(typeArgs) + ">";

+        s += "<" + TypeNames(typeArgs, wr) + ">";

       }

       return s;

     }

 

-    string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types) {

+    string/*!*/ TypeNames(List<Type/*!*/>/*!*/ types, TextWriter wr) {

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

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

-      return Util.Comma(types, TypeName);

+      string res = "";

+      string c = "";

+      foreach (var t in types) {

+        res += c + TypeName(t, wr);

+        c = ",";

+      }

+      return res;

     }

 

     string/*!*/ TypeParameters(List<TypeParameter/*!*/>/*!*/ targs) {

@@ -1241,7 +1240,7 @@ namespace Microsoft.Dafny {
       return Util.Comma(targs, tp => "@" + tp.CompileName);

     }

 

-    string DefaultValue(Type type)

+    string DefaultValue(Type type, TextWriter wr)

     {

       Contract.Requires(type != null);

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

@@ -1264,9 +1263,9 @@ namespace Microsoft.Dafny {
         if (xType.AsNewtype.NativeType != null) {

           return "0";

         }

-        return DefaultValue(xType.AsNewtype.BaseType);

+        return DefaultValue(xType.AsNewtype.BaseType, wr);

       } else if (xType.IsRefType) {

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

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

       } else if (xType.IsDatatype) {

         var udt = (UserDefinedType)xType;

         var s = "@" + udt.FullCompileName;

@@ -1287,7 +1286,7 @@ namespace Microsoft.Dafny {
           s = "@" + rc.FullCompileName;

         }

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

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

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

         }

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

       } else if (xType.IsTypeParameter) {

@@ -1295,18 +1294,18 @@ namespace Microsoft.Dafny {
         string s = "default(@" + udt.FullCompileName;

         if (udt.TypeArgs.Count != 0)

         {

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

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

         }

         s += ")";

         return s;

       } else if (xType is SetType) {

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

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

       } else if (xType is MultiSetType) {

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

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

       } else if (xType is SeqType) {

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

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

       } else if (xType is MapType) {

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

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

       } else if (xType is ArrowType) {

         return "null";

       } else {

@@ -1319,59 +1318,61 @@ namespace Microsoft.Dafny {
     public class CheckHasNoAssumes_Visitor : BottomUpVisitor

     {

       readonly Compiler compiler;

-      public CheckHasNoAssumes_Visitor(Compiler c) {

+      TextWriter wr;

+      public CheckHasNoAssumes_Visitor(Compiler c, TextWriter wr) {

         Contract.Requires(c != null);

         compiler = c;

+        this.wr = wr;

       }

       protected override void VisitOneStmt(Statement stmt) {

         if (stmt is AssumeStmt) {

-          compiler.Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);

+          compiler.Error("an assume statement cannot be compiled (line {0})", wr, stmt.Tok.line);

         } else if (stmt is AssignSuchThatStmt) {

           var s = (AssignSuchThatStmt)stmt;

           if (s.AssumeToken != null) {

-            compiler.Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);

+            compiler.Error("an assume statement cannot be compiled (line {0})", wr, s.AssumeToken.line);

           }

         } else if (stmt is ForallStmt) {

           var s = (ForallStmt)stmt;

           if (s.Body == null) {

-            compiler.Error("a forall statement without a body cannot be compiled (line {0})", stmt.Tok.line);

+            compiler.Error("a forall statement without a body cannot be compiled (line {0})", wr, stmt.Tok.line);

           }

         } else if (stmt is WhileStmt) {

           var s = (WhileStmt)stmt;

           if (s.Body == null) {

-            compiler.Error("a while statement without a body cannot be compiled (line {0})", stmt.Tok.line);

+            compiler.Error("a while statement without a body cannot be compiled (line {0})", wr, stmt.Tok.line);

           }

         }

       }

     }

 

-    void TrStmt(Statement stmt, int indent)

+    TextWriter TrStmt(Statement stmt, int indent)

     {

       Contract.Requires(stmt != null);

+      TextWriter wr = new StringWriter();

       if (stmt.IsGhost) {

-        var v = new CheckHasNoAssumes_Visitor(this);

+        var v = new CheckHasNoAssumes_Visitor(this, wr);

         v.Visit(stmt);

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

-        return;

+        Indent(indent, wr); wr.WriteLine("{ }");

+        return wr;

       }

-

       if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         foreach (var arg in s.Args) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("System.Console.Write(");

-          TrExpr(arg);

+          TrExpr(arg, wr, false);

           wr.WriteLine(");");

         }

       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.Data.AssignUniqueId("after_", idGenerator));

       } else if (stmt is ProduceStmt) {

         var s = (ProduceStmt)stmt;

         if (s.hiddenUpdate != null)

-          TrStmt(s.hiddenUpdate, indent);

-        Indent(indent);

+          wr.Write(TrStmt(s.hiddenUpdate, indent).ToString());

+        Indent(indent, wr);

         if (s is YieldStmt) {

           wr.WriteLine("yield return null;");

         } else {

@@ -1381,7 +1382,7 @@ namespace Microsoft.Dafny {
         var s = (UpdateStmt)stmt;

         var resolved = s.ResolvedStatements;

         if (resolved.Count == 1) {

-          TrStmt(resolved[0], indent);

+          wr.Write(TrStmt(resolved[0], indent).ToString());

         } else {

           // multi-assignment

           Contract.Assert(s.Lhss.Count == resolved.Count);

@@ -1393,17 +1394,17 @@ namespace Microsoft.Dafny {
               var lhs = s.Lhss[i];

               var rhs = s.Rhss[i];

               if (!(rhs is HavocRhs)) {

-                lvalues.Add(CreateLvalue(lhs, indent));

+                lvalues.Add(CreateLvalue(lhs, indent, wr));

 

                 string target = idGenerator.FreshId("_rhs");

                 rhss.Add(target);

-                TrRhs("var " + target, null, rhs, indent);

+                TrRhs("var " + target, null, rhs, indent, wr);

               }

             }

           }

           Contract.Assert(lvalues.Count == rhss.Count);

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

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);

           }

         }

@@ -1411,32 +1412,32 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         Contract.Assert(!(s.Lhs is SeqSelectExpr) || ((SeqSelectExpr)s.Lhs).SelectOne);  // multi-element array assignments are not allowed

-        TrRhs(null, s.Lhs, s.Rhs, indent);

+        TrRhs(null, s.Lhs, s.Rhs, indent, wr);

 

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;

         if (s.AssumeToken != null) {

           // Note, a non-ghost AssignSuchThatStmt may contain an assume

-          Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);

+          Error("an assume statement cannot be compiled (line {0})", wr, s.AssumeToken.line);

         } else if (s.MissingBounds != null) {

           foreach (var bv in s.MissingBounds) {

-            Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, s.Tok.line);

+            Error("this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", wr, bv.Name, s.Tok.line);

           }

         } else {

           Contract.Assert(s.Bounds != null);  // follows from s.MissingBounds == null

           TrAssignSuchThat(indent,

             s.Lhss.ConvertAll(lhs => ((IdentifierExpr)lhs.Resolved).Var),  // the resolver allows only IdentifierExpr left-hand sides

-            s.Expr, s.Bounds, s.Tok.line);

+            s.Expr, s.Bounds, s.Tok.line, wr, false);

         }

 

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

-        TrCallStmt(s, null, indent);

+        wr.Write(TrCallStmt(s, null, indent).ToString());

 

       } else if (stmt is BlockStmt) {

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

-        TrStmtList(((BlockStmt)stmt).Body, indent);

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

+        Indent(indent, wr); wr.WriteLine("{");

+        TrStmtList(((BlockStmt)stmt).Body, indent, wr);

+        Indent(indent, wr); wr.WriteLine("}");

 

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

@@ -1445,45 +1446,45 @@ namespace Microsoft.Dafny {
           if (s.Els == null) {

             // let's compile the "else" branch, since that involves no work

             // (still, let's leave a marker in the source code to indicate that this is what we did)

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("if (!false) { }");

           } else {

             // let's compile the "then" branch

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("if (true)");

-            TrStmt(s.Thn, indent);

+            wr.Write(TrStmt(s.Thn, indent).ToString());

           }

         } else {

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

-          TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard);

+          Indent(indent, wr); wr.Write("if (");

+          TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard, wr, false);

           wr.WriteLine(")");

 

           // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block

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

+          Indent(indent, wr); wr.WriteLine("{");

           if (s.IsExistentialGuard) {

-            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard);

+            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard, wr);

           }

-          TrStmtList(s.Thn.Body, indent);

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

+          TrStmtList(s.Thn.Body, indent, wr);

+          Indent(indent, wr); wr.WriteLine("}");

 

           if (s.Els != null) {

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

-            TrStmt(s.Els, indent);

+            Indent(indent, wr); wr.WriteLine("else");

+            wr.Write(TrStmt(s.Els, indent).ToString());

           }

         }

 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

-        Indent(indent);

+        Indent(indent, wr);

         foreach (var alternative in s.Alternatives) {

           wr.Write("if (");

-          TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard);

+          TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard, wr, false);

           wr.WriteLine(") {");

           if (alternative.IsExistentialGuard) {

-            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard);

+            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard, wr);

           }

-          TrStmtList(alternative.Body, indent);

-          Indent(indent);

+          TrStmtList(alternative.Body, indent, wr);

+          Indent(indent, wr);

           wr.Write("} else ");

         }

         wr.WriteLine("{ /*unreachable alternative*/ }");

@@ -1491,38 +1492,38 @@ namespace Microsoft.Dafny {
       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

         if (s.Body == null) {

-          return;

+          return wr;

         }

         if (s.Guard == null) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("while (false) { }");

         } else {

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("while (");

-          TrExpr(s.Guard);

+          TrExpr(s.Guard, wr, false);

           wr.WriteLine(")");

-          TrStmt(s.Body, indent);

+          wr.Write(TrStmt(s.Body, indent).ToString());

         }

 

       } else if (stmt is AlternativeLoopStmt) {

         var s = (AlternativeLoopStmt)stmt;

         if (s.Alternatives.Count != 0) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("while (true) {");

           int ind = indent + IndentAmount;

           foreach (var alternative in s.Alternatives) {

           }

-          Indent(ind);

+          Indent(ind, wr);

           foreach (var alternative in s.Alternatives) {

             wr.Write("if (");

-            TrExpr(alternative.Guard);

+            TrExpr(alternative.Guard, wr, false);

             wr.WriteLine(") {");

-            TrStmtList(alternative.Body, ind);

-            Indent(ind);

+            TrStmtList(alternative.Body, ind, wr);

+            Indent(ind, wr);

             wr.Write("} else ");

           }

           wr.WriteLine("{ break; }");

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("}");

         }

 

@@ -1530,17 +1531,17 @@ namespace Microsoft.Dafny {
         var s = (ForallStmt)stmt;

         if (s.Kind != ForallStmt.ParBodyKind.Assign) {

           // Call and Proof have no side effects, so they can simply be optimized away.

-          return;

+          return wr;

         } else if (s.BoundVars.Count == 0) {

           // the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body

-          TrStmt(s.Body, indent);

-          return;

+          wr.Write(TrStmt(s.Body, indent).ToString());

+          return wr;

         }

         var s0 = (AssignStmt)s.S0;

         if (s0.Rhs is HavocRhs) {

           // The forall statement says to havoc a bunch of things.  This can be efficiently compiled

           // into doing nothing.

-          return;

+          return wr;

         }

         var rhs = ((ExprRhs)s0.Rhs).Expr;

 

@@ -1584,29 +1585,29 @@ namespace Microsoft.Dafny {
         if (s0.Lhs is MemberSelectExpr) {

           var lhs = (MemberSelectExpr)s0.Lhs;

           L = 2;

-          tupleTypeArgs = TypeName(lhs.Obj.Type);

+          tupleTypeArgs = TypeName(lhs.Obj.Type, wr);

         } else if (s0.Lhs is SeqSelectExpr) {

           var lhs = (SeqSelectExpr)s0.Lhs;

           L = 3;

           // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

-          tupleTypeArgs = TypeName(lhs.Seq.Type) + ",int";

+          tupleTypeArgs = TypeName(lhs.Seq.Type, wr) + ",int";

         } else {

           var lhs = (MultiSelectExpr)s0.Lhs;

           L = 2 + lhs.Indices.Count;

           if (8 < L) {

-            Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements");

-            return;

+            Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements", wr);

+            return wr;

           }

-          tupleTypeArgs = TypeName(lhs.Array.Type);

+          tupleTypeArgs = TypeName(lhs.Array.Type, wr);

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

             // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple

             tupleTypeArgs += ",int";

           }

         }

-        tupleTypeArgs += "," + TypeName(rhs.Type);

+        tupleTypeArgs += "," + TypeName(rhs.Type, wr);

 

         // declare and construct "ingredients"

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("var {0} = new System.Collections.Generic.List<System.Tuple<{1}>>();", ingredients, tupleTypeArgs);

 

         var n = s.BoundVars.Count;

@@ -1616,38 +1617,38 @@ namespace Microsoft.Dafny {
           var bound = s.Bounds[i];

           var bv = s.BoundVars[i];

           if (bound is ComprehensionExpr.BoolBoundedPool) {

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);

           } else if (bound is ComprehensionExpr.CharBoundedPool) {

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);

           } else if (bound is ComprehensionExpr.IntBoundedPool) {

             var b = (ComprehensionExpr.IntBoundedPool)bound;

-            Indent(ind);

+            Indent(ind, wr);

             if (AsNativeType(bv.Type) != null) {

               wr.Write("foreach (var @{0} in @{1}.IntegerRange(", bv.CompileName, bv.Type.AsNewtype.FullCompileName);

             } else {

               wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);

             }

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, false);

             wr.Write(", ");

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, false);

             wr.Write(")) { ");

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Set);

+            TrExpr(b.Set, wr, false);

             wr.Write(").Elements) { ");

           } else if (bound is ComprehensionExpr.SeqBoundedPool) {

             var b = (ComprehensionExpr.SeqBoundedPool)bound;

-            Indent(ind);

+            Indent(ind, wr);

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Seq);

+            TrExpr(b.Seq, wr, false);

             wr.Write(").UniqueElements) { ");

           } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

-            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

+            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type, wr));

           } else {

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

           }

@@ -1657,55 +1658,55 @@ namespace Microsoft.Dafny {
         // if (range) {

         //   ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));

         // }

-        Indent(indent + n * IndentAmount);

+        Indent(indent + n * IndentAmount, wr);

         wr.Write("if (");

         foreach (var bv in s.BoundVars) {

           if (bv.Type.NormalizeExpand() is NatType) {

             wr.Write("0 <= {0} && ", bv.CompileName);

           }

         }

-        TrExpr(s.Range);

+        TrExpr(s.Range, wr, false);

         wr.WriteLine(") {");

 

         var indFinal = indent + (n + 1) * IndentAmount;

-        Indent(indFinal);

+        Indent(indFinal, wr);

         wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);

         if (s0.Lhs is MemberSelectExpr) {

           var lhs = (MemberSelectExpr)s0.Lhs;

-          TrExpr(lhs.Obj);

+          TrExpr(lhs.Obj, wr, false);

         } else if (s0.Lhs is SeqSelectExpr) {

           var lhs = (SeqSelectExpr)s0.Lhs;

-          TrExpr(lhs.Seq);

+          TrExpr(lhs.Seq, wr, false);

           wr.Write(", (int)(");

-          TrExpr(lhs.E0);

+          TrExpr(lhs.E0, wr, false);

           wr.Write(")");

         } else {

           var lhs = (MultiSelectExpr)s0.Lhs;

-          TrExpr(lhs.Array);

+          TrExpr(lhs.Array, wr, false);

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

             wr.Write(", (int)(");

-            TrExpr(lhs.Indices[i]);

+            TrExpr(lhs.Indices[i], wr, false);

             wr.Write(")");

           }

         }

         wr.Write(", ");

-        TrExpr(rhs);

+        TrExpr(rhs, wr, false);

         wr.WriteLine("));");

 

-        Indent(indent + n * IndentAmount);

+        Indent(indent + n * IndentAmount, wr);

         wr.WriteLine("}");

 

         for (int i = n; 0 <= --i; ) {

-          Indent(indent + i * IndentAmount);

+          Indent(indent + i * IndentAmount, wr);

           wr.WriteLine("}");

         }

 

         //   foreach (L-Tuple l in ingredients) {

         //     LHS[ l0, l1, l2, ..., l(L-2) ] = l(L-1);

         //   }

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("foreach (var {0} in {1}) {{", tup, ingredients);

-        Indent(indent + IndentAmount);

+        Indent(indent + IndentAmount, wr);

         if (s0.Lhs is MemberSelectExpr) {

           var lhs = (MemberSelectExpr)s0.Lhs;

           wr.WriteLine("{0}.Item1.@{1} = {0}.Item2;", tup, lhs.MemberName);

@@ -1722,7 +1723,7 @@ namespace Microsoft.Dafny {
           }

           wr.WriteLine("] = {0}.Item{1};", tup, L);

         }

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("}");

 

       } else if (stmt is MatchStmt) {

@@ -1739,54 +1740,56 @@ namespace Microsoft.Dafny {
         // }

         if (s.Cases.Count != 0) {

           string source = idGenerator.FreshId("_source");

-          Indent(indent);

-          wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type)), source);

-          TrExpr(s.Source);

+          Indent(indent, wr);

+          wr.Write("{0} {1} = ", TypeName(cce.NonNull(s.Source.Type), wr), source);

+          TrExpr(s.Source, wr, false);

           wr.WriteLine(";");

 

           int i = 0;

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

           foreach (MatchCaseStmt mc in s.Cases) {

-            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);

-            TrStmtList(mc.Body, indent);

+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent, wr);

+            TrStmtList(mc.Body, indent, wr);

             i++;

           }

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

+          Indent(indent, wr); wr.WriteLine("}");

         }

 

       } else if (stmt is VarDeclStmt) {

         var s = (VarDeclStmt)stmt;

         foreach (var local in s.Locals) {

-          TrLocalVar(local, true, indent);

+          TrLocalVar(local, true, indent, wr);

         }

         if (s.Update != null) {

-          TrStmt(s.Update, indent);

+          wr.Write(TrStmt(s.Update, indent).ToString());

         }

 

       } else if (stmt is ModifyStmt) {

         var s = (ModifyStmt)stmt;

         if (s.Body != null) {

-          TrStmt(s.Body, indent);

+          wr.Write(TrStmt(s.Body, indent).ToString());

         }

 

       } else {

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

       }

+

+      return wr;

     }

 

-    private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists) {

+    private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists, TextWriter wr) {

       Contract.Requires(0 <= indent);

       Contract.Requires(exists != null);

       Contract.Assume(exists.Bounds != null);  // follows from successful resolution

       Contract.Assert(exists.Range == null);  // follows from invariant of class IfStmt

       foreach (var bv in exists.BoundVars) {

-        TrLocalVar(bv, false, indent);

+        TrLocalVar(bv, false, indent, wr);

       }

       var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);

-      TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line);

+      TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line, wr, false);

     }

 

-    private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine) {

+    private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(0 <= indent);

       Contract.Requires(lhss != null);

       Contract.Requires(constraint != null);

@@ -1828,7 +1831,7 @@ namespace Microsoft.Dafny {
       int ind = indent;

       bool needIterLimit = lhss.Count != 1 && bounds.Exists(bnd => !bnd.IsFinite);

       if (needIterLimit) {

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("for (var {0} = new BigInteger(5); ; {0} *= 2) {{", iterLimit);

         ind += IndentAmount;

       }

@@ -1837,11 +1840,11 @@ namespace Microsoft.Dafny {
         var bound = bounds[i];

         var bv = lhss[i];

         if (needIterLimit) {

-          Indent(ind);

+          Indent(ind, wr);

           wr.WriteLine("var {0}_{1} = {0};", iterLimit, i);

         }

         var tmpVar = idGenerator.FreshId("_assign_such_that_");

-        Indent(ind);

+        Indent(ind, wr);

         if (bound is ComprehensionExpr.BoolBoundedPool) {

           wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is ComprehensionExpr.CharBoundedPool) {

@@ -1856,13 +1859,13 @@ namespace Microsoft.Dafny {
           if (b.LowerBound == null) {

             wr.Write("null");

           } else {

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, inLetExprBody);

           }

           wr.Write(", ");

           if (b.UpperBound == null) {

             wr.Write("null");

           } else {

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, inLetExprBody);

           }

           wr.WriteLine(")) {{ @{1} = {0};", tmpVar, bv.CompileName);

         } else if (bound is AssignSuchThatStmt.WiggleWaggleBound) {

@@ -1870,54 +1873,54 @@ namespace Microsoft.Dafny {
         } else if (bound is ComprehensionExpr.SetBoundedPool) {

           var b = (ComprehensionExpr.SetBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.Set);

+          TrExpr(b.Set, wr, inLetExprBody);

           wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.SubSetBoundedPool) {

           var b = (ComprehensionExpr.SubSetBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.UpperBound);

+          TrExpr(b.UpperBound, wr, inLetExprBody);

           wr.WriteLine(").AllSubsets) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.MapBoundedPool) {

           var b = (ComprehensionExpr.MapBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.Map);

+          TrExpr(b.Map, wr, inLetExprBody);

           wr.WriteLine(").Domain) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.SeqBoundedPool) {

           var b = (ComprehensionExpr.SeqBoundedPool)bound;

           wr.Write("foreach (var {0} in (", tmpVar);

-          TrExpr(b.Seq);

+          TrExpr(b.Seq, wr, inLetExprBody);

           wr.WriteLine(").Elements) {{ @{0} = {1};", bv.CompileName, tmpVar);

         } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

           var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

-          wr.WriteLine("foreach (var {0} in {1}.AllSingletonConstructors) {{ @{2} = {0};", tmpVar, TypeName(bv.Type), bv.CompileName);

+          wr.WriteLine("foreach (var {0} in {1}.AllSingletonConstructors) {{ @{2} = {0};", tmpVar, TypeName(bv.Type, wr), bv.CompileName);

         } else {

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

         }

         if (needIterLimit) {

-          Indent(ind + IndentAmount);

+          Indent(ind + IndentAmount, wr);

           wr.WriteLine("if ({0}_{1} == 0) {{ break; }}  {0}_{1}--;", iterLimit, i);

         }

       }

-      Indent(ind);

+      Indent(ind, wr);

       wr.Write("if (");

-      TrExpr(constraint);

+      TrExpr(constraint, wr, inLetExprBody);

       wr.WriteLine(") {");

-      Indent(ind + IndentAmount);

+      Indent(ind + IndentAmount, wr);

       wr.WriteLine("goto {0};", doneLabel);

-      Indent(ind);

+      Indent(ind, wr);

       wr.WriteLine("}");

-      Indent(indent);

+      Indent(indent, wr);

       for (int i = 0; i < n; i++) {

         wr.Write(i == 0 ? "}" : " }");

       }

       wr.WriteLine(needIterLimit ? " }" : "");

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("throw new System.Exception(\"assign-such-that search produced no value (line {0})\");", debuginfoLine);

-      Indent(indent);

+      Indent(indent, wr);

       wr.WriteLine("{0}: ;", doneLabel);

     }

 

-    string CreateLvalue(Expression lhs, int indent) {

+    string CreateLvalue(Expression lhs, int indent, TextWriter wr) {

       lhs = lhs.Resolved;

       if (lhs is IdentifierExpr) {

         var ll = (IdentifierExpr)lhs;

@@ -1925,9 +1928,9 @@ namespace Microsoft.Dafny {
       } else if (lhs is MemberSelectExpr) {

         var ll = (MemberSelectExpr)lhs;

         string obj = idGenerator.FreshId("_obj");

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", obj);

-        TrExpr(ll.Obj);

+        TrExpr(ll.Obj, wr, false);

         wr.WriteLine(";");

         return string.Format("{0}.@{1}", obj, ll.Member.CompileName);

       } else if (lhs is SeqSelectExpr) {

@@ -1935,31 +1938,31 @@ namespace Microsoft.Dafny {
         var c = idGenerator.FreshNumericId("_arr+_index");

         string arr = "_arr" + c;

         string index = "_index" + c;

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", arr);

-        TrExpr(ll.Seq);

+        TrExpr(ll.Seq, wr, false);

         wr.WriteLine(";");

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", index);

-        TrExpr(ll.E0);

+        TrExpr(ll.E0, wr, false);

         wr.WriteLine(";");

         return string.Format("{0}[(int){1}]", arr, index);

       } else {

         var ll = (MultiSelectExpr)lhs;

         var c = idGenerator.FreshNumericId("_arr+_index");

         string arr = "_arr" + c;

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", arr);

-        TrExpr(ll.Array);

+        TrExpr(ll.Array, wr, false);

         wr.WriteLine(";");

         string fullString = arr + "[";

         string sep = "";

         int i = 0;

         foreach (var idx in ll.Indices) {

           string index = "_index" + i + "_" + c;

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("var {0} = ", index);

-          TrExpr(idx);

+          TrExpr(idx, wr, false);

           wr.WriteLine(";");

           fullString += sep + "(int)" + index;

           sep = ", ";

@@ -1969,21 +1972,21 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent) {

+    void TrRhs(string target, Expression targetExpr, AssignmentRhs rhs, int indent, TextWriter wr) {

       Contract.Requires((target == null) != (targetExpr == null));

       var tRhs = rhs as TypeRhs;

       if (tRhs != null && tRhs.InitCall != null) {

         string nw = idGenerator.FreshId("_nw");

-        Indent(indent);

+        Indent(indent, wr);

         wr.Write("var {0} = ", nw);

-        TrAssignmentRhs(rhs);  // in this case, this call will not require us to spill any let variables first

+        TrAssignmentRhs(rhs, wr);  // in this case, this call will not require us to spill any let variables first

         wr.WriteLine(";");

-        TrCallStmt(tRhs.InitCall, nw, indent);

-        Indent(indent);

+        wr.Write(TrCallStmt(tRhs.InitCall, nw, indent).ToString());

+        Indent(indent, wr);

         if (target != null) {

           wr.Write(target);

         } else {

-          TrExpr(targetExpr);

+          TrExpr(targetExpr, wr, false);

         }

         wr.WriteLine(" = {0};", nw);

       } else if (rhs is HavocRhs) {

@@ -1994,22 +1997,23 @@ namespace Microsoft.Dafny {
           foreach (Expression dim in tRhs.ArrayDimensions) {

           }

         }

-        Indent(indent);

+        Indent(indent, wr);

         if (target != null) {

           wr.Write(target);

         } else {

-          TrExpr(targetExpr);

+          TrExpr(targetExpr, wr, false);

         }

         wr.Write(" = ");

-        TrAssignmentRhs(rhs);

+        TrAssignmentRhs(rhs, wr);

         wr.WriteLine(";");

       }

     }

 

-    void TrCallStmt(CallStmt s, string receiverReplacement, int indent) {

+    TextWriter TrCallStmt(CallStmt s, string receiverReplacement, int indent) {

       Contract.Requires(s != null);

       Contract.Assert(s.Method != null);  // follows from the fact that stmt has been successfully resolved

 

+      StringWriter wr = new StringWriter();

       if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {

         // compile call as tail-recursive

 

@@ -2026,9 +2030,9 @@ namespace Microsoft.Dafny {
 

           string inTmp = idGenerator.FreshId("_in");

           inTmps.Add(inTmp);

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("var {0} = ", inTmp);

-          TrExpr(s.Receiver);

+          TrExpr(s.Receiver, wr, false);

           wr.WriteLine(";");

         }

         for (int i = 0; i < s.Method.Ins.Count; i++) {

@@ -2036,29 +2040,29 @@ namespace Microsoft.Dafny {
           if (!p.IsGhost) {

             string inTmp = idGenerator.FreshId("_in");

             inTmps.Add(inTmp);

-            Indent(indent);

+            Indent(indent, wr);

             wr.Write("var {0} = ", inTmp);

-            TrExpr(s.Args[i]);

+            TrExpr(s.Args[i], wr, false);

             wr.WriteLine(";");

           }

         }

         // Now, assign to the formals

         int n = 0;

         if (!s.Method.IsStatic) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("_this = {0};", inTmps[n]);

           n++;

         }

         foreach (var p in s.Method.Ins) {

           if (!p.IsGhost) {

-            Indent(indent);

+            Indent(indent, wr);

             wr.WriteLine("{0} = {1};", p.CompileName, inTmps[n]);

             n++;

           }

         }

         Contract.Assert(n == inTmps.Count);

         // finally, the jump back to the head of the method

-        Indent(indent);

+        Indent(indent, wr);

         wr.WriteLine("goto TAIL_CALL_START;");

 

       } else {

@@ -2069,7 +2073,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < s.Method.Outs.Count; i++) {

           Formal p = s.Method.Outs[i];

           if (!p.IsGhost) {

-            lvalues.Add(CreateLvalue(s.Lhs[i], indent));

+            lvalues.Add(CreateLvalue(s.Lhs[i], indent, wr));

           }

         }

         var outTmps = new List<string>();

@@ -2078,8 +2082,8 @@ namespace Microsoft.Dafny {
           if (!p.IsGhost) {

             string target = idGenerator.FreshId("_out");

             outTmps.Add(target);

-            Indent(indent);

-            wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);

+            Indent(indent, wr);

+            wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type, wr), target);

           }

         }

         Contract.Assert(lvalues.Count == outTmps.Count);

@@ -2090,14 +2094,14 @@ namespace Microsoft.Dafny {
           }

         }

         if (receiverReplacement != null) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.Write("@" + receiverReplacement);

         } else if (s.Method.IsStatic) {

-          Indent(indent);

-          wr.Write(TypeName_Companion(s.Receiver.Type));

+          Indent(indent, wr);

+          wr.Write(TypeName_Companion(s.Receiver.Type, wr));

         } else {

-          Indent(indent);

-          TrParenExpr(s.Receiver);

+          Indent(indent, wr);

+          TrParenExpr(s.Receiver, wr, false);

         }

         wr.Write(".@{0}(", s.Method.CompileName);

 

@@ -2106,7 +2110,7 @@ namespace Microsoft.Dafny {
           Formal p = s.Method.Ins[i];

           if (!p.IsGhost) {

             wr.Write(sep);

-            TrExpr(s.Args[i]);

+            TrExpr(s.Args[i], wr, false);

             sep = ", ";

           }

         }

@@ -2119,44 +2123,45 @@ namespace Microsoft.Dafny {
 

         // assign to the actual LHSs

         for (int j = 0; j < lvalues.Count; j++) {

-          Indent(indent);

+          Indent(indent, wr);

           wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);

         }

       }

+      return wr;

     }

 

     /// <summary>

     /// Before calling TrAssignmentRhs(rhs), the caller must have spilled the let variables declared in "rhs".

     /// </summary>

-    void TrAssignmentRhs(AssignmentRhs rhs) {

+    void TrAssignmentRhs(AssignmentRhs rhs, TextWriter wr) {

       Contract.Requires(rhs != null);

       Contract.Requires(!(rhs is HavocRhs));

       if (rhs is ExprRhs) {

         ExprRhs e = (ExprRhs)rhs;

-        TrExpr(e.Expr);

+        TrExpr(e.Expr, wr, false);

 

       } else {

         TypeRhs tp = (TypeRhs)rhs;

         if (tp.ArrayDimensions == null) {

-          wr.Write("new {0}()", TypeName(tp.EType));

+          wr.Write("new {0}()", TypeName(tp.EType, wr));

         } else {

           if (tp.EType.IsIntegerType || tp.EType.IsTypeParameter) {

             // Because the default constructor for BigInteger does not generate a valid BigInteger, we have

             // to excplicitly initialize the elements of an integer array.  This is all done in a helper routine.

-            wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));

+            wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType, wr));

             string prefix = "(";

             foreach (Expression dim in tp.ArrayDimensions) {

               wr.Write(prefix);

-              TrParenExpr(dim);

+              TrParenExpr(dim, wr, false);

               prefix = ", ";

             }

             wr.Write(")");

           } else {

-            wr.Write("new {0}", TypeName(tp.EType));

+            wr.Write("new {0}", TypeName(tp.EType, wr));

             string prefix = "[";

             foreach (Expression dim in tp.ArrayDimensions) {

               wr.Write("{0}(int)", prefix);

-              TrParenExpr(dim);

+              TrParenExpr(dim, wr, false);

               prefix = ", ";

             }

             wr.Write("]");

@@ -2165,34 +2170,43 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));

+    void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent, TextWriter writer) {Contract.Requires(cce.NonNullElements(stmts));

       foreach (Statement ss in stmts) {

-        TrStmt(ss, indent + IndentAmount);

+        copyInstrWriter.Clear();

+        TextWriter wr = TrStmt(ss, indent + IndentAmount);

+        // write out any copy instructions that copies the out param

+        // used in letexpr to a local

+        string copyInstr = copyInstrWriter.ToString();

+        if (copyInstr != "") {

+          Indent(indent + IndentAmount, writer);

+          writer.Write(copyInstrWriter.ToString());

+        }

+        writer.Write(wr.ToString());

         if (ss.Labels != null) {

-          Indent(indent);  // labels are not indented as much as the statements

-          wr.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", idGenerator));

+          Indent(indent, writer);  // labels are not indented as much as the statements

+          writer.WriteLine("after_{0}: ;", ss.Labels.Data.AssignUniqueId("after_", idGenerator));

         }

       }

     }

 

-    void TrLocalVar(IVariable v, bool alwaysInitialize, int indent) {

+    void TrLocalVar(IVariable v, bool alwaysInitialize, int indent, TextWriter wr) {

       Contract.Requires(v != null);

       if (v.IsGhost) {

         // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)

         return;

       }

 

-      Indent(indent);

-      wr.Write("{0} @{1}", TypeName(v.Type), v.CompileName);

+      Indent(indent, wr);

+      wr.Write("{0} @{1}", TypeName(v.Type, wr), v.CompileName);

       if (alwaysInitialize) {

         // produce a default value

-        wr.WriteLine(" = {0};", DefaultValue(v.Type));

+        wr.WriteLine(" = {0};", DefaultValue(v.Type, wr));

       } else {

         wr.WriteLine(";");

       }

     }

 

-    void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent) {

+    void MatchCasePrelude(string source, UserDefinedType sourceType, DatatypeCtor ctor, List<BoundVar/*!*/>/*!*/ arguments, int caseIndex, int caseCount, int indent, TextWriter wr) {

       Contract.Requires(source != null);

       Contract.Requires(sourceType != null);

       Contract.Requires(ctor != null);

@@ -2201,7 +2215,7 @@ namespace Microsoft.Dafny {
       // if (source.is_Ctor0) {

       //   FormalType f0 = ((Dt_Ctor0)source._D).a0;

       //   ...

-      Indent(indent);

+      Indent(indent, wr);

       wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");

       if (caseIndex == caseCount - 1) {

         wr.Write("true");

@@ -2216,9 +2230,9 @@ namespace Microsoft.Dafny {
         if (!arg.IsGhost) {

           BoundVar bv = arguments[m];

           // FormalType f0 = ((Dt_Ctor0)source._D).a0;

-          Indent(indent + IndentAmount);

+          Indent(indent + IndentAmount, wr);

           wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};",

-            TypeName(bv.Type), bv.CompileName, DtCtorName(ctor, sourceType.TypeArgs), source, FormalName(arg, k));

+            TypeName(bv.Type, wr), bv.CompileName, DtCtorName(ctor, sourceType.TypeArgs, wr), source, FormalName(arg, k));

           k++;

         }

       }

@@ -2229,51 +2243,51 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Before calling TrParenExpr(expr), the caller must have spilled the let variables declared in "expr".

     /// </summary>

-    void TrParenExpr(string prefix, Expression expr) {

+    void TrParenExpr(string prefix, Expression expr, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(prefix != null);

       Contract.Requires(expr != null);

       wr.Write(prefix);

-      TrParenExpr(expr);

+      TrParenExpr(expr, wr, inLetExprBody);

     }

 

     /// <summary>

     /// Before calling TrParenExpr(expr), the caller must have spilled the let variables declared in "expr".

     /// </summary>

-    void TrParenExpr(Expression expr) {

+    void TrParenExpr(Expression expr, TextWriter wr, bool inLetExprBody) {

       Contract.Requires(expr != null);

       wr.Write("(");

-      TrExpr(expr);

+      TrExpr(expr, wr, inLetExprBody);

       wr.Write(")");

     }

 

     /// <summary>

     /// Before calling TrExprList(exprs), the caller must have spilled the let variables declared in expressions in "exprs".

     /// </summary>

-    void TrExprList(List<Expression/*!*/>/*!*/ exprs) {

+    void TrExprList(List<Expression/*!*/>/*!*/ exprs, TextWriter wr, bool inLetExprBody) {

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

       wr.Write("(");

       string sep = "";

       foreach (Expression e in exprs) {

         wr.Write(sep);

-        TrExpr(e);

+        TrExpr(e, wr, inLetExprBody);

         sep = ", ";

       }

       wr.Write(")");

     }

-    void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs) {

+    void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs, TextWriter wr, bool inLetExprBody) {

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

       wr.Write("(");

       string sep = "";

       foreach (ExpressionPair p in exprs) {

         wr.Write(sep);

         wr.Write("new Dafny.Pair<");

-        wr.Write(TypeName(p.A.Type));

+        wr.Write(TypeName(p.A.Type, wr));

         wr.Write(",");

-        wr.Write(TypeName(p.B.Type));

+        wr.Write(TypeName(p.B.Type, wr));

         wr.Write(">(");

-        TrExpr(p.A);

+        TrExpr(p.A, wr, inLetExprBody);

         wr.Write(",");

-        TrExpr(p.B);

+        TrExpr(p.B, wr, inLetExprBody);

         wr.Write(")");

         sep = ", ";

       }

@@ -2283,13 +2297,13 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Before calling TrExpr(expr), the caller must have spilled the let variables declared in "expr".

     /// </summary>

-    void TrExpr(Expression expr)

+    void TrExpr(Expression expr, TextWriter wr, bool inLetExprBody)

     {

       Contract.Requires(expr != null);

       if (expr is LiteralExpr) {

         LiteralExpr e = (LiteralExpr)expr;

         if (e.Value == null) {

-          wr.Write("({0})null", TypeName(e.Type));

+          wr.Write("({0})null", TypeName(e.Type, wr));

         } else if (e.Value is bool) {

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

         } else if (e is CharLiteralExpr) {

@@ -2330,41 +2344,49 @@ namespace Microsoft.Dafny {
 

       } else if (expr is IdentifierExpr) {

         var e = (IdentifierExpr)expr;

-        wr.Write("@" + e.Var.CompileName);

-

+        if (e.Var is Formal && inLetExprBody && !((Formal)e.Var).InParam) {

+          // out param in letExpr body, need to copy it to a temp since

+          // letExpr body is translated to an anonymous function that doesn't

+          // allow out parameters

+          var name = string.Format("_pat_let_tv{0}", GetUniqueAstNumber(e));

+          wr.Write("@" + name);

+          copyInstrWriter.Append("var @" + name + "= @" + e.Var.CompileName + ";\n");

+        } else {

+          wr.Write("@" + e.Var.CompileName);

+        }

       } else if (expr is SetDisplayExpr) {

         var e = (SetDisplayExpr)expr;

         var elType = e.Type.AsSetType.Arg;

-        wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));

-        TrExprList(e.Elements);

+        wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType, wr));

+        TrExprList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is MultiSetDisplayExpr) {

         var e = (MultiSetDisplayExpr)expr;

         var elType = e.Type.AsMultiSetType.Arg;

-        wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));

-        TrExprList(e.Elements);

+        wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType, wr));

+        TrExprList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is SeqDisplayExpr) {

         var e = (SeqDisplayExpr)expr;

         var elType = e.Type.AsSeqType.Arg;

-        wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));

-        TrExprList(e.Elements);

+        wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType, wr));

+        TrExprList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is MapDisplayExpr) {

         MapDisplayExpr e = (MapDisplayExpr)expr;

-        wr.Write("{0}.FromElements", TypeName(e.Type));

-        TrExprPairList(e.Elements);

+        wr.Write("{0}.FromElements", TypeName(e.Type, wr));

+        TrExprPairList(e.Elements, wr, inLetExprBody);

 

       } else if (expr is MemberSelectExpr) {

         MemberSelectExpr e = (MemberSelectExpr)expr;

         SpecialField sf = e.Member as SpecialField;

         if (sf != null) {

           wr.Write(sf.PreString);

-          TrParenExpr(e.Obj);

+          TrParenExpr(e.Obj, wr, inLetExprBody);

           wr.Write(".@{0}", sf.CompiledName);

           wr.Write(sf.PostString);

         } else {

-          TrParenExpr(e.Obj);

+          TrParenExpr(e.Obj, wr, inLetExprBody);

           wr.Write(".@{0}", e.Member.CompileName);

         }

 

@@ -2374,50 +2396,50 @@ namespace Microsoft.Dafny {
         if (e.Seq.Type.IsArrayType) {

           if (e.SelectOne) {

             Contract.Assert(e.E0 != null && e.E1 == null);

-            TrParenExpr(e.Seq);

+            TrParenExpr(e.Seq, wr, inLetExprBody);

             wr.Write("[(int)");

-            TrParenExpr(e.E0);

+            TrParenExpr(e.E0, wr, inLetExprBody);

             wr.Write("]");

           } else {

-            TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq);

+            TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq, wr, inLetExprBody);

             if (e.E1 != null) {

-              TrParenExpr(".Take", e.E1);

+              TrParenExpr(".Take", e.E1, wr, inLetExprBody);

             }

             if (e.E0 != null) {

-              TrParenExpr(".Drop", e.E0);

+              TrParenExpr(".Drop", e.E0, wr, inLetExprBody);

             }

           }

         } else if (e.SelectOne) {

           Contract.Assert(e.E0 != null && e.E1 == null);

-          TrParenExpr(e.Seq);

-          TrParenExpr(".Select", e.E0);

+          TrParenExpr(e.Seq, wr, inLetExprBody);

+          TrParenExpr(".Select", e.E0, wr, inLetExprBody);

         } else {

-          TrParenExpr(e.Seq);

+          TrParenExpr(e.Seq, wr, inLetExprBody);

           if (e.E1 != null) {

-            TrParenExpr(".Take", e.E1);

+            TrParenExpr(".Take", e.E1, wr, inLetExprBody);

           }

           if (e.E0 != null) {

-            TrParenExpr(".Drop", e.E0);

+            TrParenExpr(".Drop", e.E0, wr, inLetExprBody);

           }

         }

       } else if (expr is MultiSetFormingExpr) {

         var e = (MultiSetFormingExpr)expr;

-        wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg));

+        wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg, wr));

         var eeType = e.E.Type.NormalizeExpand();

         if (eeType is SeqType) {

-          TrParenExpr(".FromSeq", e.E);

+          TrParenExpr(".FromSeq", e.E, wr, inLetExprBody);

         } else if (eeType is SetType) {

-          TrParenExpr(".FromSet", e.E);

+          TrParenExpr(".FromSet", e.E, wr, inLetExprBody);

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();

         }

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

-        TrParenExpr(e.Array);

+        TrParenExpr(e.Array, wr, inLetExprBody);

         string prefix = "[";

         foreach (Expression idx in e.Indices) {

           wr.Write("{0}(int)", prefix);

-          TrParenExpr(idx);

+          TrParenExpr(idx, wr, inLetExprBody);

           prefix = ", ";

         }

         wr.Write("]");

@@ -2426,47 +2448,47 @@ namespace Microsoft.Dafny {
         SeqUpdateExpr e = (SeqUpdateExpr)expr;

         if (e.ResolvedUpdateExpr != null)

         {

-          TrExpr(e.ResolvedUpdateExpr);

+          TrExpr(e.ResolvedUpdateExpr, wr, inLetExprBody);

         }

         else

         {

-          TrParenExpr(e.Seq);

+          TrParenExpr(e.Seq, wr, inLetExprBody);

           wr.Write(".Update(");

-          TrExpr(e.Index);

+          TrExpr(e.Index, wr, inLetExprBody);

           wr.Write(", ");

-          TrExpr(e.Value);

+          TrExpr(e.Value, wr, inLetExprBody);

           wr.Write(")");

         }

 

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        CompileFunctionCallExpr(e, wr, TrExpr);

+        CompileFunctionCallExpr(e, wr, wr, inLetExprBody, TrExpr);

 

       } else if (expr is ApplyExpr) {

         var e = expr as ApplyExpr;

         wr.Write("Dafny.Helpers.Id<");

-        wr.Write(TypeName(e.Function.Type));

+        wr.Write(TypeName(e.Function.Type, wr));

         wr.Write(">(");

-        TrExpr(e.Function);

+        TrExpr(e.Function, wr, inLetExprBody);

         wr.Write(")");

-        TrExprList(e.Args);

+        TrExprList(e.Args, wr, inLetExprBody);

 

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

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

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

 

         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 )

-          wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs));

+          wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr));

           string sep = "";

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

             Formal formal = dtv.Ctor.Formals[i];

             if (!formal.IsGhost) {

               wr.Write(sep);

-              TrExpr(dtv.Arguments[i]);

+              TrExpr(dtv.Arguments[i], wr, inLetExprBody);

               sep = ", ";

             }

           }

@@ -2495,17 +2517,17 @@ namespace Microsoft.Dafny {
                 arg = varName;

 

                 wr.Write("var {0} = ", varName);

-                TrExpr(actual);

+                TrExpr(actual, wr, inLetExprBody);

                 wr.Write("; ");

               } else {

                 var sw = new StringWriter();

-                CompileFunctionCallExpr(fce, sw, (exp) => {

+                CompileFunctionCallExpr(fce, sw, wr, inLetExprBody, (exp, wrr, inLetExpr) => {

                   string varName = idGenerator.FreshId("_ac");

                   sw.Write(varName);

 

-                  wr.Write("var {0} = ", varName);

-                  TrExpr(exp);

-                  wr.Write("; ");

+                  wrr.Write("var {0} = ", varName);

+                  TrExpr(exp, wrr, inLetExpr);

+                  wrr.Write("; ");

 

                 });

                 arg = sw.ToString();

@@ -2517,7 +2539,7 @@ namespace Microsoft.Dafny {
 

           wr.Write("return () => { return ");

 

-          wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs), args);

+          wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs, wr), args);

           wr.Write("); }; })())");

         }

         wr.Write(")");

@@ -2530,11 +2552,11 @@ namespace Microsoft.Dafny {
         switch (e.Op) {

           case UnaryOpExpr.Opcode.Not:

             wr.Write("!");

-            TrParenExpr(e.E);

+            TrParenExpr(e.E, wr, inLetExprBody);

             break;

           case UnaryOpExpr.Opcode.Cardinality:

             wr.Write("new BigInteger(");

-            TrParenExpr(e.E);

+            TrParenExpr(e.E, wr, inLetExprBody);

             wr.Write(".Length)");

             break;

           default:

@@ -2552,7 +2574,7 @@ namespace Microsoft.Dafny {
           if (AsNativeType(e.E.Type) != null) {

             wr.Write("new BigInteger");

           }

-          TrParenExpr(e.E);

+          TrParenExpr(e.E, wr, inLetExprBody);

         };

         Action toIntCast = () => {

           Contract.Assert(toInt);

@@ -2568,7 +2590,7 @@ namespace Microsoft.Dafny {
         } else if (!fromInt && toInt) {

           // real -> int

           toIntCast();

-          TrParenExpr(e.E);

+          TrParenExpr(e.E, wr, inLetExprBody);

           wr.Write(".ToBigInteger()");

         } else if (AsNativeType(e.ToType) != null) {

           toIntCast();

@@ -2580,14 +2602,14 @@ namespace Microsoft.Dafny {
             wr.Write("(" + (BigInteger)lit.Value + AsNativeType(e.ToType).Suffix + ")");

           } else if ((u != null && u.Op == UnaryOpExpr.Opcode.Cardinality) || (m != null && m.MemberName == "Length" && m.Obj.Type.IsArrayType)) {

             // Optimize .Length to avoid intermediate BigInteger

-            TrParenExpr((u != null) ? u.E : m.Obj);

+            TrParenExpr((u != null) ? u.E : m.Obj, wr, inLetExprBody);

             if (AsNativeType(e.ToType).UpperBound <= new BigInteger(0x80000000U)) {

               wr.Write(".Length");

             } else {

               wr.Write(".LongLength");

             }

           } else {

-            TrParenExpr(e.E);

+            TrParenExpr(e.E, wr, inLetExprBody);

           }

         } else if (e.ToType.IsIntegerType && AsNativeType(e.E.Type) != null) {

           fromIntAsBigInteger();

@@ -2595,7 +2617,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(fromInt == toInt);

           Contract.Assert(AsNativeType(e.ToType) == null);

           Contract.Assert(AsNativeType(e.E.Type) == null);

-          TrParenExpr(e.E);

+          TrParenExpr(e.E, wr, inLetExprBody);

         }

 

       } else if (expr is BinaryExpr) {

@@ -2664,9 +2686,9 @@ namespace Microsoft.Dafny {
             if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {

               string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";

               wr.Write("Dafny.Helpers.EuclideanDivision" + suffix + "(");

-              TrParenExpr(e.E0);

+              TrParenExpr(e.E0, wr, inLetExprBody);

               wr.Write(", ");

-              TrExpr(e.E1);

+              TrExpr(e.E1, wr, inLetExprBody);

               wr.Write(")");

             } else {

               opString = "/";  // for reals

@@ -2676,9 +2698,9 @@ namespace Microsoft.Dafny {
             if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {

               string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";

               wr.Write("Dafny.Helpers.EuclideanModulus" + suffix + "(");

-              TrParenExpr(e.E0);

+              TrParenExpr(e.E0, wr, inLetExprBody);

               wr.Write(", ");

-              TrExpr(e.E1);

+              TrExpr(e.E1, wr, inLetExprBody);

               wr.Write(")");

             } else {

               opString = "%";  // for reals

@@ -2713,18 +2735,18 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.InSet:

           case BinaryExpr.ResolvedOpcode.InMultiSet:

           case BinaryExpr.ResolvedOpcode.InMap:

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.NotInSet:

           case BinaryExpr.ResolvedOpcode.NotInMultiSet:

           case BinaryExpr.ResolvedOpcode.NotInMap:

             wr.Write("!");

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.Union:

@@ -2744,16 +2766,16 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Concat:

             callString = "Concat";  break;

           case BinaryExpr.ResolvedOpcode.InSeq:

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.NotInSeq:

             wr.Write("!");

-            TrParenExpr(e.E1);

+            TrParenExpr(e.E1, wr, inLetExprBody);

             wr.Write(".Contains(");

-            TrExpr(e.E0);

+            TrExpr(e.E0, wr, inLetExprBody);

             wr.Write(")");

             break;

 

@@ -2767,17 +2789,17 @@ namespace Microsoft.Dafny {
             wr.Write("(" + nativeType.Name + ")(");

           }

           wr.Write(preOpString);

-          TrParenExpr(e.E0);

+          TrParenExpr(e.E0, wr, inLetExprBody);

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

-          TrParenExpr(e.E1);

+          TrParenExpr(e.E1, wr, inLetExprBody);

           if (needsCast) {

             wr.Write(")");

           }

         } else if (callString != null) {

           wr.Write(preOpString);

-          TrParenExpr(e.E0);

+          TrParenExpr(e.E0, wr, inLetExprBody);

           wr.Write(".@{0}(", callString);

-          TrExpr(e.E1);

+          TrExpr(e.E1, wr, inLetExprBody);

           wr.Write(")");

         }

 

@@ -2800,17 +2822,18 @@ namespace Microsoft.Dafny {
             if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {

               var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);

               wr.Write("Dafny.Helpers.Let<");

-              wr.Write(TypeName(e.RHSs[i].Type) + "," + TypeName(e.Body.Type));

+              wr.Write(TypeName(e.RHSs[i].Type, wr) + "," + TypeName(e.Body.Type, wr));

               wr.Write(">(");

-              TrExpr(e.RHSs[i]);

+              TrExpr(e.RHSs[i], wr, inLetExprBody);

               wr.Write(", " + rhsName + " => ");

               neededCloseParens++;

-              var c = TrCasePattern(lhs, rhsName, e.Body.Type);

+              var c = TrCasePattern(lhs, rhsName, e.Body.Type, wr);

               Contract.Assert(c != 0);  // we already checked that there's at least one non-ghost

               neededCloseParens += c;

             }

           }

-          TrExpr(e.Body);

+          

+          TrExpr(e.Body, wr, true);

           for (int i = 0; i < neededCloseParens; i++) {

             wr.Write(")");

           }

@@ -2819,7 +2842,7 @@ namespace Microsoft.Dafny {
           //    ghost var x,y :| Constraint; E

           // is compiled just like E is, because the resolver has already checked that x,y (or other ghost variables, for that matter) don't

           // occur in E (moreover, the verifier has checked that values for x,y satisfying Constraint exist).

-          TrExpr(e.Body);

+          TrExpr(e.Body, wr, inLetExprBody);

         } else {

           // The Dafny "let" expression

           //    var x,y :| Constraint; E

@@ -2834,17 +2857,17 @@ namespace Microsoft.Dafny {
           Contract.Assert(e.RHSs.Count == 1);  // checked by resolution

           if (e.Constraint_MissingBounds != null) {

             foreach (var bv in e.Constraint_MissingBounds) {

-              Error("this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", bv.Name, e.tok.line);

+              Error("this let-such-that expression is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable '{0}' (line {1})", wr, bv.Name, e.tok.line);

             }

           } else {

-            wr.Write("Dafny.Helpers.Let<int," + TypeName(e.Body.Type) + ">(0, _let_dummy_" + GetUniqueAstNumber(e) + " => {");

+            wr.Write("Dafny.Helpers.Let<int," + TypeName(e.Body.Type, wr) + ">(0, _let_dummy_" + GetUniqueAstNumber(e) + " => {");

             foreach (var bv in e.BoundVars) {

-              wr.Write("{0} @{1}", TypeName(bv.Type), bv.CompileName);

-              wr.WriteLine(" = {0};", DefaultValue(bv.Type));

+              wr.Write("{0} @{1}", TypeName(bv.Type, wr), bv.CompileName);

+              wr.WriteLine(" = {0};", DefaultValue(bv.Type, wr));

             }

-            TrAssignSuchThat(0, new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line);

+            TrAssignSuchThat(0, new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0], e.Constraint_Bounds, e.tok.line, wr, inLetExprBody);

             wr.Write(" return ");

-            TrExpr(e.Body);

+            TrExpr(e.Body, wr, true);

             wr.Write("; })");

           }

         }

@@ -2864,7 +2887,7 @@ namespace Microsoft.Dafny {
         // }(src)

 

         string source = idGenerator.FreshId("_source");

-        wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type), TypeName(e.Type), source);

+        wr.Write("new Dafny.Helpers.Function<{0}, {1}>(delegate ({0} {2}) {{ ", TypeName(e.Source.Type, wr), TypeName(e.Type, wr), source);

 

         if (e.Cases.Count == 0) {

           // the verifier would have proved we never get here; still, we need some code that will compile

@@ -2873,9 +2896,9 @@ namespace Microsoft.Dafny {
           int i = 0;

           var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();

           foreach (MatchCaseExpr mc in e.Cases) {

-            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0);

+            MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0, wr);

             wr.Write("return ");

-            TrExpr(mc.Body);

+            TrExpr(mc.Body, wr, inLetExprBody);

             wr.Write("; ");

             i++;

           }

@@ -2883,7 +2906,7 @@ namespace Microsoft.Dafny {
         }

         // We end with applying the source expression to the delegate we just built

         wr.Write("})(");

-        TrExpr(e.Source);

+        TrExpr(e.Source, wr, inLetExprBody);

         wr.Write(")");

 

       } else if (expr is QuantifierExpr) {

@@ -2905,24 +2928,24 @@ namespace Microsoft.Dafny {
           } else if (bound is ComprehensionExpr.IntBoundedPool) {

             var b = (ComprehensionExpr.IntBoundedPool)bound;

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

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, inLetExprBody);

             wr.Write(", ");

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

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

-            TrExpr(b.Set);

+            TrExpr(b.Set, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.MapBoundedPool) {

             var b = (ComprehensionExpr.MapBoundedPool)bound;

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

-            TrExpr(b.Map);

+            TrExpr(b.Map, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.SeqBoundedPool) {

             var b = (ComprehensionExpr.SeqBoundedPool)bound;

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

-            TrExpr(b.Seq);

+            TrExpr(b.Seq, wr, inLetExprBody);

             wr.Write(", ");

           } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

@@ -2935,7 +2958,7 @@ namespace Microsoft.Dafny {
           wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");

           wr.Write("@{0} => ", bv.CompileName);

         }

-        TrExpr(e.LogicalBody(true));

+        TrExpr(e.LogicalBody(true), wr, inLetExprBody);

         for (int i = 0; i < n; i++) {

           wr.Write(")");

         }

@@ -2959,7 +2982,7 @@ namespace Microsoft.Dafny {
         //   return Dafny.Set<G>.FromCollection(_coll);

         // })()

         Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds

-        var typeName = TypeName(e.Type.AsSetType.Arg);

+        var typeName = TypeName(e.Type.AsSetType.Arg, wr);

         wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);

         wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);

         var n = e.BoundVars.Count;

@@ -2978,36 +3001,36 @@ namespace Microsoft.Dafny {
             } else {

               wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);

             }

-            TrExpr(b.LowerBound);

+            TrExpr(b.LowerBound, wr, inLetExprBody);

             wr.Write(", ");

-            TrExpr(b.UpperBound);

+            TrExpr(b.UpperBound, wr, inLetExprBody);

             wr.Write(")) { ");

           } else if (bound is ComprehensionExpr.SetBoundedPool) {

             var b = (ComprehensionExpr.SetBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Set);

+            TrExpr(b.Set, wr, inLetExprBody);

             wr.Write(").Elements) { ");

           } else if (bound is ComprehensionExpr.MapBoundedPool) {

             var b = (ComprehensionExpr.MapBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Map);

+            TrExpr(b.Map, wr, inLetExprBody);

             wr.Write(").Domain) { ");

           } else if (bound is ComprehensionExpr.SeqBoundedPool) {

             var b = (ComprehensionExpr.SeqBoundedPool)bound;

             wr.Write("foreach (var @{0} in (", bv.CompileName);

-            TrExpr(b.Seq);

+            TrExpr(b.Seq, wr, inLetExprBody);

             wr.Write(").Elements) { ");

           } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

             var b = (ComprehensionExpr.DatatypeBoundedPool)bound;

-            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type));

+            wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type, wr));

           } else {

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

           }

         }

         wr.Write("if (");

-        TrExpr(e.Range);

+        TrExpr(e.Range, wr, inLetExprBody);

         wr.Write(") { _coll.Add(");

-        TrExpr(e.Term);

+        TrExpr(e.Term, wr, inLetExprBody);

         wr.Write("); }");

         for (int i = 0; i < n; i++) {

           wr.Write("}");

@@ -3034,8 +3057,8 @@ namespace Microsoft.Dafny {
         //   return Dafny.Map<U, V>.FromElements(_coll);

         // })()

         Contract.Assert(e.Bounds != null);  // the resolver would have insisted on finding bounds

-        var domtypeName = TypeName(e.Type.AsMapType.Domain);

-        var rantypeName = TypeName(e.Type.AsMapType.Range);

+        var domtypeName = TypeName(e.Type.AsMapType.Domain, wr);

+        var rantypeName = TypeName(e.Type.AsMapType.Range, wr);

         wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);

         wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);

         var n = e.BoundVars.Count;

@@ -3053,34 +3076,34 @@ namespace Microsoft.Dafny {
           } else {

             wr.Write("foreach (var @{0} in Dafny.Helpers.IntegerRange(", bv.CompileName);

           }

-          TrExpr(b.LowerBound);

+          TrExpr(b.LowerBound, wr, inLetExprBody);

           wr.Write(", ");

-          TrExpr(b.UpperBound);

+          TrExpr(b.UpperBound, wr, inLetExprBody);

           wr.Write(")) { ");

         } else if (bound is ComprehensionExpr.SetBoundedPool) {

           var b = (ComprehensionExpr.SetBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

-          TrExpr(b.Set);

+          TrExpr(b.Set, wr, inLetExprBody);

           wr.Write(").Elements) { ");

         } else if (bound is ComprehensionExpr.MapBoundedPool) {

           var b = (ComprehensionExpr.MapBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

-          TrExpr(b.Map);

+          TrExpr(b.Map, wr, inLetExprBody);

           wr.Write(").Domain) { ");

         } else if (bound is ComprehensionExpr.SeqBoundedPool) {

           var b = (ComprehensionExpr.SeqBoundedPool)bound;

           wr.Write("foreach (var @{0} in (", bv.CompileName);

-          TrExpr(b.Seq);

+          TrExpr(b.Seq, wr, inLetExprBody);

           wr.Write(").Elements) { ");

         } else {

           // TODO: handle ComprehensionExpr.SubSetBoundedPool

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

         }

         wr.Write("if (");

-        TrExpr(e.Range);

+        TrExpr(e.Range, wr, inLetExprBody);

         wr.Write(") { ");

         wr.Write("_coll.Add(new Dafny.Pair<{0},{1}>(@{2},", domtypeName, rantypeName, bv.CompileName);

-        TrExpr(e.Term);

+        TrExpr(e.Term, wr, inLetExprBody);

         wr.Write(")); }");

         wr.Write("}");

         wr.Write("return Dafny.Map<{0},{1}>.FromCollection(_coll); ", domtypeName, rantypeName);

@@ -3109,46 +3132,46 @@ namespace Microsoft.Dafny {
 

         var su = new Translator.Substituter(null, sm, new Dictionary<TypeParameter, Type>(), null);

 

-        BetaRedex(bvars, fexprs, expr.Type, () => {

+        BetaRedex(bvars, fexprs, expr.Type, wr, inLetExprBody, () => {

           wr.Write("(");

           wr.Write(Util.Comma(e.BoundVars, bv => "@" + bv.CompileName));

           wr.Write(") => ");

-          TrExpr(su.Substitute(e.Body));

+          TrExpr(su.Substitute(e.Body), wr, inLetExprBody);

         });

 

       } else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

-        TrExpr(e.E);

+        TrExpr(e.E, wr, inLetExprBody);

 

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         wr.Write("(");

-        TrExpr(e.Test);

+        TrExpr(e.Test, wr, inLetExprBody);

         wr.Write(") ? (");

-        TrExpr(e.Thn);

+        TrExpr(e.Thn, wr, inLetExprBody);

         wr.Write(") : (");

-        TrExpr(e.Els);

+        TrExpr(e.Els, wr, inLetExprBody);

         wr.Write(")");

 

       } else if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

-        TrExpr(e.ResolvedExpression);

+        TrExpr(e.ResolvedExpression, wr, inLetExprBody);

 

       } else if (expr is NamedExpr) {

-        TrExpr(((NamedExpr)expr).Body);

+        TrExpr(((NamedExpr)expr).Body, wr, inLetExprBody);

       } else {

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

       }

     }

 

-    int TrCasePattern(CasePattern pat, string rhsString, Type bodyType) {

+    int TrCasePattern(CasePattern pat, string rhsString, Type bodyType, TextWriter wr) {

       Contract.Requires(pat != null);

       Contract.Requires(rhsString != null);

       int c = 0;

       if (pat.Var != null) {

         var bv = pat.Var;

         if (!bv.IsGhost) {

-          wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type) + "," + TypeName(bodyType) + ">");

+          wr.Write("Dafny.Helpers.Let<" + TypeName(bv.Type, wr) + "," + TypeName(bodyType, wr) + ">");

           wr.Write("(" + rhsString + ", @" + bv.CompileName + " => ");

           c++;

         }

@@ -3164,7 +3187,7 @@ namespace Microsoft.Dafny {
             // nothing to compile, but do a sanity check

             Contract.Assert(!Contract.Exists(arg.Vars, bv => !bv.IsGhost));

           } else {

-            c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs), rhsString, FormalName(formal, k)), bodyType);

+            c += TrCasePattern(arg, string.Format("(({0})({1})._D).@{2}", DtCtorName(ctor, ((DatatypeValue)pat.Expr).InferredTypeArgs, wr), rhsString, FormalName(formal, k)), bodyType, wr);

             k++;

           }

         }

@@ -3172,40 +3195,40 @@ namespace Microsoft.Dafny {
       return c;

     }

 

-    delegate void FCE_Arg_Translator(Expression e);

+    delegate void FCE_Arg_Translator(Expression e, TextWriter wr, bool inLetExpr=false);

 

-    void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) {

+   void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, TextWriter wr, bool inLetExprBody, FCE_Arg_Translator tr) {

       Function f = cce.NonNull(e.Function);

       if (f.IsStatic) {

-        twr.Write(TypeName_Companion(e.Receiver.Type));

+        twr.Write(TypeName_Companion(e.Receiver.Type, wr));

       } else {

         twr.Write("(");

-        tr(e.Receiver);

+        tr(e.Receiver, wr, inLetExprBody);

         twr.Write(")");

       }

       twr.Write(".@{0}", f.CompileName);

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

           List<Type> typeArgs = f.TypeArgs.ConvertAll(ta => e.TypeArgumentSubstitutions[ta]);

-          twr.Write("<" + TypeNames(typeArgs) + ">");

+          twr.Write("<" + TypeNames(typeArgs, wr) + ">");

       }

       twr.Write("(");

       string sep = "";

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

         if (!e.Function.Formals[i].IsGhost) {

           twr.Write(sep);

-          tr(e.Args[i]);

+          tr(e.Args[i], wr);

           sep = ", ";

         }

       }

       twr.Write(")");

     }

 

-    void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, Action makeBody) {

+    void BetaRedex(List<BoundVar> bvars, List<Expression> exprs, Type bodyType, TextWriter wr, bool inLetExprBody, Action makeBody) {

       Contract.Requires(bvars != null);

       Contract.Requires(exprs != null);

       Contract.Requires(bvars.Count == exprs.Count);

       wr.Write("Dafny.Helpers.Id<");

-      wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType)));

+      wr.Write(TypeName_UDT(ArrowType.Arrow_FullCompileName, Util.Snoc(bvars.ConvertAll(bv => bv.Type), bodyType), wr));

       wr.Write(">((");

       wr.Write(Util.Comma(bvars, bv => "@" + bv.CompileName));

       wr.Write(") => ");

@@ -3213,7 +3236,7 @@ namespace Microsoft.Dafny {
       makeBody();

 

       wr.Write(")");

-      TrExprList(exprs);

+      TrExprList(exprs, wr, inLetExprBody);

     }

 

   }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 8282edc7..6cfbe7e1 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -300,14 +300,14 @@ namespace Microsoft.Dafny
 

       // Compile the Dafny program into a string that contains the C# program

       StringWriter sw = new StringWriter();

-      Dafny.Compiler compiler = new Dafny.Compiler(sw);

+      Dafny.Compiler compiler = new Dafny.Compiler();

       compiler.ErrorWriter = outputWriter;

       var hasMain = compiler.HasMain(dafnyProgram);

       if (DafnyOptions.O.RunAfterCompile && !hasMain) {

         // do no more

         return;

       }

-      compiler.Compile(dafnyProgram);

+      compiler.Compile(dafnyProgram, sw);

       var csharpProgram = sw.ToString();

       bool completeProgram = compiler.ErrorCount == 0;