From c30399af4efff99373f901bd914e8b3d8bb811dc Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Thu, 5 Jul 2012 11:41:10 -0700
Subject: Dafny: disallow importing ghost modules into physical ones.

---
 Source/Dafny/Resolver.cs | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6f9d5dae..1463c4c0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -227,7 +227,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);
     }
@@ -373,6 +373,7 @@ namespace Microsoft.Dafny {
       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) {
@@ -806,7 +807,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) {
@@ -818,7 +819,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);
         }
-- 
cgit v1.2.3


From 992a12ac28bb9ab1b51e047ec3a5840a0c37cc64 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Thu, 5 Jul 2012 11:54:03 -0700
Subject: Dafny: Fixed bug in autocontracts where the post resolver was run
 even if there were resolution errors.

---
 Source/Dafny/Resolver.cs | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1463c4c0..81d79085 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
-- 
cgit v1.2.3


From 50b708706ee9264c9f74c43552c3a8bd9c7ee6fa Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Thu, 5 Jul 2012 17:52:22 -0700
Subject: Dafny: fixed a crash in datatype argument resolution

---
 Source/Dafny/Resolver.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 81d79085..04350247 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4290,7 +4290,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]);
           }
-- 
cgit v1.2.3


From 0dbff05a81137f327080fe16120acdb033903971 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Fri, 6 Jul 2012 11:22:42 -0700
Subject: Dafny: datatype constructors can be accessed across module
 boundaries.

---
 Source/Dafny/Resolver.cs | 94 ++++++++++++++++++++++++++++--------------------
 1 file changed, 56 insertions(+), 38 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 04350247..05cbc74f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3525,44 +3525,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) {
@@ -4193,6 +4158,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);
@@ -4551,6 +4554,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) {
@@ -4571,11 +4575,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
-- 
cgit v1.2.3


From 68226762bab879cb8ba5b0fc456359682565a4b9 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Fri, 6 Jul 2012 13:58:31 -0700
Subject: Dafny: types can now be qualified with full module paths

---
 Source/Dafny/Dafny.atg                | 25 ++++++++++++++-----------
 Source/Dafny/DafnyAst.cs              | 26 +++++++++++---------------
 Source/Dafny/Parser.cs                | 17 +++++++++--------
 Source/Dafny/RefinementTransformer.cs |  2 +-
 Source/Dafny/Resolver.cs              | 31 ++++++++++++++++++++-----------
 Test/dafny0/Answer                    | 26 +++++++++++++-------------
 6 files changed, 68 insertions(+), 59 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index d0dd4169..8f9a7717 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.>
@@ -802,16 +803,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;
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index e6a693fa..9d426421 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;
     }
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 0c6cc993..15ea873c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -984,8 +984,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,16 +1005,17 @@ 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); 
+			ty = new UserDefinedType(tok, tok.val, gt, path); 
 		} else SynErr(133);
 	}
 
@@ -1576,11 +1577,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;
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 0d32e24e..0a653f6c 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -279,7 +279,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 {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 05cbc74f..0a18b783 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -577,7 +577,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 {
@@ -1885,7 +1885,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;
@@ -1894,17 +1894,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) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 85958099..a55d68a8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -714,28 +714,28 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
 Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
 Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
 Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
-Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
-Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)
-Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)
-Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)
-Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
-Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
+Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
+Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget to qualify a name?)
+Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget to qualify a name?)
+Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)
+Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget to qualify a name?)
+Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
+Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
+Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
 Modules0.dfy(221,8): Error: new can be applied only to reference types (got X)
-Modules0.dfy(230,13): Error: The name does not exist in the given module
+Modules0.dfy(230,13): Error: Undeclared type X in module B
 Modules0.dfy(240,13): Error: unresolved identifier: X
 Modules0.dfy(241,15): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget a module import?)
+Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
 Modules0.dfy(280,12): Error: new can be applied only to reference types (got D)
 Modules0.dfy(283,25): Error: type of the receiver is not fully determined at this program point
 Modules0.dfy(284,16): Error: type of the receiver is not fully determined at this program point
 Modules0.dfy(284,6): Error: expected method call, found expression
 Modules0.dfy(285,16): Error: type of the receiver is not fully determined at this program point
 Modules0.dfy(285,6): Error: expected method call, found expression
-Modules0.dfy(307,24): Error: Undeclared module name: Q_Imp (did you forget a module import?)
-Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)
+Modules0.dfy(307,24): Error: module Q_Imp does not exist
+Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name?)
 28 resolution/type errors detected in Modules0.dfy
 
 -------------------- Modules1.dfy --------------------
-- 
cgit v1.2.3


From 88e8eb7376303394afc55e2d3ffb6b662ba27cd5 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 9 Jul 2012 13:44:35 -0700
Subject: Dafny: added named expressions and replacement

---
 Source/Dafny/Dafny.atg                |  44 +-
 Source/Dafny/DafnyAst.cs              |  32 ++
 Source/Dafny/Parser.cs                | 769 ++++++++++++++++++----------------
 Source/Dafny/Printer.cs               |   7 +-
 Source/Dafny/RefinementTransformer.cs | 270 +++++++++++-
 Source/Dafny/Resolver.cs              |  13 +-
 Source/Dafny/Scanner.cs               | 122 +++---
 Source/Dafny/Translator.cs            |  16 +-
 8 files changed, 826 insertions(+), 447 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 8f9a7717..958726fd 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -730,10 +730,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;
@@ -1443,8 +1456,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>
@@ -1459,7 +1470,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); .)
@@ -1471,8 +1493,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, 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 9d426421..c2a4ace3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2495,10 +2495,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)
@@ -2508,6 +2511,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,
@@ -3373,6 +3383,28 @@ namespace Microsoft.Dafny {
     }
   }
 
+  public class NamedExpr : Expression
+  {
+    public readonly string Name;
+    public readonly Expression Body;
+    public NamedExpr(IToken tok, IToken name, Expression body)
+      : base(tok) {
+      Name = name.val;
+      Body = body;
+    }
+
+    public NamedExpr(IToken tok, string p, Expression body)
+      : base(tok) {
+      Name = p;
+      Body = body;
+    }
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        yield return Body;
+      }
+    }
+  }
+
   /// <summary>
   /// A ComprehensionExpr has the form:
   ///   BINDER x Attributes | Range(x) :: Term(x)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 15ea873c..6adc4df0 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 = 109;
 
 	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(110);
 		}
 		DefaultClassDecl defaultClass = null;
 		foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
@@ -275,7 +275,7 @@ bool IsAttribute() {
 					module.TopLevelDecls.Add(at); 
 				} else if (StartOf(2)) {
 					ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false);
