Merge

9 files changed, 501 insertions, 624 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 6fa9440a..6a448172 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -19,13 +19,13 @@ namespace Microsoft.Dafny {
     }

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(wr!=null);

     }

 

     TextWriter wr;

-    

+

     public int ErrorCount;

     void Error(string msg, params object[] args) {Contract.Requires(msg != null);

       string s = string.Format("Compilation error: " + msg, args);

@@ -33,7 +33,7 @@ namespace Microsoft.Dafny {
       wr.WriteLine("/* {0} */", s);

       ErrorCount++;

     }

-    

+

     void ReadRuntimeSystem() {

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

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

@@ -226,7 +226,7 @@ namespace Microsoft.Dafny {
         Indent(indent);  wr.WriteLine("}");

       }

     }

-    

+

     void CompileDatatypeStruct(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

 

@@ -254,23 +254,23 @@ namespace Microsoft.Dafny {
       if (dt.TypeArgs.Count != 0) {

         DtT += "<" + TypeParameters(dt.TypeArgs) + ">";

       }

-      

+

       Indent(indent);

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

       int ind = indent + IndentAmount;

-      

+

       Indent(ind);

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

-      

+

       Indent(ind);

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

       Indent(ind + IndentAmount);

       wr.WriteLine("get { if (d == null) { d = Default; } return d; }");

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

-      

+

       Indent(ind);

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

-      

+

       Indent(ind);

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

       Indent(ind + IndentAmount);

@@ -320,7 +320,7 @@ namespace Microsoft.Dafny {
       Indent(indent);

       wr.WriteLine("}");

     }

-    

+

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

     {

       Contract.Requires(sep != null);

@@ -336,20 +336,20 @@ namespace Microsoft.Dafny {
       }

       return i;  // the number of formals written

     }

-    

+

     string FormalName(Formal formal, int i) {

       Contract.Requires(formal != null);

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

 

       return formal.HasName ? formal.Name : "_a" + i;

     }

-    

+

     string DtCtorName(DatatypeCtor ctor) {

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

 

       return cce.NonNull(ctor.EnclosingDatatype).Name + "_" + ctor.Name;

     }

-        

+

     void CompileClassMembers(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

@@ -360,7 +360,7 @@ namespace Microsoft.Dafny {
             Indent(indent);

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

           }

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           if (f.IsGhost) {

@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
             CompileReturnBody(f.Body, indent);

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

           }

-          

+

         } else if (member is Method) {

           Method m = (Method)member;

           if (!m.IsGhost) {

@@ -487,7 +487,7 @@ namespace Microsoft.Dafny {
     readonly string DafnySetClass = "Dafny.Set";

     readonly string DafnyMultiSetClass = "Dafny.MultiSet";

     readonly string DafnySeqClass = "Dafny.Sequence";

-    

+

     string TypeName(Type type)

     {

       Contract.Requires(type != null);

@@ -504,7 +504,7 @@ namespace Microsoft.Dafny {
           type = tp.T;

         }

       }

-      

+

       if (type is BoolType) {

         return "bool";

       } else if (type is IntType) {

@@ -565,7 +565,7 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

-    

+

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

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

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

@@ -578,7 +578,7 @@ namespace Microsoft.Dafny {
       }

       return s;

     }

-    

+

     string DefaultValue(Type type)

     {

       Contract.Requires(type != null);

@@ -595,7 +595,7 @@ namespace Microsoft.Dafny {
           type = tp.T;

         }

       }

-      

+

       if (type is BoolType) {

         return "false";

       } else if (type is IntType) {

@@ -622,16 +622,16 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

     }

-    

+

     // ----- Stmt ---------------------------------------------------------------------------------

-    

+

     void TrStmt(Statement stmt, int indent)

     {

       Contract.Requires(stmt != null);

       if (stmt.IsGhost) {

         return;

       }

-      

+

       if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         foreach (Attributes.Argument arg in s.Args) {

@@ -732,19 +732,19 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (stmt is VarDecl) {

         TrVarDecl((VarDecl)stmt, true, indent);

-        

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         TrCallStmt(s, null, indent);

-        

+

       } else if (stmt is BlockStmt) {

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

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

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

-        

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         Indent(indent);

@@ -755,7 +755,7 @@ namespace Microsoft.Dafny {
           TrExpr(s.Guard);

           wr.WriteLine(")");

         }

-        

+

         TrStmt(s.Thn, indent);

         if (s.Els != null && s.Guard != null) {

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

@@ -825,20 +825,20 @@ namespace Microsoft.Dafny {
         tmpVarCount++;

         string TType = TypeName(s.BoundVar.Type);

         string RhsType = TypeName(cce.NonNull(s.BodyAssign.Lhs.Type));

-        

+

         Indent(indent);

         wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);

-        

+

         Indent(indent);

         wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);

         TrExpr(s.Collection);

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

-        

+

         Indent(indent + IndentAmount);

         wr.Write("if (");

         TrExpr(s.Range);

         wr.WriteLine(") {");

-        

+

         foreach (PredicateStmt p in s.BodyPrefix) {

           TrStmt(p, indent + 2*IndentAmount);

         }

@@ -851,7 +851,7 @@ namespace Microsoft.Dafny {
           wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));

         }

         wr.WriteLine("))");

-        

+

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

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

 

@@ -860,7 +860,7 @@ namespace Microsoft.Dafny {
         FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;

         wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);

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

-        

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         // Type source = e;

@@ -1044,16 +1044,16 @@ namespace Microsoft.Dafny {
       }

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

     }

-    

+

     int tmpVarCount = 0;

-    

+

     void TrAssignmentRhs(AssignmentRhs rhs) {

       Contract.Requires(rhs != null);

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

       if (rhs is ExprRhs) {

         ExprRhs e = (ExprRhs)rhs;

         TrExpr(e.Expr);

-        

+

       } else {

         TypeRhs tp = (TypeRhs)rhs;

         if (tp.ArrayDimensions == null) {

@@ -1083,7 +1083,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

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

       foreach (Statement ss in stmts) {

         TrStmt(ss, indent + IndentAmount);

@@ -1140,7 +1140,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     // ----- Expression ---------------------------------------------------------------------------

 

     void TrParenExpr(string prefix, Expression expr) {

@@ -1156,7 +1156,7 @@ namespace Microsoft.Dafny {
       TrExpr(expr);

       wr.Write(")");

     }

-    

+

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

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

       wr.Write("(");

@@ -1188,10 +1188,10 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (expr is ThisExpr) {

         wr.Write("this");

-        

+

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         wr.Write("@" + e.Var.Name);

@@ -1213,7 +1213,7 @@ namespace Microsoft.Dafny {
         Type elType = cce.NonNull((SeqType)e.Type).Arg;

         wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));

         TrExprList(e.Elements);

-      

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         SpecialField sf = e.Field as SpecialField;

@@ -1226,7 +1226,7 @@ namespace Microsoft.Dafny {
           TrParenExpr(e.Obj);

           wr.Write(".@{0}", e.Field.Name);

         }

-        

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         Contract.Assert(e.Seq.Type != null);

@@ -1288,7 +1288,7 @@ namespace Microsoft.Dafny {
         wr.Write(", ");

         TrExpr(e.Value);

         wr.Write(")");

-      

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         Function f = cce.NonNull(e.Function);

@@ -1308,7 +1308,7 @@ namespace Microsoft.Dafny {
           }

         }

         wr.Write(")");

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

@@ -1327,13 +1327,13 @@ namespace Microsoft.Dafny {
           }

         }

         wr.Write("))");

-          

+

       } else if (expr is OldExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // 'old' is always a ghost (right?)

-      

+

       } else if (expr is FreshExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // 'fresh' is always a ghost

-      

+

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         switch (e.Op) {

@@ -1358,13 +1358,13 @@ namespace Microsoft.Dafny {
           default:

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

         }

-      

+

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         string opString = null;

         string preOpString = "";

         string callString = null;

-        

+

         switch (e.ResolvedOp) {

           case BinaryExpr.ResolvedOpcode.Iff:

             opString = "==";  break;

@@ -1374,7 +1374,7 @@ namespace Microsoft.Dafny {
             opString = "||";  break;

           case BinaryExpr.ResolvedOpcode.And:

             opString = "&&";  break;

-            

+

           case BinaryExpr.ResolvedOpcode.EqCommon: {

             Type t = cce.NonNull(e.E0.Type);

             if (t.IsDatatype || t.IsTypeParameter) {

@@ -1394,7 +1394,7 @@ namespace Microsoft.Dafny {
             }

             break;

           }

-            

+

           case BinaryExpr.ResolvedOpcode.Lt:

             opString = "<";  break;

           case BinaryExpr.ResolvedOpcode.Le:

@@ -1506,7 +1506,7 @@ namespace Microsoft.Dafny {
           TrExpr(e.E1);

           wr.Write(")");

         }

-      

+

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

         Contract.Assert(e.Bounds != null);  // for non-ghost quantifiers, the resolver would have insisted on finding bounds

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 665cf33f..028d6826 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -3,39 +3,29 @@
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.

 //

 //-----------------------------------------------------------------------------*/

-

 /*---------------------------------------------------------------------------

 // Dafny

 // Rustan Leino, first created 25 January 2008

 //--------------------------------------------------------------------------*/

-

 using System.Collections.Generic;

 using System.Numerics;

 using Microsoft.Boogie;

 using System.IO;

 using System.Text;

-

-

 COMPILER Dafny

-

 /*--------------------------------------------------------------------------*/

-

 static List<ModuleDecl/*!*/> theModules;

 static BuiltIns theBuiltIns;

-

-

 static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);

 static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);

 static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);

 static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");

 static int anonymousIds = 0;

-

 struct MemberModifiers {

   public bool IsGhost;

   public bool IsStatic;

   public bool IsUnlimited;

 }

-

 // helper routine for parsing call statements

 private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)

 {

@@ -47,7 +37,6 @@ Contract.Ensures(Contract.Result<Expression>() != null);
   }

   return e;  // cannot convert to IdentifierExpr (or is already an IdentifierExpr)

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members) from "filename"

 /// and appends them in appropriate form to "modules".

@@ -68,7 +57,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module
     }

   }

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

 /// and appends them in appropriate form to "modules".

@@ -82,7 +70,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   Errors errors = new Errors();

   return Parse(s, filename, modules, builtIns, errors);

 }

-

 ///<summary>

 /// Parses top-level things (modules, classes, datatypes, class members)

 /// and appends them in appropriate form to "modules".

@@ -108,7 +95,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
   theBuiltIns = oldBuiltIns;

   return parser.errors.count;

 }

-

 /*--------------------------------------------------------------------------*/

 CHARACTERS

   letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".

@@ -116,25 +102,20 @@ CHARACTERS
   posDigit = "123456789".

   special = "'_?\\".

   glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".

-

   cr        = '\r'.

   lf        = '\n'.

   tab       = '\t'.

-

   space = ' '.

   quote = '"'.

-

   nondigit = letter + special.

   idchar = nondigit + digit.

   nonquote = letter + digit + space + glyph.

-

   /* exclude the characters in 'array' */

   nondigitMinusA = nondigit - 'a'.

   idcharMinusA = idchar - 'a'.

   idcharMinusR = idchar - 'r'.

   idcharMinusY = idchar - 'y'.

   idcharMinusPosDigit = idchar - posDigit.

-

 /*------------------------------------------------------------------------*/

 TOKENS

   ident =  nondigitMinusA {idchar}            /* if char 0 is not an 'a', then anything else is fine */

@@ -147,23 +128,16 @@ TOKENS
   digits = digit {digit}.

   arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].

   string = quote {nonquote} quote.

-

 COMMENTS FROM "/*" TO "*/" NESTED

 COMMENTS FROM "//" TO lf

-

 IGNORE cr + lf + tab

-

-

 /*------------------------------------------------------------------------*/

 PRODUCTIONS

-

 Dafny

 = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

      Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

-

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

      ModuleDecl module;

-     

      // to support multiple files, create a default module only if theModules doesn't already contain one

      DefaultModuleDecl defaultModule = null;

      foreach (ModuleDecl mdecl in theModules) {

@@ -206,7 +180,6 @@ Dafny
   .)

   EOF

   .

-

 ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>

 = (. Contract.Requires(module != null);

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

@@ -227,16 +200,15 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
   "{"                                            (. bodyStart = t; .)

   { ClassMemberDecl<members, true>

   }

-  "}"                                      

-  (. if (optionalId == null)        

+  "}"

+  (. if (optionalId == null)

        c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

-     else 

+     else

        c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

      c.BodyStartTok = bodyStart;

      c.BodyEndTok = t;

   .)

   .

-

 ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>

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

      Method/*!*/ m;

@@ -247,13 +219,12 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
   | "static"                               (. mmod.IsStatic = true; .)

   | "unlimited"                            (. mmod.IsUnlimited = true; .)

   }

-  ( FieldDecl<mmod, mm>  

+  ( FieldDecl<mmod, mm>

   | FunctionDecl<mmod, out f>                   (. mm.Add(f); .)

   | MethodDecl<mmod, allowConstructors, out m>  (. mm.Add(m); .)

-  | CouplingInvDecl<mmod, mm> 

+  | CouplingInvDecl<mmod, mm>

   )

   .

-

 DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>

 = (. Contract.Requires(module != null);

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

@@ -276,7 +247,6 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
      dt.BodyEndTok = t;

   .)

   .

-

 DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>

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

      Attributes attrs = null;

@@ -288,7 +258,6 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
   [ FormalsOptionalIds<formals> ]

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

   .

-

 FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

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

      Attributes attrs = null;

@@ -304,7 +273,6 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   }

   ";"

   .

-

 CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

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

      Attributes attrs = null;

@@ -317,17 +285,15 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
      if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }

      if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }

   .)

-  { Attribute<ref attrs> }  

+  { Attribute<ref attrs> }

   Ident<out id>                                     (. ids.Add(id); .)

   { "," Ident<out id>                               (. ids.Add(id); .)

   }

-  "by"    

+  "by"

   Expression<out e>

   ";"

-  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)  

+  (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)

   .

-

-

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

 /* isGhost always returns as false if allowGhostKeyword is false */

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

@@ -337,14 +303,12 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
   ]

   IdentType<out id, out ty>

   .

-

 IdentType<out IToken/*!*/ id, out Type/*!*/ ty>

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

   Ident<out id>

   ":"

   Type<out ty>

   .

-

 LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>

 = (. IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

   .)

@@ -353,7 +317,6 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
   ]

   (. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)

   .

-

 IdentTypeOptional<out BoundVar/*!*/ var>

 = (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

   .)

@@ -362,7 +325,6 @@ IdentTypeOptional<out BoundVar/*!*/ var>
   ]

   (. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)

   .

-

 TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>

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

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

@@ -389,9 +351,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
      }

   .)

   .

-

 /*------------------------------------------------------------------------*/

-

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

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

      IToken/*!*/ id; .)

@@ -401,9 +361,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
   }

   ">"

   .

-

 /*------------------------------------------------------------------------*/

-

 MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>

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

      IToken/*!*/ id;

@@ -447,11 +405,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)

     Formals<false, !mmod.IsGhost, outs>

   ]

-

   { MethodSpec<req, mod, ens, dec> }

   [ BlockStmt<out bb, out bodyStart, out bodyEnd>    (. body = (BlockStmt)bb; .)

   ]

-  

   (. if (isRefinement)

        m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

      else if (isConstructor)

@@ -462,7 +418,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      m.BodyEndTok = bodyEnd;

  .)

   .

-

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

            List<Expression/*!*/>/*!*/ decreases.>

 = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

@@ -480,8 +435,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
   | "decreases" DecreasesList<decreases, false> ";"

   )

   .

-

-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.> 

+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>

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

   "("

   [

@@ -491,8 +445,7 @@ Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
   ]

   ")"

   .

