Merge

4 files changed, 168 insertions, 127 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 792274f8..be2bbe33 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5226,12 +5226,14 @@ namespace Microsoft.Dafny {
       return e;

     }

 

-    public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e) {

+    public static Expression VarSubstituter(List<NonglobalVariable> oldVars, List<BoundVar> newVars, Expression e, Dictionary<TypeParameter, Type> typeMap=null) {

       Contract.Requires(oldVars != null && newVars != null);

       Contract.Requires(oldVars.Count == newVars.Count);

 

       Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();

-      Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();

+      if (typeMap == null) {

+        typeMap = new Dictionary<TypeParameter, Type>();

+      }

 

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

         var id = new IdentifierExpr(newVars[i].tok, newVars[i].Name);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index b25b8cbe..8bc0d838 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -106,96 +106,134 @@ namespace Microsoft.Dafny
     interface IAmbiguousThing<Thing>

     {

       /// <summary>

-      /// Returns a non-zero number of non-null Thing's

+      /// Returns a plural number of non-null Thing's

       /// </summary>

-      IEnumerable<Thing> AllDecls();

+      ISet<Thing> Pool { get; }

     }

-    class AmbiguousTopLevelDecl : TopLevelDecl, IAmbiguousThing<TopLevelDecl>  // only used with "classes"

+    class AmbiguousThingHelper<Thing> where Thing : class

     {

-      public override string WhatKind { get { return A.WhatKind; } }

-      readonly TopLevelDecl A;

-      readonly TopLevelDecl B;

-      public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b)

-        : base(a.tok, a.Name + "/" + b.Name, m, new List<TypeParameter>(), null) {

+      public static Thing Create(ModuleDefinition m, Thing a, Thing b, IEqualityComparer<Thing> eq, out ISet<Thing> s) {

         Contract.Requires(a != null);

         Contract.Requires(b != null);

-        A = a;

-        B = b;

+        Contract.Requires(eq != null);

+        Contract.Ensures(Contract.Result<Thing>() != null || (Contract.ValueAtReturn(out s) != null || 2 <= Contract.ValueAtReturn(out s).Count));

+        s = null;

+        if (eq.Equals(a, b)) {

+          return a;

+        }

+        ISet<Thing> sa = a is IAmbiguousThing<Thing> ? ((IAmbiguousThing<Thing>)a).Pool : new HashSet<Thing>() { a };

+        ISet<Thing> sb = b is IAmbiguousThing<Thing> ? ((IAmbiguousThing<Thing>)b).Pool : new HashSet<Thing>() { b };

+        var union = new HashSet<Thing>(sa.Union(sb, eq));

+        if (sa.Count == union.Count) {

+          // sb is a subset of sa

+          return a;

+        } else if (sb.Count == union.Count) {

+          // sa is a subset of sb

+          return b;

+        } else {

+          s = union;

+          Contract.Assert(2 <= s.Count);

+          return null;

+        }

       }

-      public IEnumerable<TopLevelDecl> AllDecls() {

-        foreach (var a in new TopLevelDecl[] { A, B }) {

-          var amb = a as AmbiguousTopLevelDecl;

-          if (amb != null) {

-            foreach (var decl in amb.AllDecls()) {

-              yield return decl;

-            }

+      public static string Name(ISet<Thing> s, Func<Thing, string> name) {

+        Contract.Requires(s != null);

+        Contract.Requires(s.Count != 0);

+        string nm = null;

+        foreach (var thing in s) {

+          string n = name(thing);

+          if (nm == null) {

+            nm = n;

           } else {

-            yield return a;

+            nm += "/" + n;

           }

         }

+        return nm;

       }

-      public string ModuleNames() {

-        string nm;

-        if (A is AmbiguousTopLevelDecl) {

-          nm = ((AmbiguousTopLevelDecl)A).ModuleNames();

-        } else {

-          nm = A.Module.Name;

-        }

-        if (B is AmbiguousTopLevelDecl) {

-          nm += ", " + ((AmbiguousTopLevelDecl)B).ModuleNames();

-        } else {

-          nm += ", " + B.Module.Name;

+      public static string ModuleNames(IAmbiguousThing<Thing> amb, Func<Thing, string> moduleName) {

+        Contract.Requires(amb != null);

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

+        string nm = null;

+        foreach (var d in amb.Pool) {

+          if (nm == null) {

+            nm = moduleName(d);

+          } else {

+            nm += ", " + moduleName(d);

+          }

         }

         return nm;

       }

     }

 

+    class AmbiguousTopLevelDecl : TopLevelDecl, IAmbiguousThing<TopLevelDecl>  // only used with "classes"

+    {

+      public static TopLevelDecl Create(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b) {

+        ISet<TopLevelDecl> s;

+        var t = AmbiguousThingHelper<TopLevelDecl>.Create(m, a, b, new Eq(), out s);

+        return t ?? new AmbiguousTopLevelDecl(m, AmbiguousThingHelper<TopLevelDecl>.Name(s, tld => tld.Name), s);

+      }

+      class Eq : IEqualityComparer<TopLevelDecl>

+      {

+        public bool Equals(TopLevelDecl d0, TopLevelDecl d1) {

+          // We'd like to resolve any AliasModuleDecl to whatever module they refer to.

+          // It seems that the only way to do that is to look at alias.Signature.ModuleDef,

+          // but that is a ModuleDefinition, which is not a TopLevelDecl.  Therefore, we

+          // convert to a ModuleDefinition anything that might refer to something that an

+          // AliasModuleDecl can refer to; this is AliasModuleDecl and LiteralModuleDecl.

+          object a = d0 is ModuleDecl ? ((ModuleDecl)d0).Dereference() : d0;

+          object b = d1 is ModuleDecl ? ((ModuleDecl)d1).Dereference() : d1;

+          return a == b;

+        }

+        public int GetHashCode(TopLevelDecl d) {

+          object a = d is ModuleDecl ? ((ModuleDecl)d).Dereference() : d;

+          return a.GetHashCode();

+        }

+      }

+

+      public override string WhatKind { get { return Pool.First().WhatKind; } }

+      readonly ISet<TopLevelDecl> Pool = new HashSet<TopLevelDecl>();

+      ISet<TopLevelDecl> IAmbiguousThing<TopLevelDecl>.Pool { get { return Pool; } }

+      private AmbiguousTopLevelDecl(ModuleDefinition m, string name, ISet<TopLevelDecl> pool)

+        : base(pool.First().tok, name, m, new List<TypeParameter>(), null) {

+        Contract.Requires(name != null);

+        Contract.Requires(pool != null && 2 <= pool.Count);

+        Pool = pool;

+      }

+      public string ModuleNames() {

+        return AmbiguousThingHelper<TopLevelDecl>.ModuleNames(this, d => d.Module.Name);

+      }

+    }

+

     class AmbiguousMemberDecl : MemberDecl, IAmbiguousThing<MemberDecl>  // only used with "classes"

     {

-      public override string WhatKind { get { return A.WhatKind; } }

-      readonly MemberDecl A;

-      readonly MemberDecl B;

-      public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)

-        : base(a.tok, a.Name + "/" + b.Name, true, a.IsGhost, null) {

-        Contract.Requires(a != null);

-        Contract.Requires(b != null);

-        A = a;

-        B = b;

+      public static MemberDecl Create(ModuleDefinition m, MemberDecl a, MemberDecl b) {

+        ISet<MemberDecl> s;

+        var t = AmbiguousThingHelper<MemberDecl>.Create(m, a, b, new Eq(), out s);

+        return t ?? new AmbiguousMemberDecl(m, AmbiguousThingHelper<MemberDecl>.Name(s, member => member.Name), s);

       }

-      public IEnumerable<MemberDecl> AllDecls() {

-        var amb = A as AmbiguousMemberDecl;

-        if (amb == null) {

-          yield return A;

-        } else {

-          foreach (var decl in amb.AllDecls()) {

-            yield return decl;

-          }

+      class Eq : IEqualityComparer<MemberDecl>

+      {

+        public bool Equals(MemberDecl d0, MemberDecl d1) {

+          return d0 == d1;

         }

-        amb = B as AmbiguousMemberDecl;

-        if (amb == null) {

-          yield return B;

-        } else {

-          foreach (var decl in amb.AllDecls()) {

-            yield return decl;

-          }

+        public int GetHashCode(MemberDecl d) {

+          return d.GetHashCode();

         }

       }

+

+      public override string WhatKind { get { return Pool.First().WhatKind; } }

+      readonly ISet<MemberDecl> Pool = new HashSet<MemberDecl>();

+      ISet<MemberDecl> IAmbiguousThing<MemberDecl>.Pool { get { return Pool; } }

+      private AmbiguousMemberDecl(ModuleDefinition m, string name, ISet<MemberDecl> pool)

+        : base(pool.First().tok, name, true, pool.First().IsGhost, null) {

+        Contract.Requires(name != null);

+        Contract.Requires(pool != null && 2 <= pool.Count);

+        Pool = pool;

+      }

       public string ModuleNames() {

-        string nm;

-        if (A is AmbiguousMemberDecl) {

-          nm = ((AmbiguousMemberDecl)A).ModuleNames();

-        } else {

-          nm = A.EnclosingClass.Module.Name;

-        }

-        if (B is AmbiguousMemberDecl) {

-          nm += ", " + ((AmbiguousMemberDecl)B).ModuleNames();

-        } else {

-          nm += ", " + B.EnclosingClass.Module.Name;

-        }

-        return nm;

+        return AmbiguousThingHelper<MemberDecl>.ModuleNames(this, d => d.EnclosingClass.Module.Name);

       }

     }

-    //Dictionary<string, Tuple<DatatypeCtor, bool>> allDatatypeCtors;

 

     readonly Dictionary<ClassDecl, Dictionary<string, MemberDecl>> classMembers = new Dictionary<ClassDecl, Dictionary<string, MemberDecl>>();

     readonly Dictionary<DatatypeDecl, Dictionary<string, MemberDecl>> datatypeMembers = new Dictionary<DatatypeDecl, Dictionary<string, MemberDecl>>();

@@ -824,7 +862,7 @@ namespace Microsoft.Dafny
             foreach (var kv in s.TopLevels) {

               TopLevelDecl d;

               if (sig.TopLevels.TryGetValue(kv.Key, out d)) {

-                sig.TopLevels[kv.Key] = new AmbiguousTopLevelDecl(moduleDef, d, kv.Value);

+                sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value);

               } else {

                 sig.TopLevels.Add(kv.Key, kv.Value);

               }

@@ -833,8 +871,12 @@ namespace Microsoft.Dafny
             foreach (var kv in s.Ctors) {

               Tuple<DatatypeCtor, bool> pair;

               if (sig.Ctors.TryGetValue(kv.Key, out pair)) {

-                // mark it as a duplicate

-                sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);

+                // The same ctor can be imported from two different imports (e.g "diamond" imports), in which case, 

+                // they are not duplicates.

+                if (kv.Value.Item1 != pair.Item1) {

+                  // mark it as a duplicate

+                  sig.Ctors[kv.Key] = new Tuple<DatatypeCtor, bool>(pair.Item1, true);

+                }

               } else {

                 // add new

                 sig.Ctors.Add(kv.Key, kv.Value);

@@ -844,7 +886,7 @@ namespace Microsoft.Dafny
             foreach (var kv in s.StaticMembers) {

               MemberDecl md;

               if (sig.StaticMembers.TryGetValue(kv.Key, out md)) {

-                sig.StaticMembers[kv.Key] = new AmbiguousMemberDecl(moduleDef, md, kv.Value);

+                sig.StaticMembers[kv.Key] = AmbiguousMemberDecl.Create(moduleDef, md, kv.Value);

               } else {

                 // add new

                 sig.StaticMembers.Add(kv.Key, kv.Value);

@@ -4081,39 +4123,6 @@ namespace Microsoft.Dafny
       return null;

     }

 

-    bool ReallyAmbiguousTopLevelDecl(ref TopLevelDecl decl) {

-      return ReallyAmbiguousThing(ref decl, (d0, d1) => {

-        // We'd like to resolve any AliasModuleDecl to whatever module they refer to.

-        // It seems that the only way to do that is to look at alias.Signature.ModuleDef,

-        // but that is a ModuleDefinition, which is not a TopLevelDecl.  Therefore, we

-        // convert to a ModuleDefinition anything that might refer to something that an

-        // AliasModuleDecl can refer to; this is AliasModuleDecl and LiteralModuleDecl.

-        object a = d0 is ModuleDecl ? ((ModuleDecl)d0).Dereference() : d0;

-        object b = d1 is ModuleDecl ? ((ModuleDecl)d1).Dereference() : d1;

-        return a == b;

-      });

-    }

-

-    bool ReallyAmbiguousThing<Thing>(ref Thing decl, Func<Thing, Thing, bool> eq = null) where Thing : class {

-      Contract.Requires(decl != null);

-      Contract.Ensures(decl != null);

-      Contract.Ensures(!Contract.Result<bool>() || (decl == Contract.OldValue<Thing>(decl) && decl is IAmbiguousThing<Thing>));

-      var amb = decl as IAmbiguousThing<Thing>;

-      if (amb != null) {

-        var allDecls = new List<Thing>(amb.AllDecls());

-        Contract.Assert(1 <= allDecls.Count);  // that's what the specification of AllDecls says

-        var repr = allDecls[0];  // pick one of them

-        // check if all are the same

-        if (amb.AllDecls().All(d => eq == null ? d == repr : eq(d, repr))) {

-          // all ambiguity gets resolved to the same declaration, so there really isn't any ambiguity after all

-          decl = repr;

-          return false;

-        }

-        return true;  // decl is an AmbiguousThing and the declarations it can stand for are not all the same--so this really is an ambiguity

-      }

-      return false;

-    }

-

     /// <summary>

     /// Adds to "typeArgs" a list of "n" type arguments, possibly extending "defaultTypeArguments".

     /// </summary>

@@ -6109,7 +6118,19 @@ namespace Microsoft.Dafny
           if (memberName == "_ctor") {

             Error(tok, "{0} {1} does not have an anonymous constructor", kind, ctype.Name);

           } else {

-            Error(tok, "member {0} does not exist in {2} {1}", memberName, ctype.Name, kind);

+            // search the static members of the enclosing module or its imports

+            if (moduleInfo.StaticMembers.TryGetValue(memberName, out member)) {

+              Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

+              if (member is AmbiguousMemberDecl) {

+                var ambiguousMember = (AmbiguousMemberDecl)member;

+                Error(tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", memberName, ambiguousMember.ModuleNames());

+              } else {

+                nptype = GetReceiverType(tok, member);

+                return member;

+              }

+            } else {

+              Error(tok, "member {0} does not exist in {2} {1}", memberName, ctype.Name, kind);

+            }

           }

           return null;

         } else {

@@ -6444,8 +6465,9 @@ namespace Microsoft.Dafny
         TopLevelDecl d;

         if (!moduleInfo.TopLevels.TryGetValue(dtv.DatatypeName, out d)) {

           Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName);

-        } else if (ReallyAmbiguousTopLevelDecl(ref d)) {

-          Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames());

+        } else if (d is AmbiguousTopLevelDecl) {

+          var ad = (AmbiguousTopLevelDecl)d;

+          Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", dtv.DatatypeName, ad.ModuleNames());

         } else if (!(d is DatatypeDecl)) {

           Error(expr.tok, "Expected datatype: {0}", dtv.DatatypeName);

         } else {

@@ -7505,8 +7527,9 @@ namespace Microsoft.Dafny
         }

       } else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {

         // ----- 3. Member of the enclosing module

-        if (ReallyAmbiguousTopLevelDecl(ref decl)) {

-          Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());

+        if (decl is AmbiguousTopLevelDecl) {

+          var ad = (AmbiguousTopLevelDecl)decl;

+          Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.Name, ad.ModuleNames());

         } else {

           // We have found a module name or a type name, neither of which is an expression. However, the NameSegment we're

           // looking at may be followed by a further suffix that makes this into an expresion. We postpone the rest of the

@@ -7518,8 +7541,9 @@ namespace Microsoft.Dafny
       } else if (moduleInfo.StaticMembers.TryGetValue(expr.Name, out member)) {

         // ----- 4. static member of the enclosing module

         Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

-        if (ReallyAmbiguousThing(ref member)) {

-          Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.Name, ((AmbiguousMemberDecl)member).ModuleNames());

+        if (member is AmbiguousMemberDecl) {

+          var ambiguousMember = (AmbiguousMemberDecl)member;

+          Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.Name, ambiguousMember.ModuleNames());

         } else {

           var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

           r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

@@ -7603,8 +7627,9 @@ namespace Microsoft.Dafny
 #endif

       } else if (moduleInfo.TopLevels.TryGetValue(expr.Name, out decl)) {

         // ----- 2. Member of the enclosing module

-        if (ReallyAmbiguousTopLevelDecl(ref decl)) {

-          Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.Name, ((AmbiguousTopLevelDecl)decl).ModuleNames());

+        if (decl is AmbiguousTopLevelDecl) {

+          var ad = (AmbiguousTopLevelDecl)decl;

+          Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.Name, ad.ModuleNames());

         } else {

           // We have found a module name or a type name, neither of which is a type expression. However, the NameSegment we're

           // looking at may be followed by a further suffix that makes this into a type expresion. We postpone the rest of the

@@ -7744,8 +7769,9 @@ namespace Microsoft.Dafny
           }

         } else if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {

           // ----- 1. Member of the specified module

-          if (ReallyAmbiguousTopLevelDecl(ref decl)) {

-            Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());

+          if (decl is AmbiguousTopLevelDecl) {

+            var ad = (AmbiguousTopLevelDecl)decl;

+            Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ad.ModuleNames());

           } else {

             // We have found a module name or a type name, neither of which is an expression. However, the ExprDotName we're

             // looking at may be followed by a further suffix that makes this into an expresion. We postpone the rest of the

@@ -7756,8 +7782,9 @@ namespace Microsoft.Dafny
         } else if (sig.StaticMembers.TryGetValue(expr.SuffixName, out member)) {

           // ----- 2. static member of the specified module

           Contract.Assert(member.IsStatic); // moduleInfo.StaticMembers is supposed to contain only static members of the module's implicit class _default

-          if (ReallyAmbiguousThing(ref member)) {

-            Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ((AmbiguousMemberDecl)member).ModuleNames());

+          if (member is AmbiguousMemberDecl) {

+            var ambiguousMember = (AmbiguousMemberDecl)member;

+            Error(expr.tok, "The name {0} ambiguously refers to a static member in one of the modules {1} (try qualifying the member name with the module name)", expr.SuffixName, ambiguousMember.ModuleNames());

           } else {

             var receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass);

             r = ResolveExprDotCall(expr.tok, receiver, member, expr.OptTypeArguments, opts.codeContext, allowMethodCall);

@@ -7885,8 +7912,9 @@ namespace Microsoft.Dafny
 

         if (sig.TopLevels.TryGetValue(expr.SuffixName, out decl)) {

           // ----- 0. Member of the specified module

-          if (ReallyAmbiguousTopLevelDecl(ref decl)) {

-            Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ((AmbiguousTopLevelDecl)decl).ModuleNames());

+          if (decl is AmbiguousTopLevelDecl) {

+            var ad = (AmbiguousTopLevelDecl)decl;

+            Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", expr.SuffixName, ad.ModuleNames());

           } else {

             // We have found a module name or a type name.  We create a temporary expression that will never be seen by the compiler

             // or verifier, just to have a placeholder where we can recorded what we have found.

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 091ee24a..72649b5f 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -672,7 +672,8 @@ namespace Microsoft.Dafny
 

       // Substitute the forall's variables for those of the fn

       var formals = fn.Formals.ConvertAll<NonglobalVariable>(x => (NonglobalVariable)x);

-      reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs);

+      var typeMap = Util.Dict<TypeParameter, Type>(fn.TypeArgs, Util.Map(origForall.TypeArgs, x => new UserDefinedType(x)));

+      reqs = Expression.VarSubstituter(formals, origForall.BoundVars, reqs, typeMap);

 

       var newImpl = Expression.CreateImplies(reqs, origImpl.E1);

       //var newForall = Expression.CreateQuantifier(origForall, true, newImpl);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index aa3e1854..18299994 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4261,12 +4261,21 @@ namespace Microsoft.Dafny {
         return CanCallAssumption(l, etran);

       } else if (expr is MemberSelectExpr) {

         MemberSelectExpr e = (MemberSelectExpr)expr;

+        Bpl.Expr r;

         if (e.Obj is ThisExpr) {

-          return Bpl.Expr.True;

+          r = Bpl.Expr.True;

         } else {

-          Bpl.Expr r = CanCallAssumption(e.Obj, etran);

-          return r;

+          r = CanCallAssumption(e.Obj, etran);

         }

+        if (e.Member is DatatypeDestructor) {

+          var dtor = (DatatypeDestructor)e.Member;

+          if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) {

+            var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj));

+            // There is only one constructor, so the value must be been constructed by it; might as well assume that here.

+            r = BplAnd(r, correctConstructor);

+          }

+        }

+        return r;

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

         Bpl.Expr total = CanCallAssumption(e.Seq, etran);

@@ -11061,14 +11070,15 @@ namespace Microsoft.Dafny {
             case BinaryExpr.ResolvedOpcode.InMap: {

               bool finite = e.E1.Type.AsMapType.Finite;

               var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;

-              return Bpl.Expr.Select(translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),

+              return Bpl.Expr.SelectTok(expr.tok, translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),

                                      BoxIfNecessary(expr.tok, e0, e.E0.Type));

             }

             case BinaryExpr.ResolvedOpcode.NotInMap: {

               bool finite = e.E1.Type.AsMapType.Finite;

               var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain;

-              return Bpl.Expr.Not(Bpl.Expr.Select(translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),

-                                     BoxIfNecessary(expr.tok, e0, e.E0.Type)));

+              Bpl.Expr inMap = Bpl.Expr.SelectTok(expr.tok, translator.FunctionCall(expr.tok, f, predef.MapType(e.tok, finite, predef.BoxType, predef.BoxType), e1),

+                                     BoxIfNecessary(expr.tok, e0, e.E0.Type));

+              return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, inMap);

             }

             case BinaryExpr.ResolvedOpcode.MapDisjoint: {

               return translator.FunctionCall(expr.tok, BuiltinFunction.MapDisjoint, null, e0, e1);