Merge

14 files changed, 2066 insertions, 914 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index e7633014..ff1a0eb1 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -45,7 +45,7 @@ namespace Microsoft.Boogie {
     public static string/*!*/ VersionSuffix {

       get {

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

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

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

       }

     }

     public string/*!*/ Version {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7d49fb8f..78e7675e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -182,7 +182,7 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl
     { Attribute<ref attrs> }

     NoUSIdent<out id>                          

     ((

-      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); .)

+      [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); .)

        "{"                                       (. module.BodyStartTok = t; .)

         { (. isGhost = false; .)

           [ "ghost"  (. isGhost = true; .) ]

@@ -536,8 +536,8 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ 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*/

-     IToken moduleName = null;

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

+     List<IToken> path;

   .)

   ( "object"                        (. tok = t;  ty = new ObjectType(); .)

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

@@ -550,11 +550,12 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
                                        }

                                        ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

                                     .)

-  | Ident<out tok>                  (. gt = new List<Type/*!*/>(); .)

-    [                               (. moduleName = tok; .)

-      "." Ident<out tok>

-    ]

-    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, moduleName); .)

+  | Ident<out tok>                  (. gt = new List<Type/*!*/>();

+                                       path = new List<IToken>(); .)

+    {                               (. path.Add(tok); .)

+      "." Ident<out tok>           

+    }

+    [ GenericInstantiation<gt> ]    (. ty = new UserDefinedType(tok, tok.val, gt, path); .)

   )

   .

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

@@ -576,9 +577,9 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
      List<Expression/*!*/> reqs = new List<Expression/*!*/>();

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

      List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

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

+     List<Expression/*!*/> decreases;

      Expression body = null;

-     bool isPredicate = false;

+     bool isPredicate = false;  bool isCoPredicate = false;

      bool isFunctionMethod = false;

      IToken openParen = null;

      IToken bodyStart = Token.NoToken;

@@ -619,14 +620,34 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
     | "..."                    (. signatureOmitted = true;

                                   openParen = Token.NoToken; .)

     )

+

+  /* ----- copredicate ----- */

+  | "copredicate"              (. isCoPredicate = true; .)

+    (. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }

+    .)

+    { Attribute<ref attrs> }

+    NoUSIdent<out id>

+    (

+      [ GenericParameters<typeArgs> ]

+      [ Formals<true, isFunctionMethod, formals, out openParen>

+        [ ":"                  (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)

+        ]

+      ]

+    | "..."                    (. signatureOmitted = true;

+                                  openParen = Token.NoToken; .)

+    )

   )

 

+  (. decreases = isCoPredicate ? null : new List<Expression/*!*/>(); .)

   { FunctionSpec<reqs, reads, ens, decreases> }

   [ FunctionBody<out body, out bodyStart, out bodyEnd>

   ]

   (. if (isPredicate) {

         f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

                           reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

+     } else if (isCoPredicate) {

+        f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

+                          reqs, reads, ens, body, attrs, signatureOmitted);

      } else {

         f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

                          reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);

@@ -635,8 +656,10 @@ 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));

+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(decreases == null || cce.NonNullElements(decreases));

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

   (

     SYNC

@@ -646,7 +669,12 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
               }

             ] SYNC ";"

   | "ensures" Expression<out e> SYNC ";"      (. ens.Add(e); .)

-  | "decreases" DecreasesList<decreases, false> SYNC ";"

+  | "decreases"                               (. if (decreases == null) {

+                                                   SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");

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

+                                                 }

+                                              .)

+    DecreasesList<decreases, false> SYNC ";"

   )

   .

 PossiblyWildExpression<out Expression/*!*/ e>

@@ -729,10 +757,23 @@ OneStmt<out Statement/*!*/ s>
     SYNC

     ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)

   | ReturnStmt<out s>

-  | "..."                              (. s = new SkeletonStatement(t); .)

+  | SkeletonStmt<out s> 

     ";"

   )

   .

+

+SkeletonStmt<out Statement s>

+= (. List<IToken> names = null;

+     List<Expression> exprs = null;

+     IToken tok, dotdotdot;

+     Expression e; .)

+  "..."                                (. dotdotdot = t; .)

+  ["where"                             (. names = new List<IToken>(); exprs = new List<Expression>(); .)

+     Ident<out tok> "=" Expression<out e>        (. names.Add(tok); exprs.Add(e); .)

+     {"," Ident<out tok> "=" Expression<out e> } (. names.Add(tok); exprs.Add(e); .)

+  ]

+                                       (. s = new SkeletonStatement(dotdotdot, names, exprs); .)

+  .

 ReturnStmt<out Statement/*!*/ s>

 = (.

    IToken returnTok = null;

@@ -802,16 +843,18 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
       "]"                              (. // make sure an array class with this dimensionality exists

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

                                        .)

-    | "." Ident<out x>

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

+    | "." Ident<out x>                 

+      "("                              (. // This case happens when we have type<typeargs>.Constructor(args)

+                                          // There is no ambiguity about where the constructor is or whether one exists.

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

         [ Expressions<args> ]

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

     | "("                              (. var udf = ty as UserDefinedType;

-                                          if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

-                                            // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+                                          if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

+                                            // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

                                             // the name of the constructor that's being invoked.

                                             x = udf.tok;

-                                            ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+                                            ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

                                           } else {

                                             SemErr(t, "expected '.'");

                                             x = null;

@@ -1440,8 +1483,6 @@ EndlessExpression<out Expression e>
 = (. IToken/*!*/ x;

      Expression e0, e1;

      e = dummyExpr;

-     BoundVar d;

-     List<BoundVar> letVars;  List<Expression> letRHSs;

   .)

   ( "if"                            (. x = t; .)

     Expression<out e>

@@ -1456,7 +1497,18 @@ EndlessExpression<out Expression e>
   | "assume"                        (. x = t; .)

     Expression<out e0> ";"

     Expression<out e1>              (. e = new AssumeExpr(x, e0, e1); .)

-  | "var"                           (. x = t;

+  | LetExpr<out e>

+  | NamedExpr<out e>

+  )

+  .

+

+LetExpr<out Expression e>

+= (. IToken/*!*/ x;

+     e = dummyExpr;

+     BoundVar d;

+     List<BoundVar> letVars;  List<Expression> letRHSs;

+  .)

+    "var"                           (. x = t;

                                        letVars = new List<BoundVar>();

                                        letRHSs = new List<Expression>(); .)

     IdentTypeOptional<out d>        (. letVars.Add(d); .)

@@ -1468,8 +1520,20 @@ EndlessExpression<out Expression e>
     }

     ";"

     Expression<out e>               (. e = new LetExpr(x, letVars, letRHSs, e); .)

-  )

   .

+

+NamedExpr<out Expression e>

+= (. IToken/*!*/ x, d;

+     e = dummyExpr;

+     Expression expr;

+  .)

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

+    NoUSIdent<out d>

+    ":"

+    Expression<out e>               (. expr = e;

+                                       e = new NamedExpr(x, d.val, expr); .)

+  .

+

 MatchExpression<out Expression/*!*/ e>

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

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

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ee4592ce..e9a4ce4b 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Dafny {
 

   public class BuiltIns

   {

-    public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null);

+    public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, true);

     Dictionary<int, ClassDecl/*!*/> arrayTypeDecls = new Dictionary<int, ClassDecl>();

     public readonly ClassDecl ObjectDecl;

     public BuiltIns() {

@@ -414,9 +414,10 @@ namespace Microsoft.Dafny {
       Contract.Invariant(tok != null);

       Contract.Invariant(Name != null);

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

+      Contract.Invariant(cce.NonNullElements(Path));

     }

 

-    public readonly IToken ModuleName;  // may be null

+    public readonly List<IToken> Path;  // may be null

     public readonly IToken tok;  // token of the Name

     public readonly string Name;

     [Rep]

@@ -454,11 +455,13 @@ namespace Microsoft.Dafny {
     public TopLevelDecl ResolvedClass;  // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype

     public TypeParameter ResolvedParam;  // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list

 

-    public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs, IToken moduleName) {

+    public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs, List<IToken> moduleName) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

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

-      this.ModuleName = moduleName;

+      Contract.Requires(moduleName == null || cce.NonNullElements(moduleName));

+      if (moduleName != null) this.Path = moduleName;

+      else this.Path = new List<IToken>();

       this.tok = tok;

       this.Name = name;

       this.TypeArgs = typeArgs;

@@ -476,6 +479,7 @@ namespace Microsoft.Dafny {
       this.Name = name;

       this.TypeArgs = typeArgs;

       this.ResolvedClass = cd;

+      this.Path = new List<IToken>();

     }

 

     /// <summary>

@@ -489,6 +493,7 @@ namespace Microsoft.Dafny {
       this.Name = name;

       this.TypeArgs = new List<Type/*!*/>();

       this.ResolvedParam = tp;

+      this.Path = new List<IToken>();

     }

 

     /// <summary>

@@ -522,19 +527,10 @@ namespace Microsoft.Dafny {
     [Pure]

     public override string ToString() {

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

-

-      string s = Name;

-      if (ModuleName != null) {

-        s = ModuleName.val + "." + s;

-      }

+      

+      string s = Util.Comma(".", Path, i => i.val) + (Path.Count == 0 ? "" : ".") + Name;

       if (TypeArgs.Count != 0) {

-        string sep = "<";

-        foreach (Type t in TypeArgs) {

-          Contract.Assume(cce.IsPeerConsistent(t));

-          s += sep + t;

-          sep = ",";

-        }

-        s += ">";

+        s += "<" + Util.Comma(",", TypeArgs, ty => ty.ToString()) + ">";

       }

       return s;

     }

@@ -840,9 +836,11 @@ namespace Microsoft.Dafny {
     

     public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();

     public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();

+    public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();

     public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.

                                        // it is abstract). Otherwise, it points to that definition.

     public ModuleSignature Refines;

+    public bool IsGhost = false;

     public ModuleSignature() {}

 

     public bool FindSubmodule(string name, out ModuleSignature pp) {

@@ -868,14 +866,14 @@ namespace Microsoft.Dafny {
     public int Height;  // height in the topological sorting of modules; filled in during resolution

     public readonly bool IsGhost;

     public readonly bool IsAbstract; // True iff this module represents an abstract interface

-

+    private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

       Contract.Invariant(CallGraph != null);

     }

 

-    public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase,  Attributes attributes)

+    public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase,  Attributes attributes, bool isBuiltinName)

       : base(tok, name, attributes) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

@@ -884,6 +882,7 @@ namespace Microsoft.Dafny {
       IsAbstract = isAbstract;

       RefinementBaseRoot = null;

       RefinementBase = null;

+      IsBuiltinName = isBuiltinName;

     }

     public virtual bool IsDefaultModule {

       get {

@@ -894,15 +893,32 @@ namespace Microsoft.Dafny {
     new public string CompileName {

       get {

         if (compileName == null) {

-          compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);

+          if (IsBuiltinName)

+            compileName = Name;

+          else

+            compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);

         }

         return compileName;

       }

     }

+

+    public static IEnumerable<Function> AllFunctions(List<TopLevelDecl> declarations) {

+      foreach (var d in declarations) {

+        var cl = d as ClassDecl;

+        if (cl != null) {

+          foreach (var member in cl.Members) {

+            var fn = member as Function;

+            if (fn != null) {

+              yield return fn;

+            }

+          }

+        }

+      }

+    }

   }

 

   public class DefaultModuleDecl : ModuleDefinition {

-    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null) {

+    public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, true) {

     }

     public override bool IsDefaultModule {

       get {

@@ -1079,7 +1095,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(EnclosingDatatype != null);

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

 

-        return "#" + EnclosingDatatype.FullName + "." + Name;

+        return "#" + EnclosingDatatype.FullCompileName + "." + Name;

       }

     }

   }

@@ -1165,11 +1181,21 @@ namespace Microsoft.Dafny {
   public class DatatypeDestructor : SpecialField

   {

     public readonly DatatypeCtor EnclosingCtor;

+    public readonly Formal CorrespondingFormal;

 

-    public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)

+    public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, Formal correspondingFormal, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)

       : base(tok, name, compiledName, preString, postString, isGhost, false, type, attributes)

     {

+      Contract.Requires(tok != null);

+      Contract.Requires(enclosingCtor != null);

+      Contract.Requires(correspondingFormal != null);

+      Contract.Requires(name != null);

+      Contract.Requires(compiledName != null);

+      Contract.Requires(preString != null);

+      Contract.Requires(postString != null);

+      Contract.Requires(type != null);

       EnclosingCtor = enclosingCtor;

+      CorrespondingFormal = correspondingFormal;

     }

   }

 

@@ -1479,6 +1505,19 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class CoPredicate : Function

+  {

+    public readonly List<FunctionCallExpr> Uses = new List<FunctionCallExpr>();  // filled in during resolution, used by verifier

+

+    public CoPredicate(IToken tok, string name, bool isStatic,

+                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,

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

+                     Expression body, Attributes attributes, bool signatureOmitted)

+      : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(),

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

+    }

+  }

+

   public class Method : MemberDecl, TypeParameter.ParentType

   {

     public readonly bool SignatureIsOmitted;

@@ -2493,10 +2532,13 @@ namespace Microsoft.Dafny {
     public readonly Statement S;

     public readonly bool ConditionOmitted;

     public readonly bool BodyOmitted;

+    public readonly List<IToken> NameReplacements;

+    public readonly List<Expression> ExprReplacements;

     public SkeletonStatement(IToken tok)

       : base(tok)

     {

       Contract.Requires(tok != null);

+      S = null;

     }

     public SkeletonStatement(Statement s, bool conditionOmitted, bool bodyOmitted)

       : base(s.Tok)

@@ -2506,6 +2548,13 @@ namespace Microsoft.Dafny {
       ConditionOmitted = conditionOmitted;

       BodyOmitted = bodyOmitted;

     }

+    public SkeletonStatement(IToken tok, List<IToken> nameReplacements, List<Expression> exprReplacements)

+      : base(tok) {

+      Contract.Requires(tok != null);

+      NameReplacements = nameReplacements;

+      ExprReplacements = exprReplacements;

+      

+    }

     public override IEnumerable<Statement> SubStatements {

       get {

         // The SkeletonStatement is really a modification of its inner statement S.  Therefore,

@@ -2948,7 +2997,7 @@ namespace Microsoft.Dafny {
     public readonly Expression/*!*/ Receiver;

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

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

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

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

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

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

 

@@ -3370,6 +3419,34 @@ namespace Microsoft.Dafny {
       }

     }

   }

+  // Represents expr Name: Body

+  //         or expr Name: (assert Body == Contract; Body)

+  public class NamedExpr : Expression

+  {

+    public readonly string Name;

+    public readonly Expression Body;

+    public readonly Expression Contract;

+    public readonly IToken ReplacerToken;

+

+    public NamedExpr(IToken tok, string p, Expression body)

+      : base(tok) {

+      Name = p;

+      Body = body;

+    }

+    public NamedExpr(IToken tok, string p, Expression body, Expression contract, IToken token)

+      : base(tok) {

+      Name = p;

+      Body = body;

+      Contract = contract;

+      ReplacerToken = token;

+    }

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Body;

+        if (Contract != null) yield return Contract;

+      }

+    }

+  }

 

   /// <summary>

   /// A ComprehensionExpr has the form:

@@ -3885,7 +3962,7 @@ namespace Microsoft.Dafny {
 

   public class Specification<T> where T : class

   {

-    public List<T> Expressions;

+    public readonly List<T> Expressions;

 

     [ContractInvariantMethod]

     private void ObjectInvariant()

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f585476d..9c47278b 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -21,7 +21,7 @@ public class Parser {
 	public const int _colon = 5;

 	public const int _lbrace = 6;

 	public const int _rbrace = 7;

-	public const int maxT = 107;

+	public const int maxT = 110;

 

 	const bool T = true;

 	const bool x = false;

@@ -212,7 +212,7 @@ bool IsAttribute() {
 				defaultModule.TopLevelDecls.Add(at); 

 			} else if (StartOf(2)) {

 				ClassMemberDecl(membersDefaultClass, isGhost, false);

-			} else SynErr(108);

+			} else SynErr(111);

 		}

 		DefaultClassDecl defaultClass = null;

 		foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

@@ -249,7 +249,7 @@ bool IsAttribute() {
 				Get();

 				QualifiedName(out idRefined);

 			}

-			module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); 

+			module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); 

 			Expect(6);

 			module.BodyStartTok = t; 

 			while (StartOf(1)) {

@@ -275,7 +275,7 @@ bool IsAttribute() {
 					module.TopLevelDecls.Add(at); 

 				} else if (StartOf(2)) {

 					ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);

-				} else SynErr(109);

+				} else SynErr(112);

 			}

 			Expect(7);

 			module.BodyEndTok = t;

@@ -291,7 +291,7 @@ bool IsAttribute() {
 			QualifiedName(out idPath);

 			Expect(12);

 			submodule = new AbstractModuleDecl(idPath, id, parent); 

-		} else SynErr(110);

+		} else SynErr(113);

 	}

 

 	void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {

@@ -303,7 +303,7 @@ bool IsAttribute() {
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

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

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

 		Expect(15);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

@@ -334,13 +334,13 @@ bool IsAttribute() {
 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		bool co = false;

 		

-		while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(112); Get();}

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

 		if (la.kind == 17) {

 			Get();

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

 			Get();

 			co = true; 

-		} else SynErr(113);

+		} else SynErr(116);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

@@ -355,7 +355,7 @@ bool IsAttribute() {
 			Get();

 			DatatypeMemberDecl(ctors);

 		}

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

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

 		Expect(12);

 		if (co) {

 		 dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

@@ -384,7 +384,7 @@ bool IsAttribute() {
 			eqSupport = TypeParameter.EqualitySupportValue.Required; 

 		}

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

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

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

 		Expect(12);

 	}

 

@@ -406,13 +406,13 @@ bool IsAttribute() {
 		}

 		if (la.kind == 20) {

 			FieldDecl(mmod, mm);

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

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

 			FunctionDecl(mmod, out f);

 			mm.Add(f); 

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

 			MethodDecl(mmod, allowConstructors, out m);

 			mm.Add(m); 

-		} else SynErr(116);

+		} else SynErr(119);

 	}

 

 	void Attribute(ref Attributes attrs) {

@@ -483,7 +483,7 @@ bool IsAttribute() {
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

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

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

 		Expect(20);

 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

 		

@@ -497,7 +497,7 @@ bool IsAttribute() {
 			IdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

 		}

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

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

 		Expect(12);

 	}

 

@@ -511,9 +511,9 @@ bool IsAttribute() {
 		List<Expression/*!*/> reqs = new List<Expression/*!*/>();

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

 		List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();

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

+		List<Expression/*!*/> decreases;

 		Expression body = null;

-		bool isPredicate = false;

+		bool isPredicate = false;  bool isCoPredicate = false;

 		bool isFunctionMethod = false;

 		IToken openParen = null;

 		IToken bodyStart = Token.NoToken;

@@ -543,7 +543,7 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(119);

+			} else SynErr(122);

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

 			Get();

 			isPredicate = true; 

@@ -572,8 +572,34 @@ bool IsAttribute() {
 				Get();

 				signatureOmitted = true;

 				openParen = Token.NoToken; 

-			} else SynErr(120);

-		} else SynErr(121);

+			} else SynErr(123);

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

+			Get();

+			isCoPredicate = true; 

+			if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }

+			

+			while (la.kind == 6) {

+				Attribute(ref attrs);

+			}

+			NoUSIdent(out id);

+			if (StartOf(3)) {

+				if (la.kind == 26) {

+					GenericParameters(typeArgs);

+				}

+				if (la.kind == 23) {

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

+					if (la.kind == 5) {

+						Get();

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

+					}

+				}

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

+				Get();

+				signatureOmitted = true;

+				openParen = Token.NoToken; 

+			} else SynErr(124);

+		} else SynErr(125);

+		decreases = isCoPredicate ? null : new List<Expression/*!*/>(); 

 		while (StartOf(4)) {

 			FunctionSpec(reqs, reads, ens, decreases);

 		}

@@ -583,6 +609,9 @@ bool IsAttribute() {
 		if (isPredicate) {

 		  f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,

 		                    reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);

+		} else if (isCoPredicate) {

+		  f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,

+		                    reqs, reads, ens, body, attrs, signatureOmitted);

 		} else {

 		  f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals, returnType,

 		                   reqs, reads, ens, new Specification<Expression>(decreases, null), body, attrs, signatureOmitted);

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

 		IToken bodyEnd = Token.NoToken;

 		

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

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

 		if (la.kind == 28) {

 			Get();

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

@@ -623,7 +652,7 @@ bool IsAttribute() {
 			 SemErr(t, "constructors are only allowed in classes");

 			}

 			

-		} else SynErr(123);