-				} else SynErr(109);
+				} else SynErr(111);
 			}
 			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(112);
 	}
 
 	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(113); 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(114); Get();}
 		if (la.kind == 17) {
 			Get();
 		} else if (la.kind == 18) {
 			Get();
 			co = true; 
-		} else SynErr(113);
+		} else SynErr(115);
 		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(116); 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(117); Get();}
 		Expect(12);
 	}
 
@@ -412,7 +412,7 @@ bool IsAttribute() {
 		} else if (la.kind == 28 || la.kind == 29) {
 			MethodDecl(mmod, allowConstructors, out m);
 			mm.Add(m); 
-		} else SynErr(116);
+		} else SynErr(118);
 	}
 
 	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(119); 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(120); Get();}
 		Expect(12);
 	}
 
@@ -543,7 +543,7 @@ bool IsAttribute() {
 				Get();
 				signatureOmitted = true;
 				openParen = Token.NoToken; 
-			} else SynErr(119);
+			} else SynErr(121);
 		} else if (la.kind == 46) {
 			Get();
 			isPredicate = true; 
@@ -572,8 +572,8 @@ bool IsAttribute() {
 				Get();
 				signatureOmitted = true;
 				openParen = Token.NoToken; 
-			} else SynErr(120);
-		} else SynErr(121);
+			} else SynErr(122);
+		} else SynErr(123);
 		while (StartOf(4)) {
 			FunctionSpec(reqs, reads, ens, decreases);
 		}
@@ -612,7 +612,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(124); Get();}
 		if (la.kind == 28) {
 			Get();
 		} else if (la.kind == 29) {
@@ -623,7 +623,7 @@ bool IsAttribute() {
 			 SemErr(t, "constructors are only allowed in classes");
 			}
 			
-		} else SynErr(123);
+		} else SynErr(125);
 		if (isConstructor) {
 		 if (mmod.IsGhost) {
 		   SemErr(t, "constructors cannot be declared 'ghost'");
@@ -650,7 +650,7 @@ bool IsAttribute() {
 		} else if (la.kind == 31) {
 			Get();
 			signatureOmitted = true; openParen = Token.NoToken; 
-		} else SynErr(124);
+		} else SynErr(126);
 		while (StartOf(5)) {
 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
 		}
@@ -844,7 +844,7 @@ bool IsAttribute() {
 			ReferenceType(out tok, out ty);
 			break;
 		}
-		default: SynErr(125); break;
+		default: SynErr(127); break;
 		}
 	}
 
@@ -869,7 +869,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(128); Get();}
 		if (la.kind == 32) {
 			Get();
 			while (IsAttribute()) {
@@ -884,7 +884,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(129); Get();}
 			Expect(12);
 		} else if (la.kind == 33 || la.kind == 34 || la.kind == 35) {
 			if (la.kind == 33) {
@@ -894,7 +894,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(130); Get();}
 				Expect(12);
 				req.Add(new MaybeFreeExpression(e, isFree)); 
 			} else if (la.kind == 35) {
@@ -903,19 +903,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(131); Get();}
 				Expect(12);
 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 
-			} else SynErr(130);
+			} else SynErr(132);
 		} 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(133); Get();}
 			Expect(12);
-		} else SynErr(132);
+		} else SynErr(134);
 	}
 
 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1016,17 +1016,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				GenericInstantiation(gt);
 			}
 			ty = new UserDefinedType(tok, tok.val, gt, path); 
-		} else SynErr(133);
+		} else SynErr(135);
 	}
 
 	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));
 		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(136); Get();}
 			Get();
 			Expression(out e);
-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();}
+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();}
 			Expect(12);
 			reqs.Add(e); 
 		} else if (la.kind == 47) {
@@ -1040,20 +1040,20 @@ 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(138); 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(139); Get();}
 			Expect(12);
 			ens.Add(e); 
 		} else if (la.kind == 36) {
 			Get();
 			DecreasesList(decreases, false);
-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();}
+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(140); Get();}
 			Expect(12);