-

-FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.> 

+FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>

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

   "("

   [

@@ -502,14 +455,11 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
   ]

   ")"

   .

-

 /*------------------------------------------------------------------------*/

-

 Type<out Type/*!*/ ty>

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

   TypeAndToken<out tok, out ty>

   .

-

 TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

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

@@ -529,7 +479,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        }

                                        ty = new MultiSetType(gt[0]);

                                     .)

-    

   | "seq"                           (. tok = t;  gt = new List<Type/*!*/>(); .)

     GenericInstantiation<gt>        (. if (gt.Count != 1) {

                                          SemErr("seq type expects exactly one type argument");

@@ -539,7 +488,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
   | ReferenceType<out tok, out ty>

   )

   .

-

 ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>

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

      tok = Token.NoToken;  ty = new BoolType();  /*keep compiler happy*/

@@ -560,7 +508,6 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
     [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt); .)

   )

   .

-

 GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>

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

   "<"

@@ -569,9 +516,7 @@ GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
     }

   ">"

   .

-

 /*------------------------------------------------------------------------*/

-

 FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>

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

      Attributes attrs = null;

@@ -594,7 +539,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
   (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }

   .)

   { Attribute<ref attrs> }

-  Ident<out id> 

+  Ident<out id>

   [ GenericParameters<typeArgs> ]

   Formals<true, isFunctionMethod, formals>

   ":"

@@ -607,7 +552,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      f.BodyEndTok = bodyEnd;

   .)

   .

-

 FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>

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

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

@@ -620,7 +564,6 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
   | "decreases" DecreasesList<decreases, false> ";"

   )

   .

-

 PossiblyWildExpression<out Expression/*!*/ e>

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

      e = dummyExpr; .)

@@ -631,7 +574,6 @@ PossiblyWildExpression<out Expression/*!*/ e>
   | Expression<out e>

   )

   .

-

 PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>

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

   /* A reads clause can list a wildcard, which allows the enclosing function to

@@ -644,7 +586,6 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
   | FrameExpression<out fe>

   )

   .

-

 FrameExpression<out FrameExpression/*!*/ fe>

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

   Expression<out e>

@@ -652,16 +593,13 @@ FrameExpression<out FrameExpression/*!*/ fe>
   ]

   (. fe = new FrameExpression(e, fieldName); .)

   .

-

 FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>

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

   "{"                         (. bodyStart = t; .)

   Expression<out e>

   "}"                         (. bodyEnd = t; .)

   .

-  

 /*------------------------------------------------------------------------*/

-

 BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>

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

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

@@ -672,13 +610,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
   "}"                                  (. bodyEnd = t;

                                           block = new BlockStmt(bodyStart, body); .)

   .

-

 Stmt<.List<Statement/*!*/>/*!*/ ss.>

 = (. Statement/*!*/ s;

   .)

   OneStmt<out s>                                (. ss.Add(s); .)

   .

-

 OneStmt<out Statement/*!*/ s>

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

      s = dummyStmt;  /* to please the compiler */

@@ -708,7 +644,6 @@ OneStmt<out Statement/*!*/ s>
   | ReturnStmt<out s>

   )

   .

-

 ReturnStmt<out Statement/*!*/ s>

 = (.

    IToken returnTok = null;

@@ -744,7 +679,6 @@ UpdateStmt<out Statement/*!*/ s>
   )

   (. s = new UpdateStmt(x, lhss, rhss); .)

   .

-

 Rhs<out AssignmentRhs r, Expression receiverForInitCall>

 = (. IToken/*!*/ x, newToken;  Expression/*!*/ e;

      List<Expression> ee = null;

@@ -772,17 +706,13 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
          r = new TypeRhs(newToken, ty, initCall);

        }

     .)

-    

   /* One day, the choose expression should be treated just as a special case of a method call. */

   | "choose"                           (. x = t; .)

     Expression<out e>                  (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)

-

   | "*"                                (. r = new HavocRhs(t); .)

-

   | Expression<out e>                  (. r = new ExprRhs(e); .)

   )

   .

-

 VarDeclStatement<.out Statement/*!*/ s.>

 = (. IToken x = null, assignTok = null;  bool isGhost = false;

      VarDecl/*!*/ d;

@@ -816,7 +746,6 @@ VarDeclStatement<.out Statement/*!*/ s.>
      s = new VarDeclStmt(x, lhss, update);

   .)

   .

-

 IfStmt<out Statement/*!*/ ifStmt>

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

      Expression guard;

@@ -842,7 +771,6 @@ IfStmt<out Statement/*!*/ ifStmt>
     (. ifStmt = new AlternativeStmt(x, alternatives); .)

   )

   .

-

 AlternativeBlock<.out List<GuardedAlternative> alternatives.>

 = (. alternatives = new List<GuardedAlternative>();

      IToken x;

@@ -859,7 +787,6 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.>
   }

   "}"

   .

-

 WhileStmt<out Statement/*!*/ stmt>

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

      Expression guard;

@@ -883,7 +810,6 @@ WhileStmt<out Statement/*!*/ stmt>
     (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)

   )

   .

-

 LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>

 = (. bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

      invariants = new List<MaybeFreeExpression/*!*/>();

@@ -904,7 +830,6 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
                ] ";"

   }

   .

-

 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

@@ -921,7 +846,6 @@ DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
                                          .)

   }

   .

-

 Guard<out Expression e>   /* null represents demonic-choice */

 = (. Expression/*!*/ ee;  e = null; .)

   "("

@@ -930,7 +854,6 @@ Guard<out Expression e>   /* null represents demonic-choice */
   )

   ")"

   .

-

 MatchStmt<out Statement/*!*/ s>

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

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

@@ -943,7 +866,6 @@ MatchStmt<out Statement/*!*/ s>
   "}"

   (. s = new MatchStmt(x, e, cases); .)

   .

-

 CaseStatement<out MatchCaseStmt/*!*/ c>

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

      IToken/*!*/ x, id, arg;

@@ -961,9 +883,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
     { Stmt<body> }

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

   .

-

 /*------------------------------------------------------------------------*/

-

 ForeachStmt<out Statement/*!*/ s>

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

      IToken/*!*/ x, boundVar;

@@ -994,19 +914,16 @@ ForeachStmt<out Statement/*!*/ s>
                                                   }

                                                .)

   .

-

 AssertStmt<out Statement/*!*/ s>

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

   "assert"                                     (. x = t; .)

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

   .

-

 AssumeStmt<out Statement/*!*/ s>

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

   "assume"                                     (. x = t; .)

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

   .

-

 PrintStmt<out Statement/*!*/ s>

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

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

@@ -1017,13 +934,11 @@ PrintStmt<out Statement/*!*/ s>
   }

   ";"                                          (. s = new PrintStmt(x, args); .)

   .

-

 /*------------------------------------------------------------------------*/

 Expression<out Expression/*!*/ e>

 =

   EquivExpression<out e>

   .

-

 /*------------------------------------------------------------------------*/

 EquivExpression<out Expression/*!*/ e0>

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

@@ -1032,9 +947,7 @@ EquivExpression<out Expression/*!*/ e0>
     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)

   }

   .

-

 EquivOp = "<==>" | '\u21d4'.

-

 /*------------------------------------------------------------------------*/

 ImpliesExpression<out Expression/*!*/ e0>

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

@@ -1043,9 +956,7 @@ ImpliesExpression<out Expression/*!*/ e0>
     ImpliesExpression<out e1>                  (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)

   ]

   .

-

 ImpliesOp = "==>" | '\u21d2'.

-

 /*------------------------------------------------------------------------*/

 LogicalExpression<out Expression/*!*/ e0>

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

@@ -1062,10 +973,8 @@ LogicalExpression<out Expression/*!*/ e0>
     }

   ]

   .

-

 AndOp = "&&" | '\u2227'.

 OrOp = "||" | '\u2228'.

-

 /*------------------------------------------------------------------------*/

 RelationalExpression<out Expression/*!*/ e>

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

@@ -1149,7 +1058,6 @@ RelationalExpression<out Expression/*!*/ e>
      }

   .)

   .

-

 RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

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

   ( "=="           (. x = t;  op = BinaryExpr.Opcode.Eq; .)

@@ -1166,7 +1074,6 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   | '\u2265'       (. x = t;  op = BinaryExpr.Opcode.Ge; .)

   )

   .

-

 /*------------------------------------------------------------------------*/

 Term<out Expression/*!*/ e0>

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

@@ -1175,14 +1082,12 @@ Term<out Expression/*!*/ e0>
     Factor<out e1>                             (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

-

 AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

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

   ( "+"            (. x = t;  op = BinaryExpr.Opcode.Add; .)

   | "-"            (. x = t;  op = BinaryExpr.Opcode.Sub; .)

   )

   .

-

 /*------------------------------------------------------------------------*/

 Factor<out Expression/*!*/ e0>

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

@@ -1191,7 +1096,6 @@ Factor<out Expression/*!*/ e0>
     UnaryExpression<out e1>                    (. e0 = new BinaryExpr(x, op, e0, e1); .)

   }

   .

-

 MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>

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

   ( "*"            (. x = t;  op = BinaryExpr.Opcode.Mul; .)

@@ -1199,7 +1103,6 @@ MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
   | "%"            (. x = t;  op = BinaryExpr.Opcode.Mod; .)

   )

   .

-

 /*------------------------------------------------------------------------*/

 UnaryExpression<out Expression/*!*/ e>

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

@@ -1216,7 +1119,6 @@ UnaryExpression<out Expression/*!*/ e>
     { Suffix<ref e> }

   )

   .

-

 Lhs<out Expression e>

 = (. e = null;  // to please the compiler

   .)

@@ -1227,9 +1129,7 @@ Lhs<out Expression e>
     { Suffix<ref e> }

   )

   .

-

 NegOp = "!" | '\u00ac'.

-

 /* A ConstAtomExpression is never an l-value.  Also, a ConstAtomExpression is never followed by

  * an open paren (but could very well have a suffix that starts with a period or a square bracket).

  * (The "Also..." part may change if expressions in Dafny could yield functions.)

@@ -1258,7 +1158,6 @@ ConstAtomExpression<out Expression/*!*/ e>
     ")"

   )

   .

-

 DisplayExpr<out Expression e>

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

      IToken/*!*/ x = null;  List<Expression/*!*/>/*!*/ elements;

@@ -1287,7 +1186,6 @@ MultiSetExpr<out Expression e>
   | (. SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); .)

   )

   .

-

 EndlessExpression<out Expression e>

 = (. IToken/*!*/ x;

      Expression e0, e1;

@@ -1302,7 +1200,6 @@ EndlessExpression<out Expression e>
   | ComprehensionExpr<out e>

   )

   .

-

 MatchExpression<out Expression/*!*/ e>

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

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

@@ -1316,7 +1213,6 @@ MatchExpression<out Expression/*!*/ e>
   }

   (. e = new MatchExpr(x, e, cases); .)

   .

-

 CaseExpression<out MatchCaseExpr/*!*/ c>

 = (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;

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

@@ -1332,9 +1228,7 @@ CaseExpression<out MatchCaseExpr/*!*/ c>
   "=>"

   Expression<out body>       (. c = new MatchCaseExpr(x, id.val, arguments, body); .)

   .

-

 /*------------------------------------------------------------------------*/

-

 DottedIdentifiersAndFunction<out Expression e>

 = (. IToken id;  IToken openParen = null;

      List<Expression> args = null;

@@ -1350,7 +1244,6 @@ DottedIdentifiersAndFunction<out Expression e>
   ]

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

   .

-

 Suffix<ref Expression/*!*/ e>

 = (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x;  List<Expression/*!*/>/*!*/ args;

      Expression e0 = null;  Expression e1 = null;  Expression/*!*/ ee;  bool anyDots = false;

@@ -1363,7 +1256,6 @@ Suffix<ref Expression/*!*/ e>
         [ Expressions<args> ]

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

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

-    

   | "["                                        (. x = t; .)

       ( Expression<out ee>                     (. e0 = ee; .)

         ( ".."                                 (. anyDots = true; .)

@@ -1408,9 +1300,7 @@ Suffix<ref Expression/*!*/ e>
     "]"

   )

   .

-

 /*------------------------------------------------------------------------*/

-

 QuantifierGuts<out Expression/*!*/ q>

 = (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;

      bool univ = false;

@@ -1441,11 +1331,9 @@ QuantifierGuts<out Expression/*!*/ q>
      }

   .)

   .

-

 Forall = "forall" | '\u2200'.

 Exists = "exists" | '\u2203'.

 QSep = "::" | '\u2022'.

-

 ComprehensionExpr<out Expression/*!*/ q>

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

      IToken/*!*/ x = Token.NoToken;

@@ -1468,22 +1356,18 @@ ComprehensionExpr<out Expression/*!*/ q>
      q = new SetComprehension(x, bvars, range, body);

   .)

   .

-

 Expressions<.List<Expression/*!*/>/*!*/ args.>

 = (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)

   Expression<out e>                            (. args.Add(e); .)

   { "," Expression<out e>                      (. args.Add(e); .)

   }

   .

-

 /*------------------------------------------------------------------------*/

-

 Attribute<ref Attributes attrs>

 = "{"

     AttributeBody<ref attrs>

   "}"

   .

-

 AttributeBody<ref Attributes attrs>

 = (. string aName;

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

@@ -1495,14 +1379,12 @@ AttributeBody<ref Attributes attrs>
     }

   ]                                    (. attrs = new Attributes(aName, aArgs, attrs); .)

   .

-

 AttributeArg<out Attributes.Argument/*!*/ arg>

 = (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e;  arg = dummyAttrArg; .)

   ( string                             (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)

   | Expression<out e>                  (. arg = new Attributes.Argument(e); .)

   )

   .

-

 AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>

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

   .)

@@ -1513,21 +1395,17 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
     )

   "}"

   .

-

 /*------------------------------------------------------------------------*/

-

 Idents<.List<string/*!*/>/*!*/ ids.>

 = (. IToken/*!*/ id; .)

   Ident<out id>                            (. ids.Add(id.val); .)

   { "," Ident<out id>                      (. ids.Add(id.val); .)

   }

   .

-

 Ident<out IToken/*!*/ x>

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

   ident            (. x = t; .)

   .

-

 Nat<out BigInteger n>

 =

   digits

@@ -1537,7 +1415,6 @@ Nat<out BigInteger n>
        SemErr("incorrectly formatted number");

        n = BigInteger.Zero;

      }

-  .) 

+  .)

   .

-

-END Dafny.
\ No newline at end of file
+END Dafny.

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 871a8b34..218f95e5 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -413,13 +413,13 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for any type.

-  /// </summary>  

+  /// </summary>

   public class InferredTypeProxy : UnrestrictedTypeProxy {

   }

 

   /// <summary>

   /// This proxy stands for any type, but it originates from an instantiated type parameter.

-  /// </summary>  