+		} else SynErr(127);

 		if (isConstructor) {

 		 if (mmod.IsGhost) {

 		   SemErr(t, "constructors cannot be declared 'ghost'");

@@ -650,7 +679,7 @@ bool IsAttribute() {
 		} else if (la.kind == 31) {

 			Get();

 			signatureOmitted = true; openParen = Token.NoToken; 

-		} else SynErr(124);

+		} else SynErr(128);

 		while (StartOf(5)) {

 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);

 		}

@@ -844,7 +873,7 @@ bool IsAttribute() {
 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(125); break;

+		default: SynErr(129); break;

 		}

 	}

 

@@ -869,7 +898,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false; Attributes ensAttrs = null;

 		

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

+		while (!(StartOf(7))) {SynErr(130); Get();}

 		if (la.kind == 32) {

 			Get();

 			while (IsAttribute()) {

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

 				}

 			}

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

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

 			Expect(12);

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

 			if (la.kind == 33) {

@@ -894,7 +923,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			if (la.kind == 34) {

 				Get();

 				Expression(out e);

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

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

 				Expect(12);

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

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

@@ -903,19 +932,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Attribute(ref ensAttrs);

 				}

 				Expression(out e);

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

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

 				Expect(12);

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

-			} else SynErr(130);

+			} else SynErr(134);

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

 			Get();

 			while (IsAttribute()) {

 				Attribute(ref decAttrs);

 			}

 			DecreasesList(decreases, false);

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

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

 			Expect(12);

-		} else SynErr(132);

+		} else SynErr(136);

 	}

 

 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

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

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

 		Expression(out e);

-		if (la.kind == 49) {

+		if (la.kind == 50) {

 			Get();

 			Ident(out id);

 			fieldName = id.val; 

@@ -984,8 +1013,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void 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*/

-		IToken moduleName = null;

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

+		List<IToken> path;

 		

 		if (la.kind == 44) {

 			Get();

@@ -1005,30 +1034,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

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

 			Ident(out tok);

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

-			if (la.kind == 14) {

-				moduleName = tok; 

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

+			path = new List<IToken>(); 

+			while (la.kind == 14) {

+				path.Add(tok); 

 				Get();

 				Ident(out tok);

 			}

 			if (la.kind == 26) {

 				GenericInstantiation(gt);

 			}

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

-		} else SynErr(133);

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

+		} else SynErr(137);

 	}

 

-	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

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

+	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {

+		Contract.Requires(cce.NonNullElements(reqs));

+		Contract.Requires(cce.NonNullElements(reads));

+		Contract.Requires(decreases == null || cce.NonNullElements(decreases));

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

 		if (la.kind == 34) {

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

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

 			Get();

 			Expression(out e);

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

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

 			Expect(12);

 			reqs.Add(e); 

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

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

 			Get();

 			if (StartOf(10)) {

 				PossiblyWildFrameExpression(out fe);

@@ -1039,20 +1071,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					reads.Add(fe); 

 				}

 			}

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

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

 			Expect(12);

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

 			Get();

 			Expression(out e);

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

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

 			Expect(12);

 			ens.Add(e); 

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

 			Get();

+			if (decreases == null) {

+			 SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");

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

+			}

+			

 			DecreasesList(decreases, false);

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

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

 			Expect(12);

-		} else SynErr(139);

+		} else SynErr(143);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

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

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

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

-		if (la.kind == 48) {

+		if (la.kind == 49) {

 			Get();

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

 		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(140);

+		} else SynErr(144);

 	}

 

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

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

 		e = dummyExpr; 

