Fix issue #72. Add the constructor questionmark to a function's axiom if the

function has a MemberSelectExpr that accesses a type with only one constructor.

2 files changed, 13 insertions, 5 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1f7e0e1f..8bc0d838 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -872,8 +872,7 @@ namespace Microsoft.Dafny
               Tuple<DatatypeCtor, bool> pair;

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

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

-                // they are not duplicates. For TopLevelDecls and static members, they are handled by 

-                // ReallyAmbiguousThing() during resolving.

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

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index eac28b05..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);