Added ghost let expressions.

9 files changed, 171 insertions, 37 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 93237acc..ee3820b3 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -156,7 +156,9 @@ namespace Microsoft.Dafny
     }

 

     public BoundVar CloneBoundVar(BoundVar bv) {

-      return new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));

+      var bvNew = new BoundVar(Tok(bv.tok), bv.Name, CloneType(bv.Type));

+      bvNew.IsGhost = bv.IsGhost;

+      return bvNew;

     }

 

     public Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index e93d1f5c..2dac29c1 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -827,9 +827,21 @@ namespace Microsoft.Dafny {
       if (expr is LetExpr) {

         var e = (LetExpr)expr;

         foreach (var v in e.Vars) {

-          Indent(indent);

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

+          if (!v.IsGhost) {

+            Indent(indent);

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

+          }

+        }

+        Contract.Assert(e.Vars.Count == e.RHSs.Count);

+        var i = 0;

+        foreach (var rhs in e.RHSs) {

+          if (!e.Vars[i].IsGhost) {

+            SpillLetVariableDecls(rhs, indent);

+          }

+          i++;

         }

+        SpillLetVariableDecls(e.Body, indent);

+        return;

       }

       foreach (var ee in expr.SubExpressions) {

         SpillLetVariableDecls(ee, indent);

@@ -2336,13 +2348,18 @@ namespace Microsoft.Dafny {
         // preceded by the declaration of x.

         Contract.Assert(e.Vars.Count == e.RHSs.Count);  // checked by resolution

         Contract.Assert(e.Exact);  // because !Exact is ghost only

+        var nonGhostVars = 0;

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

-          wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = ", e.Vars[i].CompileName);

-          TrExpr(e.RHSs[i]);

-          wr.Write(", ");

+          var v = e.Vars[i];

+          if (!v.IsGhost) {

+            wr.Write("Dafny.Helpers.ExpressionSequence(@{0} = ", e.Vars[i].CompileName);

+            TrExpr(e.RHSs[i]);

+            wr.Write(", ");

+            nonGhostVars++;

+          }

         }

         TrExpr(e.Body);

-        for (int i = 0; i < e.Vars.Count; i++) {

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

           wr.Write(")");

         }

 

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index db0b09e8..23c31b0d 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -417,16 +417,23 @@ IdentType<out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId>
   ":"

   Type<out ty>

   .

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

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

+LocalIdentTypeOptional<out VarDecl var, bool isGhost>

+= (. IToken id;  Type ty;  Type optType = null;

   .)

   WildIdent<out id, true>

   [ ":" Type<out ty>             (. optType = ty; .)

   ]

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

   .

-IdentTypeOptional<out BoundVar/*!*/ var>

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

+IdentTypeOptionalG<out BoundVar var, bool isGhost>

+= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);

+  .)

+  IdentTypeOptional<out var>

+  (. var.IsGhost = isGhost; .)

+  .

+IdentTypeOptional<out BoundVar var>

+= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);