-		if (la.kind == 48) {

+		if (la.kind == 49) {

 			Get();

 			e = new WildcardExpr(t); 

 		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(141);

+		} else SynErr(145);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -1099,26 +1136,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

-		while (!(StartOf(11))) {SynErr(142); Get();}

+		while (!(StartOf(11))) {SynErr(146); Get();}

 		switch (la.kind) {

 		case 6: {

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

 			s = bs; 

 			break;

 		}

-		case 67: {

+		case 69: {

 			AssertStmt(out s);

 			break;

 		}

-		case 55: {

+		case 57: {

 			AssumeStmt(out s);

 			break;

 		}

-		case 68: {

+		case 70: {

 			PrintStmt(out s);

 			break;

 		}

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

+		case 1: case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: case 100: {

 			UpdateStmt(out s);

 			break;

 		}

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

 			break;

 		}

-		case 60: {

+		case 62: {

 			IfStmt(out s);

 			break;

 		}

-		case 64: {

+		case 66: {

 			WhileStmt(out s);

 			break;

 		}

-		case 66: {

+		case 68: {

 			MatchStmt(out s);

 			break;

 		}

-		case 69: {

+		case 71: {

 			ParallelStmt(out s);

 			break;

 		}

-		case 50: {

+		case 51: {

 			Get();

 			x = t; 

 			NoUSIdent(out id);

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

 			break;

 		}

-		case 51: {

+		case 52: {

 			Get();

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

 			if (la.kind == 1) {

 				NoUSIdent(out id);

 				label = id.val; 

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

-				while (la.kind == 51) {

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

+				while (la.kind == 52) {

 					Get();

 					breakCount++; 

 				}

-			} else SynErr(143);

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

+			} else SynErr(147);

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

 			Expect(12);

 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

 		}

-		case 52: {

+		case 54: {

 			ReturnStmt(out s);

 			break;

 		}

 		case 31: {

-			Get();

-			s = new SkeletonStatement(t); 

+			SkeletonStmt(out s);

 			Expect(12);

 			break;

 		}

-		default: SynErr(145); break;

+		default: SynErr(149); break;

 		}

 	}

 

@@ -1186,7 +1222,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

 		Expression e = null; Attributes attrs = null;

 		

-		Expect(67);

+		Expect(69);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

@@ -1195,7 +1231,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

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

 			Get();

-		} else SynErr(146);

+		} else SynErr(150);

 		Expect(12);

 		if (e == null) {

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

@@ -1209,7 +1245,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;

 		Expression e = null; Attributes attrs = null;

 		

-		Expect(55);

+		Expect(57);

 		x = t; 

 		while (IsAttribute()) {

 			Attribute(ref attrs);

@@ -1218,7 +1254,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

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

 			Get();

-		} else SynErr(147);

+		} else SynErr(151);

 		if (e == null) {

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

 		} else {

@@ -1232,7 +1268,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;  Attributes.Argument/*!*/ arg;

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

 		

-		Expect(68);

+		Expect(70);

 		x = t; 

 		AttributeArg(out arg);

 		args.Add(arg); 

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

 			Expect(12);

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

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

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

 			lhss.Add(e);  lhs0 = e; 

 			while (la.kind == 21) {

 				Get();

 				Lhs(out e);

 				lhss.Add(e); 

 			}

-			if (la.kind == 53) {

+			if (la.kind == 55) {

 				Get();

 				x = t; 

 				Rhs(out r, lhs0);

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

 					rhss.Add(r); 

 				}

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

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

 				Get();

 				x = t; 

-				if (la.kind == 55) {

+				if (la.kind == 57) {

 					Get();

 					suchThatAssume = t; 

 				}

 				Expression(out suchThat);

-			} else SynErr(148);

+			} else SynErr(152);

 			Expect(12);

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

 			Get();

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

-		} else SynErr(149);

+		} else SynErr(153);

 		if (suchThat != null) {

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

 		} else {

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

 			lhss.Add(d); 

 		}

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

-			if (la.kind == 53) {

+		if (la.kind == 55 || la.kind == 56) {

+			if (la.kind == 55) {

 				Get();

 				assignTok = t;

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

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

 				Get();

 				assignTok = t; 

-				if (la.kind == 55) {

+				if (la.kind == 57) {

 					Get();

 					suchThatAssume = t; 

 				}

@@ -1384,7 +1420,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		ifStmt = dummyStmt;  // to please the compiler

 		

-		Expect(60);

+		Expect(62);

 		x = t; 

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

 			if (la.kind == 23) {

@@ -1394,15 +1430,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				guardOmitted = true; 

 			}

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

-			if (la.kind == 61) {

+			if (la.kind == 63) {

 				Get();

-				if (la.kind == 60) {

+				if (la.kind == 62) {

 					IfStmt(out s);

 					els = s; 

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

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

 					els = bs; 

-				} else SynErr(150);

+				} else SynErr(154);

 			}

 			if (guardOmitted) {

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(151);

+		} else SynErr(155);

 	}

 

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

@@ -1429,7 +1465,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;

 		stmt = dummyStmt;  // to please the compiler

 		

-		Expect(64);

+		Expect(66);

 		x = t; 

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

 			if (la.kind == 23) {

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

 				Get();

 				bodyOmitted = true; 

-			} else SynErr(152);

+			} else SynErr(156);

 			if (guardOmitted || bodyOmitted) {

 			 if (mod != null) {

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

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

 			AlternativeBlock(out alternatives);

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

-		} else SynErr(153);

+		} else SynErr(157);

 	}

 

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

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

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

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

-		Expect(66);

+		Expect(68);

 		x = t; 

 		Expression(out e);

 		Expect(6);

-		while (la.kind == 62) {

+		while (la.kind == 64) {

 			CaseStatement(out c);

 			cases.Add(c); 

 		}

@@ -1494,7 +1530,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;

 		IToken bodyStart, bodyEnd;

 		

-		Expect(69);

+		Expect(71);

 		x = t; 

 		Expect(23);

 		if (la.kind == 1) {

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

 		AssignmentRhs r;

 		

-		Expect(52);

+		Expect(54);

 		returnTok = t; 

 		if (StartOf(13)) {

 			Rhs(out r, null);

@@ -1542,6 +1578,31 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		s = new ReturnStmt(returnTok, rhss); 

 	}

 

+	void SkeletonStmt(out Statement s) {

+		List<IToken> names = null;

+		List<Expression> exprs = null;

+		IToken tok, dotdotdot;

+		Expression e; 

+		Expect(31);

+		dotdotdot = t; 

+		if (la.kind == 53) {

+			Get();

+			names = new List<IToken>(); exprs = new List<Expression>(); 

+			Ident(out tok);

+			Expect(11);

+			Expression(out e);

+			names.Add(tok); exprs.Add(e); 

+			while (la.kind == 21) {

+				Get();

+				Ident(out tok);

+				Expect(11);

+				Expression(out e);

+			}

+			names.Add(tok); exprs.Add(e); 

+		}

+		s = new SkeletonStatement(dotdotdot, names, exprs); 

+	}

+

 	void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {

 		IToken/*!*/ x, newToken;  Expression/*!*/ e;

 		List<Expression> ee = null;

@@ -1551,16 +1612,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		r = null;  // to please compiler

 		Attributes attrs = null;

 		

-		if (la.kind == 56) {

+		if (la.kind == 58) {

 			Get();

 			newToken = t; 

 			TypeAndToken(out x, out ty);

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

-				if (la.kind == 57) {

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

+				if (la.kind == 59) {

 					Get();

 					ee = new List<Expression>(); 

 					Expressions(ee);

-					Expect(58);

+					Expect(60);

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

 					

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

@@ -1576,11 +1637,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				} else {

 					Get();

 					var udf = ty as UserDefinedType;

-					if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {

-					 // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as

+					if (udf != null && 0 < udf.Path.Count && udf.TypeArgs.Count == 0) {

+					 // The parsed name had the form "A.B.Ctr", so treat "A.B" as the name of the type and "Ctr" as

 					 // the name of the constructor that's being invoked.

 					 x = udf.tok;

-					 ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);

+					 ty = new UserDefinedType(udf.Path[0], udf.Path[udf.Path.Count-1].val, new List<Type>(), udf.Path.GetRange(0,udf.Path.Count-1));

 					} else {

 					 SemErr(t, "expected '.'");

 					 x = null;

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

 			}

 			

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

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

 			Get();

 			x = t; 

 			Expression(out e);

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

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

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

 			Get();

 			r = new HavocRhs(t); 

 		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(154);

+		} else SynErr(158);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

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

 		if (la.kind == 1) {

 			DottedIdentifiersAndFunction(out e);

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

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

 				Suffix(ref e);

 			}

 		} else if (StartOf(14)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

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

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

 				Suffix(ref e);

 			}

-		} else SynErr(155);

+		} else SynErr(159);

 	}

 

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

@@ -1651,13 +1712,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void Guard(out Expression e) {

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

 		Expect(23);

-		if (la.kind == 48) {

+		if (la.kind == 49) {

 			Get();

 			e = null; 

 		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(156);

+		} else SynErr(160);

 		Expect(25);

 	}

 

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

 		

 		Expect(6);

-		while (la.kind == 62) {

+		while (la.kind == 64) {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(63);

+			Expect(65);

 			body = new List<Statement>(); 

 			while (StartOf(9)) {

 				Stmt(body);

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

 		

 		while (StartOf(15)) {

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

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

 				Invariant(out invariant);

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

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

 				Expect(12);

 				invariants.Add(invariant); 

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(12);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

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

 					}

 				}

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

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

 				Expect(12);

 			}

 		}

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

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

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

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

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

 		if (la.kind == 33) {

 			Get();

 			isFree = true; 

 		}

-		Expect(65);

+		Expect(67);

 		while (IsAttribute()) {

 			Attribute(ref attrs);

 		}

@@ -1748,7 +1809,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;

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

 		

-		Expect(62);

+		Expect(64);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 23) {

@@ -1762,7 +1823,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(25);

 		}

-		Expect(63);

+		Expect(65);

 		while (StartOf(9)) {

 			Stmt(body);

 		}

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

 			Expression(out e);

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

-		} else SynErr(163);

+		} else SynErr(167);

 	}

 

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

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

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

 		ImpliesExpression(out e0);

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

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

 			EquivOp();

 			x = t; 

 			ImpliesExpression(out e1);

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

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

 		LogicalExpression(out e0);

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

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

 			ImpliesOp();

 			x = t; 

 			ImpliesExpression(out e1);

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

 

 	void EquivOp() {

-		if (la.kind == 70) {

+		if (la.kind == 72) {

 			Get();

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

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

 			Get();

-		} else SynErr(164);

+		} else SynErr(168);

 	}

 

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

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

 		RelationalExpression(out e0);

 		if (StartOf(16)) {

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

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

 				AndOp();

 				x = t; 

 				RelationalExpression(out e1);

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

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

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

 					AndOp();

 					x = t; 

 					RelationalExpression(out e1);

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

 				RelationalExpression(out e1);

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

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

+				while (la.kind == 78 || la.kind == 79) {

 					OrOp();

 					x = t; 

 					RelationalExpression(out e1);

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

 

 	void ImpliesOp() {

-		if (la.kind == 72) {

+		if (la.kind == 74) {

 			Get();

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

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

 			Get();

-		} else SynErr(165);

+		} else SynErr(169);

 	}

 

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

@@ -1961,25 +2022,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void AndOp() {

-		if (la.kind == 74) {

+		if (la.kind == 76) {

 			Get();

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

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

 			Get();

-		} else SynErr(166);

+		} else SynErr(170);

 	}

 

 	void OrOp() {

-		if (la.kind == 76) {

+		if (la.kind == 78) {

 			Get();

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

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

 			Get();

-		} else SynErr(167);

+		} else SynErr(171);

 	}

 

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

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

 		Factor(out e0);

-		while (la.kind == 87 || la.kind == 88) {

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

 			AddOp(out x, out op);

 			Factor(out e1);

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

@@ -2007,35 +2068,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Gt; 

 			break;

 		}

-		case 78: {

+		case 80: {

 			Get();

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

 			break;

 		}

-		case 79: {

+		case 81: {

 			Get();

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

 			break;

 		}

-		case 80: {

+		case 82: {

 			Get();

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

 			break;

 		}

-		case 81: {

+		case 83: {

 			Get();

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

 			break;

 		}

-		case 82: {

+		case 84: {

 			Get();

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

 			break;

 		}

-		case 83: {

+		case 85: {

 			Get();

 			x = t;  y = Token.NoToken; 

-			if (la.kind == 82) {

+			if (la.kind == 84) {

 				Get();

 				y = t; 

 			}

@@ -2050,29 +2111,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			

 			break;

 		}

-		case 84: {

+		case 86: {

 			Get();

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

 			break;

 		}

-		case 85: {

+		case 87: {

 			Get();

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

 			break;

 		}

-		case 86: {

+		case 88: {

 			Get();

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

 			break;

 		}

-		default: SynErr(168); break;

+		default: SynErr(172); break;

 		}

 	}

 

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

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

 		UnaryExpression(out e0);

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

+		while (la.kind == 49 || la.kind == 91 || la.kind == 92) {

 			MulOp(out x, out op);

 			UnaryExpression(out e1);

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

@@ -2081,44 +2142,44 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 

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

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

-		if (la.kind == 87) {

+		if (la.kind == 89) {

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(169);

+		} else SynErr(173);

 	}

 

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

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

 		switch (la.kind) {

-		case 88: {

+		case 90: {

 			Get();

 			x = t; 

 			UnaryExpression(out e);

 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 

 			break;

 		}

-		case 83: case 91: {

+		case 85: case 93: {

 			NegOp();

 			x = t; 

 			UnaryExpression(out e);

 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

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

+		case 20: case 40: case 57: case 62: case 68: case 69: case 102: case 104: case 105: case 106: case 107: {

 			EndlessExpression(out e);

 			break;

 		}

 		case 1: {

 			DottedIdentifiersAndFunction(out e);

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

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

 				Suffix(ref e);

 			}

 			break;

 		}

-		case 6: case 57: {

+		case 6: case 59: {

 			DisplayExpr(out e);

 			break;

 		}

@@ -2130,63 +2191,61 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			MapExpr(out e);

 			break;

 		}

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

+		case 2: case 19: case 23: case 94: case 95: case 96: case 97: case 98: case 99: case 100: {

 			ConstAtomExpression(out e);

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

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

 				Suffix(ref e);

 			}

 			break;

 		}

-		default: SynErr(170); break;

+		default: SynErr(174); break;

 		}

 	}

 

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

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

-		if (la.kind == 48) {

+		if (la.kind == 49) {

 			Get();

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

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

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

 			Get();

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

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

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

 			Get();

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

-		} else SynErr(171);

+		} else SynErr(175);

 	}

 

 	void NegOp() {

-		if (la.kind == 83) {

+		if (la.kind == 85) {

 			Get();

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

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

 			Get();

-		} else SynErr(172);

+		} else SynErr(176);

 	}

 

 	void EndlessExpression(out Expression e) {

 		IToken/*!*/ x;

 		Expression e0, e1;

 		e = dummyExpr;

-		BoundVar d;

-		List<BoundVar> letVars;  List<Expression> letRHSs;

 		

 		switch (la.kind) {

-		case 60: {

+		case 62: {

 			Get();

 			x = t; 

 			Expression(out e);

-			Expect(99);

+			Expect(101);

 			Expression(out e0);

-			Expect(61);

+			Expect(63);

 			Expression(out e1);

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

 			break;

 		}

-		case 66: {

+		case 68: {

 			MatchExpression(out e);

 			break;

 		}

-		case 101: case 102: case 103: case 104: {

+		case 104: case 105: case 106: case 107: {

 			QuantifierGuts(out e);

 			break;

 		}

@@ -2194,7 +2253,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ComprehensionExpr(out e);

 			break;

 		}

-		case 67: {

+		case 69: {

 			Get();

 			x = t; 

 			Expression(out e0);

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

 			break;

 		}

-		case 55: {

+		case 57: {

 			Get();

 			x = t; 

 			Expression(out e0);

@@ -2213,31 +2272,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			break;

 		}

 		case 20: {

-			Get();

-			x = t;

-			letVars = new List<BoundVar>();

-			letRHSs = new List<Expression>(); 

-			IdentTypeOptional(out d);

-			letVars.Add(d); 

-			while (la.kind == 21) {

-				Get();

-				IdentTypeOptional(out d);

-				letVars.Add(d); 

-			}

-			Expect(53);

-			Expression(out e);

-			letRHSs.Add(e); 

-			while (la.kind == 21) {

-				Get();

-				Expression(out e);

-				letRHSs.Add(e); 

-			}

-			Expect(12);

-			Expression(out e);

-			e = new LetExpr(x, letVars, letRHSs, e); 

+			LetExpr(out e);

+			break;

+		}

+		case 102: {

+			NamedExpr(out e);

 			break;

 		}

-		default: SynErr(173); break;

+		default: SynErr(177); break;

 		}

 	}

 

@@ -2283,24 +2325,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				e = new FunctionCallExpr(id, id.val, e, openParen, args); 

 			}

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

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

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

 			Get();

 			x = t; 

 			if (StartOf(8)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 100) {

+				if (la.kind == 103) {

 					Get();

 					anyDots = true; 

 					if (StartOf(8)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

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

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

 					Get();

 					Expression(out ee);

 					e1 = ee; 

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

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

 					while (la.kind == 21) {

 						Get();

 						Expression(out ee);

@@ -2311,15 +2353,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(174);

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

+				} else SynErr(178);

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

 				Get();

 				anyDots = true; 

 				if (StartOf(8)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(175);

+			} else SynErr(179);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			}

 			

-			Expect(58);

-		} else SynErr(176);

+			Expect(60);

+		} else SynErr(180);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SetDisplayExpr(x, elements);

 			Expect(7);

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

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

 			Get();

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

 			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

-			Expect(58);

-		} else SynErr(177);

+			Expect(60);

+		} else SynErr(181);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2393,7 +2435,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 		} else if (StartOf(18)) {

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

-		} else SynErr(178);

+		} else SynErr(182);

 	}

 

 	void MapExpr(out Expression e) {

@@ -2404,14 +2446,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(43);

 		x = t; 

-		if (la.kind == 57) {

+		if (la.kind == 59) {

 			Get();

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

 			if (StartOf(8)) {

 				MapLiteralExpressions(out elements);

 			}

 			e = new MapDisplayExpr(x, elements);

-			Expect(58);

+			Expect(60);

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

 			BoundVar/*!*/ bv;

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

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

 		} else if (StartOf(18)) {

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

-		} else SynErr(179);

+		} else SynErr(183);

 	}

 

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

@@ -2436,17 +2478,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;

 		

 		switch (la.kind) {

-		case 92: {

+		case 94: {

 			Get();

 			e = new LiteralExpr(t, false); 

 			break;

 		}

-		case 93: {

+		case 95: {

 			Get();

 			e = new LiteralExpr(t, true); 

 			break;

 		}

-		case 94: {

+		case 96: {

 			Get();

 			e = new LiteralExpr(t); 

 			break;

@@ -2456,12 +2498,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 

 			break;

 		}

-		case 95: {

+		case 97: {

 			Get();

 			e = new ThisExpr(t); 

 			break;

 		}

-		case 96: {

+		case 98: {

 			Get();

 			x = t; 

 			Expect(23);

@@ -2470,7 +2512,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new FreshExpr(x, e); 

 			break;

 		}

-		case 97: {

+		case 99: {

 			Get();

 			x = t; 

 			Expect(23);

@@ -2479,7 +2521,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AllocatedExpr(x, e); 

 			break;

 		}

-		case 98: {

+		case 100: {

 			Get();

 			x = t; 

 			Expect(23);

@@ -2504,7 +2546,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);

 			break;

 		}

-		default: SynErr(180); break;

+		default: SynErr(184); break;

 		}

 	}

 

@@ -2523,34 +2565,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;

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

 		Expression(out d);

-		Expect(53);

+		Expect(55);

 		Expression(out r);

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

 		while (la.kind == 21) {

 			Get();

 			Expression(out d);

-			Expect(53);

+			Expect(55);

 			Expression(out r);

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

 		}

 	}

 

 	void QSep() {

-		if (la.kind == 105) {

+		if (la.kind == 108) {

 			Get();

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

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

 			Get();

-		} else SynErr(181);

+		} else SynErr(185);

 	}

 

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

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

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

 		

-		Expect(66);

+		Expect(68);

 		x = t; 

 		Expression(out e);

-		while (la.kind == 62) {

+		while (la.kind == 64) {

 			CaseExpression(out c);

 			cases.Add(c); 

 		}

@@ -2565,13 +2607,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;

 		Expression/*!*/ body;

 		

-		if (la.kind == 101 || la.kind == 102) {

+		if (la.kind == 104 || la.kind == 105) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 103 || la.kind == 104) {

+		} else if (la.kind == 106 || la.kind == 107) {

 			Exists();

 			x = t; 

-		} else SynErr(182);

+		} else SynErr(186);

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

 		QSep();

 		Expression(out body);

@@ -2602,7 +2644,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 		Expect(19);

 		Expression(out range);

-		if (la.kind == 105 || la.kind == 106) {

+		if (la.kind == 108 || la.kind == 109) {

 			QSep();

 			Expression(out body);

 		}

@@ -2611,13 +2653,57 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 	}

 

+	void LetExpr(out Expression e) {

+		IToken/*!*/ x;

+		e = dummyExpr;

+		BoundVar d;

+		List<BoundVar> letVars;  List<Expression> letRHSs;

+		

+		Expect(20);

+		x = t;

+		letVars = new List<BoundVar>();

+		letRHSs = new List<Expression>(); 

+		IdentTypeOptional(out d);

+		letVars.Add(d); 

+		while (la.kind == 21) {

+			Get();

+			IdentTypeOptional(out d);

+			letVars.Add(d); 

+		}

+		Expect(55);

+		Expression(out e);

+		letRHSs.Add(e); 

+		while (la.kind == 21) {

+			Get();

+			Expression(out e);

+			letRHSs.Add(e); 

+		}

+		Expect(12);

+		Expression(out e);

+		e = new LetExpr(x, letVars, letRHSs, e); 

+	}

+

+	void NamedExpr(out Expression e) {

+		IToken/*!*/ x, d;

+		e = dummyExpr;

+		Expression expr;

+		

+		Expect(102);

+		x = t; 

+		NoUSIdent(out d);

+		Expect(5);

+		Expression(out e);

+		expr = e;

+		e = new NamedExpr(x, d.val, expr); 

+	}

+

 	void CaseExpression(out MatchCaseExpr/*!*/ c) {

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

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

 		BoundVar/*!*/ bv;

 		Expression/*!*/ body;

 		

-		Expect(62);

+		Expect(64);

 		x = t; 

 		Ident(out id);

 		if (la.kind == 23) {

@@ -2631,25 +2717,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(25);

 		}

-		Expect(63);

+		Expect(65);

 		Expression(out body);

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

 	}

 

 	void Forall() {

-		if (la.kind == 101) {

+		if (la.kind == 104) {

 			Get();

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

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

 			Get();

-		} else SynErr(183);

+		} else SynErr(187);

 	}

 

 	void Exists() {

-		if (la.kind == 103) {

+		if (la.kind == 106) {

 			Get();

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

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

 			Get();

-		} else SynErr(184);

+		} else SynErr(188);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

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

 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

 	};

 } // end Parser

@@ -2776,144 +2862,148 @@ public class Errors {
 			case 44: s = "\"object\" expected"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 81: s = "\"!!\" expected"; break;

-			case 82: s = "\"in\" expected"; break;

-			case 83: s = "\"!\" expected"; break;

-			case 84: s = "\"\\u2260\" expected"; break;

-			case 85: s = "\"\\u2264\" expected"; break;

-			case 86: s = "\"\\u2265\" expected"; break;

-			case 87: s = "\"+\" expected"; break;

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

-			case 89: s = "\"/\" expected"; break;

-			case 90: s = "\"%\" expected"; break;

-			case 91: s = "\"\\u00ac\" expected"; break;

-			case 92: s = "\"false\" expected"; break;

-			case 93: s = "\"true\" expected"; break;

-			case 94: s = "\"null\" expected"; break;

-			case 95: s = "\"this\" expected"; break;

-			case 96: s = "\"fresh\" expected"; break;

-			case 97: s = "\"allocated\" expected"; break;

-			case 98: s = "\"old\" expected"; break;

-			case 99: s = "\"then\" expected"; break;

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

-			case 101: s = "\"forall\" expected"; break;

-			case 102: s = "\"\\u2200\" expected"; break;

-			case 103: s = "\"exists\" expected"; break;

-			case 104: s = "\"\\u2203\" expected"; break;

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

-			case 106: s = "\"\\u2022\" expected"; break;

-			case 107: s = "??? expected"; break;

-			case 108: s = "invalid Dafny"; break;

-			case 109: s = "invalid SubModuleDecl"; break;

-			case 110: s = "invalid SubModuleDecl"; break;

-			case 111: s = "this symbol not expected in ClassDecl"; break;

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

-			case 113: s = "invalid DatatypeDecl"; break;

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

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

-			case 116: s = "invalid ClassMemberDecl"; break;

-			case 117: s = "this symbol not expected in FieldDecl"; break;

-			case 118: s = "this symbol not expected in FieldDecl"; break;

-			case 119: s = "invalid FunctionDecl"; break;

-			case 120: s = "invalid FunctionDecl"; break;

-			case 121: s = "invalid FunctionDecl"; break;

-			case 122: s = "this symbol not expected in MethodDecl"; break;

-			case 123: s = "invalid MethodDecl"; break;

-			case 124: s = "invalid MethodDecl"; break;

-			case 125: s = "invalid TypeAndToken"; break;

-			case 126: s = "this symbol not expected in MethodSpec"; break;

-			case 127: s = "this symbol not expected in MethodSpec"; break;

-			case 128: s = "this symbol not expected in MethodSpec"; break;

-			case 129: s = "this symbol not expected in MethodSpec"; break;

-			case 130: s = "invalid MethodSpec"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+			case 82: s = "\"!=\" expected"; break;

+			case 83: s = "\"!!\" expected"; break;

+			case 84: s = "\"in\" expected"; break;

+			case 85: s = "\"!\" expected"; break;

+			case 86: s = "\"\\u2260\" expected"; break;

+			case 87: s = "\"\\u2264\" expected"; break;

+			case 88: s = "\"\\u2265\" expected"; break;

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

+			case 90: s = "\"-\" expected"; break;

+			case 91: s = "\"/\" expected"; break;

+			case 92: s = "\"%\" expected"; break;

+			case 93: s = "\"\\u00ac\" expected"; break;

+			case 94: s = "\"false\" expected"; break;

+			case 95: s = "\"true\" expected"; break;

+			case 96: s = "\"null\" expected"; break;

+			case 97: s = "\"this\" expected"; break;

+			case 98: s = "\"fresh\" expected"; break;

+			case 99: s = "\"allocated\" expected"; break;

+			case 100: s = "\"old\" expected"; break;

+			case 101: s = "\"then\" expected"; break;

+			case 102: s = "\"expr\" expected"; break;

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

+			case 104: s = "\"forall\" expected"; break;

+			case 105: s = "\"\\u2200\" expected"; break;

+			case 106: s = "\"exists\" expected"; break;

+			case 107: s = "\"\\u2203\" expected"; break;

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

+			case 109: s = "\"\\u2022\" expected"; break;

+			case 110: s = "??? expected"; break;

+			case 111: s = "invalid Dafny"; break;

+			case 112: s = "invalid SubModuleDecl"; break;

+			case 113: s = "invalid SubModuleDecl"; break;

+			case 114: s = "this symbol not expected in ClassDecl"; break;

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

+			case 116: s = "invalid DatatypeDecl"; break;

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

+			case 118: s = "this symbol not expected in ArbitraryTypeDecl"; break;

+			case 119: s = "invalid ClassMemberDecl"; break;

+			case 120: s = "this symbol not expected in FieldDecl"; break;

+			case 121: s = "this symbol not expected in FieldDecl"; break;

+			case 122: s = "invalid FunctionDecl"; break;

+			case 123: s = "invalid FunctionDecl"; break;

+			case 124: s = "invalid FunctionDecl"; break;

+			case 125: s = "invalid FunctionDecl"; break;

+			case 126: s = "this symbol not expected in MethodDecl"; break;

+			case 127: s = "invalid MethodDecl"; break;

+			case 128: s = "invalid MethodDecl"; break;

+			case 129: s = "invalid TypeAndToken"; break;

+			case 130: s = "this symbol not expected in MethodSpec"; break;

 			case 131: s = "this symbol not expected in MethodSpec"; break;

-			case 132: s = "invalid MethodSpec"; break;

-			case 133: s = "invalid ReferenceType"; break;

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

-			case 135: s = "this symbol not expected in FunctionSpec"; break;

-			case 136: s = "this symbol not expected in FunctionSpec"; break;

-			case 137: s = "this symbol not expected in FunctionSpec"; break;

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

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

+			case 134: s = "invalid MethodSpec"; break;

+			case 135: s = "this symbol not expected in MethodSpec"; break;

+			case 136: s = "invalid MethodSpec"; break;

+			case 137: s = "invalid ReferenceType"; break;

 			case 138: s = "this symbol not expected in FunctionSpec"; break;

-			case 139: s = "invalid FunctionSpec"; break;

-			case 140: s = "invalid PossiblyWildFrameExpression"; break;

-			case 141: s = "invalid PossiblyWildExpression"; break;

-			case 142: s = "this symbol not expected in OneStmt"; break;

-			case 143: s = "invalid OneStmt"; break;

-			case 144: s = "this symbol not expected in OneStmt"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

+			case 139: s = "this symbol not expected in FunctionSpec"; break;

+			case 140: s = "this symbol not expected in FunctionSpec"; break;

+			case 141: s = "this symbol not expected in FunctionSpec"; break;

+			case 142: s = "this symbol not expected in FunctionSpec"; break;

+			case 143: s = "invalid FunctionSpec"; break;

+			case 144: s = "invalid PossiblyWildFrameExpression"; break;

+			case 145: s = "invalid PossiblyWildExpression"; break;

+			case 146: s = "this symbol not expected in OneStmt"; break;

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

+			case 148: s = "this symbol not expected in OneStmt"; break;

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

+			case 150: s = "invalid AssertStmt"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a49a906e..8d6fa510 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -223,7 +223,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(f != null);

       var isPredicate = f is Predicate;

       Indent(indent);

-      string k = isPredicate ? "predicate" : "function";

+      string k = isPredicate ? "predicate" : f is CoPredicate ? "copredicate" : "function";

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

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

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

@@ -1167,7 +1167,12 @@ namespace Microsoft.Dafny {
         }

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

 

-      } else if (expr is SetComprehension) {

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        wr.Write("expr {0}: ", e.Name);

+        PrintExpression(e.Body);

+ 

+       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

         bool parensNeeded = !isRightmost;

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

@@ -1250,6 +1255,10 @@ namespace Microsoft.Dafny {
 

       } 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 if (expr is BoxingCastExpr) {

+        // this is not expected for a parsed program, but we may be called for /trace purposes in the translator

+        var e = (BoxingCastExpr)expr;

+        PrintExpr(e.E, contextBindingStrength, fragileContext, isRightmost, indent);

       } else {

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

       }

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 0d32e24e..5ddc1fac 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -62,13 +62,12 @@ namespace Microsoft.Dafny {
     private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

 

     public void PreResolve(ModuleDefinition m) {

-      Contract.Requires(m != null);

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

+      

+      if (m.RefinementBase == null) return;

 

       if (moduleUnderConstruction != null) {

         postTasks.Clear();

       }

-      

       moduleUnderConstruction = m;

       var prev = m.RefinementBase;     

 

@@ -279,7 +278,7 @@ namespace Microsoft.Dafny {
         return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

-        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : Tok(tt.ModuleName));

+        return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => Tok(x)));

       } else if (t is InferredTypeProxy) {

         return new InferredTypeProxy();

       } else {

@@ -424,6 +423,9 @@ namespace Microsoft.Dafny {
         var e = (LetExpr)expr;

         return new LetExpr(Tok(e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body));

 

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr) expr;

+        return new NamedExpr(Tok(e.tok), e.Name, CloneExpr(e.Body));

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var tk = Tok(e.tok);

@@ -643,6 +645,9 @@ namespace Microsoft.Dafny {
       if (f is Predicate) {

         return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

           req, reads, ens, decreases, body, moreBody != null, null, false);

+      } else if (f is CoPredicate) {

+        return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

+          req, reads, ens, body, null, false);

       } else {

         return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),

           req, reads, ens, decreases, body, null, false);

@@ -698,13 +703,18 @@ namespace Microsoft.Dafny {
         } else {

           var nwMember = nw.Members[index];

           if (nwMember is Field) {

-            reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) is not allowed replace an existing declaration in the refinement base", nwMember.Name, nw.Name);

-

+            if (member is Field && TypesAreEqual(((Field)nwMember).Type, ((Field)member).Type)) {

+              if (member.IsGhost || !nwMember.IsGhost)

+                reporter.Error(nwMember, "a field re-declaration ({0}) must be to ghostify the field", nwMember.Name, nw.Name);

+            } else {

+              reporter.Error(nwMember, "a field declaration ({0}) in a refining class ({1}) must replace a field in the refinement base", nwMember.Name, nw.Name);

+            }

           } else if (nwMember is Function) {

             var f = (Function)nwMember;

             bool isPredicate = f is Predicate;

-            string s = isPredicate ? "predicate" : "function";

-            if (!(member is Function) || isPredicate && !(member is Predicate)) {

+            bool isCoPredicate = f is CoPredicate;

+            string s = isPredicate ? "predicate" : isCoPredicate ? "copredicate" : "function";

+            if (!(member is Function) || (isPredicate && !(member is Predicate)) || (isCoPredicate && !(member is CoPredicate))) {

               reporter.Error(nwMember, "a {0} declaration ({1}) can only refine a {0}", s, nwMember.Name);

             } else {

               var prevFunction = (Function)member;

@@ -799,7 +809,228 @@ namespace Microsoft.Dafny {
 

       return nw;

     }

+    private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) {

+      if (s == null) {

+        return null;

+      } else if (s is AssertStmt) {

+        AssertStmt stmt = (AssertStmt)s;

+        return new AssertStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);

+      } else if (s is AssumeStmt) {

+        AssumeStmt stmt = (AssumeStmt)s;

+        return new AssumeStmt(stmt.Tok, SubstituteNamedExpr(stmt.Expr, p, E, ref subCount), null);

+      } else if (s is PrintStmt) {

+        throw new NotImplementedException();

+      } else if (s is BreakStmt) {

+        return s;

+      } else if (s is ReturnStmt) {

+        return s;

+      } else if (s is VarDeclStmt) {

+        return s;

+      } else if (s is AssignSuchThatStmt) {

+        return s;

+      } else if (s is UpdateStmt) {

+        UpdateStmt stmt = (UpdateStmt)s;

+        List<Expression> lhs = new List<Expression>();

+        List<AssignmentRhs> rhs = new List<AssignmentRhs>();

+        foreach (Expression l in stmt.Lhss) {

+          lhs.Add(SubstituteNamedExpr(l, p, E, ref subCount));

+        }

+        foreach (AssignmentRhs r in stmt.Rhss) {

+          if (r is HavocRhs) {

+            rhs.Add(r); // no substitution on Havoc (*);

+          } else if (r is ExprRhs) {

+            rhs.Add(new ExprRhs(SubstituteNamedExpr(((ExprRhs)r).Expr, p, E, ref subCount)));

+          } else if (r is CallRhs) {

+            CallRhs rr = (CallRhs)r;

+            rhs.Add(new CallRhs(rr.Tok, SubstituteNamedExpr(rr.Receiver, p, E, ref subCount), rr.MethodName, SubstituteNamedExprList(rr.Args, p, E, ref subCount)));

+          } else if (r is TypeRhs) {

+            rhs.Add(r);

+          } else {

+            Contract.Assert(false);  // unexpected AssignmentRhs

+            throw new cce.UnreachableException();

+          }

+        }

+        return new UpdateStmt(stmt.Tok, lhs, rhs);

+      } else if (s is AssignStmt) {

+        Contract.Assert(false);  // AssignStmt is not generated by the parser

+        throw new cce.UnreachableException();

+      } else if (s is VarDecl) {

+        return s;

+      } else if (s is CallStmt) {

+        return s;

+      } else if (s is BlockStmt) {

+        BlockStmt stmt = (BlockStmt)s;

+        List<Statement> res = new List<Statement>();

+        foreach (Statement ss in stmt.Body) {

+          res.Add(SubstituteNamedExpr(ss, p, E, ref subCount));

+        }

+        return new BlockStmt(stmt.Tok, res);

+      } else if (s is IfStmt) {

+        IfStmt stmt = (IfStmt)s;

+        return new IfStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount),

+                         (BlockStmt)SubstituteNamedExpr(stmt.Thn, p, E, ref subCount),

+                                    SubstituteNamedExpr(stmt.Els, p, E, ref subCount));

+      } else if (s is AlternativeStmt) {

+        return s;

+      } else if (s is WhileStmt) {

+        WhileStmt stmt = (WhileStmt)s;

+        return new WhileStmt(stmt.Tok, SubstituteNamedExpr(stmt.Guard, p, E, ref subCount), stmt.Invariants, stmt.Decreases, stmt.Mod, (BlockStmt)SubstituteNamedExpr(stmt.Body, p, E, ref subCount));

+      } else if (s is AlternativeLoopStmt) {

+        return s;

+      } else if (s is ParallelStmt) {

+        return s;

+      } else if (s is MatchStmt) {

+        return s;

+      } else if (s is SkeletonStatement) {

+        return s;

+      } else {

+        Contract.Assert(false);  // unexpected statement

+        throw new cce.UnreachableException();

+      }

 

+    }

+    private Expression SubstituteNamedExpr(Expression expr, IToken p, Expression E, ref int subCount) {

+      if (expr == null) {

+        return null;

+      }

+      if (expr is NamedExpr) {

+        NamedExpr n = (NamedExpr)expr;

+        if (n.Name == p.val) {

+          subCount++;

+          return new NamedExpr(n.tok, n.Name, E, CloneExpr(n.Body), p);

+        } else return new NamedExpr(n.tok, n.Name, SubstituteNamedExpr(n.Body, p, E, ref subCount));

+      } else if (expr is LiteralExpr || expr is WildcardExpr | expr is ThisExpr || expr is IdentifierExpr) {

+        return expr;

+      } else if (expr is DisplayExpression) {

+        DisplayExpression e = (DisplayExpression)expr;

+        List<Expression> newElements = SubstituteNamedExprList(e.Elements, p, E, ref subCount);

+        if (expr is SetDisplayExpr) {

+          return new SetDisplayExpr(expr.tok, newElements);

+        } else if (expr is MultiSetDisplayExpr) {

+          return new MultiSetDisplayExpr(expr.tok, newElements);

+        } else {

+          return new SeqDisplayExpr(expr.tok, newElements);

+        }

+      } else if (expr is FieldSelectExpr) {

+        FieldSelectExpr fse = (FieldSelectExpr)expr;

+        Expression substE = SubstituteNamedExpr(fse.Obj, p, E, ref subCount);

+        return new FieldSelectExpr(fse.tok, substE, fse.FieldName);

+      } else if (expr is SeqSelectExpr) {

+        SeqSelectExpr sse = (SeqSelectExpr)expr;

+        Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);

+        Expression e0 = sse.E0 == null ? null : SubstituteNamedExpr(sse.E0, p, E, ref subCount);

+        Expression e1 = sse.E1 == null ? null : SubstituteNamedExpr(sse.E1, p, E, ref subCount);

+        return new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr sse = (SeqUpdateExpr)expr;

+        Expression seq = SubstituteNamedExpr(sse.Seq, p, E, ref subCount);

+        Expression index = SubstituteNamedExpr(sse.Index, p, E, ref subCount);

+        Expression val = SubstituteNamedExpr(sse.Value, p, E, ref subCount);

+        return new SeqUpdateExpr(sse.tok, seq, index, val);

+      } else if (expr is MultiSelectExpr) {

+        MultiSelectExpr mse = (MultiSelectExpr)expr;

+        Expression array = SubstituteNamedExpr(mse.Array, p, E, ref subCount);

+        List<Expression> newArgs = SubstituteNamedExprList(mse.Indices, p, E, ref subCount);

+        return new MultiSelectExpr(mse.tok, array, newArgs);

+      } else if (expr is FunctionCallExpr) {

+        FunctionCallExpr e = (FunctionCallExpr)expr;

+        Expression receiver = SubstituteNamedExpr(e.Receiver, p, E, ref subCount);

+        List<Expression> newArgs = SubstituteNamedExprList(e.Args, p, E, ref subCount);

+        return new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);

+      } else if (expr is DatatypeValue) {

+        DatatypeValue dtv = (DatatypeValue)expr;

+        List<Expression> newArgs = SubstituteNamedExprList(dtv.Arguments, p, E, ref subCount);

+        return new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);

+      } else if (expr is OldExpr) {

+        OldExpr e = (OldExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new OldExpr(expr.tok, se);

+      } else if (expr is FreshExpr) {

+        FreshExpr e = (FreshExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new FreshExpr(expr.tok, se);

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new AllocatedExpr(expr.tok, se);

+      } else if (expr is UnaryExpr) {

+        UnaryExpr e = (UnaryExpr)expr;

+        Expression se = SubstituteNamedExpr(e.E, p, E, ref subCount);

+        return new UnaryExpr(expr.tok, e.Op, se);

+      } else if (expr is BinaryExpr) {

+        BinaryExpr e = (BinaryExpr)expr;

+        Expression e0 = SubstituteNamedExpr(e.E0, p, E, ref subCount);

+        Expression e1 = SubstituteNamedExpr(e.E1, p, E, ref subCount);

+        return new BinaryExpr(expr.tok, e.Op, e0, e1);

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        var rhss = SubstituteNamedExprList(e.RHSs, p, E, ref subCount);

+        var body = SubstituteNamedExpr(e.Body, p, E, ref subCount);

+        return new LetExpr(e.tok, e.Vars, rhss, body);

+      } else if (expr is ComprehensionExpr) {

+        var e = (ComprehensionExpr)expr;

+        Expression newRange = e.Range == null ? null : SubstituteNamedExpr(e.Range, p, E, ref subCount);

+        Expression newTerm = SubstituteNamedExpr(e.Term, p, E, ref subCount);

+        Attributes newAttrs = e.Attributes;//SubstituteNamedExpr(e.Attributes, p, E, ref subCount);

+        if (e is SetComprehension) {

+          return new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+        } else if (e is MapComprehension) {

+          return new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+        } else if (e is QuantifierExpr) {

+          var q = (QuantifierExpr)e;

+          if (expr is ForallExpr) {

+            return new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+          } else {

+            return new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+          }

+        } else {

+          Contract.Assert(false);  // unexpected ComprehensionExpr

+          throw new cce.UnreachableException();

+        }

+

+      } else if (expr is PredicateExpr) {

+        var e = (PredicateExpr)expr;

+        Expression g = SubstituteNamedExpr(e.Guard, p, E, ref subCount);

+        Expression b = SubstituteNamedExpr(e.Body, p, E, ref subCount);

+        if (expr is AssertExpr) {

+          return new AssertExpr(e.tok, g, b);

+        } else {

+          return new AssumeExpr(e.tok, g, b);

+        }

+      } else if (expr is ITEExpr) {

+        ITEExpr e = (ITEExpr)expr;

+        Expression test = SubstituteNamedExpr(e.Test, p, E, ref subCount);

+        Expression thn = SubstituteNamedExpr(e.Thn, p, E, ref subCount);

+        Expression els = SubstituteNamedExpr(e.Els, p, E, ref subCount);

+        return new ITEExpr(expr.tok, test, thn, els);

+      } else if (expr is ConcreteSyntaxExpression) {

+        if (expr is ParensExpression) {

+          return SubstituteNamedExpr(((ParensExpression)expr).E, p, E, ref subCount);

+        } else if (expr is IdentifierSequence) {

+          return expr;

+        } else if (expr is ExprDotName) {

+          ExprDotName edn = (ExprDotName)expr;

+          return new ExprDotName(edn.tok, SubstituteNamedExpr(edn.Obj, p, E, ref subCount), edn.SuffixName);

+        } else if (expr is ChainingExpression) {

+          ChainingExpression ch = (ChainingExpression)expr;

+          return SubstituteNamedExpr(ch.E, p, E, ref subCount);

+        } else {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        }

+      } else {

+        Contract.Assert(false);

+        throw new cce.UnreachableException();

+      }

+    }

+

+    private List<Expression> SubstituteNamedExprList(List<Expression> list, IToken p, Expression E, ref int subCount) {

+      List<Expression> res = new List<Expression>();

+      foreach (Expression e in list) {

+        res.Add(SubstituteNamedExpr(e, p, E, ref subCount));

+      }

+      return res;

+    }

     void CheckAgreement_TypeParameters(IToken tok, List<TypeParameter> old, List<TypeParameter> nw, string name, string thing) {

       Contract.Requires(tok != null);

       Contract.Requires(old != null);

@@ -915,7 +1146,8 @@ namespace Microsoft.Dafny {
            *   while (G) LoopSpec ...      while (*) LoopSpec' Body     while (G) Merge(LoopSpec,LoopSpec') Body

            *   while (G) LoopSpec Body     while (*) LoopSpec' Body'    while (G) Merge(LoopSpec,LoopSpec') Merge(Body,Body')

            *   

-           *   ...; S                      StmtThatDoesNotMatchS; S'    StatementThatDoesNotMatchS; Merge( ...;S , S')

+           *   ... where x = e; S          StmtThatDoesNotMatchS; S'    StatementThatDoesNotMatchS[e/x]; Merge( ... where x = e; S , S')

+           *   ... where x = e; S          StmtThatMatchesS; S'         StmtThatMatchesS; S'

            * 

            * Note, LoopSpec must contain only invariant declarations (as the parser ensures for the first three cases).

            * Note, there is an implicit "...;" at the end of every block in a skeleton.

@@ -924,23 +1156,26 @@ namespace Microsoft.Dafny {
            */

           if (cur is SkeletonStatement) {

             var S = ((SkeletonStatement)cur).S;

+            var c = (SkeletonStatement) cur;

             if (S == null) {

-              if (i + 1 == skeleton.Body.Count) {

-                // this "...;" is the last statement of the skeleton, so treat it like the default case

+              var nxt = i + 1 == skeleton.Body.Count ? null : skeleton.Body[i+1];

+              if (nxt != null && nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {

+                // "...; ...;" is the same as just "...;", so skip this one

               } else {

-                var nxt = skeleton.Body[i+1];

-                if (nxt is SkeletonStatement && ((SkeletonStatement)nxt).S == null) {

-                  // "...; ...;" is the same as just "...;", so skip this one

-                } else {

-                  // skip up until the next thing that matches "nxt"

-                  while (!PotentialMatch(nxt, oldS)) {

-                    // loop invariant:  oldS == oldStmt.Body[j]

-                    body.Add(CloneStmt(oldS));

-                    j++;

-                    if (j == oldStmt.Body.Count) { break; }

-                    oldS = oldStmt.Body[j];

-                  }

+                int subCount = 0;

+                // skip up until the next thing that matches "nxt"

+                while (nxt == null || !PotentialMatch(nxt, oldS)) {

+                  // loop invariant:  oldS == oldStmt.Body[j]

+                  var s = CloneStmt(oldS);

+                  if (c.NameReplacements != null)

+                    s = SubstituteNamedExpr(s, c.NameReplacements[0], c.ExprReplacements[0], ref subCount);

+                  body.Add(s);

+                  j++;

+                  if (j == oldStmt.Body.Count) { break; }

+                  oldS = oldStmt.Body[j];

                 }

+                if (c.NameReplacements != null && subCount == 0)

+                  reporter.Error(c.NameReplacements[0], "did not find expression labeled {0}", c.NameReplacements[0].val);

               }

               i++;

 

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c3eccb51..71210c9f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -97,6 +97,7 @@ namespace Microsoft.Dafny {
     readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();

     readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();

     readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();

+    ModuleSignature systemNameInfo = null;

     public Resolver(Program prog) {

       Contract.Requires(prog != null);

       builtIns = prog.BuiltIns;

@@ -142,7 +143,7 @@ namespace Microsoft.Dafny {
       var refinementTransformer = new RefinementTransformer(this);

       

       IRewriter rewriter = new AutoContractsRewriter();

-      var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);

+      systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);

       foreach (var decl in sortedDecls) {

         if (decl is LiteralModuleDecl) {

           // The declaration is a literal module, so it has members and such that we need

@@ -171,18 +172,16 @@ namespace Microsoft.Dafny {
           }

           literalDecl.Signature = RegisterTopLevelDecls(m);

           literalDecl.Signature.Refines = refinedSig;

+          var sig = literalDecl.Signature;

           // set up environment

-          moduleInfo = MergeSignature(literalDecl.Signature, systemNameInfo);

-          // resolve

-          var datatypeDependencies = new Graph<IndDatatypeDecl>();

-          int prevErrorCount = ErrorCount;

-          ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

-          if (ErrorCount == prevErrorCount)

-          ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+          var errorCount = ErrorCount;

+          ResolveModuleDefinition(m, sig);

 

-          refinementTransformer.PostResolve(m);

-          // give rewriter a chance to do processing

-          rewriter.PostResolve(m);

+          if (ErrorCount == errorCount) {

+            refinementTransformer.PostResolve(m);

+            // give rewriter a chance to do processing

+            rewriter.PostResolve(m);

+          }

         } else if (decl is AliasModuleDecl) {

           var alias = (AliasModuleDecl)decl;

           // resolve the path

@@ -194,16 +193,11 @@ namespace Microsoft.Dafny {
           }

         } else if (decl is AbstractModuleDecl) {

           var abs = (AbstractModuleDecl)decl;

-          ModuleSignature p; ModuleDefinition mod;

+          ModuleSignature p;

           if (ResolvePath(abs.Root, abs.Path, out p)) {

-            abs.Signature = MakeAbstractSignature(p, abs.Name, abs.Height, out mod);

+            abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules);

             abs.OriginalSignature = p;

-            moduleInfo = MergeSignature(abs.Signature, systemNameInfo);

             // resolve

-            var datatypeDependencies = new Graph<IndDatatypeDecl>();

-            ResolveTopLevelDecls_Signatures(mod.TopLevelDecls, datatypeDependencies);

-            ResolveTopLevelDecls_Meat(mod.TopLevelDecls, datatypeDependencies);

-            prog.Modules.Add(mod);

           } else {

             abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature

           }

@@ -212,23 +206,26 @@ namespace Microsoft.Dafny {
       }

       // compute IsRecursive bit for mutually recursive functions

       foreach (ModuleDefinition m in prog.Modules) {

-        foreach (TopLevelDecl decl in m.TopLevelDecls) {

-          ClassDecl cl = decl as ClassDecl;

-          if (cl != null) {

-            foreach (MemberDecl member in cl.Members) {

-              Function fn = member as Function;

-              if (fn != null && !fn.IsRecursive) {  // note, self-recursion has already been determined

-                int n = m.CallGraph.GetSCCSize(fn);

-                if (2 <= n) {

-                  // the function is mutually recursive (note, the SCC does not determine self recursion)

-                  fn.IsRecursive = true;

-                }

-              }

+        foreach (var fn in ModuleDefinition.AllFunctions(m.TopLevelDecls)) {

+          if (!fn.IsRecursive) {  // note, self-recursion has already been determined

+            int n = m.CallGraph.GetSCCSize(fn);

+            if (2 <= n) {

+              // the function is mutually recursive (note, the SCC does not determine self recursion)

+              fn.IsRecursive = true;

             }

           }

         }

       }

-      

+    }

+

+    private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {

+      moduleInfo = MergeSignature(sig, systemNameInfo);

+      // resolve

+      var datatypeDependencies = new Graph<IndDatatypeDecl>();

+      int prevErrorCount = ErrorCount;

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

+      if (ErrorCount == prevErrorCount)

+        ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

     }

 

 

@@ -362,12 +359,17 @@ namespace Microsoft.Dafny {
       foreach (var kv in m.Ctors) {

         info.Ctors[kv.Key] = kv.Value;

       }

+      foreach (var kv in m.StaticMembers) {

+        info.StaticMembers[kv.Key] = kv.Value;

+      }

+      info.IsGhost = m.IsGhost;

       return info;

     }

     ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {

       Contract.Requires(moduleDef != null);

       var sig = new ModuleSignature();

       sig.ModuleDef = moduleDef;

+      sig.IsGhost = moduleDef.IsGhost;

       List<TopLevelDecl> declarations = moduleDef.TopLevelDecls;

 

       foreach (TopLevelDecl d in declarations) {

@@ -402,7 +404,13 @@ namespace Microsoft.Dafny {
             }

           }

           cl.HasConstructor = hasConstructor;

-

+          if (cl.IsDefaultClass) {

+            foreach (MemberDecl m in cl.Members) {

+              if (!sig.StaticMembers.ContainsKey(m.Name) && m.IsStatic && (m is Function || m is Method)) {

+                sig.StaticMembers.Add(m.Name, m);

+              }

+            }

+          }

         } else {

           DatatypeDecl dt = (DatatypeDecl)d;

 

@@ -447,7 +455,7 @@ namespace Microsoft.Dafny {
                 if (members.ContainsKey(formal.Name)) {

                   Error(ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);

                 } else {

-                  dtor = new DatatypeDestructor(formal.tok, ctor, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);

+                  dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.Name, "", "", formal.IsGhost, formal.Type, null);

                   dtor.EnclosingClass = dt;  // resolve here

                   members.Add(formal.Name, dtor);

                 }

@@ -460,17 +468,19 @@ namespace Microsoft.Dafny {
       return sig;

     }

 

-    private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, out ModuleDefinition mod) {

-      mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null);

+    private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List<ModuleDefinition> mods) {

+      var mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null, false);

       mod.Height = Height;

       foreach (var kv in p.TopLevels) {

-        mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod));

+        mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));

       }

       var sig = RegisterTopLevelDecls(mod);

       sig.Refines = p.Refines;

+      mods.Add(mod);

+      ResolveModuleDefinition(mod, sig);

       return sig;

     }

-    TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {

+    TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m, List<ModuleDefinition> mods, string Name) {

       Contract.Requires(d != null);

       Contract.Requires(m != null);

 

@@ -493,8 +503,9 @@ namespace Microsoft.Dafny {
         var dd = (ClassDecl)d;

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

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

-        var cl = new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);

-        return cl;

+        if (dd is DefaultClassDecl) {

+          return new DefaultClassDecl(m, mm);

+        } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null); 

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

           return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);

@@ -504,9 +515,17 @@ namespace Microsoft.Dafny {
           alias.ModuleReference = a.ModuleReference;

           alias.Signature = a.Signature;

           return alias;

+        } else if (d is AbstractModuleDecl) {

+          var abs = (AbstractModuleDecl)d;

+          var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);

+          var a = new AbstractModuleDecl(abs.Path, abs.tok, m);

+          a.Signature = sig;

+          a.OriginalSignature = abs.OriginalSignature;

+          return a;

+        } else {

+          Contract.Assert(false);  // unexpected declaration

+          return null;  // to please compiler

         }

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

-        return null;  // to please compiler

       } else {

         Contract.Assert(false);  // unexpected declaration

         return null;  // to please compiler

@@ -551,7 +570,7 @@ namespace Microsoft.Dafny {
         return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

       } else if (t is UserDefinedType) {

         var tt = (UserDefinedType)t;

-        return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : tt.ModuleName);

+        return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x));

       } else if (t is InferredTypeProxy) {

         return new InferredTypeProxy();

       } else {

@@ -574,6 +593,9 @@ namespace Microsoft.Dafny {
       if (f is Predicate) {

         return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

           req, reads, ens, decreases, body, false, null, false);

+      } else if (f is CoPredicate) {

+        return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

+          req, reads, ens, body, null, false);

       } else {

         return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),

           req, reads, ens, decreases, body, null, false);

@@ -784,7 +806,7 @@ namespace Microsoft.Dafny {
       }

       return i == Path.Count;

     }

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

+    public void ResolveTopLevelDecls_Signatures(ModuleDefinition def, List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies) {

       Contract.Requires(declarations != null);

       Contract.Requires(datatypeDependencies != null);  // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies));

       foreach (TopLevelDecl d in declarations) {

@@ -796,7 +818,18 @@ namespace Microsoft.Dafny {
         } else if (d is ClassDecl) {

           ResolveClassMemberTypes((ClassDecl)d);

         } else if (d is ModuleDecl) {

-          // TODO: what goes here?

+          var decl = (ModuleDecl)d;

+          if (!def.IsGhost) {

+            if (decl.Signature.IsGhost) {

+              if (!(def.IsDefaultModule)) // _module is allowed to contain ghost modules, but not by ghost itself. Note this presents a challenge to 

+                                          // trusted verification, as toplevels can't be trusted if they invoke ghost module members.

+                Error(d.tok, "ghost modules can only be imported into other ghost modules, not physical ones.");

+            } else {

+              // physical modules are allowed everywhere

+            }

+          } else {

+            // everything is allowed in a ghost module

+          }

         } else {

           ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies);

         }

@@ -829,29 +862,25 @@ namespace Microsoft.Dafny {
           DetermineEqualitySupport(dtd, datatypeDependencies);

         }

       }

+

       if (ErrorCount == prevErrorCount) {  // because CheckCoCalls requires the given expression to have been successfully resolved

         // Perform the guardedness check on co-datatypes

-        foreach (var decl in declarations) {

-          var cl = decl as ClassDecl;

-          if (cl != null) {

-            foreach (var member in cl.Members) {

-              var fn = member as Function;

-              if (fn != null && fn.Body != null && cl.Module.CallGraph.GetSCCRepresentative(fn) == fn) {

-                bool dealsWithCodatatypes = false;

-                foreach (var m in cl.Module.CallGraph.GetSCC(fn)) {

-                  var f = (Function)m;

-                  if (f.ResultType.InvolvesCoDatatype) {

-                    dealsWithCodatatypes = true;

-                    break;

-                  }

-                }

-                foreach (var m in cl.Module.CallGraph.GetSCC(fn)) {

-                  var f = (Function)m;

-                  var checker = new CoCallResolution(f, dealsWithCodatatypes);

-                  checker.CheckCoCalls(f.Body);

-                }

+        foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {

+          var module = fn.EnclosingClass.Module;

+          if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) {

+            bool dealsWithCodatatypes = false;

+            foreach (var m in module.CallGraph.GetSCC(fn)) {

+              var f = (Function)m;

+              if (f.ResultType.InvolvesCoDatatype) {

+                dealsWithCodatatypes = true;

+                break;

               }

             }

+            foreach (var m in module.CallGraph.GetSCC(fn)) {

+              var f = (Function)m;

+              var checker = new CoCallResolution(f, dealsWithCodatatypes);

+              checker.CheckCoCalls(f.Body);

+            }

           }

         }

         // Inferred required equality support for datatypes and for Function and Method signatures

@@ -978,9 +1007,85 @@ namespace Microsoft.Dafny {
             }

           }

         }

+        // Check that copredicates are not recursive with non-copredicate functions.

+        foreach (var fn in ModuleDefinition.AllFunctions(declarations)) {

+          if (fn.Body != null && (fn is CoPredicate || fn.IsRecursive)) {

+            CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);

+          }

+        }

       }

     }

 

+    enum CallingPosition { Positive, Negative, Neither }

+

+    static CallingPosition Invert(CallingPosition cp) {

+      switch (cp) {

+        case CallingPosition.Positive: return CallingPosition.Negative;

+        case CallingPosition.Negative: return CallingPosition.Positive;

+        default: return CallingPosition.Neither;

+      }

+    }

+

+    void CoPredicateChecks(Expression expr, Function context, CallingPosition cp) {

+      Contract.Requires(expr != null);

+      Contract.Requires(context != null);

+      if (expr is ConcreteSyntaxExpression) {

+        var e = (ConcreteSyntaxExpression)expr;

+        CoPredicateChecks(e.Resolved, context, cp);

+        return;

+      } else  if (expr is FunctionCallExpr) {

+        var e = (FunctionCallExpr)expr;

+        var moduleCaller = context.EnclosingClass.Module;

+        var moduleCallee = e.Function.EnclosingClass.Module;

+        if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {

+          // we're looking at a recursive call

+          if (context is CoPredicate) {

+            if (!(e.Function is CoPredicate)) {

+              Error(e, "a recursive call from a copredicate can go only to other copredicates");

+            } else if (cp != CallingPosition.Positive) {

+              Error(e, "a recursive copredicate call can only be done in positive positions");

+            }

+          } else if (e.Function is CoPredicate) {

+            Error(e, "a recursive call from a non-copredicate can go only to other non-copredicates");

+          }

+        }

+        // fall through to do the subexpressions

+      } else if (expr is UnaryExpr) {

+        var e = (UnaryExpr)expr;

+        if (e.Op == UnaryExpr.Opcode.Not) {

+          CoPredicateChecks(e.E, context, Invert(cp));

+          return;

+        }

+      } else if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        switch (e.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.And:

+          case BinaryExpr.ResolvedOpcode.Or:

+            CoPredicateChecks(e.E0, context, cp);

+            CoPredicateChecks(e.E1, context, cp);

+            return;

+          case BinaryExpr.ResolvedOpcode.Imp:

+            CoPredicateChecks(e.E0, context, Invert(cp));

+            CoPredicateChecks(e.E1, context, cp);

+            return;

+          default:

+            break;

+        }

+      } else if (expr is LetExpr) {

+        var e = (LetExpr)expr;

+        CoPredicateChecks(e.Body, context, cp);

+        return;

+      } else if (expr is QuantifierExpr) {

+        var e = (QuantifierExpr)expr;

+        if (e.Range != null) {

+          CoPredicateChecks(e.Range, context, e is ExistsExpr ? Invert(cp) : cp);

+        }

+        CoPredicateChecks(e.Term, context, cp);

+        return;

+      }

+      expr.SubExpressions.Iter(ee => CoPredicateChecks(ee, context, CallingPosition.Neither));

+    }

+

     void CheckEqualityTypes_Stmt(Statement stmt) {

       Contract.Requires(stmt != null);

       if (stmt.IsGhost) {

@@ -1848,7 +1953,7 @@ namespace Microsoft.Dafny {
             Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");

           }

         }

-        TypeParameter tp = t.ModuleName == null ? allTypeParameters.Find(t.Name) : null;

+        TypeParameter tp = t.Path.Count == 0 ? allTypeParameters.Find(t.Name) : null;

         if (tp != null) {

           if (t.TypeArgs.Count == 0) {

             t.ResolvedParam = tp;

@@ -1857,17 +1962,26 @@ namespace Microsoft.Dafny {
           }

         } else if (t.ResolvedClass == null) {  // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')

           TopLevelDecl d = null;

-          if (t.ModuleName != null) {

-            ModuleSignature sig;

-            if (moduleInfo.FindSubmodule(t.ModuleName.val, out sig)) {

-              if (!sig.TopLevels.TryGetValue(t.Name, out d)) {

-                Error(t.tok, "The name does not exist in the given module");

-              }

+

+          int j = 0;

+          var sig = moduleInfo;

+          while (j < t.Path.Count) {

+            if (sig.FindSubmodule(t.Path[j].val, out sig)) {

+              j++;

             } else {

-              Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);

+              Error(t.Path[j], "module {0} does not exist", t.Path[j].val);

+              break;

             }

-          } else if (!moduleInfo.TopLevels.TryGetValue(t.Name, out d)) {

-            Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);

+          }

+          if (j == t.Path.Count) {

+            if (!sig.TopLevels.TryGetValue(t.Name, out d)) {

+              if (j == 0)

+                Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget to qualify a name?)", t.Name);

+              else

+                Error(t.tok, "Undeclared type {0} in module {1}", t.Name, t.Path[t.Path.Count - 1].val);

+            }

+          } else {

+            // error has already been reported

           }

 

           if (d == null) {

@@ -3488,44 +3602,9 @@ namespace Microsoft.Dafny {
         } else if (d is AmbiguousTopLevelDecl) {

           Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());

         } else if (!(d is DatatypeDecl)) {

-          Error(expr.tok, "Expected datatype, found class: {0}", dtv.DatatypeName);

+          Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);

         } else {

-          // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)

-          DatatypeDecl dt = (DatatypeDecl)d;

-          List<Type> gt = new List<Type>(dt.TypeArgs.Count);

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

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

-            Type t = new InferredTypeProxy();

-            gt.Add(t);

-            dtv.InferredTypeArgs.Add(t);

-            subst.Add(dt.TypeArgs[i], t);

-          }

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

-          ResolveType(expr.tok, expr.Type, null, true);

-

-          DatatypeCtor ctor;

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

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

-          } else {

-            Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

-            dtv.Ctor = ctor;

-            if (ctor.Formals.Count != dtv.Arguments.Count) {

-              Error(expr.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);

-            }

-          }

-          int j = 0;

-          foreach (Expression arg in dtv.Arguments) {

-            Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

-            ResolveExpression(arg, twoState, null);

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

-            if (formal != null) {

-              Type st = SubstType(formal.Type, subst);

-              if (!UnifyTypes(arg.Type, st)) {

-                Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);

-              }

-            }

-            j++;

-          }

+          ResolveDatatypeValue(twoState, dtv, (DatatypeDecl)d);

         }

 

       } else if (expr is DisplayExpression) {

@@ -3892,7 +3971,12 @@ namespace Microsoft.Dafny {
         scope.PopMarker();

         expr.Type = e.Body.Type;

 

-      } else if (expr is QuantifierExpr) {

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        ResolveExpression(e.Body, twoState);

+        if (e.Contract != null) ResolveExpression(e.Contract, twoState);

+        e.Type = e.Body.Type;

+      }else if (expr is QuantifierExpr) {

         QuantifierExpr e = (QuantifierExpr)expr;

         int prevErrorCount = ErrorCount;

         scope.PushMarker();

@@ -4156,6 +4240,44 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private void ResolveDatatypeValue(bool twoState, DatatypeValue dtv, DatatypeDecl dt) {

+      // this resolution is a little special, in that the syntax shows only the base name, not its instantiation (which is inferred)

+      List<Type> gt = new List<Type>(dt.TypeArgs.Count);

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

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

+        Type t = new InferredTypeProxy();

+        gt.Add(t);

+        dtv.InferredTypeArgs.Add(t);

+        subst.Add(dt.TypeArgs[i], t);

+      }

+      // Construct a resolved type directly, as we know the declaration is dt.

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

+      

+      DatatypeCtor ctor;

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

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

+      } else {

+        Contract.Assert(ctor != null);  // follows from postcondition of TryGetValue

+        dtv.Ctor = ctor;

+        if (ctor.Formals.Count != dtv.Arguments.Count) {

+          Error(dtv.tok, "wrong number of arguments to datatype constructor {0} (found {1}, expected {2})", dtv.DatatypeName, dtv.Arguments.Count, ctor.Formals.Count);

+        }

+      }

+      int j = 0;

+      foreach (Expression arg in dtv.Arguments) {

+        Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

+        ResolveExpression(arg, twoState, null);

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

+        if (formal != null) {

+          Type st = SubstType(formal.Type, subst);

+          if (!UnifyTypes(arg.Type, st)) {

+            Error(arg.tok, "incorrect type of datatype constructor argument (found {0}, expected {1})", arg.Type, st);

+          }

+        }

+        j++;

+      }

+    }

+

     private bool ComparableTypes(Type A, Type B) {

       if (A.IsArrayType && B.IsArrayType) {

         Type a = UserDefinedType.ArrayElementType(A);

@@ -4253,7 +4375,8 @@ namespace Microsoft.Dafny {
       } else if (expr is DatatypeValue) {

         var e = (DatatypeValue)expr;

         // check all NON-ghost arguments

-        for (int i = 0; i < e.Ctor.Formals.Count; i++) {

+        // note that if resolution is successful, then |e.Arguments| == |e.Ctor.Formals|

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

           if (!e.Ctor.Formals[i].IsGhost) {

             CheckIsNonGhost(e.Arguments[i]);

           }

@@ -4297,6 +4420,9 @@ namespace Microsoft.Dafny {
           }

           return;

         }

+      } else if (expr is NamedExpr) {

+        if (moduleInfo.IsGhost) return;

+        else CheckIsNonGhost(((NamedExpr)expr).Body);

       }

 

       foreach (var ee in expr.SubExpressions) {

@@ -4331,6 +4457,9 @@ namespace Microsoft.Dafny {
       } else {

         Function function = (Function)member;

         e.Function = function;

+        if (function is CoPredicate) {

+          ((CoPredicate)function).Uses.Add(e);

+        }

         if (e.Receiver is StaticReceiverExpr && !function.IsStatic) {

           Error(e, "an instance function must be selected via an object, not just a class name");

         }

@@ -4402,9 +4531,9 @@ namespace Microsoft.Dafny {
       //       (if two imported types have the same name, an error message is produced here)

       //  - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)

       //  - imported module name

-      //  - field name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

-      // Note, at present, modules do not give rise to new namespaces, which is something that should

-      // be changed in the language when modules are given more attention.

+      //  - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")

+      //  - static function or method in the enclosing module.

+      

       Expression r = null;  // resolved version of e

       CallRhs call = null;

 

@@ -4466,18 +4595,20 @@ namespace Microsoft.Dafny {
           }

         }

 

-      } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) {

+      } else if ((classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))

+                 || moduleInfo.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

+      {

         // ----- field, function, or method

         Expression receiver;

         if (member.IsStatic) {

-          receiver = new StaticReceiverExpr(id, currentClass);

+          receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

         } else {

           if (!scope.AllowInstance) {

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

             // nevertheless, set "receiver" to a value so we can continue resolution

           }

           receiver = new ImplicitThisExpr(id);

-          receiver.Type = GetThisType(id, currentClass);  // resolve here

+          receiver.Type = GetThisType(id, (ClassDecl)member.EnclosingClass);  // resolve here

         }

         r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, out call);

 

@@ -4498,10 +4629,11 @@ namespace Microsoft.Dafny {
       return call;

     }

 

-    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature info, bool twoState, bool allowMethodCall) {

+    CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, bool allowMethodCall) {

       // Look up "id" as follows:

       //  - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)

       //       (if two imported types have the same name, an error message is produced here)

+      //  - static function or method of sig.

       // This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but

       // should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored.

       Contract.Requires(p < e.Tokens.Count);

@@ -4509,8 +4641,10 @@ namespace Microsoft.Dafny {
       CallRhs call = null;

 

       TopLevelDecl decl;

+      MemberDecl member;

+      Tuple<DatatypeCtor, bool> pair;

       var id = e.Tokens[p];

-      if (info.TopLevels.TryGetValue(id.val, out decl)) {

+      if (sig.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

           Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());

         } else if (decl is ClassDecl) {

@@ -4529,11 +4663,33 @@ namespace Microsoft.Dafny {
           var dt = (DatatypeDecl)decl;  // otherwise, unexpected TopLevelDecl

           var args = (e.Tokens.Count == p + 2 ? e.Arguments : null) ?? new List<Expression>();

           r = new DatatypeValue(id, id.val, e.Tokens[p + 1].val, args);

-          ResolveExpression(r, twoState);

+          ResolveDatatypeValue(twoState, (DatatypeValue) r, dt);

           if (e.Tokens.Count != p + 2) {

             r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);

           }

         }

+      } else if (sig.Ctors.TryGetValue(id.val, out pair)) {

+        // ----- root is a datatype constructor

+        if (pair.Item2) {

+          // there is more than one constructor with this name

+          Error(id, "the name '{0}' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, '{1}.{0}')", id.val, pair.Item1.EnclosingDatatype.Name);

+        } else {

+          var dt = pair.Item1.EnclosingDatatype;

+          var args = (e.Tokens.Count == p+1 ? e.Arguments : null) ?? new List<Expression>();

+          r = new DatatypeValue(id, dt.Name, id.val, args);

+          ResolveDatatypeValue(twoState, (DatatypeValue)r, dt);

+          if (e.Tokens.Count != p+1) {

+            r = ResolveSuffix(r, e, p+1, twoState, allowMethodCall, out call);

+          }

+        }

+      } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.

+      {

+        // ----- function, or method

+        Expression receiver;

+        Contract.Assert(member.IsStatic);

+        receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);

+        r = ResolveSuffix(receiver, e, p, twoState, allowMethodCall, out call);

+

       } else {

         Error(id, "unresolved identifier: {0}", id.val);

         // resolve arguments, if any

@@ -5303,6 +5459,8 @@ namespace Microsoft.Dafny {
           return true;

         }

         return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);

+      }  else if (expr is NamedExpr) {

+         return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body);

       } else if (expr is ComprehensionExpr) {

         if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) {

           return true;  // the quantifier cannot be compiled if the resolver found no bounds

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index af41a679..4dea968e 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -322,7 +322,7 @@ namespace Microsoft.Dafny
       return true;

     }

 

-    BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {

+    public static BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {

       var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);

       p.ResolvedOp = rop;

       p.Type = Type.Bool;

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 32c92a8b..1bfa80a0 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 107;

-	const int noSym = 107;

+	const int maxT = 110;

+	const int noSym = 110;

 

 

 	[ContractInvariantMethod]

@@ -516,33 +516,36 @@ public class Scanner {
 			case "object": t.kind = 44; break;

 			case "function": t.kind = 45; break;

 			case "predicate": t.kind = 46; break;

-			case "reads": t.kind = 47; break;

-			case "label": t.kind = 50; break;

-			case "break": t.kind = 51; break;

-			case "return": t.kind = 52; break;

-			case "assume": t.kind = 55; break;

-			case "new": t.kind = 56; break;

-			case "choose": t.kind = 59; break;

-			case "if": t.kind = 60; break;

-			case "else": t.kind = 61; break;

-			case "case": t.kind = 62; break;

-			case "while": t.kind = 64; break;

-			case "invariant": t.kind = 65; break;

-			case "match": t.kind = 66; break;

-			case "assert": t.kind = 67; break;

-			case "print": t.kind = 68; break;

-			case "parallel": t.kind = 69; break;

-			case "in": t.kind = 82; break;

-			case "false": t.kind = 92; break;

-			case "true": t.kind = 93; break;

-			case "null": t.kind = 94; break;

-			case "this": t.kind = 95; break;

-			case "fresh": t.kind = 96; break;

-			case "allocated": t.kind = 97; break;

-			case "old": t.kind = 98; break;

-			case "then": t.kind = 99; break;

-			case "forall": t.kind = 101; break;

-			case "exists": t.kind = 103; break;

+			case "copredicate": t.kind = 47; break;

+			case "reads": t.kind = 48; break;

+			case "label": t.kind = 51; break;

+			case "break": t.kind = 52; break;

+			case "where": t.kind = 53; break;

+			case "return": t.kind = 54; break;

+			case "assume": t.kind = 57; break;

+			case "new": t.kind = 58; break;

+			case "choose": t.kind = 61; break;

+			case "if": t.kind = 62; break;

+			case "else": t.kind = 63; break;

+			case "case": t.kind = 64; break;

+			case "while": t.kind = 66; break;

+			case "invariant": t.kind = 67; break;

+			case "match": t.kind = 68; break;

+			case "assert": t.kind = 69; break;

+			case "print": t.kind = 70; break;

+			case "parallel": t.kind = 71; break;

+			case "in": t.kind = 84; break;

+			case "false": t.kind = 94; break;

+			case "true": t.kind = 95; break;

+			case "null": t.kind = 96; break;

+			case "this": t.kind = 97; break;

+			case "fresh": t.kind = 98; break;

+			case "allocated": t.kind = 99; break;

+			case "old": t.kind = 100; break;

+			case "then": t.kind = 101; break;

+			case "expr": t.kind = 102; break;

+			case "forall": t.kind = 104; break;

+			case "exists": t.kind = 106; break;

 			default: break;

 		}

 	}

@@ -658,71 +661,71 @@ public class Scanner {
 			case 23:

 				{t.kind = 31; break;}

 			case 24:

-				{t.kind = 48; break;}

-			case 25:

 				{t.kind = 49; break;}

+			case 25:

+				{t.kind = 50; break;}

 			case 26:

-				{t.kind = 53; break;}

+				{t.kind = 55; break;}

 			case 27:

-				{t.kind = 54; break;}

+				{t.kind = 56; break;}

 			case 28:

-				{t.kind = 57; break;}

+				{t.kind = 59; break;}

 			case 29:

-				{t.kind = 58; break;}

+				{t.kind = 60; break;}

 			case 30:

-				{t.kind = 63; break;}

+				{t.kind = 65; break;}

 			case 31:

 				if (ch == '>') {AddCh(); goto case 32;}

 				else {goto case 0;}

 			case 32:

-				{t.kind = 70; break;}

+				{t.kind = 72; break;}

 			case 33:

-				{t.kind = 71; break;}

+				{t.kind = 73; break;}

 			case 34:

-				{t.kind = 72; break;}

+				{t.kind = 74; break;}

 			case 35:

-				{t.kind = 73; break;}

+				{t.kind = 75; break;}

 			case 36:

 				if (ch == '&') {AddCh(); goto case 37;}

 				else {goto case 0;}

 			case 37:

-				{t.kind = 74; break;}

+				{t.kind = 76; break;}

 			case 38:

-				{t.kind = 75; break;}

+				{t.kind = 77; break;}

 			case 39:

-				{t.kind = 76; break;}

+				{t.kind = 78; break;}

 			case 40:

-				{t.kind = 77; break;}

-			case 41:

 				{t.kind = 79; break;}

+			case 41:

+				{t.kind = 81; break;}

 			case 42:

-				{t.kind = 80; break;}

+				{t.kind = 82; break;}

 			case 43:

-				{t.kind = 81; break;}

+				{t.kind = 83; break;}

 			case 44:

-				{t.kind = 84; break;}

+				{t.kind = 86; break;}

 			case 45:

-				{t.kind = 85; break;}

+				{t.kind = 87; break;}

 			case 46:

-				{t.kind = 86; break;}

+				{t.kind = 88; break;}

 			case 47:

-				{t.kind = 87; break;}

+				{t.kind = 89; break;}

 			case 48:

-				{t.kind = 88; break;}

+				{t.kind = 90; break;}

 			case 49:

-				{t.kind = 89; break;}

+				{t.kind = 91; break;}

 			case 50:

-				{t.kind = 90; break;}

+				{t.kind = 92; break;}

 			case 51:

-				{t.kind = 91; break;}

+				{t.kind = 93; break;}

 			case 52:

-				{t.kind = 102; break;}

+				{t.kind = 105; break;}

 			case 53:

-				{t.kind = 104; break;}

+				{t.kind = 107; break;}

 			case 54:

-				{t.kind = 105; break;}

+				{t.kind = 108; break;}

 			case 55:

-				{t.kind = 106; break;}

+				{t.kind = 109; break;}

 			case 56:

 				recEnd = pos; recKind = 5;

 				if (ch == '=') {AddCh(); goto case 26;}

@@ -751,22 +754,22 @@ public class Scanner {
 				if (ch == '=') {AddCh(); goto case 41;}

 				else {t.kind = 27; break;}

 			case 62:

-				recEnd = pos; recKind = 83;

+				recEnd = pos; recKind = 85;

 				if (ch == '=') {AddCh(); goto case 42;}

 				else if (ch == '!') {AddCh(); goto case 43;}

-				else {t.kind = 83; break;}

+				else {t.kind = 85; break;}

 			case 63:

 				recEnd = pos; recKind = 24;

 				if (ch == '>') {AddCh(); goto case 34;}

 				else {t.kind = 24; break;}

 			case 64:

-				recEnd = pos; recKind = 100;

+				recEnd = pos; recKind = 103;

 				if (ch == '.') {AddCh(); goto case 23;}

-				else {t.kind = 100; break;}

+				else {t.kind = 103; break;}

 			case 65:

-				recEnd = pos; recKind = 78;

+				recEnd = pos; recKind = 80;

 				if (ch == '=') {AddCh(); goto case 31;}

-				else {t.kind = 78; break;}

+				else {t.kind = 80; break;}

 

 		}

 		t.val = new String(tval, 0, tlen);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 75a1e174..2758e189 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -26,6 +26,7 @@ namespace Microsoft.Dafny {
     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/*!*/>();

+    readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();

     Program program;

 

     [ContractInvariantMethod]

@@ -53,6 +54,7 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type HeapType;

       public readonly string HeapVarName;

       public readonly Bpl.Type ClassNameType;

+      public readonly Bpl.Type NameFamilyType;

       public readonly Bpl.Type DatatypeType;

       public readonly Bpl.Type DtCtorId;

       public readonly Bpl.Expr Null;

@@ -71,6 +73,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(HeapType != null);

         Contract.Invariant(HeapVarName != null);

         Contract.Invariant(ClassNameType != null);

+        Contract.Invariant(NameFamilyType != null);

         Contract.Invariant(DatatypeType != null);

         Contract.Invariant(DtCtorId != null);

         Contract.Invariant(Null != null);

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

       public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,

                              Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,

-                             Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,

+                             Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType,

                              Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,

                              Bpl.Constant allocField, Bpl.Constant classDotArray) {

         #region Non-null preconditions on parameters

@@ -158,6 +161,7 @@ namespace Microsoft.Dafny {
         this.HeapType = heap.TypedIdent.Type;

         this.HeapVarName = heap.Name;

         this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());

+        this.NameFamilyType = new Bpl.CtorType(Token.NoToken, nameFamilyType, new Bpl.TypeSeq());

         this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());

         this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());

         this.allocField = allocField;

@@ -180,6 +184,7 @@ namespace Microsoft.Dafny {
       Bpl.TypeCtorDecl seqTypeCtor = null;

       Bpl.TypeCtorDecl fieldNameType = null;

       Bpl.TypeCtorDecl classNameType = null;

+      Bpl.TypeCtorDecl nameFamilyType = null;

       Bpl.TypeCtorDecl datatypeType = null;

       Bpl.TypeCtorDecl dtCtorId = null;

       Bpl.TypeCtorDecl boxType = null;

@@ -203,6 +208,8 @@ namespace Microsoft.Dafny {
             dtCtorId = dt;

           } else if (dt.Name == "ref") {

             refType = dt;

+          } else if (dt.Name == "NameFamily") {

+            nameFamilyType = dt;

           } else if (dt.Name == "BoxType") {

             boxType = dt;

           } else if (dt.Name == "TickType") {

@@ -250,6 +257,8 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");

       } else if (classNameType == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");

+      } else if (nameFamilyType == null) {

+        Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily");

       } else if (datatypeType == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");

       } else if (dtCtorId == null) {

@@ -268,7 +277,7 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of class._System.array");

       } else {

         return new PredefinedDecls(refType, boxType, tickType,

-                                   setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,

+                                   setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, nameFamilyType, datatypeType, dtCtorId,

                                    allocField, classDotArray);

       }

       return null;

@@ -310,8 +319,9 @@ namespace Microsoft.Dafny {
     public Bpl.Program Translate(Program p) {

       Contract.Requires(p != null);

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

+      

       program = p;

-

+      

       if (sink == null || predef == null) {

         // something went wrong during construction, which reads the prelude; an error has

         // already been printed, so just return an empty program here (which is non-null)

@@ -333,15 +343,18 @@ namespace Microsoft.Dafny {
             // nothing to do--this is treated just like a type parameter

           } else if (d is DatatypeDecl) {

             AddDatatype((DatatypeDecl)d);

+          } else if (d is ModuleDecl) {

+            // submodules have already been added as a top level module, ignore this.

           } else if (d is ClassDecl) {

             AddClassMembers((ClassDecl)d);

-          } else if (d is ModuleDecl) {

-            // nop, sub-modules are handled in their own iteration.

           } else {

             Contract.Assert(false);

           }

         }

       }

+      foreach(var c in fieldConstants.Values) {

+        sink.TopLevelDeclarations.Add(c);

+      }

       return sink;

     }

 

@@ -396,7 +409,7 @@ namespace Microsoft.Dafny {
         if (bvs.Length != 0) {

           q = new Bpl.ExistsExpr(ctor.tok, bvs, q);

         }

-        q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, dId), q);

+        q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, dId), q);

         q = new Bpl.ForallExpr(ctor.tok, new VariableSeq(dBv), q);

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

 

@@ -525,11 +538,11 @@ namespace Microsoft.Dafny {
       var cases_dId = new Bpl.IdentifierExpr(dt.tok, cases_dBv.Name, predef.DatatypeType);

       Bpl.Expr cases_body = null;

       foreach (DatatypeCtor ctor in dt.Ctors) {

-        var disj = FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, cases_dId);

+        var disj = FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, cases_dId);

         cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj);

       }

       var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-      var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullName, new Bpl.VariableSeq(cases_dBv), cases_resType);