+  /// </summary>

   public class ParamTypeProxy : UnrestrictedTypeProxy {

     TypeParameter orig;

     [ContractInvariantMethod]

@@ -445,7 +445,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for any datatype.

-  /// </summary>  

+  /// </summary>

   public class DatatypeProxy : RestrictedTypeProxy {

     public override int OrderID {

       get {

@@ -456,7 +456,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// This proxy stands for object or any class/array type.

-  /// </summary>  

+  /// </summary>

   public class ObjectTypeProxy : RestrictedTypeProxy {

     public override int OrderID {

       get {

@@ -504,7 +504,7 @@ namespace Microsoft.Dafny {
   /// if AllowSeq, or:

   ///     int or set or multiset

   /// if !AllowSeq.

-  /// </summary>  

+  /// </summary>

   public class OperationTypeProxy : RestrictedTypeProxy {

     public readonly bool AllowSeq;

     public OperationTypeProxy(bool allowSeq) {

@@ -688,7 +688,7 @@ namespace Microsoft.Dafny {
 

   public class ClassRefinementDecl : ClassDecl {

     public readonly IToken/*!*/ RefinedClass;

-    public ClassDecl Refined; // filled in during resolution 

+    public ClassDecl Refined; // filled in during resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(RefinedClass != null);

@@ -733,7 +733,7 @@ namespace Microsoft.Dafny {
       Dims = dims;

     }

   }

-  

+

   public class DatatypeDecl : TopLevelDecl {

     public readonly List<DatatypeCtor/*!*/>/*!*/ Ctors;

     [ContractInvariantMethod]

@@ -1698,7 +1698,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Mod == null || cce.NonNullElements(Mod));

     }

     public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)

-    : base(tok) 

+    : base(tok)

     {

       Contract.Requires(tok != null);

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

@@ -2564,7 +2564,7 @@ namespace Microsoft.Dafny {
 

     public List<BoundedPool> Bounds;  // initialized and filled in by resolver

     // invariant Bounds == null || Bounds.Count == BoundVars.Count;

-    public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found 

+    public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found

     // invariant Bounds == null || MissingBounds == null;

 

     public ComprehensionExpr(IToken/*!*/ tok, List<BoundVar/*!*/>/*!*/ bvars, Expression range, Expression/*!*/ term, Attributes attrs)

@@ -2582,7 +2582,7 @@ namespace Microsoft.Dafny {
     public override IEnumerable<Expression> SubExpressions {

       get {

         if (Range != null) { yield return Range; }

-        yield return Term; 

+        yield return Term;

       }

     }

   }

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index a18ea938..3f0b6e97 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -27,21 +27,21 @@ namespace Microsoft.Dafny {
         if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {

           Bpl.CommandLineOptions.Clo.XmlSink.WriteFileFragment(dafnyFileName);

         }

-        if (Bpl.CommandLineOptions.Clo.Trace) 

+        if (Bpl.CommandLineOptions.Clo.Trace)

         {

           Console.WriteLine("Parsing " + dafnyFileName);

         }

 

         int errorCount;

-        try 

+        try

         {

           errorCount = Dafny.Parser.Parse(dafnyFileName, modules, builtIns);

-          if (errorCount != 0) 

+          if (errorCount != 0)

           {

             return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);

           }

-        } 

-        catch (IOException e) 

+        }

+        catch (IOException e)

         {

           return string.Format("Error opening file \"{0}\": {1}", dafnyFileName, e.Message);

         }

@@ -61,7 +61,7 @@ namespace Microsoft.Dafny {
           }

         }

       }

-      

+

       if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }

 

       Dafny.Resolver r = new Dafny.Resolver(program);

@@ -73,4 +73,4 @@ namespace Microsoft.Dafny {
       return null;  // success

     }

   }

-}
\ No newline at end of file
+}

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 7f063c2c..6a15b1f7 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

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

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

   <PropertyGroup>

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

@@ -147,11 +147,11 @@
     </BootstrapperPackage>

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it.

        Other similar extension points exist, see Microsoft.Common.targets.

   <Target Name="BeforeBuild">

   </Target>

   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>
\ No newline at end of file
+</Project>

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 15a3f65d..63b5f926 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny {
   class Printer {

     TextWriter wr;

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(wr!=null);

     }

@@ -23,7 +23,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wr != null);

       this.wr = wr;

     }

-    

+

     public void PrintProgram(Program prog) {

       Contract.Requires(prog != null);

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

@@ -56,7 +56,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void PrintTopLevelDecls(List<TopLevelDecl> classes, int indent) {

       Contract.Requires(classes!= null);

       int i = 0;

@@ -79,7 +79,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void PrintClass(ClassDecl c, int indent) {

       Contract.Requires(c != null);

       Indent(indent);

@@ -97,12 +97,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

     }

-    

+

     public void PrintClass_Members(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

       Contract.Requires( c.Members.Count != 0);

-    

+

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

       foreach (MemberDecl m in c.Members) {

         if (m is Method) {

@@ -126,7 +126,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

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

       Contract.Requires(kind != null);

       Contract.Requires(name != null);

@@ -147,7 +147,7 @@ namespace Microsoft.Dafny {
         wr.Write(">");

       }

     }

-    

+

     public void PrintDatatype(DatatypeDecl dt, int indent) {

       Contract.Requires(dt != null);

       Indent(indent);

@@ -164,17 +164,17 @@ namespace Microsoft.Dafny {
       }

       wr.WriteLine(";");

     }

-    

+

     public void PrintAttributes(Attributes a) {

       if (a != null) {

         PrintAttributes(a.Prev);

-        

+

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

         PrintAttributeArgs(a.Args);

         wr.Write("} ");

       }

     }

-    

+

     public void PrintAttributeArgs(List<Attributes.Argument> args) {

       Contract.Requires(args != null);

       string prefix = " ";

@@ -190,7 +190,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void PrintField(Field field, int indent) {

       Contract.Requires(field != null);

       Indent(indent);

@@ -203,7 +203,7 @@ namespace Microsoft.Dafny {
       PrintType(field.Type);

       wr.WriteLine(";");

     }

-    

+

     public void PrintCouplingInvariant(CouplingInvariant inv, int indent) {

       Contract.Requires(inv != null);

       Indent(indent);

@@ -218,7 +218,7 @@ namespace Microsoft.Dafny {
       PrintExpression(inv.Expr);

       wr.WriteLine(";");

     }

-    

+

     public void PrintFunction(Function f, int indent) {

       Contract.Requires(f != null);

       Indent(indent);

@@ -245,20 +245,20 @@ namespace Microsoft.Dafny {
         wr.WriteLine("}");

       }

     }

-    

+

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

 

     const int IndentAmount = 2;

     const string BunchaSpaces = "                                ";

     void Indent(int amount)

     {  Contract.Requires( 0 <= amount);

-    

+

       while (0 < amount) {

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

         amount -= BunchaSpaces.Length;

       }

     }

-    

+

     public void PrintMethod(Method method, int indent) {

       Contract.Requires(method != null);

       Indent(indent);

@@ -284,14 +284,14 @@ namespace Microsoft.Dafny {
       PrintFrameSpecLine("modifies", method.Mod, ind);

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

       PrintSpecLine("decreases", method.Decreases, ind);

-      

+

       if (method.Body != null) {

         Indent(indent);

         PrintStatement(method.Body, indent);

         wr.WriteLine();

       }

     }

-    

+

     void PrintFormals(List<Formal> ff) {

       Contract.Requires(ff!=null);

       wr.Write("(");

@@ -304,7 +304,7 @@ namespace Microsoft.Dafny {
       }

       wr.Write(")");

     }

-    

+

     void PrintFormal(Formal f) {

       Contract.Requires(f != null);

       if (f.IsGhost) {

@@ -315,7 +315,7 @@ namespace Microsoft.Dafny {
       }

       PrintType(f.Type);

     }

-    

+

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

       Contract.Requires(kind != null);

       Contract.Requires(ee != null);

@@ -363,7 +363,7 @@ namespace Microsoft.Dafny {
     }

 

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

-    

+

     public void PrintType(Type ty) {

       Contract.Requires(ty != null);

       wr.Write(ty.ToString());

@@ -379,7 +379,7 @@ namespace Microsoft.Dafny {
     }

 

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

-    

+

     /// <summary>

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

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

@@ -393,23 +393,23 @@ namespace Microsoft.Dafny {
           Indent(indent);

         }

       }

-        

+

       if (stmt is AssertStmt) {

         wr.Write("assert ");

         PrintExpression(((AssertStmt)stmt).Expr);

         wr.Write(";");

-        

+

       } else if (stmt is AssumeStmt) {

         wr.Write("assume ");

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

         wr.Write(";");

-        

+

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         wr.Write("print");

         PrintAttributeArgs(s.Args);

         wr.Write(";");

-        

+

       } else if (stmt is BreakStmt) {

         BreakStmt s = (BreakStmt)stmt;

         if (s.TargetLabel != null) {

@@ -422,7 +422,7 @@ namespace Microsoft.Dafny {
           }

           wr.Write(";");

         }

-        

+

       } else if (stmt is ReturnStmt) {

         var s = (ReturnStmt) stmt;

         wr.Write("return");

@@ -435,14 +435,14 @@ namespace Microsoft.Dafny {
           }

         }

           wr.Write(";");

-        

+

       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         PrintExpression(s.Lhs);

         wr.Write(" := ");

         PrintRhs(s.Rhs);

         wr.Write(";");

-        

+

       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

         if (s.IsGhost) {

@@ -451,7 +451,7 @@ namespace Microsoft.Dafny {
         wr.Write("var {0}", s.Name);

         PrintType(": ", s.OptionalType);

         wr.Write(";");

-      

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         wr.Write("call ");

@@ -471,7 +471,7 @@ namespace Microsoft.Dafny {
         wr.Write("{0}(", s.MethodName);

         PrintExpressionList(s.Args);

         wr.Write(");");

-        

+

       } else if (stmt is BlockStmt) {

         wr.WriteLine("{");

         int ind = indent + IndentAmount;

@@ -482,7 +482,7 @@ namespace Microsoft.Dafny {
         }

         Indent(indent);

         wr.Write("}");

-        

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         while (true) {

@@ -508,7 +508,7 @@ namespace Microsoft.Dafny {
         PrintAlternatives(indent, s.Alternatives);

         Indent(indent);

         wr.Write("}");

-      

+

       } else if (stmt is WhileStmt) {

         WhileStmt s = (WhileStmt)stmt;

         wr.Write("while (");

@@ -556,7 +556,7 @@ namespace Microsoft.Dafny {
         wr.WriteLine();

         Indent(indent);

         wr.Write("}");

-        

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         wr.Write("match ");

@@ -644,7 +644,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     void PrintRhs(AssignmentRhs rhs) {

       Contract.Requires(rhs != null);

       if (rhs is ExprRhs) {

@@ -673,7 +673,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

       }

     }

-    

+

     void PrintGuard(Expression guard) {

       if (guard == null) {

         wr.Write("*");

@@ -681,7 +681,7 @@ namespace Microsoft.Dafny {
         PrintExpression(guard);

       }

     }

-    

+

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

 

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

@@ -739,12 +739,12 @@ namespace Microsoft.Dafny {
         wr.WriteLine(endWithCloseParen ? ")" : "");

       }

     }

-    

+

     public void PrintExpression(Expression expr) {

       Contract.Requires(expr != null);

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

     }

-    

+

     /// <summary>

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

     /// </summary>

@@ -752,7 +752,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

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

     }

-    

+

     /// <summary>

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

     /// </summary>

@@ -770,13 +770,13 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-      

+

       } else if (expr is ThisExpr) {

         wr.Write("this");

-  

+

       } else if (expr is IdentifierExpr) {

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

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

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

@@ -785,14 +785,14 @@ namespace Microsoft.Dafny {
           PrintExpressionList(dtv.Arguments);

           wr.Write(")");

         }

-        

+

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         if (e is MultiSetDisplayExpr) wr.Write("multiset");

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

         PrintExpressionList(e.Elements);

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

-        

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         // determine if parens are needed

@@ -800,7 +800,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !(e.Obj is ImplicitThisExpr) &&

           opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

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

         if (!(e.Obj is ImplicitThisExpr)) {

           PrintExpr(e.Obj, opBindingStrength, false, false, -1);

@@ -815,7 +815,7 @@ namespace Microsoft.Dafny {
         int opBindingStrength = 0x70;

         bool parensNeeded = opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

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

         PrintExpr(e.Seq, 0x00, false, false, indent);  // BOGUS: fix me

         wr.Write("[");

@@ -859,7 +859,7 @@ namespace Microsoft.Dafny {
         int opBindingStrength = 0x70;

         bool parensNeeded = opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

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

         PrintExpr(e.Seq, 00, false, false, indent);  // BOGUS: fix me

         wr.Write("[");

@@ -868,7 +868,7 @@ namespace Microsoft.Dafny {
         PrintExpression(e.Value);

         wr.Write("]");

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

-      

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         // determine if parens are needed

@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
         bool parensNeeded = !(e.Receiver is ImplicitThisExpr) &&

           opBindingStrength < contextBindingStrength ||

           (fragileContext && opBindingStrength == contextBindingStrength);

-        

+

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

         if (!(e.Receiver is ImplicitThisExpr)) {

           PrintExpr(e.Receiver, opBindingStrength, false, false, -1);

@@ -935,14 +935,14 @@ namespace Microsoft.Dafny {
           PrintExpr(e.E, opBindingStrength, false, parensNeeded || isRightmost, -1);

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

         }

-      

+

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         // determine if parens are needed

         int opBindingStrength;

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

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

-        switch (e.Op) 

+        switch (e.Op)

         {

           case BinaryExpr.Opcode.Add:

             opBindingStrength = 0x40; break;

@@ -1070,7 +1070,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is WildcardExpr) {

         wr.Write("*");

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr ite = (ITEExpr)expr;

         bool parensNeeded = !isRightmost;

@@ -1082,7 +1082,7 @@ namespace Microsoft.Dafny {
         wr.Write(" else ");

         PrintExpression(ite.Els);

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

-        

+

       } else if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

         // printing of parentheses is done optimally, not according to the parentheses in the given program

@@ -1100,24 +1100,24 @@ namespace Microsoft.Dafny {
           PrintExpressionList(e.Arguments);

           wr.Write(")");

         }

-        

+

       } else if (expr is MatchExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

       } else {

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

       }

     }

-    

+

     void PrintTriggers(Triggers trigs) {

       if (trigs != null) {

         PrintTriggers(trigs.Prev);

-        

+

         wr.Write("{ ");

         PrintExpressionList(trigs.Terms);

         wr.Write(" } ");

       }

     }

-    

+

     void PrintExpressionList(List<Expression> exprs) {

       Contract.Requires(exprs != null);

       string sep = "";

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1321a987..098dbad2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Dafny {
     }

 

     bool checkRefinements = true; // used to indicate a cycle in refinements

-      

+

     public void ResolveProgram(Program prog) {

       Contract.Requires(prog != null);

       // register modules

@@ -119,15 +119,15 @@ namespace Microsoft.Dafny {
         }

       }

 

-      // resolve top-level declarations of refinements      

-      foreach (ModuleDecl m in prog.Modules) 

-        foreach (TopLevelDecl decl in m.TopLevelDecls) 

+      // resolve top-level declarations of refinements

+      foreach (ModuleDecl m in prog.Modules)

+        foreach (TopLevelDecl decl in m.TopLevelDecls)

           if (decl is ClassRefinementDecl) {

             ClassRefinementDecl rdecl = (ClassRefinementDecl) decl;

             ResolveTopLevelRefinement(rdecl);

             if (rdecl.Refined != null) refines.AddEdge(rdecl, rdecl.Refined);

           }

-      

+

       // attempt finding refinement cycles

       List<TopLevelDecl> refinesCycle = refines.TryFindCycle();

       if (refinesCycle != null) {

@@ -139,8 +139,8 @@ namespace Microsoft.Dafny {
         }

         Error(refinesCycle[0], "Detected a cyclic refinement declaration: {0}", cy);

         checkRefinements = false;

-      } 

-      

+      }

+

       // resolve top-level declarations

       Graph<DatatypeDecl> datatypeDependencies = new Graph<DatatypeDecl>();

       foreach (ModuleDecl m in prog.Modules) {

@@ -168,7 +168,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     public void RegisterTopLevelDecls(List<TopLevelDecl> declarations) {

       Contract.Requires(declarations != null);

       foreach (TopLevelDecl d in declarations) {

@@ -209,7 +209,7 @@ namespace Microsoft.Dafny {
           // ... and of the other members

           Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();

           datatypeMembers.Add(dt, members);

-        

+

           foreach (DatatypeCtor ctor in dt.Ctors) {

             if (ctor.Name.EndsWith("?")) {

               Error(ctor, "a datatype constructor name is not allowed to end with '?'");

@@ -224,7 +224,7 @@ namespace Microsoft.Dafny {
               query.EnclosingClass = dt;  // resolve here

               members.Add(queryName, query);

               ctor.QueryField = query;

-                

+

               // also register the constructor name globally

               Tuple<DatatypeCtor, bool> pair;

               if (allDatatypeCtors.TryGetValue(ctor.Name, out pair)) {

@@ -268,9 +268,9 @@ namespace Microsoft.Dafny {
         }

         decl.Refined = cce.NonNull((ClassDecl) a);

         // TODO: copy over remaining members of a

-      }        

-    }  

-      

+      }

+    }

+

     public void ResolveTopLevelDecls_Signatures(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<DatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

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

@@ -286,7 +286,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

     }

-    

+

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

       Contract.Requires(declarations != null);

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

@@ -306,7 +306,7 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();

       }

     }

-    

+

     ClassDecl currentClass;

     Function currentFunction;

     readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();

@@ -314,7 +314,7 @@ namespace Microsoft.Dafny {
     readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();

     readonly List<Statement> loopStack = new List<Statement>();  // the enclosing loops (from which it is possible to break out)

     readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>();  // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -323,13 +323,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-    

+

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         member.EnclosingClass = cl;

         if (member is Field) {

           ResolveType(member.tok, ((Field)member).Type);

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

@@ -343,15 +343,15 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, true, m);

           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

-          

+

         } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

-          if (currentClass is ClassRefinementDecl) {      

+          if (currentClass is ClassRefinementDecl) {

             ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

             if (refined != null) {

               Contract.Assert(classMembers.ContainsKey(refined));

               Dictionary<string,MemberDecl> members = classMembers[refined];

-            

+

               // resolve abstracted fields in the refined class

               List<Field> fields = new List<Field>();

               foreach (IToken tok in inv.Toks) {

@@ -359,29 +359,29 @@ namespace Microsoft.Dafny {
                   Error(tok, "Refined class does not declare a field: {0}", tok.val);

                 else {

                   MemberDecl field = members[tok.val];

-                  if (!(field is Field)) 

+                  if (!(field is Field))

                     Error(tok, "Coupling invariant refers to a non-field member: {0}", tok.val);

                   else if (fields.Contains(cce.NonNull((Field)field)))

                     Error(tok, "Duplicate reference to a field in the refined class: {0}", tok.val);

                   else

                     fields.Add(cce.NonNull((Field)field));

-                }                  

-              }            

+                }

+              }

               inv.Refined = fields;

             }

-            

+

           } else {

             Error(member, "Coupling invariants can only be declared in refinement classes");

           }

         } else {

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

         }

-        

-        if (currentClass is ClassRefinementDecl) {          

+

+        if (currentClass is ClassRefinementDecl) {

           ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;

           if (refined != null) {

             Contract.Assert(classMembers.ContainsKey(refined));

-          

+

             // there is a member with the same name in refined class if and only if the member is a refined method

             if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))

               Error(member, "Refined class has a member with the same name as in the refinement class: {0}", member.Name);

@@ -399,14 +399,14 @@ namespace Microsoft.Dafny {
       Contract.Requires(cl != null);

       Contract.Requires(currentClass == null);

       Contract.Ensures(currentClass == null);

-    

+

       ResolveAttributes(cl.Attributes, false);

       currentClass = cl;

       foreach (MemberDecl member in cl.Members) {

         ResolveAttributes(member.Attributes, false);

         if (member is Field) {

           // nothing more to do

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           allTypeParameters.PushMarker();

@@ -420,13 +420,13 @@ namespace Microsoft.Dafny {
           ResolveTypeParameters(m.TypeArgs, false, m);

           ResolveMethod(m);

           allTypeParameters.PopMarker();

-          

+

           // check if signature of the refined method matches the refinement method

           if (member is MethodRefinement) {

             MethodRefinement mf = (MethodRefinement)member;

             if (currentClass is ClassRefinementDecl) {

               // should have already been resolved

-              if (((ClassRefinementDecl)currentClass).Refined != null) { 

+              if (((ClassRefinementDecl)currentClass).Refined != null) {

                 MemberDecl d = classMembers[((ClassRefinementDecl)currentClass).Refined][mf.Name];

                 if (d is Method) {

                   mf.Refined = (Method)d;

@@ -434,18 +434,18 @@ namespace Microsoft.Dafny {
                     Error(mf, "Different number of input variables");

                   if (mf.Outs.Count != mf.Refined.Outs.Count)

                     Error(mf, "Different number of output variables");

-                  if (mf.IsStatic || mf.Refined.IsStatic) 

+                  if (mf.IsStatic || mf.Refined.IsStatic)

                     Error(mf, "Refined methods cannot be static");

                 } else {

                   Error(member, "Refined class has a non-method member with the same name: {0}", member.Name);

-                }            

+                }

               }

             } else {

               Error(member, "Refinement methods can only be declared in refinement classes: {0}", member.Name);

             }

           }

-        

-        } else if (member is CouplingInvariant) {        

+

+        } else if (member is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)member;

           if (inv.Refined != null) {

             inv.Formals = new List<Formal>();

@@ -460,7 +460,7 @@ namespace Microsoft.Dafny {
             }

             ResolveExpression(inv.Expr, false);

             scope.PopMarker();

-          }                

+          }

         } else {

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

         }

@@ -476,13 +476,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(dt != null);

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

       foreach (DatatypeCtor ctor in dt.Ctors) {

-        

+

         ctor.EnclosingDatatype = dt;

 

         allTypeParameters.PushMarker();

         ResolveCtorSignature(ctor);

         allTypeParameters.PopMarker();

-        

+

         foreach (Formal p in ctor.Formals) {

           DatatypeDecl dependee = p.Type.AsDatatype;

           if (dependee != null) {

@@ -497,7 +497,7 @@ namespace Microsoft.Dafny {
     /// datatype has some value that can be constructed from datatypes in lower stratospheres only.

     /// The algorithm used here is quadratic in the number of datatypes in the SCC.  Since that number is

     /// deemed to be rather small, this seems okay.

-    /// </summary>    

+    /// </summary>

     void SccStratosphereCheck(DatatypeDecl startingPoint, Graph<DatatypeDecl/*!*/>/*!*/ dependencies)

     {

       Contract.Requires(startingPoint != null);

@@ -573,7 +573,7 @@ namespace Microsoft.Dafny {
         ResolveAttributeArgs(attrs.Args, twoState);

       }

     }

-        

+

     void ResolveAttributeArgs(List<Attributes.Argument/*!*/>/*!*/ args, bool twoState) {

       Contract.Requires(args != null);

       foreach (Attributes.Argument aa in args) {

@@ -583,7 +583,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     void ResolveTriggers(Triggers trigs, bool twoState) {

       // order does not matter for resolution, so resolve them in reverse order

       for (; trigs != null; trigs = trigs.Prev) {

@@ -592,9 +592,9 @@ namespace Microsoft.Dafny {
         }

       }

     }

-        

+

     void ResolveTypeParameters(List<TypeParameter/*!*/>/*!*/ tparams, bool emitErrors, TypeParameter.ParentType/*!*/ parent) {

-      

+

       Contract.Requires(tparams != null);

       Contract.Requires(parent != null);

       // push type arguments of the refined class

@@ -603,7 +603,7 @@ namespace Microsoft.Dafny {
         if (refined != null)

           ResolveTypeParameters(refined.TypeArgs, false, refined);

       }

-    

+

       // push non-duplicated type parameter names

       foreach (TypeParameter tp in tparams) {

         Contract.Assert(tp != null);

@@ -616,7 +616,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -683,7 +683,7 @@ namespace Microsoft.Dafny {
       currentFunction = null;

       scope.PopMarker();

     }

-    

+

     void ResolveFrameExpression(FrameExpression fe, string kind) {

       Contract.Requires(fe != null);

       Contract.Requires(kind != null);

@@ -717,7 +717,7 @@ namespace Microsoft.Dafny {
         Error(fe.E, "a {0}-clause expression must denote an object or a collection of objects (instead got {1})", kind, fe.E.Type);

       }

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -740,7 +740,7 @@ namespace Microsoft.Dafny {
       }

       scope.PopMarker();

     }

-    

+

     /// <summary>

     /// Assumes type parameters have already been pushed

     /// </summary>

@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
       foreach (Formal p in m.Ins) {

         scope.Push(p.Name, p);

       }

-      

+

       // Start resolving specification...

       foreach (MaybeFreeExpression e in m.Req) {

         ResolveExpression(e.E, false);

@@ -770,7 +770,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(e, false);

         // any type is fine

       }

-      

+

       // Add out-parameters to a new scope that will also include the outermost-level locals of the body

       // Don't care about any duplication errors among the out-parameters, since they have already been reported

       scope.PushMarker();

@@ -786,16 +786,16 @@ namespace Microsoft.Dafny {
           Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);

         }

       }

-      

+

       // Resolve body

       if (m.Body != null) {

         ResolveBlockStatement(m.Body, m.IsGhost, m);

       }

-      

+

       scope.PopMarker();  // for the out-parameters and outermost-level locals

       scope.PopMarker();  // for the in-parameters

     }

-    

+

     void ResolveCtorSignature(DatatypeCtor ctor) {

       Contract.Requires(ctor != null);

       foreach (Formal p in ctor.Formals) {

@@ -839,18 +839,18 @@ namespace Microsoft.Dafny {
             Error(t.tok, "Wrong number of type arguments ({0} instead of {1}) passed to class/datatype: {2}", t.TypeArgs.Count, d.TypeArgs.Count, t.Name);

           }

         }

-      

+

       } else if (type is TypeProxy) {

         TypeProxy t = (TypeProxy)type;

         if (t.T != null) {

           ResolveType(tok, t.T);

         }

-        

+

       } else {

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

       }

     }

-    

+

     public bool UnifyTypes(Type a, Type b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -866,7 +866,7 @@ namespace Microsoft.Dafny {
           a = proxy.T;

         }

       }

-      

+

       while (b is TypeProxy) {

         TypeProxy proxy = (TypeProxy)b;

         if (proxy.T == null) {

@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
           b = proxy.T;

         }

       }

-      

+

 #if !NO_CHEAP_OBJECT_WORKAROUND

       if (a is ObjectType || b is ObjectType) {  // TODO: remove this temporary hack

         var other = a is ObjectType ? b : a;

@@ -888,7 +888,7 @@ namespace Microsoft.Dafny {
       }

 #endif

       // Now, a and b are non-proxies and stand for the same things as the original a and b, respectively.

-      

+

       if (a is BoolType) {

         return b is BoolType;

       } else if (a is IntType) {

@@ -925,12 +925,12 @@ namespace Microsoft.Dafny {
           // something is wrong; either aa or bb wasn't properly resolved, or they don't unify

           return false;

         }

-        

+

       } else {

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

       }

     }

-    

+

     bool AssignProxy(TypeProxy proxy, Type t){

       Contract.Requires(proxy != null);

       Contract.Requires(t != null);

@@ -941,15 +941,15 @@ namespace Microsoft.Dafny {
       if (proxy == t) {

         // they are already in the same equivalence class

         return true;

-      

+

       } else if (proxy is UnrestrictedTypeProxy) {

         // it's fine to redirect proxy to t (done below)

-        

+

       } else if (t is UnrestrictedTypeProxy) {

           // merge proxy and t by redirecting t to proxy, rather than the other way around

           ((TypeProxy)t).T = proxy;

           return true;

-      

+

       } else if (t is RestrictedTypeProxy) {

         // Both proxy and t are restricted type proxies.  To simplify unification, order proxy and t

         // according to their types.

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

           return AssignRestrictedProxies(r1, r0);

         }

-      

+

       // In the remaining cases, proxy is a restricted proxy and t is a non-proxy

       } else if (proxy is DatatypeProxy) {

         if (t.IsDatatype) {

@@ -968,14 +968,14 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-      

+

       } else if (proxy is ObjectTypeProxy) {

         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

           // all is fine, proxy can be redirected to t

         } else {

           return false;

         }

-      

+

       } else if (proxy is ObjectsTypeProxy) {

         if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {

           // all is good

@@ -983,7 +983,7 @@ namespace Microsoft.Dafny {
           proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());

           return UnifyTypes(proxy.T, t);

         }

-        

+

       } else if (proxy is CollectionTypeProxy) {

         CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;

         if (t is CollectionType) {

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

           return false;

         }

-      

+

       } else if (proxy is OperationTypeProxy) {

         OperationTypeProxy opProxy = (OperationTypeProxy)proxy;

         if (t is IntType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {

@@ -1016,11 +1016,11 @@ namespace Microsoft.Dafny {
         } else {

           return false;

         }

-                

+

       } else {

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

       }

-      

+

       // do the merge, but never infer a subrange type

       if (t is NatType) {

         proxy.T = Type.Int;

@@ -1029,7 +1029,7 @@ namespace Microsoft.Dafny {
       }

       return true;

     }

-    

+

     bool AssignRestrictedProxies(RestrictedTypeProxy a, RestrictedTypeProxy b)

     { Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -1038,7 +1038,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(a.OrderID <= b.OrderID);

       //modifies a.T, b.T;

       Contract.Ensures(Contract.Result<bool>() || a.T != null || b.T != null);

-    

+

       if (a is DatatypeProxy) {

         if (b is DatatypeProxy) {

           // all is fine

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

           return false;

         }

-        

+

       } else if (a is ObjectsTypeProxy) {

         if (b is ObjectsTypeProxy) {

           // fine

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

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

         }

-          

+

       } else if (a is CollectionTypeProxy) {

         if (b is CollectionTypeProxy) {

           a.T = b;

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

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

         }

-        

+

       } else if (a is OperationTypeProxy) {

         OperationTypeProxy pa = (OperationTypeProxy)a;

         if (b is OperationTypeProxy) {

@@ -1140,12 +1140,12 @@ namespace Microsoft.Dafny {
             return false;

           }

         }

-        

+

       } else if (a is IndexableTypeProxy) {

         Contract.Assert(b is IndexableTypeProxy);  // else we have unexpected restricted-proxy type

         a.T = b;

         return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);

-        

+

       } else {

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

       }

@@ -1166,14 +1166,14 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(s.Expr.Type, Type.Bool)) {

           Error(s.Expr, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Expr.Type);

         }

-      

+

       } else if (stmt is PrintStmt) {

         PrintStmt s = (PrintStmt)stmt;

         ResolveAttributeArgs(s.Args, false);

         if (specContextOnly) {

           Error(stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

         }

-          

+

       } else if (stmt is BreakStmt) {

         var s = (BreakStmt)stmt;

         if (s.TargetLabel != null) {

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

           Error(stmt, "LHS of assignment must denote a mutable variable or field");

         }

-        

+

         s.IsGhost = lvalueIsGhost;

         Type lhsType = s.Lhs.Type;

         if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {

@@ -1378,16 +1378,16 @@ namespace Microsoft.Dafny {
           // a local variable in a specification-only context might as well be ghost

           s.IsGhost = true;

         }

-      

+

       } else if (stmt is CallStmt) {

         CallStmt s = (CallStmt)stmt;

         ResolveCallStmt(s, specContextOnly, method, null);

-        

+

       } else if (stmt is BlockStmt) {

         scope.PushMarker();

         ResolveBlockStatement((BlockStmt)stmt, specContextOnly, method);

         scope.PopMarker();

-      

+

       } else if (stmt is IfStmt) {

         IfStmt s = (IfStmt)stmt;

         bool branchesAreSpecOnly = specContextOnly;

@@ -1481,20 +1481,20 @@ namespace Microsoft.Dafny {
         if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {

           Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);

         }

-        

+

         scope.PushMarker();

         bool b = scope.Push(s.BoundVar.Name, s.BoundVar);

         Contract.Assert(b);  // since we just pushed a marker, we expect the Push to succeed

         ResolveType(s.BoundVar.tok, s.BoundVar.Type);

         int prevErrorCount = ErrorCount;

-        

+

         ResolveExpression(s.Range, true);

         Contract.Assert(s.Range.Type != null);  // follows from postcondition of ResolveExpression

         if (!UnifyTypes(s.Range.Type, Type.Bool)) {

           Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);

         }

         bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;

-        

+

         foreach (PredicateStmt ss in s.BodyPrefix) {

           ResolveStatement(ss, specContextOnly, method);

         }

@@ -1528,7 +1528,7 @@ namespace Microsoft.Dafny {
         }

 

         scope.PopMarker();

-      

+

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

         bool bodyIsSpecOnly = specContextOnly;

@@ -1554,14 +1554,14 @@ namespace Microsoft.Dafny {
           Contract.Assert(sourceType != null);  // dtd and sourceType are set together above

           ctors = datatypeCtors[dtd];

           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

-          

+

           // build the type-parameter substitution map for this use of the datatype

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

             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);

           }

         }

         s.IsGhost = bodyIsSpecOnly;

-        

+

         Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>();  // this is really a set

         foreach (MatchCaseStmt mc in s.Cases) {

           DatatypeCtor ctor = null;

@@ -1616,8 +1616,8 @@ namespace Microsoft.Dafny {
           }

           Contract.Assert(memberNamesUsed.Count + s.MissingCases.Count == dtd.Ctors.Count);

         }

-        

-        

+

+

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();

       }

@@ -2186,7 +2186,7 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

-    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression; 

+    /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;

     /// if null, no "match" expression will be allowed.

     /// </summary>

     void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {

@@ -2197,7 +2197,7 @@ namespace Microsoft.Dafny {
         // expression has already been resovled

         return;

       }

-      

+

       // The following cases will resolve the subexpressions and will attempt to assign a type of expr.  However, if errors occur

       // and it cannot be determined what the type of expr is, then it is fine to leave expr.Type as null.  In that case, the end

       // of this method will assign proxy type to the expression, which reduces the number of error messages that are produced

@@ -2230,13 +2230,13 @@ namespace Microsoft.Dafny {
         } else {

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

         }

-        

+

       } else if (expr is ThisExpr) {

         if (!scope.AllowInstance) {

           Error(expr, "'this' is not allowed in a 'static' context");

         }

         expr.Type = GetThisType(expr.tok, currentClass);  // do this regardless of scope.AllowInstance, for better error reporting

-        

+

       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         e.Var = scope.Find(e.Name);

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

           expr.Type = e.Var.Type;

         }

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         TopLevelDecl d;

@@ -2266,7 +2266,7 @@ namespace Microsoft.Dafny {
           }

           expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);

           ResolveType(expr.tok, expr.Type);

-          

+

           DatatypeCtor ctor;

           if (!datatypeCtors[dt].TryGetValue(dtv.MemberName, out ctor)) {

             Error(expr.tok, "undeclared constructor {0} in datatype {1}", dtv.MemberName, dtv.DatatypeName);

@@ -2291,7 +2291,7 @@ namespace Microsoft.Dafny {
             j++;

           }

         }

-        

+

       } else if (expr is DisplayExpression) {

         DisplayExpression e = (DisplayExpression)expr;

         Type elementType = new InferredTypeProxy();

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

           expr.Type = new SeqType(elementType);

         }

-        

+

       } else if (expr is FieldSelectExpr) {

         var e = (FieldSelectExpr)expr;

         ResolveExpression(e.Obj, twoState);

@@ -2336,7 +2336,7 @@ namespace Microsoft.Dafny {
           }

           e.Type = SubstType(e.Field.Type, subst);

         }

-      

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         ResolveSeqSelectExpr(e, twoState, true);

@@ -2385,7 +2385,7 @@ namespace Microsoft.Dafny {
         if (!seqErr) {

           expr.Type = e.Seq.Type;

         }

-        

+

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         ResolveFunctionCallExpr(e, twoState, false);

@@ -2459,7 +2459,7 @@ namespace Microsoft.Dafny {
           default:

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

         }

-        

+

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

         ResolveExpression(e.E0, twoState);

@@ -2479,7 +2479,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Eq:

           case BinaryExpr.Opcode.Neq:

             if (!UnifyTypes(e.E0.Type, e.E1.Type)) {

@@ -2487,7 +2487,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Disjoint:

             // TODO: the error messages are backwards from what (ideally) they should be. this is necessary because UnifyTypes can't backtrack.

             if (!UnifyTypes(e.E0.Type, e.E1.Type)) {

@@ -2498,7 +2498,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-          

+

           case BinaryExpr.Opcode.Lt:

           case BinaryExpr.Opcode.Le:

           case BinaryExpr.Opcode.Add:

@@ -2526,7 +2526,7 @@ namespace Microsoft.Dafny {
               }

             }

             break;

-          

+

           case BinaryExpr.Opcode.Sub:

           case BinaryExpr.Opcode.Mul:

           case BinaryExpr.Opcode.Gt:

@@ -2563,7 +2563,7 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Bool;

             break;

-            

+

           case BinaryExpr.Opcode.Div:

           case BinaryExpr.Opcode.Mod:

             if (!UnifyTypes(e.E0.Type, Type.Int)) {

@@ -2574,12 +2574,12 @@ namespace Microsoft.Dafny {
             }

             expr.Type = Type.Int;

             break;

-          

+

           default:

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

         }

         e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);

-        

+

       } else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

@@ -2652,7 +2652,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is WildcardExpr) {

         expr.Type = new SetType(new ObjectType());

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         ResolveExpression(e.Test, twoState);

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

           Error(expr, "the two branches of an if-then-else expression must have the same type (got {0} and {1})", e.Thn.Type, e.Els.Type);

         }

-      

+

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         Contract.Assert(!twoState);  // currently, match expressions are allowed only at the outermost level of function bodies

@@ -2695,7 +2695,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(sourceType != null);  // dtd and sourceType are set together above

           ctors = datatypeCtors[dtd];

           Contract.Assert(ctors != null);  // dtd should have been inserted into datatypeCtors during a previous resolution stage

-          

+

           IdentifierExpr ie = me.Source.Resolved as IdentifierExpr;

           if (ie == null || !(ie.Var is Formal || ie.Var is BoundVar)) {

             Error(me.Source.tok, "match source expression must be a formal parameter of the enclosing function or an enclosing match expression");

@@ -2704,13 +2704,13 @@ namespace Microsoft.Dafny {
           } else {

             goodMatchVariable = ie.Var;

           }

-          

+

           // build the type-parameter substitution map for this use of the datatype

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

             subst.Add(dtd.TypeArgs[i], sourceType.TypeArgs[i]);

           }

         }

-        

+

         Dictionary<string,object> memberNamesUsed = new Dictionary<string,object>();  // this is really a set

         expr.Type = new InferredTypeProxy();

         foreach (MatchCaseExpr mc in me.Cases) {

@@ -2773,7 +2773,7 @@ namespace Microsoft.Dafny {
           }

           Contract.Assert(memberNamesUsed.Count + me.MissingCases.Count == dtd.Ctors.Count);

         }

-        

+

       } else {

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

       }

@@ -3498,13 +3498,13 @@ namespace Microsoft.Dafny {
         return s == null ? new HashSet<IVariable>() : s;

       }

     }

-    

+

     void ResolveReceiver(Expression expr, bool twoState)

     {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

-    

+

       if (expr is ThisExpr) {

         // Allow 'this' here, regardless of scope.AllowInstance.  The caller is responsible for

         // making sure 'this' does not really get used when it's not available.

@@ -3513,7 +3513,7 @@ namespace Microsoft.Dafny {
         ResolveExpression(expr, twoState);

       }

     }

-    

+

     void ResolveSeqSelectExpr(SeqSelectExpr e, bool twoState, bool allowNonUnitArraySelection) {

       Contract.Requires(e != null);

       if (e.Type != null) {

@@ -3557,7 +3557,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     /// <summary>

     /// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if

     /// resolution of the binary expression failed.  If so, an arbitrary resolved opcode is returned.

@@ -3693,7 +3693,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

-    

+

       if (expr is LiteralExpr) {

         return false;

       } else if (expr is ThisExpr) {

@@ -3769,7 +3769,7 @@ namespace Microsoft.Dafny {
     [Rep] readonly List<string> names = new List<string>();  // a null means a marker

     [Rep] readonly List<Thing> things = new List<Thing>();

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(names != null);

       Contract.Invariant(things != null);

@@ -3778,7 +3778,7 @@ namespace Microsoft.Dafny {
     }

 

     int scopeSizeWhereInstancesWereDisallowed = -1;

-    

+

     public bool AllowInstance {

       get { return scopeSizeWhereInstancesWereDisallowed == -1; }

       set

@@ -3791,7 +3791,7 @@ namespace Microsoft.Dafny {
       names.Add(null);

       things.Add(null);

     }

-    

+

     public void PopMarker() {

       int n = names.Count;

       while (true) {

@@ -3806,7 +3806,7 @@ namespace Microsoft.Dafny {
         scopeSizeWhereInstancesWereDisallowed = -1;

       }

     }

-    

+

     // Pushes name-->thing association and returns "true", if name has not already been pushed since the last marker.

     // If name already has been pushed since the last marker, does nothing and returns "false".

     public bool Push(string name, Thing thing) {

@@ -3820,7 +3820,7 @@ namespace Microsoft.Dafny {
         return true;

       }

     }

-    

+

     Thing Find(string name, bool topScopeOnly) {

       Contract.Requires(name != null);

       for (int n = names.Count; 0 <= --n; ) {

@@ -3836,7 +3836,7 @@ namespace Microsoft.Dafny {
       }

       return null;  // not present

     }

-    

+

     public Thing Find(string name) {

       Contract.Requires(name != null);

       return Find(name, false);

diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index 9f4b22c5..4ae1c185 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -12,14 +12,14 @@ namespace Microsoft.Dafny {
       public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();

       public List<Vertex/*!*/> SccMembers;  // non-null only for the representative of the SCC

       [ContractInvariantMethod]

-      void ObjectInvariant() 

+      void ObjectInvariant()

       {

         Contract.Invariant(cce.NonNullElements(Successors));

         Contract.Invariant(SccMembers==null || cce.NonNullElements(SccMembers));

       }

 

       public Vertex SccRepresentative;  // null if not computed

-      

+

       public int SccId;  // valid only for SCC representatives; indicates position of this representative vertex in the graph's topological sort

       // the following field is used during the computation of SCCs and of reachability

       public VisitedStatus Visited;

@@ -28,7 +28,7 @@ namespace Microsoft.Dafny {
       public int LowLink;

       // the following field is used during a Reaches computation

       public int Gen;  // generation <= Gen means this vertex has been visited in the current generation

-      

+

       public Vertex(Node n) {

         N = n;

       }

@@ -40,7 +40,7 @@ namespace Microsoft.Dafny {
 

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(vertices!=null);

       Contract.Invariant(cce.NonNullElements(vertices.Values));

@@ -51,7 +51,7 @@ namespace Microsoft.Dafny {
     Dictionary<Node, Vertex/*!*/>/*!*/ vertices = new Dictionary<Node, Vertex/*!*/>();

     bool sccComputed = false;

     List<Vertex/*!*/> topologicallySortedRepresentatives;  // computed by the SCC computation

-    

+

     public int SccCount {

       get {

         ComputeSCCs();

@@ -60,11 +60,11 @@ namespace Microsoft.Dafny {
       }

     }

     int generation = 0;

-    

+

     public Graph()

     {

     }

-    

+

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph.

     /// </summary>

@@ -74,7 +74,7 @@ namespace Microsoft.Dafny {
 

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph and then returns the Vertex for it.

-    /// </summary>    

+    /// </summary>

     Vertex GetVertex(Node n) {

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

 

@@ -93,7 +93,7 @@ namespace Microsoft.Dafny {
       }

       return v;

     }

-    

+

     /// <summary>

     /// Returns the vertex for 'n' if 'n' is in the graph.  Otherwise, returns null.

     /// </summary>

@@ -117,7 +117,7 @@ namespace Microsoft.Dafny {
       v0.AddSuccessor(v1);

       sccComputed = false;  // the addition of an edge may invalidate any previous computation of the graph's SCCs

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns a Node that is the representative element of the

     /// strongly connected component containing 'n'.

@@ -125,7 +125,7 @@ namespace Microsoft.Dafny {
     public Node GetSCCRepresentative(Node n) {

       return GetSCCRepr(n).N;

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex.  Then, returns the number of SCCs before the SCC of 'n' in the

     /// topologically sorting of SCCs.

@@ -133,7 +133,7 @@ namespace Microsoft.Dafny {
     public int GetSCCRepresentativeId(Node n) {

       return GetSCCRepr(n).SccId;

     }

-    

+

     Vertex GetSCCRepr(Node n) {

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

 

@@ -142,7 +142,7 @@ namespace Microsoft.Dafny {
       Contract.Assert(v.SccRepresentative != null);  // follows from what ComputeSCCs does

       return v.SccRepresentative;

     }

-    

+

     /// <summary>

     /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node.

     /// </summary>

@@ -172,21 +172,21 @@ namespace Microsoft.Dafny {
       }

       return nn;

     }

-    

+

     /// <summary>

     /// Idempotently adds 'n' as a vertex and then returns the size of the set of Node's in the strongly connected component

     /// that contains 'n'.

     /// </summary>

     public int GetSCCSize(Node n){

       Contract.Ensures(1 <= Contract.Result<int>());

-    

+

       Vertex v = GetVertex(n);

       ComputeSCCs();

       Vertex repr = v.SccRepresentative;

       Contract.Assert(repr != null && repr.SccMembers != null);  // follows from postcondition of ComputeSCCs

       return repr.SccMembers.Count;

     }

-    

+

     /// <summary>

     /// This method sets the SccRepresentative fields of the graph's vertices so that two

     /// vertices have the same representative iff they are in the same strongly connected

@@ -197,7 +197,7 @@ namespace Microsoft.Dafny {
     void ComputeSCCs()

     {

       Contract.Ensures(sccComputed);

-    

+

       if (sccComputed) { return; }  // check if already computed

 

       // reset all SCC information

@@ -217,7 +217,7 @@ namespace Microsoft.Dafny {
 

       sccComputed = true;

     }

-    

+

     /// <summary>

     /// This is the 'SearchC' procedure from the Aho, Hopcroft, and Ullman book 'The Design and Analysis of Computer Algorithms'.

     /// </summary>

@@ -227,13 +227,13 @@ namespace Microsoft.Dafny {
      Contract.Requires(v.Visited == VisitedStatus.Unvisited);

      Contract.Requires(topologicallySortedRepresentatives != null);

       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);

-    

+

       v.DfNumber = cnt;

       cnt++;

       v.LowLink = v.DfNumber;

       stack.Push(v);

       v.Visited = VisitedStatus.OnStack;

-      

+

       foreach (Vertex w in v.Successors) {

         if (w.Visited == VisitedStatus.Unvisited) {

           SearchC(w, stack, ref cnt);

@@ -243,7 +243,7 @@ namespace Microsoft.Dafny {
           v.LowLink = Math.Min(v.LowLink, w.DfNumber);

         }

       }

-      

+

       if (v.LowLink == v.DfNumber) {

         // The SCC containing 'v' has now been computed.

         v.SccId = topologicallySortedRepresentatives.Count;

@@ -258,7 +258,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     /// <summary>

     /// Returns null if the graph has no cycles.  If the graph does contain some cycle, returns the list of

     /// vertices on one such cycle.

@@ -268,7 +268,7 @@ namespace Microsoft.Dafny {
       foreach (Vertex v in vertices.Values) {

         v.Visited = VisitedStatus.Unvisited;

       }

-      

+

       foreach (Vertex v in vertices.Values) {

         Contract.Assert(v.Visited != VisitedStatus.OnStack);

         if (v.Visited == VisitedStatus.Unvisited) {

@@ -284,7 +284,7 @@ namespace Microsoft.Dafny {
       }

       return null;  // there are no cycles

     }

-    

+

     /// <summary>

     /// A return of null means there are no cycles involving any vertex in the subtree rooted at v.

     /// A non-null return means a cycle has been found.  Then:

@@ -300,7 +300,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(v.Visited != VisitedStatus.Unvisited);

       Contract.Ensures(Contract.Result<List<Vertex>>() != null || v.Visited == VisitedStatus.Visited);

       Contract.Ensures(Contract.Result<List<Vertex>>() == null || Contract.Result<List<Vertex>>().Count != 0);

-    

+

       v.Visited = VisitedStatus.OnStack;

       foreach (Vertex succ in v.Successors) {

         // todo:  I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.

@@ -337,7 +337,7 @@ namespace Microsoft.Dafny {
       v.Visited = VisitedStatus.Visited;  // there are no cycles from here on

       return null;

     }

-    

+

     /// <summary>

     /// Returns whether or not 'source' reaches 'sink' in the graph.

     /// 'source' and 'sink' need not be in the graph; if neither is, the return value

@@ -352,7 +352,7 @@ namespace Microsoft.Dafny {
       generation++;

       return ReachSearch(a, b);

     }

-    

+

     bool ReachSearch(Vertex source, Vertex sink) {

       Contract.Requires(source != null);

       Contract.Requires(sink != null);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 4d84a5f5..cc97fb40 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -21,14 +21,14 @@ namespace Microsoft.Dafny {
         predef = FindPredefinedDecls(boogieProgram);

       }

     }

-    

+

     // translation state

     readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();

     readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();

 

     [ContractInvariantMethod]

-    void ObjectInvariant() 

+    void ObjectInvariant()

     {

       Contract.Invariant(cce.NonNullDictionaryAndValues(classes));

       Contract.Invariant(cce.NonNullDictionaryAndValues(fields));

@@ -81,7 +81,7 @@ namespace Microsoft.Dafny {
 

         return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

@@ -96,7 +96,7 @@ namespace Microsoft.Dafny {
         Contract.Ensures(Contract.Result<Bpl.Type>() != null);

         return new Bpl.CtorType(Token.NoToken, seqTypeCtor, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.Type FieldName(IToken tok, Bpl.Type ty) {

         Contract.Requires(tok != null);

         Contract.Requires(ty != null);

@@ -104,7 +104,7 @@ namespace Microsoft.Dafny {
 

         return new Bpl.CtorType(tok, fieldName, new Bpl.TypeSeq(ty));

       }

-      

+

       public Bpl.IdentifierExpr Alloc(IToken tok) {

         Contract.Requires(tok != null);

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

@@ -150,7 +150,7 @@ namespace Microsoft.Dafny {
         this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);

       }

     }

-    

+

     static PredefinedDecls FindPredefinedDecls(Bpl.Program prog) {

       Contract.Requires(prog != null);

       if (prog.Resolve() != 0) {

@@ -248,7 +248,7 @@ namespace Microsoft.Dafny {
       }

       return null;

     }

-    

+

     static Bpl.Program ReadPrelude() {

       string preludePath = Bpl.CommandLineOptions.Clo.DafnyPrelude;

       if (preludePath == null)

@@ -257,7 +257,7 @@ namespace Microsoft.Dafny {
           string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));

           preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl");

       }

-      

+

       Bpl.Program prelude;

       int errorCount = Bpl.Parser.Parse(preludePath, null, out prelude);

       if (prelude == null || errorCount > 0) {

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

         return prelude;

       }

-/*      

+/*

       List<string!> defines = new List<string!>();

       using (System.IO.Stream stream = new System.IO.FileStream(preludePath, System.IO.FileMode.Open, System.IO.FileAccess.Read))

       {

@@ -279,9 +279,9 @@ namespace Microsoft.Dafny {
           return prelude;

         }

       }

-*/      

+*/

     }

-    

+

     public Bpl.Program Translate(Program program) {

       Contract.Requires(program != null);

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

@@ -310,13 +310,13 @@ namespace Microsoft.Dafny {
       }

       return sink;

     }

-    

+

     void AddDatatype(DatatypeDecl dt)

     {

       Contract.Requires(dt != null);

       Contract.Requires(sink != null && predef != null);

       sink.TopLevelDeclarations.Add(GetClass(dt));

-    

+

       foreach (DatatypeCtor ctor in dt.Ctors) {

         // Add:  function #dt.ctor(paramTypes) returns (DatatypeType);

         Bpl.VariableSeq argTypes = new Bpl.VariableSeq();

@@ -376,7 +376,7 @@ namespace Microsoft.Dafny {
         fn.Body = Bpl.Expr.Eq(lhs, new Bpl.IdentifierExpr(ctor.tok, cid));  // this uses the "cid" defined for the previous axiom

         sink.TopLevelDeclarations.Add(fn);

 

-        // Add:  axiom (forall params, h: HeapType :: 

+        // Add:  axiom (forall params, h: HeapType ::

         //                 { DtAlloc(#dt.ctor(params), h) }

         //                 $IsGoodHeap(h) ==>

         //                     (DtAlloc(#dt.ctor(params), h) <==> ...each param has its expected type...));

@@ -482,7 +482,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)

     {

       Contract.Requires(formals != null);

@@ -501,13 +501,13 @@ namespace Microsoft.Dafny {
         args.Add(new Bpl.IdentifierExpr(arg.tok, bv));

       }

     }

-    

+

     void AddClassMembers(ClassDecl c)

     {

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(c != null);

       sink.TopLevelDeclarations.Add(GetClass(c));

-      

+

       foreach (MemberDecl member in c.Members) {

         if (member is Field) {

           Field f = (Field)member;

@@ -521,7 +521,7 @@ namespace Microsoft.Dafny {
           }

 

           AddAllocationAxiom(f);

-          

+

         } else if (member is Function) {

           Function f = (Function)member;

           AddFunction(f);

@@ -543,7 +543,7 @@ namespace Microsoft.Dafny {
           }

           AddFrameAxiom(f);

           AddWellformednessCheck(f);

-          

+

         } else if (member is Method) {

           Method m = (Method)member;

           // wellformedness check for method specification

@@ -557,14 +557,14 @@ namespace Microsoft.Dafny {
             // ...and its implementation

             AddMethodImpl(m, proc, false);

           }

-          

+

           // refinement condition

           if (member is MethodRefinement) {

             AddMethodRefinement((MethodRefinement)member);

           }

-        

+

         } else if (member is CouplingInvariant) {

-          // TODO: define a well-foundedness condition to check          

+          // TODO: define a well-foundedness condition to check

 

         } else {

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

@@ -659,9 +659,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));

       Contract.Requires(predef != null);

       Contract.Requires(f.EnclosingClass != null);

- 

+

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

-      

+

       // axiom

       //   mh < ModuleContextHeight ||

       //   (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext))

@@ -702,7 +702,7 @@ namespace Microsoft.Dafny {
       args.Add(new Bpl.IdentifierExpr(f.tok, bv));

       // ante:  $IsHeap($Heap) && this != null && formals-have-the-expected-types &&

       Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

-      

+

       Bpl.BoundVariable bvThis;

       Bpl.Expr bvThisIdExpr;

       if (f.IsStatic) {

@@ -754,7 +754,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Or(

             Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),

             etran.InMethodContext())));

-      

+

       var substMap = new Dictionary<IVariable, Expression>();

       if (specialization != null) {

         substMap = specialization.SubstMap;

@@ -813,7 +813,7 @@ namespace Microsoft.Dafny {
       }

       return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);

     }

-    

+

     void AddLimitedAxioms(Function f, int fromLayer) {

       Contract.Requires(f != null);

       Contract.Requires(f.IsRecursive && !f.IsUnlimited);

@@ -850,7 +850,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);

       Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));

       Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);

-      

+

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

 

       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));

@@ -876,7 +876,7 @@ namespace Microsoft.Dafny {
       }

       return name;

     }

-    

+

     /// <summary>

     /// Generate:

     ///   axiom (forall h: [ref, Field x]x, o: ref ::

@@ -887,13 +887,13 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

-    

+

       Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));

       Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);

       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));

       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);

-      

+

       // h[o,f]

       Bpl.Expr oDotF;

       if (f.IsMutable) {

@@ -937,7 +937,7 @@ namespace Microsoft.Dafny {
       }

       return Bpl.Expr.And(lower, upper);

     }

-    

+

     Method currentMethod = null;  // the method whose implementation is currently being translated

     int loopHeapVarCount = 0;

     int otherTmpVarCount = 0;

@@ -970,7 +970,7 @@ namespace Microsoft.Dafny {
 

       return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);

     }

-    

+

     Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals)  // local variable that's shared between statements that need it

     {

       Contract.Requires(tok != null);

@@ -1013,7 +1013,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(wellformednessProc || m.Body != null);

       Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);

       Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);

-    

+

       currentMethod = m;

 

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

@@ -1075,7 +1075,7 @@ namespace Microsoft.Dafny {
         typeParams, inParams, outParams,

         localVariables, stmts);

       sink.TopLevelDeclarations.Add(impl);

-      

+

       currentMethod = null;

       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

@@ -1090,7 +1090,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(localVariables != null);

       Contract.Requires(predef != null);

-    

+

       // set up the information used to verify the method's modifies clause

       DefineFrame(m.tok, m.Mod, builder, localVariables, null);

     }

@@ -1107,14 +1107,14 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Cmd>() != null);

       return CaptureState(tok, null);

     }

-    

+

     void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, Bpl.StmtListBuilder/*!*/ builder, Bpl.VariableSeq/*!*/ localVariables, string name){

       Contract.Requires(tok != null);

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

       Contract.Requires(builder != null);

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

       Contract.Requires(predef != null);

-    

+

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, tok);

       // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool

       Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type of the $_Frame variable

@@ -1131,7 +1131,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null);

       Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null,

                                            Bpl.Expr.Imp(ante, consequent));

-    

+

       builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));

     }

 

@@ -1162,7 +1162,7 @@ namespace Microsoft.Dafny {
                                       Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));

       builder.Add(Assert(tok, q, errorMessage, kv));

     }

-    

+

     /// <summary>

     /// Generates:

     ///   axiom (forall h0: HeapType, h1: HeapType, formals... ::

@@ -1184,18 +1184,18 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

-    

+

       Bpl.BoundVariable h0Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h0", predef.HeapType));

       Bpl.BoundVariable h1Var = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h1", predef.HeapType));

       Bpl.Expr h0 = new Bpl.IdentifierExpr(f.tok, h0Var);

       Bpl.Expr h1 = new Bpl.IdentifierExpr(f.tok, h1Var);

       ExpressionTranslator etran0 = new ExpressionTranslator(this, predef, h0);

       ExpressionTranslator etran1 = new ExpressionTranslator(this, predef, h1);

-      

+

       Bpl.Expr wellFormed = Bpl.Expr.And(

         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr),

         FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr));

-      

+

       Bpl.TypeVariable alpha = new Bpl.TypeVariable(f.tok, "alpha");

       Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$o", predef.RefType));

       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);

@@ -1204,12 +1204,12 @@ namespace Microsoft.Dafny {
       Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null);

       Bpl.Expr oNotNullAlloced = Bpl.Expr.And(oNotNull, Bpl.Expr.And(etran0.IsAlloced(f.tok, o), etran1.IsAlloced(f.tok, o)));

       Bpl.Expr unchanged = Bpl.Expr.Eq(ExpressionTranslator.ReadHeap(f.tok, h0, o, field), ExpressionTranslator.ReadHeap(f.tok, h1, o, field));

-      

+

       Bpl.Expr heapSucc = FunctionCall(f.tok, BuiltinFunction.HeapSucc, null, h0, h1);

       Bpl.Expr r0 = InRWClause(f.tok, o, field, f.Reads, etran0, null, null);

       Bpl.Expr q0 = new Bpl.ForallExpr(f.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fieldVar),

         Bpl.Expr.Imp(Bpl.Expr.And(oNotNullAlloced, r0), unchanged));

-      

+

       // bvars:  h0, h1, formals

       // f0args:  h0, formals

       // f1args:  h1, formals

@@ -1243,7 +1243,7 @@ namespace Microsoft.Dafny {
         wh = GetWhereClause(p.tok, formal, p.Type, etran1);

         if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }

       }

-      

+

       string axiomComment = "frame axiom for " + f.FullName;

       Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

       while (fn != null) {

@@ -1251,7 +1251,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);

         Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);

         Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(heapSucc, F1));

-        

+

         Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

         Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, bvars, null, tr,

           Bpl.Expr.Imp(Bpl.Expr.And(wellFormed, heapSucc),

@@ -1265,7 +1265,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List<FrameExpression/*!*/>/*!*/ rw, ExpressionTranslator/*!*/ etran,

                              Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap) {

       Contract.Requires(tok != null);

@@ -1280,7 +1280,7 @@ namespace Microsoft.Dafny {
 

       // requires o to denote an expression of type RefType

       // "rw" is is allowed to contain a WildcardExpr

-    

+

       Bpl.Expr disjunction = null;

       foreach (FrameExpression rwComponent in rw) {

         Expression e = rwComponent.E;

@@ -1323,12 +1323,12 @@ namespace Microsoft.Dafny {
         return disjunction;

       }

     }

-    

+

     void AddWellformednessCheck(Function f) {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(f.EnclosingClass != null);

-    

+

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

       // parameters of the procedure

       Bpl.VariableSeq inParams = new Bpl.VariableSeq();

@@ -1360,7 +1360,7 @@ namespace Microsoft.Dafny {
       VariableSeq implInParams = Bpl.Formal.StripWhereClauses(proc.InParams);

       Bpl.VariableSeq locals = new Bpl.VariableSeq();

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

-      

+

       // check well-formedness of the preconditions (including termination, but no reads checks), and then

       // assume each one of them

       foreach (Expression p in f.Req) {

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

       Contract.Requires(predef != null);

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

-    

+

       if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {

         return Bpl.Expr.True;

       } else if (expr is DisplayExpression) {

@@ -1632,7 +1632,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

     }

-    

+

     Bpl.Expr/*!*/ IsTotal(List<Expression/*!*/>/*!*/ exprs, ExpressionTranslator/*!*/ etran) {

       Contract.Requires(etran != null);

       Contract.Requires(exprs != null);

@@ -1795,7 +1795,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.And(a, b);

       }

     }

-    

+

     Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -1807,14 +1807,14 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Imp(a, b);

       }

     }

-    

+

     void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {

       Contract.Requires(tok != null);

       Contract.Requires(e != null);

       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

-    

+

       if (e is ThisExpr) {

         // already known to be non-null

       } else {

@@ -1889,7 +1889,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

-    

+

       if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) {

         // always allowed

       } else if (expr is DisplayExpression) {

@@ -2136,7 +2136,7 @@ namespace Microsoft.Dafny {
         CheckWellformed(e.Thn, options, locals, bThen, etran);

         CheckWellformed(e.Els, options, locals, bElse, etran);

         builder.Add(new Bpl.IfCmd(expr.tok, etran.TrExpr(e.Test), bThen.Collect(expr.tok), null, bElse.Collect(expr.tok)));

-      

+

       } else if (expr is MatchExpr) {

         MatchExpr me = (MatchExpr)expr;

         CheckWellformed(me.Source, options, locals, builder, etran);

@@ -2360,7 +2360,7 @@ namespace Microsoft.Dafny {
         return s;

       }

     }

-    

+

     Bpl.Constant GetClass(TopLevelDecl cl)

     {

       Contract.Requires(cl != null);

@@ -2376,7 +2376,7 @@ namespace Microsoft.Dafny {
       }

       return cc;

     }

-    

+

     Bpl.Expr GetTypeExpr(IToken tok, Type type)

     {

       Contract.Requires(tok != null);

@@ -2425,13 +2425,13 @@ namespace Microsoft.Dafny {
         return t;

       }

     }

-    

+

     Bpl.Constant GetField(Field f)

     {

       Contract.Requires(f != null && f.IsMutable);

       Contract.Requires(sink != null && predef != null);

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

-     

+

       Bpl.Constant fc;

       if (fields.TryGetValue(f, out fc)) {

         Contract.Assert(fc != null);

@@ -2490,13 +2490,13 @@ namespace Microsoft.Dafny {
       Contract.Requires(fse != null);

       Contract.Requires(fse.Field != null && fse.Field.IsMutable);

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

-     

+

       return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));

     }

 

     /// <summary>

     /// This method is expected to be called just once for each function in the program.

-    /// </summary>    

+    /// </summary>

     void AddFunction(Function f)

     {

       Contract.Requires(f != null);

@@ -2513,7 +2513,7 @@ namespace Microsoft.Dafny {
       Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);

       Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);

       sink.TopLevelDeclarations.Add(func);

-      

+

       if (f.IsRecursive && !f.IsUnlimited) {

         sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));

         sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));

@@ -2523,12 +2523,12 @@ namespace Microsoft.Dafny {
       Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);

       sink.TopLevelDeclarations.Add(canCallF);

     }

-    

+

     /// <summary>

     /// This method is expected to be called just twice for each procedure in the program (once with

     /// wellformednessProc set to true, once with wellformednessProc set to false).

     /// In addition, it is used once to generate refinement conditions.

-    /// </summary>    

+    /// </summary>

     Bpl.Procedure AddMethod(Method m, bool wellformednessProc, bool skipEnsures)

     {

       Contract.Requires(m != null);

@@ -2538,7 +2538,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Procedure>() != null);

 

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);

-      

+

       Bpl.VariableSeq inParams = new Bpl.VariableSeq();

       Bpl.VariableSeq outParams = new Bpl.VariableSeq();

       if (!m.IsStatic) {

@@ -2558,7 +2558,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

         outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));

       }

-      

+

       Bpl.RequiresSeq req = new Bpl.RequiresSeq();

       Bpl.IdentifierExprSeq mod = new Bpl.IdentifierExprSeq();

       Bpl.EnsuresSeq ens = new Bpl.EnsuresSeq();

@@ -2569,7 +2569,7 @@ namespace Microsoft.Dafny {
       req.Add(Requires(m.tok, true, context, null, null));

       mod.Add(etran.HeapExpr);

       mod.Add(etran.Tick());

-      

+

       if (!wellformednessProc) {

         string comment = "user-defined preconditions";

         foreach (MaybeFreeExpression p in m.Req) {

@@ -2607,54 +2607,54 @@ namespace Microsoft.Dafny {
       return proc;

     }

 

-    #region Refinement extension    

-    

-    void AddMethodRefinement(MethodRefinement m) 

+    #region Refinement extension

+

+    void AddMethodRefinement(MethodRefinement m)

      {

       Contract.Requires(m != null);

       Contract.Requires(sink != null && predef != null);

-      // r is abstract, m is concrete 

+      // r is abstract, m is concrete

       Method r = m.Refined;

       Contract.Assert(r != null);

       Contract.Assert(m.EnclosingClass != null);

       string name = "Refinement$$" + m.FullName;

       string that = "that";

-      

+

       Bpl.IdentifierExpr heap = new Bpl.IdentifierExpr(m.tok, predef.HeapVarName, predef.HeapType);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, heap, that);

-      

+

       // TODO: this straight inlining does not handle recursive calls

-      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames      

-            

+      // TODO: we assume frame allows anything to be changed -- we don't include post-conditions in the refinement procedure, or check refinement of frames

+

       // generate procedure declaration with pre-condition wp(r, true)

       Bpl.Procedure proc = AddMethod(r, false, true);

       proc.Name = name;

-      

+

       // create "that" for m

       Bpl.Expr wh = Bpl.Expr.And(

         Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, that, predef.RefType), predef.Null),

         etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, that, predef.RefType), Resolver.GetReceiverType(m.tok, m)));

       Bpl.Formal thatVar = new Bpl.Formal(m.tok, new Bpl.TypedIdent(m.tok, that, predef.RefType, wh), true);

       proc.InParams.Add(thatVar);

-      

-      // add outs of m to the outs of the refinement procedure   

+

+      // add outs of m to the outs of the refinement procedure

       foreach (Formal p in m.Outs) {

         Bpl.Type varType = TrType(p.Type);

         Bpl.Expr w = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.UniqueName, varType), p.Type, etran);

         proc.OutParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, w), false));

       }

       sink.TopLevelDeclarations.Add(proc);

-           

-      // generate procedure implementation:      

+

+      // generate procedure implementation:

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

       Bpl.VariableSeq inParams = Bpl.Formal.StripWhereClauses(proc.InParams);

       Bpl.VariableSeq outParams = Bpl.Formal.StripWhereClauses(proc.OutParams);

       Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

       Bpl.VariableSeq localVariables = new Bpl.VariableSeq();

-      

+

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

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

-      

+

       // declare a frame variable that allows anything to be changed (not checking modifies clauses)

       Bpl.IdentifierExpr theFrame = etran.TheFrame(m.tok);

       Contract.Assert(theFrame.Type != null);

@@ -2666,12 +2666,12 @@ namespace Microsoft.Dafny {
       Bpl.BoundVariable fVar = new Bpl.BoundVariable(m.tok, new Bpl.TypedIdent(m.tok, "$f", predef.FieldName(m.tok, alpha)));

       Bpl.Expr lambda = new Bpl.LambdaExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, Bpl.Expr.True);

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, frame), lambda));

-      

-      // assume I($Heap, $Heap)              

+

+      // assume I($Heap, $Heap)

       builder.Add(new Bpl.AssumeCmd(m.tok, TrCouplingInvariant(m, heap, "this", heap, that)));

-      

+

       // assign input formals of m (except "this")

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

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

         Bpl.LocalVariable arg = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, m.Ins[i].UniqueName, TrType(m.Ins[i].Type)));

         localVariables.Add(arg);

         Bpl.Variable var = inParams[i+1];

@@ -2684,7 +2684,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

       _tmpIEs.Clear();

-            

+

       //  call inlined m;

       TrStmt(m.Body, builder, localVariables, etran);

 

@@ -2692,10 +2692,10 @@ namespace Microsoft.Dafny {
       Bpl.LocalVariable heap2 = new Bpl.LocalVariable(m.tok, new Bpl.TypedIdent(m.tok, heap.Name+"2", predef.HeapType));

       localVariables.Add(heap2);

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, heap2), etran.HeapExpr));

-      

+

       //  $Heap := old($Heap);

       builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.OldExpr(m.tok, heap)));

-                                

+

       //  call inlined r;

       currentMethod = r;

       etran = new ExpressionTranslator(this, predef, heap);

@@ -2706,7 +2706,7 @@ namespace Microsoft.Dafny {
       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

       _tmpIEs.Clear();

-      

+

       // assert output variables of r and m are pairwise equal

       Contract.Assert(outParams.Length % 2 == 0);

       int k = outParams.Length / 2;

@@ -2714,21 +2714,21 @@ namespace Microsoft.Dafny {
         Bpl.Variable rOut = outParams[i];

         Bpl.Variable mOut = outParams[i+k];

         Contract.Assert(rOut != null && mOut != null);

-        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)), 

+        builder.Add(Assert(m.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(m.tok, mOut), new Bpl.IdentifierExpr(m.tok, rOut)),

           "Refinement method may not produce the same value for output variable " + m.Outs[i].Name));

       }

