Allow sharing of names of destructors among the constructors of a (co)datatype.

Author: Rustan Leino

Source/Dafny/Compiler.cs

@@ -566,7 +566,14 @@ void CompileDatatypeStruct(DatatypeDecl dt, int indent, TextWriter wr) {
       //   public bool is_Ctor0 { get { return _D is Dt_Ctor0; } }
       //   ...
       //
-      //   public T0 dtor_Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }
+      //   public T0 dtor_Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }  // This is in essence what gets generated for the case where the destructor is used in one use constructor
+      //   public T0 dtor_Dtor0 { get { var d = _D;                       // This is the general case
+      //       if (d is DT_Ctor0) { return ((DT_Ctor0)d).@Dtor0; }
+      //       if (d is DT_Ctor1) { return ((DT_Ctor1)d).@Dtor0; }
+      //       ...
+      //       if (d is DT_Ctor(n-2)) { return ((DT_Ctor(n-2))d).@Dtor0; }
+      //       return ((DT_Ctor(n-1))d).@Dtor0;
+      //    }}
       //   ...
       // }
       string DtT = dt.CompileName;
@@ -683,11 +690,28 @@ void CompileDatatypeStruct(DatatypeDecl dt, int indent, TextWriter wr) {
 
       // destructors
       foreach (var ctor in dt.Ctors) {
-        foreach (var arg in ctor.Formals) {
-          if (!arg.IsGhost && arg.HasName) {
-            //   public T0 @Dtor0 { get { return ((DT_Ctor)_D).@Dtor0; } }
-            Indent(ind, wr);
-            wr.WriteLine("public {0} dtor_{1} {{ get {{ return (({2}_{3}{4})_D).@{1}; }} }}", TypeName(arg.Type, wr), arg.CompileName, dt.CompileName, ctor.CompileName, DtT_TypeArgs);
+        foreach (var dtor in ctor.Destructors) {
+          if (dtor.EnclosingCtors[0] == ctor) {
+            var arg = dtor.CorrespondingFormals[0];
+            if (!arg.IsGhost && arg.HasName) {
+              Indent(ind, wr);
+              //   public T0 dtor_Dtor0 { get { var d = _D;
+              //       if (d is DT_Ctor0) { return ((DT_Ctor0)d).@Dtor0; }
+              //       if (d is DT_Ctor1) { return ((DT_Ctor1)d).@Dtor0; }
+              //       ...
+              //       if (d is DT_Ctor(n-2)) { return ((DT_Ctor(n-2))d).@Dtor0; }
+              //       return ((DT_Ctor(n-1))d).@Dtor0;
+              //    }}
+              wr.Write("public {0} dtor_{1} {{ get {{ var d = _D; ", TypeName(arg.Type, wr), arg.CompileName);
+              var n = dtor.EnclosingCtors.Count;
+              for (int i = 0; i < n-1; i++) {
+                var ctor_i = dtor.EnclosingCtors[i];
+                Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[i].CompileName);
+                wr.Write("if (d is {0}_{1}{2}) {{ return (({0}_{1}{2})d).@{3}; }} ", dt.CompileName, ctor_i.CompileName, DtT_TypeArgs, arg.CompileName);
+              }
+              Contract.Assert(arg.CompileName == dtor.CorrespondingFormals[n-1].CompileName);
+              wr.WriteLine("return (({0}_{1}{2})d).@{3}; }} }}", dt.CompileName, dtor.EnclosingCtors[n-1].CompileName, DtT_TypeArgs, arg.CompileName);
+            }
           }
         }
       }

Source/Dafny/DafnyAst.cs

@@ -3866,8 +3866,15 @@ public override string FullCompileName {
 
   public class DatatypeDestructor : SpecialField
   {
-    public readonly DatatypeCtor EnclosingCtor;
-    public readonly Formal CorrespondingFormal;
+    public readonly List<DatatypeCtor> EnclosingCtors = new List<DatatypeCtor>();  // is always a nonempty list
+    public readonly List<Formal> CorrespondingFormals = new List<Formal>();  // is always a nonempty list
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(EnclosingCtors != null);
+      Contract.Invariant(CorrespondingFormals != null);
+      Contract.Invariant(EnclosingCtors.Count > 0);
+      Contract.Invariant(EnclosingCtors.Count == CorrespondingFormals.Count);
+    }
 
     public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, Formal correspondingFormal, string name, string compiledName, string preString, string postString, bool isGhost, Type type, Attributes attributes)
       : base(tok, name, compiledName, preString, postString, isGhost, false, false, type, attributes)
@@ -3880,8 +3887,35 @@ public DatatypeDestructor(IToken tok, DatatypeCtor enclosingCtor, Formal corresp
       Contract.Requires(preString != null);
       Contract.Requires(postString != null);
       Contract.Requires(type != null);
-      EnclosingCtor = enclosingCtor;
-      CorrespondingFormal = correspondingFormal;
+      EnclosingCtors.Add(enclosingCtor);  // more enclosing constructors may be added later during resolution
+      CorrespondingFormals.Add(correspondingFormal);  // more corresponding formals may be added later during resolution
+    }
+
+    /// <summary>
+    /// To be called only by the resolver. Called to share this datatype destructor between multiple constructors
+    /// of the same datatype.
+    /// </summary>
+    internal void AddAnotherEnclosingCtor(DatatypeCtor ctor, Formal formal) {
+      Contract.Requires(ctor != null);
+      Contract.Requires(formal != null);
+      EnclosingCtors.Add(ctor);  // more enclosing constructors may be added later during resolution
+      CorrespondingFormals.Add(formal);  // more corresponding formals may be added later during resolution
+    }
+
+    internal string EnclosingCtorNames(string grammaticalConjunction) {
+      Contract.Requires(grammaticalConjunction != null);
+      var n = EnclosingCtors.Count;
+      if (n == 1) {
+        return string.Format("'{0}'", EnclosingCtors[0].Name);
+      } else if (n == 2) {
+        return string.Format("'{0}' {1} '{2}'", EnclosingCtors[0].Name, grammaticalConjunction, EnclosingCtors[1].Name);
+      } else {
+        var s = "";
+        for (int i = 0; i < n - 1; i++) {
+          s += string.Format("'{0}', ", EnclosingCtors[i].Name);
+        }
+        return s + string.Format("{0} '{1}'", grammaticalConjunction, EnclosingCtors[n - 1].Name);
+      }
     }
   }
 

Source/Dafny/Resolver.cs

@@ -1732,17 +1732,37 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport
           }
           // add deconstructors now (that is, after the query methods have been added)
           foreach (DatatypeCtor ctor in dt.Ctors) {
+            var formalsUsedInThisCtor = new HashSet<string>();
             foreach (var formal in ctor.Formals) {
-              bool nameError = false;
-              if (formal.HasName && members.ContainsKey(formal.Name)) {
-                reporter.Error(MessageSource.Resolver, ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
-                nameError = true;
+              MemberDecl previousMember = null;
+              var localDuplicate = false;
+              if (formal.HasName) {
+                if (members.TryGetValue(formal.Name, out previousMember)) {
+                  localDuplicate = formalsUsedInThisCtor.Contains(formal.Name);
+                  if (localDuplicate) {
+                    reporter.Error(MessageSource.Resolver, ctor, "Duplicate use of deconstructor name in the same constructor: {0}", formal.Name);
+                  } else if (previousMember is DatatypeDestructor) {
+                    // this is okay, if the destructor has the appropriate type; this will be checked later, after type checking
+                  } else {
+                    reporter.Error(MessageSource.Resolver, ctor, "Name of deconstructor is used by another member of the datatype: {0}", formal.Name);
+                  }
+                }
+                formalsUsedInThisCtor.Add(formal.Name);
               }
-              var dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.CompileName, "", "", formal.IsGhost, formal.Type, null);
-              dtor.InheritVisibility(dt);
-              dtor.EnclosingClass = dt;  // resolve here
-              if (!nameError && formal.HasName) {
-                members.Add(formal.Name, dtor);
+              DatatypeDestructor dtor;
+              if (!localDuplicate && previousMember is DatatypeDestructor) {
+                // a destructor with this name already existed in (a different constructor in) the datatype
+                dtor = (DatatypeDestructor)previousMember;
+                dtor.AddAnotherEnclosingCtor(ctor, formal);
+              } else {
+                // either the destructor has no explicit name, or this constructor declared another destructor with this name, or no previous destructor had this name
+                dtor = new DatatypeDestructor(formal.tok, ctor, formal, formal.Name, "dtor_" + formal.CompileName, "", "", formal.IsGhost, formal.Type, null);
+                dtor.InheritVisibility(dt);
+                dtor.EnclosingClass = dt;  // resolve here
+                if (formal.HasName && !localDuplicate && previousMember == null) {
+                  // the destructor has an explict name and there was no member at all with this name before
+                  members.Add(formal.Name, dtor);
+                }
               }
               ctor.Destructors.Add(dtor);
             }
@@ -2119,6 +2139,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
       // ---------------------------------- Pass 1 ----------------------------------
       // This pass:
       // * checks that type inference was able to determine all types
+      // * check that shared destructors in datatypes are in agreement
       // * fills in the .ResolvedOp field of binary expressions
       // * discovers bounds for:
       //     - forall statements
@@ -2140,6 +2161,7 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
       }
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions
+        // Also, for each datatype, check that shared destructors are in agreement
         foreach (TopLevelDecl d in declarations) {
           if (d is IteratorDecl) {
             var iter = (IteratorDecl)d;
@@ -2191,6 +2213,28 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl/*!*/>/*!*/ declarations,
               CheckExpression(dd.Constraint, this, dd);
             }
             FigureOutNativeType(dd, nativeTypeMap);
+          } else if (d is DatatypeDecl) {
+            var dd = (DatatypeDecl)d;
+            foreach (var member in datatypeMembers[dd].Values) {
+              var dtor = member as DatatypeDestructor;
+              if (dtor != null) {
+                var rolemodel = dtor.CorrespondingFormals[0];
+                for (int i = 1; i < dtor.CorrespondingFormals.Count; i++) {
+                  var other = dtor.CorrespondingFormals[i];
+                  if (!rolemodel.Type.ExactlyEquals(other.Type)) {
+                    reporter.Error(MessageSource.Resolver, other,
+                      "shared destructors must have the same type, but '{0}' has type '{1}' in constructor '{2}' and type '{3}' in constructor '{4}'",
+                      rolemodel.Name, rolemodel.Type, dtor.EnclosingCtors[0].Name, other.Type, dtor.EnclosingCtors[i].Name);
+                  } else if (rolemodel.IsGhost != other.IsGhost) {
+                    reporter.Error(MessageSource.Resolver, other,
+                      "shared destructors must agree on whether or not they are ghost, but '{0}' is {1} in constructor '{2}' and {3} in constructor '{4}'",
+                      rolemodel.Name,
+                      rolemodel.IsGhost ? "ghost" : "non-ghost", dtor.EnclosingCtors[0].Name,
+                      other.IsGhost ? "ghost" : "non-ghost", dtor.EnclosingCtors[i].Name);
+                  }
+                }
+              }
+            }
           }
         }
       }
@@ -9885,7 +9929,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) {
         if (!ty.IsDatatype) {
           reporter.Error(MessageSource.Resolver, expr, "datatype update expression requires a root expression of a datatype (got {0})", ty);
         } else {
-          var let = ResolveDatatypeUpdate(expr.tok, e.Root, ty.AsDatatype, e.Updates, false, opts);
+          var let = ResolveDatatypeUpdate(expr.tok, e.Root, ty.AsDatatype, e.Updates, opts);
           if (let != null) {
             e.ResolvedExpression = let;
             expr.Type = ty;
@@ -10409,7 +10453,7 @@ private void AddXConstraint(IToken tok, string constraintName, Type type, Expres
     /// <summary>
     /// Attempts to produce a let expression from the given datatype updates.  Returns that let expression upon success, and null otherwise.
     /// </summary>
-    Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List<Tuple<IToken, string, Expression>> memberUpdates, bool sequentialUpdates, ResolveOpts opts) {
+    Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List<Tuple<IToken, string, Expression>> memberUpdates, ResolveOpts opts) {
       Contract.Requires(tok != null);
       Contract.Requires(root != null);
       Contract.Requires(dt != null);
@@ -10427,28 +10471,29 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L
       foreach (var entry in memberUpdates) {
         var destructor_str = entry.Item2;
         if (memberNames.Contains(destructor_str)) {
-          if (sequentialUpdates) {
-            reporter.Warning(MessageSource.Resolver, entry.Item1, "update to '{0}' overwritten by another update to '{0}'", destructor_str);
-          } else {
-            reporter.Error(MessageSource.Resolver, entry.Item1, "duplicate update member '{0}'", destructor_str);
-          }
+          reporter.Error(MessageSource.Resolver, entry.Item1, "duplicate update member '{0}'", destructor_str);
         } else {
           memberNames.Add(destructor_str);
           MemberDecl member;
           if (!datatypeMembers[dt].TryGetValue(destructor_str, out member)) {
             reporter.Error(MessageSource.Resolver, entry.Item1, "member '{0}' does not exist in datatype '{1}'", destructor_str, dt.Name);
+          } else if (!(member is DatatypeDestructor)) {
+            reporter.Error(MessageSource.Resolver, entry.Item1, "member '{0}' is not a destructor in datatype '{1}'", destructor_str, dt.Name);
           } else {
             var destructor = (DatatypeDestructor)member;
-            if (ctor != null && ctor != destructor.EnclosingCtor) {
-              if (sequentialUpdates) {
-                // This would eventually give rise to a verification error.  However, since the 'sequentialUpdates' case is being depricated,
-                // we don't mind giving resolution error about this now.
-              }
+            if (destructor.EnclosingCtors.Count > 1) {
+              // Note: This restriction could be relaxed.  For example, thing would still be okay if the intersection of constructors of
+              // the indicated memberUpdates names indicate a unique constructor.  In addition, the syntax could be extended to allow an
+              // update member to have the form ctor.x:=E where ctor would be used to disambiguate which constructor the x is supposed to
+              // be looked up in.
+              reporter.Error(MessageSource.Resolver, entry.Item1, "datatype member update is supported only for uniquely named destructors " +
+                "('{0}' belongs to '{1}')", entry.Item2, destructor.EnclosingCtorNames("and"));
+            } else if (ctor != null && ctor != destructor.EnclosingCtors[0]) {
               reporter.Error(MessageSource.Resolver, entry.Item1, "updated datatype members must belong to the same constructor " +
-                "('{0}' belongs to '{1}' and '{2}' belongs to '{3}'", entry.Item2, destructor.EnclosingCtor.Name, ctorSource.Item2, ctor.Name);
+                "('{0}' belongs to '{1}' and '{2}' belongs to '{3}')", entry.Item2, destructor.EnclosingCtors[0].Name, ctorSource.Item2, ctor.Name);
             } else {
-              updates.Add(destructor.CorrespondingFormal, entry.Item3);
-              ctor = destructor.EnclosingCtor;
+              updates.Add(destructor.CorrespondingFormals[0], entry.Item3);
+              ctor = destructor.EnclosingCtors[0];
               ctorSource = entry;
             }
           }

Source/Dafny/Translator.cs

@@ -1339,9 +1339,12 @@ void AddDatatype(DatatypeDecl dt) {
           var sf = ctor.Destructors[i];
           Contract.Assert(sf != null);
           fn = GetReadonlyField(sf);
-          if (fn != predef.Tuple2Destructors0 && fn != predef.Tuple2Destructors1) {
+          if (fn == predef.Tuple2Destructors0 || fn == predef.Tuple2Destructors1) {
             // the two destructors for 2-tuples are predefined in Prelude for use
             // by the Map#Items axiom
+          } else if (sf.EnclosingCtors[0] != ctor) {
+            // this special field, which comes from a shared destructor, is being declared in a different iteration of this loop
+          } else {
             sink.AddTopLevelDeclaration(fn);
           }
           // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i);
@@ -5349,9 +5352,10 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) {
         var 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.
+          if (dtor.EnclosingCtors.Count == dtor.EnclosingCtors[0].EnclosingDatatype.Ctors.Count) {
+            // Every constructor has this destructor; might as well assume that here.
+            var correctConstructor = BplOr(dtor.EnclosingCtors.ConvertAll(
+              ctor => FunctionCall(e.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj))));
             r = BplAnd(r, correctConstructor);
           }
         }
@@ -5949,13 +5953,14 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
           }
         } else if (e.Member is DatatypeDestructor) {
           var dtor = (DatatypeDestructor)e.Member;
-          var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj));
-          if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) {
-            // There is only one constructor, so the value must be been constructed by it; might as well assume that here.
+          var correctConstructor = BplOr(dtor.EnclosingCtors.ConvertAll(
+            ctor => FunctionCall(e.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj))));
+          if (dtor.EnclosingCtors.Count == dtor.EnclosingCtors[0].EnclosingDatatype.Ctors.Count) {
+            // Every constructor has this destructor; might as well assume that here.
             builder.Add(TrAssumeCmd(expr.tok, correctConstructor));
           } else {
             builder.Add(Assert(expr.tok, correctConstructor,
-              string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name)));
+              string.Format("destructor '{0}' can only be applied to datatype values constructed by {1}", dtor.Name, dtor.EnclosingCtorNames("or"))));
           }
         }
         if (options.DoReadsChecks && e.Member is Field && ((Field)e.Member).IsMutable) {

Test/dafny0/DatatypeUpdateResolution.dfy

@@ -18,3 +18,12 @@ method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:
   ghi := MyConstructor(2, false).(otherbool := true);  // allowed, and will generate verification error
   jkl := foo.(42 := 7, otherbool := true);  // error: members are from different constructors
 }
+
+datatype Dt = Make(x: int)
+
+method Main()
+{
+  var d := Make(5);
+  d := d.(x := 20);
+  d := d.(Make? := d);  // error: Make? is not a destructor (this previously crashed the resolver)
+}