+      var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullCompileName, new Bpl.VariableSeq(cases_dBv), cases_resType);

       cases_fn.Body = cases_body;

       sink.TopLevelDeclarations.Add(cases_fn);

     }

@@ -596,6 +609,9 @@ namespace Microsoft.Dafny {
           }

           AddFrameAxiom(f);

           AddWellformednessCheck(f);

+          if (f is CoPredicate) {

+            AddCoinductionPrinciple((CoPredicate)f);

+          }

 

         } else if (member is Method) {

           Method m = (Method)member;

@@ -706,7 +722,7 @@ namespace Microsoft.Dafny {
     }

 

     void AddFunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {

-      if (f is Predicate) {

+      if (f is Predicate || f is CoPredicate) {

         var ax = FunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, body, ens, specialization, layerOffset);

         sink.TopLevelDeclarations.Add(ax);

         ax = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, body, ens, specialization, layerOffset);

@@ -849,7 +865,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),

           etran.InMethodContext());

       // useViaCanCall: f#canCall(args)

-      Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool);

+      Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);

       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);

 

       // ante := useViaCanCall || (useViaContext && typeAnte && pre)

@@ -865,11 +881,11 @@ namespace Microsoft.Dafny {
         if (layerOffset == 0) {

           meat = Bpl.Expr.And(

             CanCallAssumption(bodyWithSubst, etran),

-            visibility == FunctionAxiomVisibility.ForeignModuleOnly && f is Predicate ?

+            visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?

               Bpl.Expr.Imp(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)) :

               Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));

         } else {

-          meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && f is Predicate ?

+          meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?

             Bpl.Expr.Imp(funcAppl, etran.TrExpr(bodyWithSubst)) :

             Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));

         }