+     IToken id;  Type ty;  Type optType = null;

   .)

   WildIdent<out id, true>

   [ ":" Type<out ty>             (. optType = ty; .)

@@ -437,7 +444,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t
 = (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

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

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

-     string name = null; id = Token.NoToken; ty = null; isGhost = false; .)

+     string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; .)

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

   ]

   ( TypeAndToken<out id, out ty>

@@ -1908,17 +1915,20 @@ StmtInExpr<out Statement s>
   .

 

 LetExpr<out Expression e, bool allowSemi>

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

+= (. IToken x = null;

      e = dummyExpr;

      BoundVar d;

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

      bool exact = true;

+     bool isGhost = false;

   .)

-    "var"                           (. x = t;

+    [ "ghost"                       (. isGhost = true;  x = t; .)

+    ]

+    "var"                           (. if (!isGhost) { x = t; }

                                        letVars = new List<BoundVar>();

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

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

-    { "," IdentTypeOptional<out d>  (. letVars.Add(d); .)

+    IdentTypeOptionalG<out d, isGhost>        (. letVars.Add(d); .)

+    { "," IdentTypeOptionalG<out d, isGhost>  (. letVars.Add(d); .)

     }

     ( ":="

     | ":|"                          (. exact = false; .)

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 8f89b1cd..c9d7dfe2 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1821,7 +1821,7 @@ namespace Microsoft.Dafny {
     public abstract bool IsMutable {

       get;

     }

-    bool isGhost;  // readonly, except for BoundVar's of match expressions/statements during resolution

+    bool isGhost;  // readonly after resolution

     public bool IsGhost {

       get {

         return isGhost;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ea209e0e..f11e1396 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1024,8 +1024,8 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		TypeAndToken(out tok, out ty);

 	}

 

-	void LocalIdentTypeOptional(out VarDecl/*!*/ var, bool isGhost) {

-		IToken/*!*/ id;  Type/*!*/ ty;  Type optType = null;

+	void LocalIdentTypeOptional(out VarDecl var, bool isGhost) {

+		IToken id;  Type ty;  Type optType = null;

 		

 		WildIdent(out id, true);

 		if (la.kind == 6) {

@@ -1036,8 +1036,16 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		var = new VarDecl(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); 

 	}

 

-	void IdentTypeOptional(out BoundVar/*!*/ var) {

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

+	void IdentTypeOptionalG(out BoundVar var, bool isGhost) {

+		Contract.Ensures(Contract.ValueAtReturn(out var) != null);

+		

+		IdentTypeOptional(out var);

+		var.IsGhost = isGhost; 

+	}

+

+	void IdentTypeOptional(out BoundVar var) {

+		Contract.Ensures(Contract.ValueAtReturn(out var) != null);

+		IToken id;  Type ty;  Type optType = null;

 		

 		WildIdent(out id, true);

 		if (la.kind == 6) {

@@ -1052,7 +1060,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);

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

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

-		string name = null; id = Token.NoToken; ty = null; isGhost = false; 

+		string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; 

 		if (la.kind == 24) {

 			Get();

 			isGhost = true; 

@@ -2810,7 +2818,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); 

 			break;

 		}

-		case 29: case 55: case 64: case 70: case 74: case 80: case 81: case 83: case 85: case 118: case 119: case 120: {

+		case 24: case 29: case 55: case 64: case 70: case 74: case 80: case 81: case 83: case 85: case 118: case 119: case 120: {

 			EndlessExpression(out e, allowSemi);

 			break;

 		}

@@ -2919,7 +2927,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new StmtExpr(s.Tok, s, e); 

 			break;

 		}

-		case 29: {

+		case 24: case 29: {

 			LetExpr(out e, allowSemi);

 			break;

 		}

@@ -3333,21 +3341,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}

 

 	void LetExpr(out Expression e, bool allowSemi) {

-		IToken/*!*/ x;

+		IToken x = null;

 		e = dummyExpr;

 		BoundVar d;

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

 		bool exact = true;

+		bool isGhost = false;

 		

+		if (la.kind == 24) {

+			Get();

+			isGhost = true;  x = t; 

+		}

 		Expect(29);

-		x = t;

+		if (!isGhost) { x = t; }

 		letVars = new List<BoundVar>();

 		letRHSs = new List<Expression>(); 

-		IdentTypeOptional(out d);

+		IdentTypeOptionalG(out d, isGhost);

 		letVars.Add(d); 

 		while (la.kind == 30) {

 			Get();

-			IdentTypeOptional(out d);

+			IdentTypeOptionalG(out d, isGhost);

 			letVars.Add(d); 

 		}

 		if (la.kind == 67) {

@@ -3468,17 +3481,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,T,T,x, T,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, 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,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,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},

 		{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,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,T,T,T, x,x,x,x, T,x,T,x, x,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,T, T,x,T,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

+		{x,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, 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,T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,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, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,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, x,x,T,T, T,T,T,T, 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,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,T, x,x,x,x, T,x,T,x, x,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

-		{x,T,T,T, x,x,x,x, T,x,T,T, x,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,T, T,x,T,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

+		{x,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

+		{x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

 		{T,T,T,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, x,x,x,x, x,T,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, T,T,x,x, T,x,T,x, x,x,T,x, x,x,T,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, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x},

-		{x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

-		{x,T,T,T, x,x,x,x, T,x,T,T, x,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

+		{x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

+		{x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, 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, T,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,T, T,T,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,T,T,T, x,x,x,x, T,x,T,T, x,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

+		{x,T,T,T, x,x,x,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x},

 		{x,x,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,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,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,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,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,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},

@@ -3486,7 +3499,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{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, T,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,T, T,T,T,T, T,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,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,T, T,T,x,T, x,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, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x},

 		{x,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,T,x,x, x,T,T,T, x,x,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,T,x,T, T,T,x,T, x,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, T,x,x,x, x,x,x,x, T,T,x,x, x,T,T,x, x},

-		{x,T,T,T, x,T,x,x, T,x,T,x, x,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x}

+		{x,T,T,T, x,T,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,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,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,x,x,x, x}

 

 	};

 } // end Parser

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index fe2c2d4a..048a75b8 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -6382,6 +6382,16 @@ namespace Microsoft.Dafny
         if (!e.Exact) {

           Error(expr, "let-such-that expressions are allowed only in ghost contexts");

         }

+        Contract.Assert(e.Vars.Count == e.RHSs.Count);

+        var i = 0;

+        foreach (var ee in e.RHSs) {

+          if (!e.Vars[i].IsGhost) {

+            CheckIsNonGhost(ee);

+          }

+          i++;

+        }

+        CheckIsNonGhost(e.Body);

+        return;

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

         if (e.MissingBounds != null) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5ef39185..0ce33b47 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -434,6 +434,10 @@ ResolutionErrors.dfy(735,19): Error: a while statement used inside a hint is not
 ResolutionErrors.dfy(760,4): Error: calls to methods with side-effects are not allowed inside a statement expression

 ResolutionErrors.dfy(761,4): Error: only ghost methods can be called from this context

 ResolutionErrors.dfy(762,4): Error: wrong number of method result arguments (got 0, expected 1)

+ResolutionErrors.dfy(773,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(783,4): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(794,36): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(803,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -507,7 +511,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses

-110 resolution/type errors detected in ResolutionErrors.dfy

+114 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -2320,7 +2324,7 @@ Dafny program verifier finished with 9 verified, 6 errors
 

 Dafny program verifier finished with 0 verified, 0 errors

 

-Dafny program verifier finished with 37 verified, 0 errors

+Dafny program verifier finished with 44 verified, 0 errors

 Compiled assembly into Compilation.exe

 

 Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 734cc3e6..27691178 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -170,3 +170,40 @@ method hidden_test()
   reveal_hidden();

   assert hidden() == 7;

 }

+

+// ----- LetExpr with ghosts and in ghost contexts -----

+

+module GhostLetExpr {

+  method M() {

+    ghost var y;

+    var x;

+    var g := G(x, y);

+    ghost var h := var ta := F(); 5;

+    var j := ghost var tb := F(); 5;

+    assert h == j;

+  }

+

+  function F(): int

+  { 5 }

+

+  function method G(x: int, ghost y: int): int

+  { assert y == y; x }

+

+  datatype Dt = MyRecord(a: int, ghost b: int)

+

+  method P(dt: Dt) {

+    match dt {

+      case MyRecord(aa, bb) =>

+        ghost var z := bb + F();

+        ghost var t0 := var y := z; z + 3;

+        ghost var t1 := ghost var y := z; z + 3;

+        var t2 := ghost var y := z; aa + 3;

+    }

+  }

+

+  function method FM(): int

+  {

+    ghost var xyz := F();

+    G(5, xyz)

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 926f08ae..40963e36 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -763,3 +763,44 @@ module StatementsInExpressions {
     10

   }

 }

+

+module GhostLetExpr {

+  method M() {

+    ghost var y;

+    var x;

+    var g := G(x, y);

+    ghost var h := ghost var ta := F(); 5;

+    var j := var tb := F(); 5;  // error: allowed only if 'tb' were ghost

+    assert h == j;

+  }

+

+  function F(): int

+  { 5 }

+

+  function method G(x: int, ghost y: int): int

+  {

+    assert y == x;

+    y  // error: not allowed in non-ghost context

+  }

+

+  datatype Dt = MyRecord(a: int, ghost b: int)

+

+  method P(dt: Dt) {

+    match dt {

+      case MyRecord(aa, bb) =>

+        ghost var z := aa + F();

+        ghost var t0 := var y := z; z + 3;

+        ghost var t1 := ghost var y := z + bb; y + z + 3;

+        var t2 := ghost var y := z; y + 3;  // error: 'y' can only be used in ghost contexts

+    }

+  }

+

+  function method FM(e: bool): int

+  {

+    if e then

+      G(5, F())

+    else

+      var xyz := F();  // error: 'xyz' needs to be declared ghost to allow this

+      G(5, xyz)

+  }

+}