-            

-      // assert I($Heap1, $Heap)      

+

+      // assert I($Heap1, $Heap)

       builder.Add(Assert(m.tok, TrCouplingInvariant(m, heap, "this", new Bpl.IdentifierExpr(m.tok, heap2), that),

         "Refinement method may not preserve the coupling invariant"));

-                                                

+

       Bpl.StmtList stmts = builder.Collect(m.tok);

       Bpl.Implementation impl = new Bpl.Implementation(m.tok, proc.Name,

         typeParams, inParams, outParams,

         localVariables, stmts);

       sink.TopLevelDeclarations.Add(impl);

     }

-    

+

     private sealed class NominalSubstituter : Duplicator

     {

       private readonly Dictionary<string,Bpl.Expr> subst;

@@ -2742,7 +2742,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(cce.NonNullDictionaryAndValues(subst));

       }

 

-          

+

       public override Expr VisitIdentifierExpr(Bpl.IdentifierExpr node)

       {

         Contract.Requires(node != null);

@@ -2750,7 +2750,7 @@ namespace Microsoft.Dafny {
 

         if (subst.ContainsKey(node.Name))

           return subst[node.Name];

-        else 

+        else

           return base.VisitIdentifierExpr(node);

       }

     }

@@ -2767,32 +2767,32 @@ namespace Microsoft.Dafny {
       ClassRefinementDecl c = m.EnclosingClass as ClassRefinementDecl;

       Contract.Assert(c != null);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, conHeap, conThis);