@@ -954,7 +970,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(0 <= layer && layer < 3);

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

 

-      string name = f.FullName;

+      string name = f.FullCompileName;

       switch (layer) {

         case 2: name += "#2"; break;

         case 0: name += "#limited"; break;

@@ -1137,7 +1153,7 @@ namespace Microsoft.Dafny {
             foreach (var inFormal in m.Ins) {

               var dt = inFormal.Type.AsDatatype;

               if (dt != null) {

-                var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullName, Bpl.Type.Bool));

+                var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullCompileName, Bpl.Type.Bool));

                 var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));

                 builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));

               }

@@ -1452,8 +1468,8 @@ namespace Microsoft.Dafny {
         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)));

+      string axiomComment = "frame axiom for " + f.FullCompileName;

+      Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));

       while (fn != null) {

         Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);

         Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);

@@ -1575,7 +1591,7 @@ namespace Microsoft.Dafny {
           }

         }

       }

-      Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),

+      Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullCompileName, typeParams, inParams, new Bpl.VariableSeq(),

         req, new Bpl.IdentifierExprSeq(), ens, etran.TrAttributes(f.Attributes, null));

       sink.TopLevelDeclarations.Add(proc);

 

@@ -1637,7 +1653,7 @@ namespace Microsoft.Dafny {
         // don't fall through to postcondition checks

         bodyCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));

       } else {

-        Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));

