Merge

6 files changed, 494 insertions, 114 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7c8536a3..78e7675e 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -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.>

@@ -756,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;

@@ -829,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;

@@ -1467,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>

@@ -1483,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); .)

@@ -1495,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 e5f17cc8..e9a4ce4b 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -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;

     }

@@ -844,6 +840,7 @@ namespace Microsoft.Dafny {
     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) {

@@ -921,7 +918,7 @@ namespace Microsoft.Dafny {
   }

 

   public class DefaultModuleDecl : ModuleDefinition {

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

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

     }

     public override bool IsDefaultModule {

       get {

@@ -2535,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)

@@ -2548,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,

@@ -3412,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:

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index ead518ec..8d6fa510 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -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("("); }

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index bc394f04..5ddc1fac 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -62,10 +62,8 @@ 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) {

-      if (m.RefinementBase == null) {

-        // This Rewriter doesn't do anything

-        return;

-      }

+      

+      if (m.RefinementBase == null) return;

 

       if (moduleUnderConstruction != null) {

         postTasks.Clear();

@@ -280,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 {

@@ -425,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);

@@ -702,8 +703,12 @@ 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;

@@ -804,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);

@@ -920,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.

@@ -929,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 403a7352..71210c9f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -174,11 +174,14 @@ namespace Microsoft.Dafny {
           literalDecl.Signature.Refines = refinedSig;

           var sig = literalDecl.Signature;

           // set up environment

+          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

@@ -220,7 +223,7 @@ namespace Microsoft.Dafny {
       // resolve

       var datatypeDependencies = new Graph<IndDatatypeDecl>();

       int prevErrorCount = ErrorCount;

-      ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

+      ResolveTopLevelDecls_Signatures(m, m.TopLevelDecls, datatypeDependencies);

       if (ErrorCount == prevErrorCount)

         ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

     }

@@ -359,13 +362,14 @@ namespace Microsoft.Dafny {
       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) {

@@ -566,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 {

@@ -802,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) {

@@ -814,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);

         }

@@ -1938,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;

@@ -1947,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;

+            }

+          }

+          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 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);

+          } else {

+            // error has already been reported

           }

 

           if (d == null) {

@@ -3578,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) {

@@ -3982,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();

@@ -4246,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);

@@ -4343,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]);

           }

@@ -4387,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) {

@@ -4606,6 +4642,7 @@ namespace Microsoft.Dafny {
 

       TopLevelDecl decl;

       MemberDecl member;

+      Tuple<DatatypeCtor, bool> pair;

       var id = e.Tokens[p];

       if (sig.TopLevels.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

@@ -4626,11 +4663,25 @@ 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

@@ -5408,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/Translator.cs b/Source/Dafny/Translator.cs
index fdc9ed9e..0d97456d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2052,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);

@@ -2515,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);

@@ -6008,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();

@@ -8090,6 +8105,11 @@ namespace Microsoft.Dafny {
             newExpr = new LetExpr(e.tok, e.Vars, rhss, body);

           }

 

+      } else if (expr is NamedExpr) {

+        var e = (NamedExpr)expr;

+        var body = Substitute(e.Body, receiverReplacement, substMap);

+        var contract = e.Contract == null ? null : Substitute(e.Contract, receiverReplacement, substMap);

+        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);