-            

-      foreach (MemberDecl d in c.Members) 

+

+      foreach (MemberDecl d in c.Members)

         if (d is CouplingInvariant) {

           CouplingInvariant inv = (CouplingInvariant)d;

 

           Contract.Assert(inv.Refined != null);

           Contract.Assert(inv.Formals != null);

-          

-          // replace formals with field dereferences                    

+

+          // replace formals with field dereferences

           Dictionary<string,Bpl.Expr> map = new Dictionary<string,Bpl.Expr>();

           Bpl.Expr absVar = new Bpl.IdentifierExpr(d.tok, absThis, predef.RefType);

-          for (int i = 0; i < inv.Refined.Count; i++) {     

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

             // TODO: boxing/unboxing?

             Bpl.Expr result = ExpressionTranslator.ReadHeap(inv.Toks[i], absHeap, absVar, new Bpl.IdentifierExpr(inv.Toks[i], GetField(cce.NonNull(inv.Refined[i]))));

             map.Add(inv.Formals[i].UniqueName, result);

           }

-                              

+

           Bpl.Expr e = new NominalSubstituter(map).VisitExpr(etran.TrExpr(inv.Expr));

           cond = Bpl.Expr.And(cond, e);

         }

-            

+

       return cond;

     }

-    

+

     #endregion