-		} else SynErr(139);
+		} else SynErr(141);
 	}
 
 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1072,7 +1072,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			fe = new FrameExpression(new WildcardExpr(t), null); 
 		} else if (StartOf(8)) {
 			FrameExpression(out fe);
-		} else SynErr(140);
+		} else SynErr(142);
 	}
 
 	void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -1083,7 +1083,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new WildcardExpr(t); 
 		} else if (StartOf(8)) {
 			Expression(out e);
-		} else SynErr(141);
+		} else SynErr(143);
 	}
 
 	void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1100,26 +1100,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(144); Get();}
 		switch (la.kind) {
 		case 6: {
 			BlockStmt(out bs, out bodyStart, out bodyEnd);
 			s = bs; 
 			break;
 		}
-		case 67: {
+		case 68: {
 			AssertStmt(out s);
 			break;
 		}
-		case 55: {
+		case 56: {
 			AssumeStmt(out s);
 			break;
 		}
-		case 68: {
+		case 69: {
 			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 93: case 94: case 95: case 96: case 97: case 98: case 99: {
 			UpdateStmt(out s);
 			break;
 		}
@@ -1127,19 +1127,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			VarDeclStatement(out s);
 			break;
 		}
-		case 60: {
+		case 61: {
 			IfStmt(out s);
 			break;
 		}
-		case 64: {
+		case 65: {
 			WhileStmt(out s);
 			break;
 		}
-		case 66: {
+		case 67: {
 			MatchStmt(out s);
 			break;
 		}
-		case 69: {
+		case 70: {
 			ParallelStmt(out s);
 			break;
 		}
@@ -1163,23 +1163,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Get();
 					breakCount++; 
 				}
-			} else SynErr(143);
-			while (!(la.kind == 0 || la.kind == 12)) {SynErr(144); Get();}
+			} else SynErr(145);
+			while (!(la.kind == 0 || la.kind == 12)) {SynErr(146); Get();}
 			Expect(12);
 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 
 			break;
 		}
-		case 52: {
+		case 53: {
 			ReturnStmt(out s);
 			break;
 		}
 		case 31: {
-			Get();
-			s = new SkeletonStatement(t); 
+			SkeletonStmt(out s);
 			Expect(12);
 			break;
 		}
-		default: SynErr(145); break;
+		default: SynErr(147); break;
 		}
 	}
 
@@ -1187,7 +1186,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(68);
 		x = t; 
 		while (IsAttribute()) {
 			Attribute(ref attrs);
@@ -1196,7 +1195,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);
 		} else if (la.kind == 31) {
 			Get();
-		} else SynErr(146);
+		} else SynErr(148);
 		Expect(12);
 		if (e == null) {
 		 s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false);
@@ -1210,7 +1209,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(56);
 		x = t; 
 		while (IsAttribute()) {
 			Attribute(ref attrs);
@@ -1219,7 +1218,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);
 		} else if (la.kind == 31) {
 			Get();
-		} else SynErr(147);
+		} else SynErr(149);
 		if (e == null) {
 		 s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
 		} else {
@@ -1233,7 +1232,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(69);
 		x = t; 
 		AttributeArg(out arg);
 		args.Add(arg); 
@@ -1264,14 +1263,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 == 54 || la.kind == 55) {
 			lhss.Add(e);  lhs0 = e; 
 			while (la.kind == 21) {
 				Get();
 				Lhs(out e);
 				lhss.Add(e); 
 			}
-			if (la.kind == 53) {
+			if (la.kind == 54) {
 				Get();
 				x = t; 
 				Rhs(out r, lhs0);
@@ -1281,20 +1280,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 == 55) {
 				Get();
 				x = t; 
-				if (la.kind == 55) {
+				if (la.kind == 56) {
 					Get();
 					suchThatAssume = t; 
 				}
 				Expression(out suchThat);
-			} else SynErr(148);
+			} else SynErr(150);
 			Expect(12);
 		} else if (la.kind == 5) {
 			Get();
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 
-		} else SynErr(149);
+		} else SynErr(151);
 		if (suchThat != null) {
 		 s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
 		} else {
@@ -1329,8 +1328,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 == 54 || la.kind == 55) {
+			if (la.kind == 54) {
 				Get();
 				assignTok = t;
 				lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1346,7 +1345,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {
 				Get();
 				assignTok = t; 
-				if (la.kind == 55) {
+				if (la.kind == 56) {
 					Get();
 					suchThatAssume = t; 
 				}
@@ -1385,7 +1384,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;
 		ifStmt = dummyStmt;  // to please the compiler
 		
-		Expect(60);
+		Expect(61);
 		x = t; 
 		if (la.kind == 23 || la.kind == 31) {
 			if (la.kind == 23) {
@@ -1395,15 +1394,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 == 62) {
 				Get();
-				if (la.kind == 60) {
+				if (la.kind == 61) {
 					IfStmt(out s);
 					els = s; 
 				} else if (la.kind == 6) {
 					BlockStmt(out bs, out bodyStart, out bodyEnd);
 					els = bs; 
-				} else SynErr(150);
+				} else SynErr(152);
 			}
 			if (guardOmitted) {
 			 ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false);
@@ -1414,7 +1413,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(153);
 	}
 
 	void WhileStmt(out Statement/*!*/ stmt) {
@@ -1430,7 +1429,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<GuardedAlternative> alternatives;
 		stmt = dummyStmt;  // to please the compiler
 		
-		Expect(64);
+		Expect(65);
 		x = t; 
 		if (la.kind == 23 || la.kind == 31) {
 			if (la.kind == 23) {
@@ -1446,7 +1445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else if (la.kind == 31) {
 				Get();
 				bodyOmitted = true; 
-			} else SynErr(152);
+			} else SynErr(154);
 			if (guardOmitted || bodyOmitted) {
 			 if (mod != null) {
 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -1464,18 +1463,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(155);
 	}
 
 	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(67);
 		x = t; 
 		Expression(out e);
 		Expect(6);
-		while (la.kind == 62) {
+		while (la.kind == 63) {
 			CaseStatement(out c);
 			cases.Add(c); 
 		}
@@ -1495,7 +1494,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BlockStmt/*!*/ block;
 		IToken bodyStart, bodyEnd;
 		
-		Expect(69);
+		Expect(70);
 		x = t; 
 		Expect(23);
 		if (la.kind == 1) {
@@ -1528,7 +1527,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<AssignmentRhs> rhss = null;
 		AssignmentRhs r;
 		
-		Expect(52);
+		Expect(53);
 		returnTok = t; 
 		if (StartOf(13)) {
 			Rhs(out r, null);
@@ -1543,6 +1542,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 == 52) {
+			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;
@@ -1552,16 +1576,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 == 57) {
 			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 == 58) {
+				if (la.kind == 58) {
 					Get();
 					ee = new List<Expression>(); 
 					Expressions(ee);
-					Expect(58);
+					Expect(59);
 					UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
 					
 				} else if (la.kind == 14) {
@@ -1603,7 +1627,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 r = new TypeRhs(newToken, ty, initCall);
 			}
 			
-		} else if (la.kind == 59) {
+		} else if (la.kind == 60) {
 			Get();
 			x = t; 
 			Expression(out e);
@@ -1614,7 +1638,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(8)) {
 			Expression(out e);
 			r = new ExprRhs(e); 
-		} else SynErr(154);
+		} else SynErr(156);
 		while (la.kind == 6) {
 			Attribute(ref attrs);
 		}
@@ -1626,16 +1650,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 == 58) {
 				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 == 58) {
 				Suffix(ref e);
 			}
-		} else SynErr(155);
+		} else SynErr(157);
 	}
 
 	void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1658,7 +1682,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(8)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(156);
+		} else SynErr(158);
 		Expect(25);
 	}
 
@@ -1669,11 +1693,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		List<Statement> body;
 		
 		Expect(6);
-		while (la.kind == 62) {
+		while (la.kind == 63) {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(63);
+			Expect(64);
 			body = new List<Statement>(); 
 			while (StartOf(9)) {
 				Stmt(body);
@@ -1691,22 +1715,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 == 66) {
 				Invariant(out invariant);
-				while (!(la.kind == 0 || la.kind == 12)) {SynErr(157); Get();}
+				while (!(la.kind == 0 || la.kind == 12)) {SynErr(159); 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(160); 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(161); Get();}
 				Expect(12);
 			} else {
-				while (!(la.kind == 0 || la.kind == 32)) {SynErr(160); Get();}
+				while (!(la.kind == 0 || la.kind == 32)) {SynErr(162); Get();}
 				Get();
 				while (IsAttribute()) {
 					Attribute(ref modAttrs);
@@ -1721,7 +1745,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(163); Get();}
 				Expect(12);
 			}
 		}
@@ -1729,12 +1753,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 == 66)) {SynErr(164); Get();}
 		if (la.kind == 33) {
 			Get();
 			isFree = true; 
 		}
-		Expect(65);
+		Expect(66);
 		while (IsAttribute()) {
 			Attribute(ref attrs);
 		}
@@ -1749,7 +1773,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BoundVar/*!*/ bv;
 		List<Statement/*!*/> body = new List<Statement/*!*/>();
 		
-		Expect(62);
+		Expect(63);
 		x = t; 
 		Ident(out id);
 		if (la.kind == 23) {
@@ -1763,7 +1787,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			Expect(25);
 		}
-		Expect(63);
+		Expect(64);
 		while (StartOf(9)) {
 			Stmt(body);
 		}
@@ -1778,7 +1802,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(165);
 	}
 
 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1806,7 +1830,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 == 71 || la.kind == 72) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1817,7 +1841,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 == 73 || la.kind == 74) {
 			ImpliesOp();
 			x = t; 
 			ImpliesExpression(out e1);
@@ -1826,23 +1850,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	void EquivOp() {
-		if (la.kind == 70) {
+		if (la.kind == 71) {
 			Get();
-		} else if (la.kind == 71) {
+		} else if (la.kind == 72) {
 			Get();
-		} else SynErr(164);
+		} else SynErr(166);
 	}
 
 	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 == 75 || la.kind == 76) {
 				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 == 75 || la.kind == 76) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1853,7 +1877,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 == 77 || la.kind == 78) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1864,11 +1888,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 72) {
+		if (la.kind == 73) {
 			Get();
-		} else if (la.kind == 73) {
+		} else if (la.kind == 74) {
 			Get();
-		} else SynErr(165);
+		} else SynErr(167);
 	}
 
 	void RelationalExpression(out Expression/*!*/ e) {
@@ -1962,25 +1986,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	}
 
 	void AndOp() {
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			Get();
-		} else if (la.kind == 75) {
+		} else if (la.kind == 76) {
 			Get();
-		} else SynErr(166);
+		} else SynErr(168);
 	}
 
 	void OrOp() {
-		if (la.kind == 76) {
+		if (la.kind == 77) {
 			Get();
-		} else if (la.kind == 77) {
+		} else if (la.kind == 78) {
 			Get();
-		} else SynErr(167);
+		} else SynErr(169);
 	}
 
 	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 == 88 || la.kind == 89) {
 			AddOp(out x, out op);
 			Factor(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -2008,35 +2032,35 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Gt; 
 			break;
 		}
-		case 78: {
+		case 79: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 79: {
+		case 80: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 80: {
+		case 81: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 81: {
+		case 82: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Disjoint; 
 			break;
 		}
-		case 82: {
+		case 83: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.In; 
 			break;
 		}
-		case 83: {
+		case 84: {
 			Get();
 			x = t;  y = Token.NoToken; 
-			if (la.kind == 82) {
+			if (la.kind == 83) {
 				Get();
 				y = t; 
 			}
@@ -2051,29 +2075,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			
 			break;
 		}
-		case 84: {
+		case 85: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 85: {
+		case 86: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 86: {
+		case 87: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(168); break;
+		default: SynErr(170); 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 == 48 || la.kind == 90 || la.kind == 91) {
 			MulOp(out x, out op);
 			UnaryExpression(out e1);
 			e0 = new BinaryExpr(x, op, e0, e1); 
@@ -2082,44 +2106,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 == 88) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Add; 
-		} else if (la.kind == 88) {
+		} else if (la.kind == 89) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Sub; 
-		} else SynErr(169);
+		} else SynErr(171);
 	}
 
 	void UnaryExpression(out Expression/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 
 		switch (la.kind) {
-		case 88: {
+		case 89: {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e); 
 			break;
 		}
-		case 83: case 91: {
+		case 84: case 92: {
 			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 56: case 61: case 67: case 68: case 101: case 103: case 104: case 105: case 106: {
 			EndlessExpression(out e);
 			break;
 		}
 		case 1: {
 			DottedIdentifiersAndFunction(out e);
-			while (la.kind == 14 || la.kind == 57) {
+			while (la.kind == 14 || la.kind == 58) {
 				Suffix(ref e);
 			}
 			break;
 		}
-		case 6: case 57: {
+		case 6: case 58: {
 			DisplayExpr(out e);
 			break;
 		}
@@ -2131,14 +2155,14 @@ 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 93: case 94: case 95: case 96: case 97: case 98: case 99: {
 			ConstAtomExpression(out e);
-			while (la.kind == 14 || la.kind == 57) {
+			while (la.kind == 14 || la.kind == 58) {
 				Suffix(ref e);
 			}
 			break;
 		}
-		default: SynErr(170); break;
+		default: SynErr(172); break;
 		}
 	}
 
@@ -2147,47 +2171,45 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		if (la.kind == 48) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mul; 
-		} else if (la.kind == 89) {
+		} else if (la.kind == 90) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Div; 
-		} else if (la.kind == 90) {
+		} else if (la.kind == 91) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mod; 
-		} else SynErr(171);
+		} else SynErr(173);
 	}
 
 	void NegOp() {
-		if (la.kind == 83) {
+		if (la.kind == 84) {
 			Get();
-		} else if (la.kind == 91) {
+		} else if (la.kind == 92) {
 			Get();
-		} else SynErr(172);
+		} else SynErr(174);
 	}
 
 	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 61: {
 			Get();
 			x = t; 
 			Expression(out e);
-			Expect(99);
+			Expect(100);
 			Expression(out e0);
-			Expect(61);
+			Expect(62);
 			Expression(out e1);
 			e = new ITEExpr(x, e, e0, e1); 
 			break;
 		}
-		case 66: {
+		case 67: {
 			MatchExpression(out e);
 			break;
 		}
-		case 101: case 102: case 103: case 104: {
+		case 103: case 104: case 105: case 106: {
 			QuantifierGuts(out e);
 			break;
 		}
@@ -2195,7 +2217,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ComprehensionExpr(out e);
 			break;
 		}
-		case 67: {
+		case 68: {
 			Get();
 			x = t; 
 			Expression(out e0);
@@ -2204,7 +2226,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AssertExpr(x, e0, e1); 
 			break;
 		}
-		case 55: {
+		case 56: {
 			Get();
 			x = t; 
 			Expression(out e0);
@@ -2214,31 +2236,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 101: {
+			NamedExpr(out e);
 			break;
 		}
-		default: SynErr(173); break;
+		default: SynErr(175); break;
 		}
 	}
 
@@ -2284,24 +2289,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 == 58) {
 			Get();
 			x = t; 
 			if (StartOf(8)) {
 				Expression(out ee);
 				e0 = ee; 
-				if (la.kind == 100) {
+				if (la.kind == 102) {
 					Get();
 					anyDots = true; 
 					if (StartOf(8)) {
 						Expression(out ee);
 						e1 = ee; 
 					}
-				} else if (la.kind == 53) {
+				} else if (la.kind == 54) {
 					Get();
 					Expression(out ee);
 					e1 = ee; 
-				} else if (la.kind == 21 || la.kind == 58) {
+				} else if (la.kind == 21 || la.kind == 59) {
 					while (la.kind == 21) {
 						Get();
 						Expression(out ee);
@@ -2312,15 +2317,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);
 						
 					}
-				} else SynErr(174);
-			} else if (la.kind == 100) {
+				} else SynErr(176);
+			} else if (la.kind == 102) {
 				Get();
 				anyDots = true; 
 				if (StartOf(8)) {
 					Expression(out ee);
 					e1 = ee; 
 				}
-			} else SynErr(175);
+			} else SynErr(177);
 			if (multipleIndices != null) {
 			 e = new MultiSelectExpr(x, e, multipleIndices);
 			 // make sure an array class with this dimensionality exists
@@ -2343,8 +2348,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }
 			}
 			
-			Expect(58);
-		} else SynErr(176);
+			Expect(59);
+		} else SynErr(178);
 	}
 
 	void DisplayExpr(out Expression e) {
@@ -2360,15 +2365,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 == 58) {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(8)) {
 				Expressions(elements);
 			}
 			e = new SeqDisplayExpr(x, elements); 