+        Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));

         Bpl.ExprSeq args = new Bpl.ExprSeq();

         args.Add(etran.HeapExpr);

         foreach (Variable p in implInParams) {

@@ -1729,7 +1745,7 @@ namespace Microsoft.Dafny {
             t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));

           } else if (e.Field is DatatypeDestructor) {

             var dtor = (DatatypeDestructor)e.Field;

-            t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));

+            t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullCompileName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));

           }

           return t;

         }

@@ -1988,7 +2004,7 @@ namespace Microsoft.Dafny {
         // check well-formedness of the other parameters

         r = BplAnd(r, CanCallAssumption(e.Args, etran));

         // get to assume canCall

-        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);

         ExprSeq args = etran.FunctionInvocationArguments(e);

         Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

         r = BplAnd(r, canCallFuncAppl);

@@ -2036,6 +2052,12 @@ namespace Microsoft.Dafny {
         }

         return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));

 

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        var canCall = CanCallAssumption(e.Body, etran);

+        if (e.Contract != null)

+          return BplAnd(canCall, CanCallAssumption(e.Contract, etran));

+        else return canCall;

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var total = CanCallAssumption(e.Term, etran);

@@ -2231,7 +2253,7 @@ namespace Microsoft.Dafny {
           CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);

         } else if (e.Field is DatatypeDestructor) {

           var dtor = (DatatypeDestructor)e.Field;

-          var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj));

+          var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullCompileName, Bpl.Type.Bool, etran.TrExpr(e.Obj));

           if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) {

             // There is only one constructor, so the value must be been constructed by it; might as well assume that here.

             builder.Add(new Bpl.AssumeCmd(expr.tok, correctConstructor));

@@ -2376,7 +2398,7 @@ namespace Microsoft.Dafny {
             CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);

           }

 

-          if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes) {

+          if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is CoPredicate)) {

             // check that the decreases measure goes down

             ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;

             if (module == cce.NonNull(options.Decr.EnclosingClass).Module) {

@@ -2420,7 +2442,7 @@ namespace Microsoft.Dafny {
           }

         }

         // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.

-        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);

         ExprSeq args = etran.FunctionInvocationArguments(e);

         Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

         builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));

@@ -2499,6 +2521,14 @@ namespace Microsoft.Dafny {
         CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran);

         result = null;

 

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        CheckWellformedWithResult(e.Body, options, result, resultType, locals, builder, etran);

+        if (e.Contract != null) {

+          CheckWellformedWithResult(e.Contract, options, result, resultType, locals, builder, etran);

+          var theSame = Bpl.Expr.Eq(etran.TrExpr(e.Body), etran.TrExpr(e.Contract));

+          builder.Add(Assert(new ForceCheckToken(e.ReplacerToken), theSame, "replacement must be the same value"));

+        }

       } else if (expr is ComprehensionExpr) {

         var e = (ComprehensionExpr)expr;

         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);

@@ -2796,12 +2826,26 @@ namespace Microsoft.Dafny {
       if (classes.TryGetValue(cl, out cc)) {

         Contract.Assert(cc != null);

       } else {

-        cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullName, predef.ClassNameType), true);

+        cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullCompileName, predef.ClassNameType), !cl.Module.IsAbstract);

         classes.Add(cl, cc);

       }

       return cc;

     }

 

+    Bpl.Constant GetFieldNameFamily(string n) {

+      Contract.Requires(n != null);

+      Contract.Requires(predef != null);

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

+      Bpl.Constant cc;

+      if (fieldConstants.TryGetValue(n, out cc)) {

+        Contract.Assert(cc != null);

+      } else {

+        cc = new Bpl.Constant(Token.NoToken, new Bpl.TypedIdent(Token.NoToken, "field$" + n, predef.NameFamilyType), true);

+        fieldConstants.Add(n, cc);

+      }

+      return cc;

+    }

+

     Bpl.Expr GetTypeExpr(IToken tok, Type type)

     {

       Contract.Requires(tok != null);

@@ -2861,13 +2905,13 @@ namespace Microsoft.Dafny {
       if (fields.TryGetValue(f, out fc)) {

         Contract.Assert(fc != null);

       } else {

-        // const unique f: Field ty;

+        // const f: Field ty;

         Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));

-        fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);

+        fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), false);

         fields.Add(f, fc);

-        // axiom FDim(f) == 0 && DeclType(f) == C;

+        // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f;

         Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0));

-        Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))));

+        Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FieldOfDecl, ty, new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))), new Bpl.IdentifierExpr(f.tok, GetFieldNameFamily(f.Name))), Bpl.Expr.Ident(fc));

         Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fdim, declType));

         sink.TopLevelDeclarations.Add(ax);

       }

@@ -2894,7 +2938,7 @@ namespace Microsoft.Dafny {
         Bpl.Type receiverType = f.EnclosingClass is ClassDecl ? predef.RefType : predef.DatatypeType;

         args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", receiverType), true));

         Bpl.Formal result = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, ty), false);

-        ff = new Bpl.Function(f.tok, f.FullName, args, result);

+        ff = new Bpl.Function(f.tok, f.FullCompileName, args, result);

         fieldFunctions.Add(f, ff);

         // treat certain fields specially

         if (f.EnclosingClass is ArrayClassDecl) {

@@ -2936,7 +2980,7 @@ namespace Microsoft.Dafny {
         args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true));

       }

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

+      Bpl.Function func = new Bpl.Function(f.tok, f.FullCompileName, typeParams, args, res);

       sink.TopLevelDeclarations.Add(func);

 

       if (f.IsRecursive) {

@@ -2945,7 +2989,7 @@ namespace Microsoft.Dafny {
       }

 

       res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);

-      Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);

+      Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res);

       sink.TopLevelDeclarations.Add(canCallF);

     }

 

@@ -3052,10 +3096,10 @@ namespace Microsoft.Dafny {
       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);

       string name;

       switch (kind) {

-        case 0: name = "CheckWellformed$$" + m.FullName; break;

-        case 1: name = m.FullName; break;

-        case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break;

-        case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break;

+        case 0: name = "CheckWellformed$$" + m.FullCompileName; break;

+        case 1: name = m.FullCompileName; break;

+        case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;

+        case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;

         default: Contract.Assert(false); throw new cce.UnreachableException();  // unexpected kind

       }

       Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);

@@ -4432,9 +4476,9 @@ namespace Microsoft.Dafny {
       // Make the call

       string name;

       if (RefinementToken.IsInherited(method.tok, currentModule)) {

-        name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullName);

+        name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);

       } else {

-        name = method.FullName;

+        name = method.FullCompileName;

       }

       Bpl.CallCmd call = new Bpl.CallCmd(tok, name, ins, outs);

       builder.Add(call);

@@ -4795,7 +4839,7 @@ namespace Microsoft.Dafny {
         return Bpl.Expr.Le(Bpl.Expr.Literal(0), x);

 

       } else  if (type is BoolType || type is IntType) {

-        // nothing todo

+        // nothing to do

 

       } else if (type is SetType) {

         SetType st = (SetType)type;

@@ -5304,7 +5348,7 @@ namespace Microsoft.Dafny {
           typeArgs.Add(tRhs.EType);

           rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class._System." + BuiltIns.ArrayClassName(tRhs.ArrayDimensions.Count), predef.ClassNameType), typeArgs, true);

         } else if (tRhs.EType is ObjectType) {

-          rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(Token.NoToken,GetClass(program.BuiltIns.ObjectDecl)), new List<Type>(), true);

+          rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(Token.NoToken, GetClass(program.BuiltIns.ObjectDecl)), new List<Type>(), true);

         } else {

           rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);

         }

@@ -5978,7 +6022,8 @@ namespace Microsoft.Dafny {
         } else if (expr is LetExpr) {

           var e = (LetExpr)expr;

           return TrExpr(GetSubstitutedBody(e));

-

+        } else if (expr is NamedExpr) {

+          return TrExpr(((NamedExpr)expr).Body);

         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

           Bpl.VariableSeq bvars = new Bpl.VariableSeq();

@@ -6538,6 +6583,7 @@ namespace Microsoft.Dafny {
       DtTypeParams, // type parameters of datatype

       TypeTuple,

       DeclType,

+      FieldOfDecl,

       FDim,  // field dimension (0 - named, 1 or more - indexed)

 

       DatatypeCtorId,

@@ -6776,6 +6822,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

           return FunctionCall(tok, "DeclType", predef.ClassNameType, args);

+        case BuiltinFunction.FieldOfDecl:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation != null);

+          return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok, typeInstantiation) , args);

         case BuiltinFunction.FDim:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

@@ -7019,7 +7069,7 @@ namespace Microsoft.Dafny {
               // Note that "body" does not contain limited calls.

 

               // F#canCall(args)

-              Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullName + "#canCall", Bpl.Type.Bool);

+              Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);

               ExprSeq args = etran.FunctionInvocationArguments(fexp);

               Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

 

@@ -7463,6 +7513,231 @@ namespace Microsoft.Dafny {
       }

     }

 

+    void AddCoinductionPrinciple(CoPredicate coPredicate) {

+      Contract.Requires(coPredicate != null);

+      if (coPredicate.Body == null) {

+        return;  // we can't generate any useful coinduction principle if the copredicate doesn't have a body

+      } else if (2 <= coPredicate.EnclosingClass.Module.CallGraph.GetSCCSize(coPredicate)) {

+        return;  // this copredicate involves mutually recursive calls; for now, we don't handle those

+      }

+      var n = (coPredicate.IsStatic ? 0 : 1) + coPredicate.Formals.Count;

+      var templates = new List<FunctionCallExpr[/*of length n*/]>();

+      foreach (var fce in coPredicate.Uses) {

+        // Compute a template of instantiation for this use:  for each actual argument, record

+        // a function F if the argument is a call to F, or record null otherwise.

+        var t = new FunctionCallExpr[n];

+        var i = 0;

+        if (!coPredicate.IsStatic) {

+          t[i] = fce.Receiver.Resolved as FunctionCallExpr;

+          i++;

+        }

+        foreach (var a in fce.Args) {

+          t[i] = a.Resolved as FunctionCallExpr;

+          i++;

+        }

+        Contract.Assert(i == t.Length);

+        // See if this template has been done before (for now, this is a slow check; it would be nice to speed it up)

+        foreach (var prev in templates) {

+          var j = 0;

+          for (; j < n; j++) {

+            if (prev[j] == null && t[j] == null) {

+              // things are equal

+            } else if (prev[j] != null && t[j] != null && prev[j].Function == t[j].Function) {

+              // things are equal

+            } else {

+              // we found an unequal part of the template

+              break;

+            }

+          }

+          if (j == n) {

+            // template 't' matches 'prev', so we've already spilled out an axiom for this template

+            // TODO: this is not the complete test, because of possible type parameters

+            goto Next_Use;

+          }

+          // 't' does not match this 'prev'; try the next 'prev'

+        }

+        // No 'prev' matches the current template 't'.  So, generate an axiom for 't'.

+        string comment = string.Format("Coinduction principle for copredicate {0} instantiated like:", coPredicate.FullName);

+        foreach (var tf in t) {

+          comment += tf == null ? " ." : " " + tf.Name;

+        }

+        sink.TopLevelDeclarations.Add(new Bpl.Axiom(fce.tok, CoinductionPrinciple(coPredicate, fce, t), comment));

+        templates.Add(t);

+      Next_Use: ;

+      }

+    }