-    

+

     class BoilerplateTriple {  // a triple that is now a quintuple

       [ContractInvariantMethod]

       void ObjectInvariant() {

@@ -2820,7 +2820,7 @@ namespace Microsoft.Dafny {
         Comment = comment;

       }

     }

-    

+

     /// <summary>

     /// There are 3 states of interest when generating two-state boilerplate:

     ///  S0. the beginning of the method or loop, which is where the modifies clause is interpreted

@@ -2837,17 +2837,17 @@ namespace Microsoft.Dafny {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));

 

       List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();

-      

+

       // the frame condition, which is free since it is checked with every heap update and call

       boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));

 

       // HeapSucc(S1, S2)

       Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);

       boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));

-      

+

       return boilerplate;

     }

-    

+

     /// <summary>

     /// There are 3 states of interest when generating a frame condition:

     ///  S0. the beginning of the method/loop, which is where the modifies clause is interpreted

@@ -2879,9 +2879,9 @@ namespace Microsoft.Dafny {
       Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);

       Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));

       Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);

-      

+

       consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));

-      

+

       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

     }

@@ -2913,15 +2913,15 @@ namespace Microsoft.Dafny {
 

       Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

-    }    

+    }

     // ----- Type ---------------------------------------------------------------------------------

-    

+

     Bpl.Type TrType(Type type)

      {

       Contract.Requires(type != null);

       Contract.Requires(predef != null);

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

-     

+

       while (true) {

         TypeProxy tp = type as TypeProxy;

         if (tp == null) {

@@ -2933,7 +2933,7 @@ namespace Microsoft.Dafny {
           type = tp.T;

         }

       }

-      

+

       if (type is BoolType) {

         return Bpl.Type.Bool;

       } else if (type is IntType) {

@@ -2955,7 +2955,7 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

     }

-    

+

     Bpl.TypeVariableSeq TrTypeParamDecls(List<TypeParameter/*!*/>/*!*/ tps)

     {

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

@@ -2966,7 +2966,7 @@ namespace Microsoft.Dafny {
     }

 

     // ----- Statement ----------------------------------------------------------------------------

-    

+

     Bpl.AssertCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage)

     {

       Contract.Requires(tok != null);

@@ -3036,10 +3036,10 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

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

-     

+

       return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);

     }

-    

+

     Bpl.StmtList TrStmt2StmtList(Bpl.StmtListBuilder builder, Statement block, Bpl.VariableSeq locals, ExpressionTranslator etran)

      {

       Contract.Requires(builder != null);

@@ -3048,11 +3048,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(currentMethod != null && predef != null);

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

-      

+

       TrStmt(block, builder, locals, etran);

       return builder.Collect(block.Tok);  // TODO: would be nice to have an end-curly location for "block"

     }

-    

+

     void TrStmt(Statement stmt, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran)

     {

       Contract.Requires(stmt != null);

@@ -3093,7 +3093,7 @@ namespace Microsoft.Dafny {
             TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);

           }

         }