-			Expect(58);
-		} else SynErr(177);
+			Expect(59);
+		} else SynErr(179);
 	}
 
 	void MultiSetExpr(out Expression e) {
@@ -2394,7 +2399,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(180);
 	}
 
 	void MapExpr(out Expression e) {
@@ -2405,14 +2410,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		
 		Expect(43);
 		x = t; 
-		if (la.kind == 57) {
+		if (la.kind == 58) {
 			Get();
 			elements = new List<ExpressionPair/*!*/>(); 
 			if (StartOf(8)) {
 				MapLiteralExpressions(out elements);
 			}
 			e = new MapDisplayExpr(x, elements);
-			Expect(58);
+			Expect(59);
 		} else if (la.kind == 1) {
 			BoundVar/*!*/ bv;
 			List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2428,7 +2433,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(181);
 	}
 
 	void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2437,17 +2442,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		e = dummyExpr;
 		
 		switch (la.kind) {
-		case 92: {
+		case 93: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 93: {
+		case 94: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 94: {
+		case 95: {
 			Get();
 			e = new LiteralExpr(t); 
 			break;
@@ -2457,12 +2462,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new LiteralExpr(t, n); 
 			break;
 		}
-		case 95: {
+		case 96: {
 			Get();
 			e = new ThisExpr(t); 
 			break;
 		}
-		case 96: {
+		case 97: {
 			Get();
 			x = t; 
 			Expect(23);
@@ -2471,7 +2476,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new FreshExpr(x, e); 
 			break;
 		}
-		case 97: {
+		case 98: {
 			Get();
 			x = t; 
 			Expect(23);
@@ -2480,7 +2485,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			e = new AllocatedExpr(x, e); 
 			break;
 		}
-		case 98: {
+		case 99: {
 			Get();
 			x = t; 
 			Expect(23);
@@ -2505,7 +2510,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(25);
 			break;
 		}
-		default: SynErr(180); break;
+		default: SynErr(182); break;
 		}
 	}
 
@@ -2524,34 +2529,34 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression/*!*/ d, r;
 		elements = new List<ExpressionPair/*!*/>(); 
 		Expression(out d);
-		Expect(53);
+		Expect(54);
 		Expression(out r);
 		elements.Add(new ExpressionPair(d,r)); 
 		while (la.kind == 21) {
 			Get();
 			Expression(out d);
-			Expect(53);
+			Expect(54);
 			Expression(out r);
 			elements.Add(new ExpressionPair(d,r)); 
 		}
 	}
 
 	void QSep() {
-		if (la.kind == 105) {
+		if (la.kind == 107) {
 			Get();
-		} else if (la.kind == 106) {
+		} else if (la.kind == 108) {
 			Get();
-		} else SynErr(181);
+		} else SynErr(183);
 	}
 
 	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(67);
 		x = t; 
 		Expression(out e);
-		while (la.kind == 62) {
+		while (la.kind == 63) {
 			CaseExpression(out c);
 			cases.Add(c); 
 		}
@@ -2566,13 +2571,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression range;
 		Expression/*!*/ body;
 		
-		if (la.kind == 101 || la.kind == 102) {
+		if (la.kind == 103 || la.kind == 104) {
 			Forall();
 			x = t;  univ = true; 
-		} else if (la.kind == 103 || la.kind == 104) {
+		} else if (la.kind == 105 || la.kind == 106) {
 			Exists();
 			x = t; 
-		} else SynErr(182);
+		} else SynErr(184);
 		QuantifierDomain(out bvars, out attrs, out range);
 		QSep();
 		Expression(out body);
@@ -2603,7 +2608,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 == 107 || la.kind == 108) {
 			QSep();
 			Expression(out body);
 		}
@@ -2612,13 +2617,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(54);
+		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(101);
+		x = t; 
+		NoUSIdent(out d);
+		Expect(5);
+		Expression(out e);
+		expr = e;
+		e = new NamedExpr(x, d, 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(63);
 		x = t; 
 		Ident(out id);
 		if (la.kind == 23) {
@@ -2632,25 +2681,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}
 			Expect(25);
 		}
-		Expect(63);
+		Expect(64);
 		Expression(out body);
 		c = new MatchCaseExpr(x, id.val, arguments, body); 
 	}
 
 	void Forall() {
-		if (la.kind == 101) {
+		if (la.kind == 103) {
 			Get();
-		} else if (la.kind == 102) {
+		} else if (la.kind == 104) {
 			Get();
-		} else SynErr(183);
+		} else SynErr(185);
 	}
 
 	void Exists() {
-		if (la.kind == 103) {
+		if (la.kind == 105) {
 			Get();
-		} else if (la.kind == 104) {
+		} else if (la.kind == 106) {
 			Get();
-		} else SynErr(184);
+		} else SynErr(186);
 	}
 
 	void AttributeBody(ref Attributes attrs) {
@@ -2686,26 +2735,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, 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,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,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},
+		{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,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, 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,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, 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,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,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, 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,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,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,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,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, 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, 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
@@ -2782,139 +2831,141 @@ public class Errors {
 			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 52: s = "\"where\" expected"; break;
+			case 53: s = "\"return\" expected"; break;
+			case 54: s = "\":=\" expected"; break;
+			case 55: s = "\":|\" expected"; break;
+			case 56: s = "\"assume\" expected"; break;
+			case 57: s = "\"new\" expected"; break;
+			case 58: s = "\"[\" expected"; break;
+			case 59: s = "\"]\" expected"; break;
+			case 60: s = "\"choose\" expected"; break;
+			case 61: s = "\"if\" expected"; break;
+			case 62: s = "\"else\" expected"; break;
+			case 63: s = "\"case\" expected"; break;
+			case 64: s = "\"=>\" expected"; break;
+			case 65: s = "\"while\" expected"; break;
+			case 66: s = "\"invariant\" expected"; break;
+			case 67: s = "\"match\" expected"; break;
+			case 68: s = "\"assert\" expected"; break;
+			case 69: s = "\"print\" expected"; break;
+			case 70: s = "\"parallel\" expected"; break;
+			case 71: s = "\"<==>\" expected"; break;
+			case 72: s = "\"\\u21d4\" expected"; break;
+			case 73: s = "\"==>\" expected"; break;
+			case 74: s = "\"\\u21d2\" expected"; break;
+			case 75: s = "\"&&\" expected"; break;
+			case 76: s = "\"\\u2227\" expected"; break;
+			case 77: s = "\"||\" expected"; break;
+			case 78: s = "\"\\u2228\" expected"; break;
+			case 79: s = "\"<=\" expected"; break;
+			case 80: s = "\">=\" expected"; break;
+			case 81: s = "\"!=\" expected"; break;
+			case 82: s = "\"!!\" expected"; break;
+			case 83: s = "\"in\" expected"; break;
+			case 84: s = "\"!\" expected"; break;
+			case 85: s = "\"\\u2260\" expected"; break;
+			case 86: s = "\"\\u2264\" expected"; break;
+			case 87: s = "\"\\u2265\" expected"; break;
+			case 88: s = "\"+\" expected"; break;
+			case 89: s = "\"-\" expected"; break;
+			case 90: s = "\"/\" expected"; break;
+			case 91: s = "\"%\" expected"; break;
+			case 92: s = "\"\\u00ac\" expected"; break;
+			case 93: s = "\"false\" expected"; break;
+			case 94: s = "\"true\" expected"; break;
+			case 95: s = "\"null\" expected"; break;
+			case 96: s = "\"this\" expected"; break;
+			case 97: s = "\"fresh\" expected"; break;
+			case 98: s = "\"allocated\" expected"; break;
+			case 99: s = "\"old\" expected"; break;
+			case 100: s = "\"then\" expected"; break;
+			case 101: s = "\"expr\" expected"; break;
+			case 102: s = "\"..\" expected"; break;
+			case 103: s = "\"forall\" expected"; break;
+			case 104: s = "\"\\u2200\" expected"; break;
+			case 105: s = "\"exists\" expected"; break;
+			case 106: s = "\"\\u2203\" expected"; break;
+			case 107: s = "\"::\" expected"; break;
+			case 108: s = "\"\\u2022\" expected"; break;
+			case 109: s = "??? expected"; break;
+			case 110: s = "invalid Dafny"; break;
+			case 111: s = "invalid SubModuleDecl"; break;
+			case 112: s = "invalid SubModuleDecl"; break;
+			case 113: s = "this symbol not expected in ClassDecl"; 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 115: s = "invalid DatatypeDecl"; break;
+			case 116: s = "this symbol not expected in DatatypeDecl"; break;
+			case 117: s = "this symbol not expected in ArbitraryTypeDecl"; break;
+			case 118: s = "invalid ClassMemberDecl"; break;
+			case 119: s = "this symbol not expected in FieldDecl"; break;
+			case 120: s = "this symbol not expected in FieldDecl"; 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 122: s = "invalid FunctionDecl"; break;
+			case 123: s = "invalid FunctionDecl"; break;
+			case 124: s = "this symbol not expected in MethodDecl"; break;
+			case 125: s = "invalid MethodDecl"; break;
+			case 126: s = "invalid MethodDecl"; break;
+			case 127: s = "invalid TypeAndToken"; 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 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 133: s = "this symbol not expected in MethodSpec"; break;
+			case 134: s = "invalid MethodSpec"; break;
+			case 135: s = "invalid ReferenceType"; break;
 			case 136: s = "this symbol not expected in FunctionSpec"; break;
 			case 137: s = "this symbol not expected in FunctionSpec"; 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 139: s = "this symbol not expected in FunctionSpec"; break;
+			case 140: s = "this symbol not expected in FunctionSpec"; break;
+			case 141: s = "invalid FunctionSpec"; break;
+			case 142: s = "invalid PossiblyWildFrameExpression"; break;
+			case 143: s = "invalid PossiblyWildExpression"; 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 146: s = "this symbol not expected in OneStmt"; break;
+			case 147: s = "invalid OneStmt"; break;
+			case 148: s = "invalid AssertStmt"; break;
+			case 149: s = "invalid AssumeStmt"; break;
+			case 150: s = "invalid UpdateStmt"; break;
+			case 151: s = "invalid UpdateStmt"; break;
+			case 152: s = "invalid IfStmt"; break;
+			case 153: s = "invalid IfStmt"; break;
+			case 154: s = "invalid WhileStmt"; break;
+			case 155: s = "invalid WhileStmt"; break;
+			case 156: s = "invalid Rhs"; break;
+			case 157: s = "invalid Lhs"; break;
+			case 158: s = "invalid Guard"; break;
 			case 159: s = "this symbol not expected in LoopSpec"; break;
 			case 160: s = "this symbol not expected in LoopSpec"; 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 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 Invariant"; break;
+			case 165: s = "invalid AttributeArg"; break;
+			case 166: s = "invalid EquivOp"; break;
+			case 167: s = "invalid ImpliesOp"; break;
+			case 168: s = "invalid AndOp"; break;
+			case 169: s = "invalid OrOp"; break;
+			case 170: s = "invalid RelOp"; break;
+			case 171: s = "invalid AddOp"; break;
+			case 172: s = "invalid UnaryExpression"; break;
+			case 173: s = "invalid MulOp"; break;
+			case 174: s = "invalid NegOp"; break;
+			case 175: s = "invalid EndlessExpression"; 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 177: s = "invalid Suffix"; break;
+			case 178: s = "invalid Suffix"; break;
+			case 179: s = "invalid DisplayExpr"; break;
+			case 180: s = "invalid MultiSetExpr"; break;
+			case 181: s = "invalid MapExpr"; break;
+			case 182: s = "invalid ConstAtomExpression"; break;
+			case 183: s = "invalid QSep"; break;
+			case 184: s = "invalid QuantifierGuts"; break;
+			case 185: s = "invalid Forall"; break;
+			case 186: s = "invalid Exists"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a49a906e..0b922413 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 0a653f6c..68ab2c20 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -62,8 +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) {
-      Contract.Requires(m != null);
-      Contract.Requires(m.RefinementBase != null);
+      
+      if (m.RefinementBase == null) return;
 
       if (moduleUnderConstruction != null) {
         postTasks.Clear();
@@ -424,6 +424,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);
@@ -698,8 +701,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;
@@ -799,7 +806,228 @@ namespace Microsoft.Dafny {
 
       return nw;
     }
+    private Statement SubstituteNamedExpr(Statement s, string 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, string p, Expression E, ref int subCount) {
+      if (expr == null) {
+        return null;
+      }
+      if (expr is NamedExpr) {
+        NamedExpr n = (NamedExpr)expr;
+        if (n.Name == p) {
+          subCount++;
+          return new NamedExpr(n.tok, n.Name, E);
+        } 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, string 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 +1143,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 +1153,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].val, 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 labeld {0}", c.NameReplacements[0].val);
               }
               i++;
 
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0a18b783..b226c3fe 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -369,7 +369,7 @@ 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) {
@@ -3903,7 +3903,11 @@ 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);
+        e.Type = e.Body.Type;
+      }else if (expr is QuantifierExpr) {
         QuantifierExpr e = (QuantifierExpr)expr;
         int prevErrorCount = ErrorCount;
         scope.PushMarker();
@@ -4347,6 +4351,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) {
@@ -5380,6 +5387,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/Scanner.cs b/Source/Dafny/Scanner.cs
index 32c92a8b..efd31cbe 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 = 109;
+	const int noSym = 109;
 
 
 	[ContractInvariantMethod]
@@ -519,30 +519,32 @@ public class Scanner {
 			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 "where": t.kind = 52; break;
+			case "return": t.kind = 53; break;
+			case "assume": t.kind = 56; break;
+			case "new": t.kind = 57; break;
+			case "choose": t.kind = 60; break;
+			case "if": t.kind = 61; break;
+			case "else": t.kind = 62; break;
+			case "case": t.kind = 63; break;
+			case "while": t.kind = 65; break;
+			case "invariant": t.kind = 66; break;
+			case "match": t.kind = 67; break;
+			case "assert": t.kind = 68; break;
+			case "print": t.kind = 69; break;
+			case "parallel": t.kind = 70; break;
+			case "in": t.kind = 83; break;
+			case "false": t.kind = 93; break;
+			case "true": t.kind = 94; break;
+			case "null": t.kind = 95; break;
+			case "this": t.kind = 96; break;
+			case "fresh": t.kind = 97; break;
+			case "allocated": t.kind = 98; break;
+			case "old": t.kind = 99; break;
+			case "then": t.kind = 100; break;
+			case "expr": t.kind = 101; break;
+			case "forall": t.kind = 103; break;
+			case "exists": t.kind = 105; break;
 			default: break;
 		}
 	}
@@ -662,67 +664,67 @@ public class Scanner {
 			case 25:
 				{t.kind = 49; break;}
 			case 26:
-				{t.kind = 53; break;}
-			case 27:
 				{t.kind = 54; break;}
+			case 27:
+				{t.kind = 55; break;}
 			case 28:
-				{t.kind = 57; break;}
-			case 29:
 				{t.kind = 58; break;}
+			case 29:
+				{t.kind = 59; break;}
 			case 30:
-				{t.kind = 63; break;}
+				{t.kind = 64; break;}
 			case 31:
 				if (ch == '>') {AddCh(); goto case 32;}
 				else {goto case 0;}
 			case 32:
-				{t.kind = 70; break;}
-			case 33:
 				{t.kind = 71; break;}
-			case 34:
+			case 33:
 				{t.kind = 72; break;}
-			case 35:
+			case 34:
 				{t.kind = 73; break;}
+			case 35:
+				{t.kind = 74; break;}
 			case 36:
 				if (ch == '&') {AddCh(); goto case 37;}
 				else {goto case 0;}
 			case 37:
-				{t.kind = 74; break;}
-			case 38:
 				{t.kind = 75; break;}
-			case 39:
+			case 38:
 				{t.kind = 76; break;}
-			case 40:
+			case 39:
 				{t.kind = 77; break;}
+			case 40:
+				{t.kind = 78; break;}
 			case 41:
-				{t.kind = 79; break;}
-			case 42:
 				{t.kind = 80; break;}
-			case 43:
+			case 42:
 				{t.kind = 81; break;}
+			case 43:
+				{t.kind = 82; break;}
 			case 44:
-				{t.kind = 84; break;}
-			case 45:
 				{t.kind = 85; break;}
-			case 46:
+			case 45:
 				{t.kind = 86; break;}
-			case 47:
+			case 46:
 				{t.kind = 87; break;}
-			case 48:
+			case 47:
 				{t.kind = 88; break;}
-			case 49:
+			case 48:
 				{t.kind = 89; break;}
-			case 50:
+			case 49:
 				{t.kind = 90; break;}
-			case 51:
+			case 50:
 				{t.kind = 91; break;}
+			case 51:
+				{t.kind = 92; break;}
 			case 52:
-				{t.kind = 102; break;}
-			case 53:
 				{t.kind = 104; break;}
+			case 53:
+				{t.kind = 106; break;}
 			case 54:
-				{t.kind = 105; break;}
+				{t.kind = 107; break;}
 			case 55:
-				{t.kind = 106; break;}
+				{t.kind = 108; break;}
 			case 56:
 				recEnd = pos; recKind = 5;
 				if (ch == '=') {AddCh(); goto case 26;}
@@ -751,22 +753,22 @@ public class Scanner {
 				if (ch == '=') {AddCh(); goto case 41;}
 				else {t.kind = 27; break;}
 			case 62:
-				recEnd = pos; recKind = 83;
+				recEnd = pos; recKind = 84;
 				if (ch == '=') {AddCh(); goto case 42;}
 				else if (ch == '!') {AddCh(); goto case 43;}
-				else {t.kind = 83; break;}
+				else {t.kind = 84; 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 = 102;
 				if (ch == '.') {AddCh(); goto case 23;}
-				else {t.kind = 100; break;}
+				else {t.kind = 102; break;}
 			case 65:
-				recEnd = pos; recKind = 78;
+				recEnd = pos; recKind = 79;
 				if (ch == '=') {AddCh(); goto case 31;}
-				else {t.kind = 78; break;}
+				else {t.kind = 79; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index aecd8e3d..5d0baaed 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2049,6 +2049,8 @@ namespace Microsoft.Dafny {
         }
         return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));
 
+      } else if (expr is NamedExpr) {
+        return CanCallAssumption(((NamedExpr)expr).Body, etran);
       } else if (expr is ComprehensionExpr) {
         var e = (ComprehensionExpr)expr;
         var total = CanCallAssumption(e.Term, etran);
@@ -2078,7 +2080,9 @@ namespace Microsoft.Dafny {
         total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran)));
         total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran)));
         return total;
-      } else if (expr is ConcreteSyntaxExpression) {
+      } else if (expr is NamedExpr) {
+        return CanCallAssumption(((NamedExpr)expr).Body, etran);
+       } else if (expr is ConcreteSyntaxExpression) {
         var e = (ConcreteSyntaxExpression)expr;
         return CanCallAssumption(e.ResolvedExpression, etran);
       } else {
@@ -2512,6 +2516,8 @@ namespace Microsoft.Dafny {
         CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran);
         result = null;
 
+      } else if (expr is NamedExpr) {
+        CheckWellformedWithResult(((NamedExpr)expr).Body, options, result, resultType, locals, builder, etran);
       } else if (expr is ComprehensionExpr) {
         var e = (ComprehensionExpr)expr;
         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran);
@@ -6006,6 +6012,8 @@ namespace Microsoft.Dafny {
           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();
@@ -7673,6 +7681,12 @@ 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);
+        if (body != e.Body) {
+          newExpr = new NamedExpr(e.tok, e.Name, body);
+        }
       } else if (expr is ComprehensionExpr) {
         var e = (ComprehensionExpr)expr;
         Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap);
-- 
cgit v1.2.3


From c0f3a8d08762275bab645d666ed6a2e566701ff4 Mon Sep 17 00:00:00 2001
From: Jason Koenig <unknown>
Date: Mon, 9 Jul 2012 18:08:44 -0700
Subject: Dafny: added verification that replaced expressions are the same as
 the original

---
 Source/Dafny/Dafny.atg                |  2 +-
 Source/Dafny/DafnyAst.cs              | 18 ++++++++++++------
 Source/Dafny/Parser.cs                |  2 +-
 Source/Dafny/RefinementTransformer.cs | 14 +++++++-------
 Source/Dafny/Resolver.cs              |  1 +
 Source/Dafny/Translator.cs            | 24 +++++++++++++++---------
 6 files changed, 37 insertions(+), 24 deletions(-)

(limited to 'Source/Dafny/Resolver.cs')

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 958726fd..c63c5d3c 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1504,7 +1504,7 @@ NamedExpr<out Expression e>
     NoUSIdent<out d>
     ":"
     Expression<out e>               (. expr = e;
-                                       e = new NamedExpr(x, d, expr); .)
+                                       e = new NamedExpr(x, d.val, expr); .)
   .
 
 MatchExpression<out Expression/*!*/ e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c2a4ace3..d20d0d56 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -904,7 +904,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 {
@@ -3382,25 +3382,31 @@ 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 NamedExpr(IToken tok, IToken name, Expression body)
+    public readonly Expression Contract;
+    public readonly IToken ReplacerToken;
+
+    public NamedExpr(IToken tok, string p, Expression body)
       : base(tok) {
-      Name = name.val;
+      Name = p;
       Body = body;
     }
-
-    public NamedExpr(IToken tok, string p, Expression 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;
       }
     }
   }
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 6adc4df0..b8324dab 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2658,7 +2658,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(5);
 		Expression(out e);
 		expr = e;