+

+    /// <summary>

+    /// It's the "callOfInterest" that determines the (type-parameter instantiated) types of the arguments

+    /// </summary>

+    Bpl.Expr CoinductionPrinciple(CoPredicate coPredicate, FunctionCallExpr callOfInterest, FunctionCallExpr[] t) {

+      Contract.Requires(coPredicate != null);

+      Contract.Requires(coPredicate.Body != null);

+      Contract.Requires(t != null);

+      Contract.Requires(t.Length == (coPredicate.IsStatic ? 0 : 1) + coPredicate.Formals.Count);

+      // Let C be the name of the coPredicate, and suppose it is defined by:

+      //     copredicate C(x)

+      //       requires PreC(x);

+      //     {

+      //       Body[C]

+      //     }

+      // where the notation Body[_] means an expression Body with holes and in particular one whole

+      // for every recursive use of C.

+      // The general form of the coinduction principle of which we will generate an instance is:

+      //   forall P ::

+      //     forall s ::   // where s is a list of arguments to coPredicate

+      //       P(s) &&

+      //       (forall s' :: P(s') ==> Body[P][x := s'])

+      //       ==>

+      //       C(s)

+      // We will pick particular P's, and will therefore instead generate the axiom once for each

+      // such P.  We will also redistribute the terms as follows:

+      //   (forall s :: P(s) ==> Body[P][x := s])

+      //   ==>

+      //   (forall s :: P(s) ==> C(s))

+      // Furthermore, if the C of interest has actual parameters that are function-call expressions,

+      // then the P will be chosen to fit that pattern.  As a specific example, suppose C takes 3

+      // parameters (that is, 's' is a triple (s0,s1,s2)) and that the actual arguments for these, in

+      // the C use of interest, are of the form C(E0,F(E1),G(E2,E3)), where E0 denotes an expression that

+      // is not a function-call expression and E1,E2,E3 are any expressions.  Also, suppose the

+      // preconditions of C,F,G are PreC(s0,s1,s2), PreF(f), PreG(g0,g1).

+      // Then, we pick P(s0,s1,s2) :=

+      //   exists a,b,c,d :: PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d)) && (s0,s1,s2) == (a,F(b),G(c,d))

+      // So, the axiom looks like:

+      //   (forall a,b,c,d :: PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d))

+      //                      ==> Body[P][x0,x1,x2 := a,F(b),G(c,d)])

+      //   ==>

+      //   (forall a,b,c,d { C(a,F(b),G(c,d)) } ::

+      //                      PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d))

+      //                      ==> C(a,F(b),G(c,d)))

+      //

+      // To be usable, we need to do more.  In particular, we need to do some preprocessing of the expressions

+      // of the form C(E0,E1,E2) in Body, which are turned into P(E0,E1,E2) in Body[P] (where these are any

+      // expressions E0,E1,E2, not necessarily the ones as above).  We know that such C(E0,E1,E2) occurrences

+      // sit only in positive positions.  Hence, we can soundly replace each (exists a,b,c,d :: Q(a,b,c,d))

+      // expressions in Body[P] in the axiom with Q(A,B,C,D) for any A,B,C,D.  For this to be useful, we need

+      // good guesses for A,B,C,D.

+      //

+      // TODO: also need a module/function-height antecedent for the axiom!

+      var tok = coPredicate.tok;

+      var bvs = new Bpl.VariableSeq();

+      var boundVars = new List<BoundVar>();

+      Bpl.BoundVariable heapVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$h", predef.HeapType));

+      bvs.Add(heapVar);

+      var bHeap = new Bpl.IdentifierExpr(tok, heapVar);

+      Bpl.Expr typeAntecedents = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, bHeap);

+      var etran = new ExpressionTranslator(this, predef, bHeap);

+      Expression pre = new LiteralExpr(tok, true);

+      var i = 0;

+      Expression receiverReplacement = null;

+      if (!coPredicate.IsStatic) {

+        Expression preF;

+        receiverReplacement = FG(tok, callOfInterest.Receiver.Type, t[i], boundVars, bvs, ref typeAntecedents, out preF, etran);

+        typeAntecedents = BplAnd(typeAntecedents, Bpl.Expr.Neq(etran.TrExpr(receiverReplacement), predef.Null));

+        if (preF != null) {

+          pre = AutoContractsRewriter.BinBoolExpr(receiverReplacement.tok, BinaryExpr.ResolvedOpcode.And, pre, preF);

+        }

+        i++;

+      }

+      var substMap = new Dictionary<IVariable, Expression>();

+      var j = 0;

+      foreach (var p in coPredicate.Formals) {

+        Expression preF;

+        var e = FG(tok, callOfInterest.Args[j].Type, t[i], boundVars, bvs, ref typeAntecedents, out preF, etran);

+        substMap.Add(p, e);

+        if (preF != null) {

+          pre = AutoContractsRewriter.BinBoolExpr(e.tok, BinaryExpr.ResolvedOpcode.And, pre, preF);

+        }

+        i++; j++;

+      }

+      // conjoin subst(preC) to pre

+      foreach (var req in coPredicate.Req) {

+        var preC = Substitute(req, receiverReplacement, substMap);

+        pre = AutoContractsRewriter.BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, pre, preC);

+      }

+      // build up the term C(a,F(b),G(c,d))

+      var args = new List<Expression>();

+      foreach (var p in coPredicate.Formals) {

+        args.Add(substMap[p]);

+      }

+      var C = new FunctionCallExpr(tok, coPredicate.Name, receiverReplacement, tok, args);

+      C.Function = coPredicate;

+      C.Type = coPredicate.ResultType;

+      // We are now ready to produce the Conclusion of the axiom

+      var preStuff = Bpl.Expr.And(typeAntecedents, etran.TrExpr(pre));

+      Bpl.Expr Conclusion = new Bpl.ForallExpr(tok, bvs, new Bpl.Trigger(tok, true, new ExprSeq(etran.TrExpr(C))),

+        Bpl.Expr.Imp(preStuff, etran.TrExpr(C)));

+      // Now for the antecedent of the axiom

+      // TODO: if e.Body uses a 'match' expression, first desugar it into an ordinary expression

+      var s = new CoinductionSubstituter(coPredicate, receiverReplacement, substMap, pre, boundVars, receiverReplacement, args);

+      var body = s.Substitute(coPredicate.Body);

+      Bpl.Expr Antecedent = new Bpl.ForallExpr(tok, bvs, Bpl.Expr.Imp(preStuff, etran.TrExpr(body)));

+      // Put it all together and we're ready to go

+      return Bpl.Expr.Imp(Antecedent, Conclusion);

+    }

+

+    /// <summary>

+    /// "templateFunc" is passed in as "null", then "precondition" is guaranteed to come out as "null".

+    /// </summary>

+    Expression FG(IToken tok, Type argumentType, FunctionCallExpr templateFunc, List<BoundVar> boundVars, Bpl.VariableSeq bvs, ref Bpl.Expr typeAntecedents, out Expression precondition, ExpressionTranslator etran) {

+      Contract.Requires(tok != null);

+      Contract.Requires(argumentType != null);

+      Contract.Requires(boundVars != null);

+      Contract.Requires(bvs != null);

+      Contract.Requires(etran != null);

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

+      Contract.Ensures(Contract.ValueAtReturn<Expression>(out precondition) != null);

+      // TODO: also need to return type antecedents

+      precondition = new LiteralExpr(tok, true);

+      if (templateFunc == null) {

+        // generate a fresh variable of type "argumentType"

+        var k = new BoundVar(tok, "_coind" + otherTmpVarCount, argumentType);

+        otherTmpVarCount++;

+        boundVars.Add(k);

+        // convert it to a Boogie variable and add it to "bvs"

+        var bvar = new Bpl.BoundVariable(k.tok, new Bpl.TypedIdent(k.tok, k.UniqueName, TrType(k.Type)));

+        bvs.Add(bvar);

+        // update typeAntecedents

+        var wh = GetWhereClause(k.tok, new Bpl.IdentifierExpr(k.tok, bvar), k.Type, etran);

+        if (wh != null) {

+          typeAntecedents = BplAnd(typeAntecedents, wh);

+        }

+        // make an IdentifierExpr out of it and return it

+        IdentifierExpr ie = new IdentifierExpr(k.tok, k.UniqueName);

+        ie.Var = k; ie.Type = ie.Var.Type;  // resolve it here

+        return ie;

+

+      } else {

+        // for each formal parameter to "templateFunc", generate a fresh variable

+        // for each one, convert it to a Boogie variable and add it to "bvs"

+        // make a FunctionCallExpr, passing in these variables as arguments, and then returning the FunctionCallExpr

+        Expression preIgnore;

+        Expression receiver = null;

+        if (!templateFunc.Function.IsStatic) {

+          receiver = FG(tok, templateFunc.Receiver.Type, null, boundVars, bvs, ref typeAntecedents, out preIgnore, etran);

+          typeAntecedents = BplAnd(typeAntecedents, Bpl.Expr.Neq(etran.TrExpr(receiver), predef.Null));

+        }

+        var args = new List<Expression>();

+        var i = 0;

+        var substMap = new Dictionary<IVariable, Expression>();

+        foreach (var arg in templateFunc.Args) {

+          var e = FG(tok, arg.Type, null, boundVars, bvs, ref typeAntecedents, out preIgnore, etran);

+          args.Add(e);

+          substMap.Add(templateFunc.Function.Formals[i], e);

+          i++;

+        }

+        var F = new FunctionCallExpr(tok, templateFunc.Name, receiver, tok, args);

+        F.Function = templateFunc.Function;

+        F.Type = templateFunc.Function.ResultType;

+

+        foreach (var req in templateFunc.Function.Req) {

+          var pre = Substitute(req, receiver, substMap);

+          precondition = AutoContractsRewriter.BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.And, precondition, pre);

+        }

+        return F;

+      }

+    }

+

     /// <summary>

     /// Returns true iff 'v' occurs as a free variable in 'expr'.

     /// Parameter 'v' is allowed to be a ThisSurrogate, in which case the method return true iff 'this'

@@ -7507,254 +7782,447 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

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

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

+      var s = new Substituter(receiverReplacement, substMap);

+      return s.Substitute(expr);

+    }

 

-      Expression newExpr = null;  // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end

-

-      if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {

-        // nothing to substitute

-      } else if (expr is ThisExpr) {

-        return receiverReplacement == null ? expr : receiverReplacement;

-      } else if (expr is IdentifierExpr) {

-        IdentifierExpr e = (IdentifierExpr)expr;

-        Expression substExpr;

-        if (substMap.TryGetValue(e.Var, out substExpr)) {

-          return cce.NonNull(substExpr);

-        }

-      } else if (expr is DisplayExpression) {

-        DisplayExpression e = (DisplayExpression)expr;

-        List<Expression> newElements = SubstituteExprList(e.Elements, receiverReplacement, substMap);

-        if (newElements != e.Elements) {

-          if (expr is SetDisplayExpr) {

-            newExpr = new SetDisplayExpr(expr.tok, newElements);

-          } else if (expr is MultiSetDisplayExpr) {

-            newExpr = new MultiSetDisplayExpr(expr.tok, newElements);

+    public class CoinductionSubstituter : Substituter

+    {

+      CoPredicate coPredicate;

+      Expression existentialAntecedent;

+      List<BoundVar> existentialVariables;

+      Expression existentialReceiver;

+      List<Expression> existentialTemplates;

+

+      public CoinductionSubstituter(CoPredicate coPredicate, Expression receiverReplacement, Dictionary<IVariable, Expression> substMap,

+        Expression existentialAntecedent, List<BoundVar> existentialVariables, Expression existentialReceiver, List<Expression> existentialTemplates)

+        : base(receiverReplacement, substMap)

+      {

+        Contract.Requires(coPredicate != null);

+        Contract.Requires(substMap != null);

+        Contract.Requires(existentialAntecedent != null);

+        Contract.Requires(existentialVariables != null);

+        Contract.Requires(existentialTemplates != null);

+        this.coPredicate = coPredicate;

+        this.existentialAntecedent = existentialAntecedent;

+        this.existentialVariables = existentialVariables;

+        this.existentialReceiver = existentialReceiver;

+        this.existentialTemplates = existentialTemplates;

+      }

+      public override Expression Substitute(Expression expr) {

+        expr = base.Substitute(expr);

+        var e = expr as FunctionCallExpr;

+        if (e == null || e.Function != coPredicate) {

+          return expr;

+        }

+        // We found a call coPredicate(args).  Replace it with P(args), where P is the predicate we're

+        // using in the coinduction principle.  As described in method CoinductionPrinciple above, the

+        // predicate P has the form:

+        //     exists a,b,c,d :: PreF(b) && PreG(c,d) && PredC(a,F(b),G(c,d)) && (s0,s1,s2) == (a,F(b),G(c,d))

+        // where s0,s1,s2 are shows as the actual arguments to coPredicate (called "args" four lines

+        // above).  This existential corresponds to the parameters passed to this CoinductionSubstituter

+        // as follows:

+        //     exists existentialVariables :: existentialAntecedent           && (s0,s1,s2) == (existentialTemplate)

+        // The idea is now to build up a substitution for a,b,c,d, such that the last conjunct

+        // in the existential will be true in any context.  We can then replace coPredicate(s0,s1,s2) with

+        //     existentialAntecedent[a,b,c,d := A,B,C,D]

+        var substMap = new Dictionary<IVariable, Expression>();

+        var j = 0;

+        for (int i = -1; i < existentialTemplates.Count; i++) {

+          Expression templ;

+          Expression si;

+          if (0 <= i) {

+            templ = existentialTemplates[i].Resolved;

+            si = e.Args[i];

+          } else if (existentialReceiver != null) {

+            templ = existentialReceiver.Resolved;

+            si = e.Receiver;

+          } else {

+            continue;

+          }

+          templ = PossiblyInline(templ);

+          if (templ is IdentifierExpr) {

+            // this one is easy--use the instantiation a:=si

+            Contract.Assert(((IdentifierExpr)templ).Var == existentialVariables[j]);

+            substMap.Add(existentialVariables[j], si);

+            j++;

           } else {

-            newExpr = new SeqDisplayExpr(expr.tok, newElements);

+            var templFce = (FunctionCallExpr)templ;

+            var psi = PartiallyEvaluate(si, 1);

+            var fce = psi as FunctionCallExpr;

+            if (fce == null || fce.Function != templFce.Function) {

+              // This is not what we were hoping for.  What can we do?

+              // One option would be to existentially quantify over the variable for which we didn't get an instantiation.

+              // Another option would be to guess some arbitrary but value.

+              // A third option, which is what we'll do, is to return false.

+              return new LiteralExpr(e.tok, false);

+            } else {

+              // We're in luck.  Pick the parameters of the partially evaluated call

+              if (templFce.Receiver != null) {

+                Contract.Assert(templFce.Receiver is IdentifierExpr && ((IdentifierExpr)templFce.Receiver).Var == existentialVariables[j]);

+                substMap.Add(existentialVariables[j], fce.Receiver);

+                j++;

+              }

+              var k = 0;

+              foreach (var arg in fce.Args) {

+                Contract.Assert(templFce.Args[k] is IdentifierExpr && ((IdentifierExpr)templFce.Args[k]).Var == existentialVariables[j]);

+                substMap.Add(existentialVariables[j], arg);

+                j++;

+                k++;

+              }

+            }

           }

         }

+        Contract.Assert(j == existentialVariables.Count);

+        return Translator.Substitute(existentialAntecedent, null, substMap);

+      }

 

-      } else if (expr is FieldSelectExpr) {

-        FieldSelectExpr fse = (FieldSelectExpr)expr;

-        Expression substE = Substitute(fse.Obj, receiverReplacement, substMap);

-        if (substE != fse.Obj) {

-          FieldSelectExpr fseNew = new FieldSelectExpr(fse.tok, substE, fse.FieldName);

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

-        Expression e0 = sse.E0 == null ? null : Substitute(sse.E0, receiverReplacement, substMap);

-        Expression e1 = sse.E1 == null ? null : Substitute(sse.E1, receiverReplacement, substMap);

-        if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {

-          newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

+      Expression PossiblyInline(Expression expr) {

+        Contract.Requires(expr != null);

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

+        if (expr is FunctionCallExpr) {

+          var e = (FunctionCallExpr)expr;

+          if (e.Function.Body != null && !e.Function.IsRecursive) {

+            var inlinedBody = InlineFunctionCall(e);

+            // use the inlinedBody if it consists of only IdentifierExpr's and FunctionCallExpr's

+            if (IsTemplateLike(inlinedBody)) {

+              return PossiblyInline(inlinedBody);

+            }

+          }

         }

+        return expr;

+      }

 

-      } else if (expr is SeqUpdateExpr) {

-        SeqUpdateExpr sse = (SeqUpdateExpr)expr;

-        Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);

-        Expression index = Substitute(sse.Index, receiverReplacement, substMap);

-        Expression val = Substitute(sse.Value, receiverReplacement, substMap);

-        if (seq != sse.Seq || index != sse.Index || val != sse.Value) {

-          newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);

+      bool IsTemplateLike(Expression expr) {

+        Contract.Requires(expr != null);

+        expr = expr.Resolved;

+        if (expr is IdentifierExpr) {

+          return true;

+        } else if (expr is FunctionCallExpr) {

+          var e = (FunctionCallExpr)expr;

+          if (e.Receiver == null || IsTemplateLike(e.Receiver)) {

+            return e.Args.TrueForAll(IsTemplateLike);

+          }

         }

+        return false;

+      }

+    }

 

-      } else if (expr is MultiSelectExpr) {

-        MultiSelectExpr mse = (MultiSelectExpr)expr;

-        Expression array = Substitute(mse.Array, receiverReplacement, substMap);

-        List<Expression> newArgs = SubstituteExprList(mse.Indices, receiverReplacement, substMap);

-        if (array != mse.Array || newArgs != mse.Indices) {

-          newExpr = new MultiSelectExpr(mse.tok, array, newArgs);

+    /// <summary>

+    /// Returns a (resolved) expression that evaluates to the same value as "expr".

+    /// Assumes "expr" to be well defined.

+    /// </summary>

+    public static Expression PartiallyEvaluate(Expression expr, int recursiveInlineDepth) {

+      Contract.Requires(expr != null);

+      Contract.Requires(0 <= recursiveInlineDepth);

+      if (expr is ConcreteSyntaxExpression) {

+        var e = (ConcreteSyntaxExpression)expr;

+        return PartiallyEvaluate(e.ResolvedExpression, recursiveInlineDepth);

+      } else if (expr is FieldSelectExpr) {

+        var e = (FieldSelectExpr)expr;

+        // check if it's a destructor around a constructor

+        var dtor = e.Field as DatatypeDestructor;

+        if (dtor != null) {

+          var obj = PartiallyEvaluate(e.Obj, recursiveInlineDepth);

+          var dtv = obj as DatatypeValue;

+          if (dtv != null) {

+            for (int i = 0; i < dtv.Ctor.Formals.Count; i++) {

+              if (dtv.Ctor.Formals[i] == dtor.CorrespondingFormal) {

+                return dtv.Arguments[i];

+              }

+            }

+            Contract.Assert(false);  // we expect to have found the destructor among the constructor's formals

+          } else if (obj != e.Obj) {

+            var peE = new FieldSelectExpr(e.tok, obj, e.FieldName);

+            peE.Field = e.Field;  // resolve here

+            peE.Type = e.Type;  // resolve here

+            return peE;

+          }

         }

-

       } else if (expr is FunctionCallExpr) {

-        FunctionCallExpr e = (FunctionCallExpr)expr;

-        Expression receiver = Substitute(e.Receiver, receiverReplacement, substMap);

-        List<Expression> newArgs = SubstituteExprList(e.Args, receiverReplacement, substMap);

-        if (receiver != e.Receiver || newArgs != e.Args) {

-          FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);

-          newFce.Function = e.Function;  // resolve on the fly (and set newFce.Type below, at end)

-          newExpr = newFce;

+        var e = (FunctionCallExpr)expr;

+        if (e.Function.Body != null && (!e.Function.IsRecursive || 0 < recursiveInlineDepth)) {

+          var inlinedBody = InlineFunctionCall(e);

+          return PartiallyEvaluate(inlinedBody, recursiveInlineDepth - (e.Function.IsRecursive ? 1 : 0));

         }

+      }

+      return expr;

+    }

 

-      } else if (expr is DatatypeValue) {

-        DatatypeValue dtv = (DatatypeValue)expr;

-        List<Expression> newArgs = SubstituteExprList(dtv.Arguments, receiverReplacement, substMap);

-        if (newArgs != dtv.Arguments) {

-          DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);

-          newDtv.Ctor = dtv.Ctor;  // resolve on the fly (and set newDtv.Type below, at end)

-          newExpr = newDtv;

-        }

+    static Expression InlineFunctionCall(FunctionCallExpr fce) {

+      Contract.Requires(fce != null);

+      var substMap = new Dictionary<IVariable, Expression>();

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

+        substMap.Add(fce.Function.Formals[i], fce.Args[i]);

+      }

+      // TODO: in the following substitution, it may be that we also need to update the types of the resulting subexpressions (is this true for all Substitute calls?)

+      return Substitute(fce.Function.Body, fce.Receiver, substMap);

+    }

 

-      } else if (expr is OldExpr) {

-        OldExpr e = (OldExpr)expr;

-        // Note, it is up to the caller to avoid variable capture.  In most cases, this is not a

-        // problem, since variables have unique declarations.  However, it is an issue if the substitution

-        // takes place inside an OldExpr.  In those cases (see LetExpr), the caller can use a

-        // BoogieWrapper before calling Substitute.

-        Expression se = Substitute(e.E, receiverReplacement, substMap);

-        if (se != e.E) {

-          newExpr = new OldExpr(expr.tok, se);

-        }

-      } else if (expr is FreshExpr) {

-        FreshExpr e = (FreshExpr)expr;

-        Expression se = Substitute(e.E, receiverReplacement, substMap);

-        if (se != e.E) {

-          newExpr = new FreshExpr(expr.tok, se);

-        }

-      } else if (expr is AllocatedExpr) {

-        AllocatedExpr e = (AllocatedExpr)expr;

-        Expression se = Substitute(e.E, receiverReplacement, substMap);

-        if (se != e.E) {

-          newExpr = new AllocatedExpr(expr.tok, se);

-        }

-      } else if (expr is UnaryExpr) {

-        UnaryExpr e = (UnaryExpr)expr;

-        Expression se = Substitute(e.E, receiverReplacement, substMap);

-        if (se != e.E) {

-          newExpr = new UnaryExpr(expr.tok, e.Op, se);

-        }

-      } else if (expr is BinaryExpr) {

-        BinaryExpr e = (BinaryExpr)expr;

-        Expression e0 = Substitute(e.E0, receiverReplacement, substMap);

-        Expression e1 = Substitute(e.E1, receiverReplacement, substMap);

-        if (e0 != e.E0 || e1 != e.E1) {

-          BinaryExpr newBin = new BinaryExpr(expr.tok, e.Op, e0, e1);

-          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;

-        }

+    public class Substituter

+    {

+      public readonly Expression receiverReplacement;

+      public readonly Dictionary<IVariable, Expression/*!*/>/*!*/ substMap;

+      public Substituter(Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

+        Contract.Requires(substMap != null);

+        this.receiverReplacement = receiverReplacement;

+        this.substMap = substMap;

+      }

+      public virtual Expression Substitute(Expression expr) {

+        Contract.Requires(expr != null);

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

 

-      } else if (expr is LetExpr) {

-        var e = (LetExpr)expr;

-        var rhss = new List<Expression>();

-        bool anythingChanged = false;

-        foreach (var rhs in e.RHSs) {

-          var r = Substitute(rhs, receiverReplacement, substMap);

-          if (r != rhs) {

-            anythingChanged = true;

-          }

-          rhss.Add(r);

-        }

-        var body = Substitute(e.Body, receiverReplacement, substMap);

-        if (anythingChanged || body != e.Body) {

-          newExpr = new LetExpr(e.tok, e.Vars, rhss, body);

-        }

+        Expression newExpr = null;  // set to non-null value only if substitution has any effect; if non-null, newExpr will be resolved at end

 

-      } else if (expr is ComprehensionExpr) {

-        var e = (ComprehensionExpr)expr;

-        Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);

-        Expression newTerm = Substitute(e.Term, receiverReplacement, substMap);

-        Attributes newAttrs = SubstAttributes(e.Attributes, receiverReplacement, substMap);

-        if (e is SetComprehension) {

-          if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

-            newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);

-          }

-        } else if (e is MapComprehension) {

-          if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

-            newExpr = new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);

-          }

-        } else if (e is QuantifierExpr) {

-          var q = (QuantifierExpr)e;

-          if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

-            if (expr is ForallExpr) {

-              newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+        if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {

+          // nothing to substitute

+        } else if (expr is ThisExpr) {

+          return receiverReplacement == null ? expr : receiverReplacement;

+        } else if (expr is IdentifierExpr) {

+          IdentifierExpr e = (IdentifierExpr)expr;

+          Expression substExpr;

+          if (substMap.TryGetValue(e.Var, out substExpr)) {

+            return cce.NonNull(substExpr);

+          }

+        } else if (expr is DisplayExpression) {

+          DisplayExpression e = (DisplayExpression)expr;

+          List<Expression> newElements = SubstituteExprList(e.Elements);

+          if (newElements != e.Elements) {

+            if (expr is SetDisplayExpr) {

+              newExpr = new SetDisplayExpr(expr.tok, newElements);

+            } else if (expr is MultiSetDisplayExpr) {

+              newExpr = new MultiSetDisplayExpr(expr.tok, newElements);

             } else {

-              newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+              newExpr = new SeqDisplayExpr(expr.tok, newElements);

             }

           }

-        } else {

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

-        }

 

-      } else if (expr is PredicateExpr) {

-        var e = (PredicateExpr)expr;

-        Expression g = Substitute(e.Guard, receiverReplacement, substMap);

-        Expression b = Substitute(e.Body, receiverReplacement, substMap);

-        if (g != e.Guard || b != e.Body) {

-          if (expr is AssertExpr) {

-            newExpr = new AssertExpr(e.tok, g, b);

-          } else {

-            newExpr = new AssumeExpr(e.tok, g, b);

+        } else if (expr is FieldSelectExpr) {

+          FieldSelectExpr fse = (FieldSelectExpr)expr;

+          Expression substE = Substitute(fse.Obj);

+          if (substE != fse.Obj) {

+            FieldSelectExpr fseNew = new FieldSelectExpr(fse.tok, substE, fse.FieldName);

+            fseNew.Field = fse.Field;  // resolve on the fly (and fseExpr.Type is set at end of method)

+            newExpr = fseNew;

           }

-        }

 

-      } else if (expr is ITEExpr) {

-        ITEExpr e = (ITEExpr)expr;

-        Expression test = Substitute(e.Test, receiverReplacement, substMap);

-        Expression thn = Substitute(e.Thn, receiverReplacement, substMap);

-        Expression els = Substitute(e.Els, receiverReplacement, substMap);

-        if (test != e.Test || thn != e.Thn || els != e.Els) {

-          newExpr = new ITEExpr(expr.tok, test, thn, els);

-        }

+        } else if (expr is SeqSelectExpr) {

+          SeqSelectExpr sse = (SeqSelectExpr)expr;

+          Expression seq = Substitute(sse.Seq);

+          Expression e0 = sse.E0 == null ? null : Substitute(sse.E0);

+          Expression e1 = sse.E1 == null ? null : Substitute(sse.E1);

+          if (seq != sse.Seq || e0 != sse.E0 || e1 != sse.E1) {

+            newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

+          }

 

-      } else if (expr is ConcreteSyntaxExpression) {

-        var e = (ConcreteSyntaxExpression)expr;

-        return Substitute(e.ResolvedExpression, receiverReplacement, substMap);

-      }

+        } else if (expr is SeqUpdateExpr) {

+          SeqUpdateExpr sse = (SeqUpdateExpr)expr;

+          Expression seq = Substitute(sse.Seq);

+          Expression index = Substitute(sse.Index);

+          Expression val = Substitute(sse.Value);

+          if (seq != sse.Seq || index != sse.Index || val != sse.Value) {

+            newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);

+          }

 

-      if (newExpr == null) {

-        return expr;

-      } else {

-        newExpr.Type = expr.Type;  // resolve on the fly (any additional resolution must be done above)

-        return newExpr;

-      }

-    }