-         

+

       } else if (stmt is BreakStmt) {

         AddComment(builder, stmt, "break statement");

         var s = (BreakStmt)stmt;

@@ -3316,7 +3316,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);

           builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined"));  // totality check

         }

-        

+

         // Here comes:  assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);

         Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));

         Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);

@@ -3350,14 +3350,14 @@ namespace Microsoft.Dafny {
           qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);

           builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));

         }

-        

+

         builder.Add(CaptureState(stmt.Tok));

-        

+

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);

         Bpl.Expr source = etran.TrExpr(s.Source);

-        

+

         var b = new Bpl.StmtListBuilder();

         b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));

         Bpl.StmtList els = b.Collect(stmt.Tok);

@@ -3512,7 +3512,7 @@ namespace Microsoft.Dafny {
       }

       // add a free invariant which says that the heap hasn't changed outside of the modifies clause.

       invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));

-      

+

       // include a free invariant that says that all completed iterations so far have only decreased the termination metric

       if (initDecr != null) {

         List<IToken> toks = new List<IToken>();

@@ -3669,7 +3669,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

-      

+

       Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver);

       Bpl.ExprSeq ins = new Bpl.ExprSeq();

       if (!method.IsStatic) {

@@ -3754,7 +3754,7 @@ namespace Microsoft.Dafny {
         }

       }

     }

-    

+

     static Expression CreateIntLiteral(IToken tok, int n)

     {

       Contract.Requires(tok != null);

@@ -3768,13 +3768,13 @@ namespace Microsoft.Dafny {
         return CreateIntSub(tok, CreateIntLiteral(tok, 0), CreateIntLiteral(tok, -n));

       }

     }

-    