-		e = new NamedExpr(x, d, expr); 
+		e = new NamedExpr(x, d.val, expr); 
 	}
 
 	void CaseExpression(out MatchCaseExpr/*!*/ c) {
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 68ab2c20..d27ef13d 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -806,7 +806,7 @@ namespace Microsoft.Dafny {
 
       return nw;
     }
-    private Statement SubstituteNamedExpr(Statement s, string p, Expression E, ref int subCount) {
+    private Statement SubstituteNamedExpr(Statement s, IToken p, Expression E, ref int subCount) {
       if (s == null) {
         return null;
       } else if (s is AssertStmt) {
@@ -886,15 +886,15 @@ namespace Microsoft.Dafny {
       }
 
     }
-    private Expression SubstituteNamedExpr(Expression expr, string p, Expression E, ref int subCount) {
+    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) {
+        if (n.Name == p.val) {
           subCount++;
-          return new NamedExpr(n.tok, n.Name, E);
+          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;
@@ -1021,7 +1021,7 @@ namespace Microsoft.Dafny {
       }
     }
 
-    private List<Expression> SubstituteNamedExprList(List<Expression> list, string p, Expression E, ref int subCount) {
+    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));
@@ -1165,14 +1165,14 @@ namespace Microsoft.Dafny {
                   // loop invariant:  oldS == oldStmt.Body[j]
                   var s = CloneStmt(oldS);
                   if (c.NameReplacements != null)
-                    s = SubstituteNamedExpr(s, c.NameReplacements[0].val, c.ExprReplacements[0], ref subCount);
+                    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 labeld {0}", c.NameReplacements[0].val);
+                  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 b226c3fe..33f86258 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3906,6 +3906,7 @@ namespace Microsoft.Dafny {
       } 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;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 5d0baaed..75b2e845 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2050,7 +2050,11 @@ namespace Microsoft.Dafny {
         return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran));
 
       } else if (expr is NamedExpr) {
-        return CanCallAssumption(((NamedExpr)expr).Body, etran);
+        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);
@@ -2080,9 +2084,7 @@ namespace Microsoft.Dafny {
         total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran)));
         total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran)));
         return total;
-      } else if (expr is NamedExpr) {
-        return CanCallAssumption(((NamedExpr)expr).Body, etran);
-       } else if (expr is ConcreteSyntaxExpression) {
+      } else if (expr is ConcreteSyntaxExpression) {
         var e = (ConcreteSyntaxExpression)expr;
         return CanCallAssumption(e.ResolvedExpression, etran);
       } else {
@@ -2517,7 +2519,13 @@ namespace Microsoft.Dafny {
         result = null;
 
       } else if (expr is NamedExpr) {
-        CheckWellformedWithResult(((NamedExpr)expr).Body, options, result, resultType, locals, builder, etran);
+        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);
@@ -6011,7 +6019,6 @@ 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) {
@@ -7684,9 +7691,8 @@ namespace Microsoft.Dafny {
       } else if (expr is NamedExpr) {
         var e = (NamedExpr)expr;
         var body = Substitute(e.Body, receiverReplacement, substMap);
-        if (body != e.Body) {
-          newExpr = new NamedExpr(e.tok, e.Name, body);
-        }
+        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, receiverReplacement, substMap);
-- 
cgit v1.2.3