+        } else if (expr is MultiSelectExpr) {

+          MultiSelectExpr mse = (MultiSelectExpr)expr;

+          Expression array = Substitute(mse.Array);

+          List<Expression> newArgs = SubstituteExprList(mse.Indices);

+          if (array != mse.Array || newArgs != mse.Indices) {

+            newExpr = new MultiSelectExpr(mse.tok, array, newArgs);

+          }

 

-    static List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist,

-                                                 Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {

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

-      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Expression>>()));

+        } else if (expr is FunctionCallExpr) {

+          FunctionCallExpr e = (FunctionCallExpr)expr;

+          Expression receiver = Substitute(e.Receiver);

+          List<Expression> newArgs = SubstituteExprList(e.Args);

+          if (receiver != e.Receiver || newArgs != e.Args) {

+            FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs);

+            newFce.Function = e.Function;  // resolve on the fly (and set newFce.Type below, at end)

+            newExpr = newFce;

+          }

 

-      List<Expression> newElist = null;  // initialized lazily

-      for (int i = 0; i < elist.Count; i++)

-      {cce.LoopInvariant(  newElist == null || newElist.Count == i);

+        } else if (expr is DatatypeValue) {

+          DatatypeValue dtv = (DatatypeValue)expr;

+          List<Expression> newArgs = SubstituteExprList(dtv.Arguments);

+          if (newArgs != dtv.Arguments) {

+            DatatypeValue newDtv = new DatatypeValue(dtv.tok, dtv.DatatypeName, dtv.MemberName, newArgs);

+            newDtv.Ctor = dtv.Ctor;  // resolve on the fly (and set newDtv.Type below, at end)

+            newExpr = newDtv;

+          }

 

-        Expression substE = Substitute(elist[i], receiverReplacement, substMap);

-        if (substE != elist[i] && newElist == null) {

-          newElist = new List<Expression>();

-          for (int j = 0; j < i; j++) {

-            newElist.Add(elist[j]);

+        } else if (expr is OldExpr) {

+          OldExpr e = (OldExpr)expr;

+          // Note, it is up to the caller to avoid variable capture.  In most cases, this is not a

+          // problem, since variables have unique declarations.  However, it is an issue if the substitution

+          // takes place inside an OldExpr.  In those cases (see LetExpr), the caller can use a

+          // BoogieWrapper before calling Substitute.

+          Expression se = Substitute(e.E);

+          if (se != e.E) {

+            newExpr = new OldExpr(expr.tok, se);

+          }

+        } else if (expr is FreshExpr) {

+          FreshExpr e = (FreshExpr)expr;

+          Expression se = Substitute(e.E);

+          if (se != e.E) {

+            newExpr = new FreshExpr(expr.tok, se);

+          }

+        } else if (expr is AllocatedExpr) {

+          AllocatedExpr e = (AllocatedExpr)expr;

+          Expression se = Substitute(e.E);

+          if (se != e.E) {

+            newExpr = new AllocatedExpr(expr.tok, se);

+          }

+        } else if (expr is UnaryExpr) {

+          UnaryExpr e = (UnaryExpr)expr;

+          Expression se = Substitute(e.E);

+          if (se != e.E) {

+            newExpr = new UnaryExpr(expr.tok, e.Op, se);

+          }

+        } else if (expr is BinaryExpr) {

+          BinaryExpr e = (BinaryExpr)expr;

+          Expression e0 = Substitute(e.E0);

+          Expression e1 = Substitute(e.E1);

+          if (e0 != e.E0 || e1 != e.E1) {

+            BinaryExpr newBin = new BinaryExpr(expr.tok, e.Op, e0, e1);

+            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 LetExpr) {

+          var e = (LetExpr)expr;

+          var rhss = new List<Expression>();

+          bool anythingChanged = false;

+          foreach (var rhs in e.RHSs) {

+            var r = Substitute(rhs);

+            if (r != rhs) {

+              anythingChanged = true;

+            }

+            rhss.Add(r);

+          }

+          var body = Substitute(e.Body);

+          if (anythingChanged || body != e.Body) {

+            newExpr = new LetExpr(e.tok, e.Vars, rhss, body);

+          }

+

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        var body = Substitute(e.Body);

+        var contract = e.Contract == null ? null : Substitute(e.Contract);

+        newExpr = new NamedExpr(e.tok, e.Name, body, contract, e.ReplacerToken);

+        } else if (expr is ComprehensionExpr) {

+          var e = (ComprehensionExpr)expr;

+          Expression newRange = e.Range == null ? null : Substitute(e.Range);

+          Expression newTerm = Substitute(e.Term);

+          Attributes newAttrs = SubstAttributes(e.Attributes);

+          if (e is SetComprehension) {

+            if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

+              newExpr = new SetComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+            }

+          } else if (e is MapComprehension) {

+            if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

+              newExpr = new MapComprehension(expr.tok, e.BoundVars, newRange, newTerm);

+            }

+          } else if (e is QuantifierExpr) {

+            var q = (QuantifierExpr)e;

+            if (newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

+              if (expr is ForallExpr) {

+                newExpr = new ForallExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+              } else {

+                newExpr = new ExistsExpr(expr.tok, e.BoundVars, newRange, newTerm, newAttrs);

+              }

+            }

+          } else {

+            Contract.Assert(false);  // unexpected ComprehensionExpr

           }

+

+        } else if (expr is PredicateExpr) {

+          var e = (PredicateExpr)expr;

+          Expression g = Substitute(e.Guard);

+          Expression b = Substitute(e.Body);

+          if (g != e.Guard || b != e.Body) {

+            if (expr is AssertExpr) {

+              newExpr = new AssertExpr(e.tok, g, b);

+            } else {

+              newExpr = new AssumeExpr(e.tok, g, b);

+            }

+          }

+

+        } else if (expr is ITEExpr) {

+          ITEExpr e = (ITEExpr)expr;

+          Expression test = Substitute(e.Test);

+          Expression thn = Substitute(e.Thn);

+          Expression els = Substitute(e.Els);

+          if (test != e.Test || thn != e.Thn || els != e.Els) {

+            newExpr = new ITEExpr(expr.tok, test, thn, els);

+          }

+

+        } else if (expr is ConcreteSyntaxExpression) {

+          var e = (ConcreteSyntaxExpression)expr;

+          return Substitute(e.ResolvedExpression);

         }

-        if (newElist != null) {

-          newElist.Add(substE);

+

+        if (newExpr == null) {

+          return expr;

+        } else {

+          newExpr.Type = expr.Type;  // resolve on the fly (any additional resolution must be done above)

+          return newExpr;

         }

       }

-      if (newElist == null) {

-        return elist;

-      } else {

-        return newElist;

-      }

-    }

 

-    static Attributes SubstAttributes(Attributes attrs, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

-      Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

-      if (attrs != null) {

-        List<Attributes.Argument> newArgs = new List<Attributes.Argument>();  // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes

-        bool anyArgSubst = false;

-        foreach (Attributes.Argument arg in attrs.Args) {

-          Attributes.Argument newArg = arg;

-          if (arg.E != null) {

-            Expression newE = Substitute(arg.E, receiverReplacement, substMap);

-            if (newE != arg.E) {

-              newArg = new Attributes.Argument(arg.Tok, newE);

-              anyArgSubst = true;

+      protected List<Expression/*!*/>/*!*/ SubstituteExprList(List<Expression/*!*/>/*!*/ elist) {

+        Contract.Requires(cce.NonNullElements(elist));

+        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]);

+          if (substE != elist[i] && newElist == null) {

+            newElist = new List<Expression>();

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

+              newElist.Add(elist[j]);

             }

           }

-          newArgs.Add(newArg);

+          if (newElist != null) {

+            newElist.Add(substE);

+          }

         }

-        if (!anyArgSubst) {

-          newArgs = attrs.Args;

+        if (newElist == null) {

+          return elist;

+        } else {

+          return newElist;

         }

+      }

+

+      Attributes SubstAttributes(Attributes attrs) {

+        Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

+        if (attrs != null) {

+          List<Attributes.Argument> newArgs = new List<Attributes.Argument>();  // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes

+          bool anyArgSubst = false;

+          foreach (Attributes.Argument arg in attrs.Args) {

+            Attributes.Argument newArg = arg;

+            if (arg.E != null) {

+              Expression newE = Substitute(arg.E);

+              if (newE != arg.E) {

+                newArg = new Attributes.Argument(arg.Tok, newE);

+                anyArgSubst = true;

+              }

+            }

+            newArgs.Add(newArg);

+          }

+          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);

+          Attributes prev = SubstAttributes(attrs.Prev);

+          if (newArgs != attrs.Args || prev != attrs.Prev) {

+            return new Attributes(attrs.Name, newArgs, prev);

+          }

         }

+        return attrs;

       }

-      return attrs;

     }

 

   }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 638ccf9f..803e30d3 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -339,9 +339,11 @@ namespace GPUVerify
             PullOutNonLocalAccesses();

         }

 

-        

-

-        

+        private void MergeBlocksIntoPredecessors()

+        {

+            foreach (var impl in Program.TopLevelDeclarations.OfType<Implementation>())

+                VC.VCGen.MergeBlocksIntoPredecessors(Program, impl);

+        }

 

         internal void doit()

         {

@@ -401,6 +403,13 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_abstracted");

             }

 

+            MergeBlocksIntoPredecessors();

+

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_merged_pre_predication");

+            }

+

             MakeKernelPredicated();

 

             if (CommandLineOptions.ShowStages)

@@ -408,6 +417,13 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_predicated");

             }

 

+            MergeBlocksIntoPredecessors();

+

+            if (CommandLineOptions.ShowStages)

+            {

+                emitProgram(outputFilename + "_merged_post_predication");

+            }

+

             MakeKernelDualised();

 

             if (CommandLineOptions.ShowStages)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 31afbdfa..8c6ad875 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -425,7 +425,7 @@ namespace Microsoft.Boogie.SMTLib
               xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

             }

             else {

-              labels = CalculatePath(0);

+              labels = CalculatePath(handler.StartingProcId());

               xlabels = labels;

             }

             Model model = GetErrorModel();

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e3b1cb2d..1f50d4a8 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -367,6 +367,12 @@ namespace Microsoft.Boogie {
       Undetermined

     }

     public class ErrorHandler {

+      // Used in CheckOutcomeCore

+      public virtual int StartingProcId()

+      {

+          return 0;

+      }

+

       public virtual void OnModel(IList<string> labels, Model model) {

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

       }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 1c3fa979..4fa7f0b7 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -7,6 +7,7 @@ using System;
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics;

+using System.Linq;

 using System.Threading;

 using System.IO;

 using Microsoft.Boogie;

@@ -3036,6 +3037,31 @@ namespace VC {
       }

     }

 

+    /// <summary>

+    /// Simplifies the CFG of the given implementation impl by merging each

+    /// basic block with a single predecessor into that predecessor if the

+    /// predecessor has a single successor.

+    /// </summary>

+    public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl) {

+      var blockGraph = prog.ProcessLoops(impl);

+      var predMap = new Dictionary<Block, Block>();

+      foreach (var block in blockGraph.Nodes) {

+        try {

+          var pred = blockGraph.Predecessors(block).Single();

+          if (blockGraph.Successors(pred).Single() == block) {

+            Block predMapping;

+            while (predMap.TryGetValue(pred, out predMapping))

+              pred = predMapping;

+            pred.Cmds.AddRange(block.Cmds);

+            pred.TransferCmd = block.TransferCmd;

+            impl.Blocks.Remove(block);

+            predMap[block] = pred;

+          }

+        // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.

+        } catch (InvalidOperationException) {}

+      }

+    }

+

     static void DumpMap(Hashtable /*Variable->Expr*/ map) {

       Contract.Requires(map != null);

       foreach (DictionaryEntry de in map) {