+

     static Expression CreateIntSub(IToken tok, Expression e0, Expression e1)

      {

       Contract.Requires(tok != null);

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

-      

+

 

       Contract.Requires(e0.Type is IntType && e1.Type is IntType);

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

@@ -3783,7 +3783,7 @@ namespace Microsoft.Dafny {
       s.Type = Type.Int;  // resolve here

       return s;

     }

-    

+

     static Expression CreateIntITE(IToken tok, Expression test, Expression e0, Expression e1)

      {

       Contract.Requires(tok != null);

@@ -3797,7 +3797,7 @@ namespace Microsoft.Dafny {
       ite.Type = Type.Int;  // resolve here

       return ite;

     }

-    

+

     public IEnumerable<Expression> Conjuncts(Expression expr)

      {

       Contract.Requires(expr != null);

@@ -3835,7 +3835,7 @@ namespace Microsoft.Dafny {
         // record value of each decreases expression at beginning of the loop iteration

         Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(e.tok, bf, etran.TrExpr(e));

         builder.Add(cmd);

-        

+

         c++;

       }

       return oldBfs;

@@ -3887,7 +3887,7 @@ namespace Microsoft.Dafny {
       }

       builder.Add(Assert(tok, decrExpr, inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"));

     }

-    

+

     /// <summary>

     /// Returns the expression that says whether or not the decreases function has gone down (if !allowNoChange)

     /// or has gone down or stayed the same (if allowNoChange).

@@ -3908,7 +3908,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

 

       int N = types.Count;

-      

+

       // compute eq and less for each component of the lexicographic pair

       List<Bpl.Expr> Eq = new List<Bpl.Expr>(N);

       List<Bpl.Expr> Less = new List<Bpl.Expr>(N);

@@ -3975,7 +3975,7 @@ namespace Microsoft.Dafny {
         return false;  // don't consider any type parameters to be the same (since we have no comparison function for them anyway)

       }

     }

-    

+

     void ComputeLessEq(IToken/*!*/ tok, Type/*!*/ ty, Bpl.Expr/*!*/ e0, Bpl.Expr/*!*/ e1, out Bpl.Expr/*!*/ less, out Bpl.Expr/*!*/ atmost, out Bpl.Expr/*!*/ eq,

                        ExpressionTranslator/*!*/ etran, bool includeLowerBound)

      {

@@ -3988,7 +3988,7 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.ValueAtReturn(out less)!=null);

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

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

-     

+

       if (ty is BoolType) {

         eq = Bpl.Expr.Iff(e0, e1);

         less = Bpl.Expr.And(Bpl.Expr.Not(e0), e1);

@@ -4017,7 +4017,7 @@ namespace Microsoft.Dafny {
         eq = Bpl.Expr.Eq(b0, b1);

         less = Bpl.Expr.Lt(b0, b1);

         atmost = Bpl.Expr.Le(b0, b1);

-        

+

       } else {

         // reference type

         Bpl.Expr b0 = Bpl.Expr.Neq(e0, predef.Null);

@@ -4027,14 +4027,14 @@ namespace Microsoft.Dafny {
         atmost = Bpl.Expr.Imp(b0, b1);

       }

     }

-    

+

     void AddComment(Bpl.StmtListBuilder builder, Statement stmt, string comment) {

       Contract.Requires(builder != null);

       Contract.Requires(stmt != null);

       Contract.Requires(comment != null);

       builder.Add(new Bpl.CommentCmd(string.Format("----- {0} ----- {1}({2},{3})", comment, stmt.Tok.filename, stmt.Tok.line, stmt.Tok.col)));

-    }    

-    

+    }

+

     Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran)

     {

       Contract.Requires(tok != null);

@@ -4063,7 +4063,7 @@ namespace Microsoft.Dafny {
 

       } else  if (type is BoolType || type is IntType) {

         // nothing todo

-      

+

       } else if (type is SetType) {

         SetType st = (SetType)type;

         // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t)-has-the-expected-type)

@@ -4131,7 +4131,7 @@ namespace Microsoft.Dafny {
 

       } else if (type.IsTypeParameter) {

         return FunctionCall(tok, BuiltinFunction.GenericAlloc, null, x, etran.HeapExpr);

-        

+

       } else {

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

       }

@@ -4322,7 +4322,7 @@ namespace Microsoft.Dafny {
 

           var obj = SaveInTemp(etran.TrExpr(mse.Array), rhsCanAffectPreviouslyKnownExpressions,

             "$obj" + i, predef.RefType, builder, locals);

-          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions, 

+          var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions,

             "$index" + i, predef.FieldName(mse.tok, predef.BoxType), builder, locals);

           prevObj[i] = obj;

           prevIndex[i] = fieldName;

@@ -4512,7 +4512,7 @@ namespace Microsoft.Dafny {
       readonly int layerOffset = 0;

       public int Statistics_FunctionCount = 0;

       [ContractInvariantMethod]

-      void ObjectInvariant() 

+      void ObjectInvariant()

       {

         Contract.Invariant(HeapExpr != null);

         Contract.Invariant(predef != null);

@@ -4531,7 +4531,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);

         this.This = "this";

       }

-      

+

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

@@ -4541,7 +4541,7 @@ namespace Microsoft.Dafny {
         this.HeapExpr = heap;

         this.This = "this";

       }

-      

+

       public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) {

         Contract.Requires(translator != null);

         Contract.Requires(predef != null);

@@ -4599,7 +4599,7 @@ namespace Microsoft.Dafny {
           return HeapExpr is Bpl.OldExpr;

         }

       }

-      

+

       public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction) {

         Contract.Requires(applyLimited_CurrentFunction != null);

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

@@ -4674,10 +4674,10 @@ namespace Microsoft.Dafny {
           } else {

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

           }

-          

+

         } else if (expr is ThisExpr) {

           return new Bpl.IdentifierExpr(expr.tok, This, predef.RefType);

-        

+

         } else if (expr is IdentifierExpr) {

           IdentifierExpr e = (IdentifierExpr)expr;

           return TrVar(expr.tok, cce.NonNull(e.Var));

@@ -4714,7 +4714,7 @@ namespace Microsoft.Dafny {
             i++;

           }

           return s;

-        

+

         } else if (expr is FieldSelectExpr) {

           FieldSelectExpr e = (FieldSelectExpr)expr;

           Contract.Assert(e.Field != null);

@@ -4766,7 +4766,7 @@ namespace Microsoft.Dafny {
             // if e0 == null && e1 == null, then we have the identity operation seq[..] == seq;

             return seq;

           }

-        

+

         } else if (expr is SeqUpdateExpr) {

           SeqUpdateExpr e = (SeqUpdateExpr)expr;

           Bpl.Expr seq = TrExpr(e.Seq);

@@ -4804,7 +4804,7 @@ namespace Microsoft.Dafny {
           Bpl.ExprSeq args = FunctionInvocationArguments(e);

           Bpl.Expr result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(id), args);

           return CondApplyUnbox(expr.tok, result, e.Function.ResultType, expr.Type);

-        

+

         } else if (expr is DatatypeValue) {

           DatatypeValue dtv = (DatatypeValue)expr;

           Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

@@ -4890,7 +4890,7 @@ namespace Microsoft.Dafny {
             default:

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

           }

-        

+

         } else if (expr is BinaryExpr) {

           BinaryExpr e = (BinaryExpr)expr;

           Bpl.Expr e0 = TrExpr(e.E0);

@@ -4916,12 +4916,12 @@ namespace Microsoft.Dafny {
               bOpcode = BinaryOperator.Opcode.And; break;

             case BinaryExpr.ResolvedOpcode.Or:

               bOpcode = BinaryOperator.Opcode.Or; break;

-              

+

             case BinaryExpr.ResolvedOpcode.EqCommon:

               bOpcode = BinaryOperator.Opcode.Eq; break;

             case BinaryExpr.ResolvedOpcode.NeqCommon:

               bOpcode = BinaryOperator.Opcode.Neq; break;

-              

+

             case BinaryExpr.ResolvedOpcode.Lt:

               bOpcode = BinaryOperator.Opcode.Lt; break;

             case BinaryExpr.ResolvedOpcode.Le:

@@ -5031,12 +5031,12 @@ namespace Microsoft.Dafny {
               return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Gt,

                 translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e0),

                 translator.FunctionCall(expr.tok, BuiltinFunction.DtRank, null, e1));

-              

+

             default:

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

           }

           return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);

-        

+

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

@@ -5055,7 +5055,7 @@ namespace Microsoft.Dafny {
             antecedent = Bpl.Expr.And(antecedent, TrExpr(e.Range));

           }

           Bpl.Expr body = TrExpr(e.Term);

-          

+

           if (e is ForallExpr) {

             return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(antecedent, body));

           } else {

@@ -5094,11 +5094,11 @@ namespace Microsoft.Dafny {
         } else if (expr is BoxingCastExpr) {

           BoxingCastExpr e = (BoxingCastExpr)expr;

           return CondApplyBox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

-          

+

         } else if (expr is UnboxingCastExpr) {

           UnboxingCastExpr e = (UnboxingCastExpr)expr;

           return CondApplyUnbox(e.tok, TrExpr(e.E), e.FromType, e.ToType);

-          

+

         } else {

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

         }

@@ -5107,7 +5107,7 @@ namespace Microsoft.Dafny {
       public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {

         Contract.Requires(boundVars != null);

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

-        

+

         Bpl.Expr typeAntecedent = Bpl.Expr.True;

         foreach (BoundVar bv in boundVars) {

           Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));

@@ -5186,7 +5186,7 @@ namespace Microsoft.Dafny {
           return e;

         }

       }

-      

+

       public Bpl.Expr BoxIfNecessary(IToken tok, Bpl.Expr e, Type fromType) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5195,7 +5195,7 @@ namespace Microsoft.Dafny {
 

         return CondApplyBox(tok, e, fromType, null);

       }

-      

+

       public Bpl.Expr CondApplyUnbox(IToken tok, Bpl.Expr e, Type fromType, Type toType) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5209,7 +5209,7 @@ namespace Microsoft.Dafny {
           return e;

         }

       }

-      

+

       public static bool ModeledAsBoxType(Type t) {

         Contract.Requires(t != null);

         while (true) {

@@ -5371,7 +5371,7 @@ namespace Microsoft.Dafny {
         }

         return kv;

       }

-      

+

       // --------------- help routines ---------------

 

       public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e) {

@@ -5381,7 +5381,7 @@ namespace Microsoft.Dafny {
 

         return IsAlloced(tok, e, HeapExpr);

       }

-          

+

       Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5390,7 +5390,7 @@ namespace Microsoft.Dafny {
 

         return ReadHeap(tok, heap, e, predef.Alloc(tok));

       }

-      

+

       public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

@@ -5405,7 +5405,7 @@ namespace Microsoft.Dafny {
           return IsAlloced(tok, e);

         }

       }

-      

+

       public Bpl.Expr GoodRef_Class(IToken tok, Bpl.Expr e, UserDefinedType type, bool isNew)

        {

         Contract.Requires(tok != null);

@@ -5427,12 +5427,12 @@ namespace Microsoft.Dafny {
         if (isNew) {

           r = Bpl.Expr.Not(r);  // use the conjunct:  !Heap[e, alloc]

         }

-        

+

         // dtype(e) == C

         Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);

         Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);

         r = r == null ? dtype : Bpl.Expr.And(r, dtype);

-        

+

         // TypeParams(e, #) == T

         int n = 0;

         foreach (Type arg in typeArgs) {

@@ -5443,7 +5443,7 @@ namespace Microsoft.Dafny {
           }

           n++;

         }

-        

+

         return r;

       }

 

@@ -5471,7 +5471,7 @@ namespace Microsoft.Dafny {
         return r;

       }

     }

-    

+

     enum BuiltinFunction {

       SetEmpty,

       SetUnionOne,

@@ -5507,17 +5507,17 @@ namespace Microsoft.Dafny {
       SeqEqual,

       SeqSameUntil,

       SeqFromArray,

-      

+

       IndexField,

       MultiIndexField,

-      

+

       Box,

       Unbox,

       IsCanonicalBoolBox,

 

       IsGoodHeap,

       HeapSucc,

-      

+

       DynamicType,  // allocated type (of object reference)

       DtType,       // type of datatype value

       TypeParams,   // type parameters of allocated type

@@ -5532,7 +5532,7 @@ namespace Microsoft.Dafny {
 

       GenericAlloc,

     }

-    

+

     // The "typeInstantiation" argument is passed in to help construct the result type of the function.

     Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)

     {

@@ -5684,7 +5684,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation != null);

           return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);

-          

+

         case BuiltinFunction.IndexField:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

@@ -5767,7 +5767,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected built-in function

       }

     }

-    

+

     Bpl.NAryExpr FunctionCall(IToken tok, string function, Bpl.Type returnType, params Bpl.Expr[] args)

     {

       Contract.Requires(tok != null);

@@ -6238,7 +6238,7 @@ namespace Microsoft.Dafny {
         for (int i = 0; i < dt.TypeArgs.Count; i++) {

           subst.Add(dt.TypeArgs[i], instantiatedType.TypeArgs[i]);

         }

-        

+

         foreach (DatatypeCtor ctor in dt.Ctors) {

           Bpl.VariableSeq bvs;

           List<Bpl.Expr> args;

@@ -6293,7 +6293,7 @@ namespace Microsoft.Dafny {
             newExpr = new SeqDisplayExpr(expr.tok, newElements);

           }

         }

-        

+

       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr fse = (FieldSelectExpr)expr;

         Expression substE = Substitute(fse.Obj, receiverReplacement, substMap);

@@ -6302,7 +6302,7 @@ namespace Microsoft.Dafny {
           fseNew.Field = fse.Field;  // resolve on the fly (and fseExpr.Type is set at end of method)

           newExpr = fseNew;

         }

-        

+

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr sse = (SeqSelectExpr)expr;

         Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);

@@ -6311,7 +6311,7 @@ namespace Microsoft.Dafny {
         if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {

           newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

         }

-        

+

       } else if (expr is SeqUpdateExpr) {

         SeqUpdateExpr sse = (SeqUpdateExpr)expr;

         Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);

@@ -6338,7 +6338,7 @@ namespace Microsoft.Dafny {
           newFce.Function = e.Function;  // resolve on the fly (and set newFce.Type below, at end)

           newExpr = newFce;

         }

-      

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         List<Expression> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);

@@ -6381,7 +6381,7 @@ namespace Microsoft.Dafny {
           newBin.ResolvedOp = e.ResolvedOp;  // part of what needs to be done to resolve on the fly (newBin.Type is set below, at end)

           newExpr = newBin;

         }

-        

+

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

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

           Contract.Assume(false);  // unexpected ComprehensionExpr

         }

-        

+

       } else if (expr is ITEExpr) {

         ITEExpr e = (ITEExpr)expr;

         Expression test = Substitute(e.Test, receiverReplacement, substMap);

@@ -6418,7 +6418,7 @@ namespace Microsoft.Dafny {
         var e = (ConcreteSyntaxExpression)expr;

         return Substitute(e.ResolvedExpression, receiverReplacement, substMap);

       }

-      

+

       if (newExpr == null) {

         return expr;

       } else {

@@ -6426,18 +6426,18 @@ namespace Microsoft.Dafny {
         return newExpr;

       }

     }

-    

+

     static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

                                                  Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

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

       Contract.Requires((receiverReplacement == null) == (substMap == null));

       Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

-      

+

       List<Expression> newElist = null;  // initialized lazily

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

       {cce.LoopInvariant(  newElist == null || newElist.Count == i);

-      

+

         Expression substE = Substitute(elist[i], receiverReplacement, substMap);

         if (substE != elist[i] && newElist == null) {

           newElist = new List<Expression>();

@@ -6455,7 +6455,7 @@ namespace Microsoft.Dafny {
         return newElist;

       }

     }

-    

+

     static Triggers SubstTriggers(Triggers trigs, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

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

       if (trigs != null) {

@@ -6487,7 +6487,7 @@ namespace Microsoft.Dafny {
         if (!anyArgSubst) {

           newArgs = attrs.Args;

         }

-        

+

         Attributes prev = SubstAttributes(attrs.Prev, receiverReplacement, substMap);

         if (newArgs != attrs.Args || prev != attrs.Prev) {

           return new Attributes(attrs.Name, newArgs, prev);

@@ -6495,6 +6495,6 @@ namespace Microsoft.Dafny {
       }

       return attrs;

     }

-        

+

   }

-}
\ No newline at end of file
+}