Allow datatype updates to update shared destructors

Author: Rustan Leino

Source/Dafny/DafnyAst.cs

@@ -3904,21 +3904,27 @@ internal void AddAnotherEnclosingCtor(DatatypeCtor ctor, Formal formal) {
 
     internal string EnclosingCtorNames(string grammaticalConjunction) {
       Contract.Requires(grammaticalConjunction != null);
-      var n = EnclosingCtors.Count;
+      return PrintableCtorNameList(EnclosingCtors, grammaticalConjunction);
+    }
+
+    static internal string PrintableCtorNameList(List<DatatypeCtor> ctors, string grammaticalConjunction) {
+      Contract.Requires(ctors != null && ctors.Count != 1);
+      Contract.Requires(grammaticalConjunction != null);
+      var n = ctors.Count;
       if (n == 1) {
-        return string.Format("'{0}'", EnclosingCtors[0].Name);
+        return string.Format("'{0}'", ctors[0].Name);
       } else if (n == 2) {
-        return string.Format("'{0}' {1} '{2}'", EnclosingCtors[0].Name, grammaticalConjunction, EnclosingCtors[1].Name);
+        return string.Format("'{0}' {1} '{2}'", ctors[0].Name, grammaticalConjunction, ctors[1].Name);
       } else {
         var s = "";
         for (int i = 0; i < n - 1; i++) {
-          s += string.Format("'{0}', ", EnclosingCtors[i].Name);
+          s += string.Format("'{0}', ", ctors[i].Name);
         }
-        return s + string.Format("{0} '{1}'", grammaticalConjunction, EnclosingCtors[n - 1].Name);
+        return s + string.Format("{0} '{1}'", grammaticalConjunction, ctors[n - 1].Name);
       }
     }
   }
-  
+
   public class ConstantField : SpecialField, ICallable
   {
     public override string WhatKind { get { return "const field"; } }

Source/Dafny/Resolver.cs

@@ -10464,10 +10464,10 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L
       // We're currently looking at e = e(n-1)[en.Index := en.Value]
       // Let e(n-2) = e(n-1).Seq, e(n-3) = e(n-2).Seq, etc.
       // Let's extract e = e0[e1.Index := e1.Value]...[en.Index := en.Value]
-      DatatypeCtor ctor = null;
-      Tuple<IToken, string, Expression> ctorSource = default(Tuple<IToken, string, Expression>);  // relevant only if "ctor" is non-null
+      var possibleCtors = dt.Ctors;  // list of constructors that have all the so-far-mentioned destructors
       var memberNames = new HashSet<string>();
-      var updates = new Dictionary<Formal, Expression>();
+      var updates = new Dictionary<DatatypeDestructor, Expression>();
+      var suppressUniquenessCheck = false;
       foreach (var entry in memberUpdates) {
         var destructor_str = entry.Item2;
         if (memberNames.Contains(destructor_str)) {
@@ -10477,35 +10477,51 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L
           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);
+            suppressUniquenessCheck = true;
           } else if (!(member is DatatypeDestructor)) {
             reporter.Error(MessageSource.Resolver, entry.Item1, "member '{0}' is not a destructor in datatype '{1}'", destructor_str, dt.Name);
+            suppressUniquenessCheck = true;
           } else {
             var destructor = (DatatypeDestructor)member;
-            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.EnclosingCtors[0].Name, ctorSource.Item2, ctor.Name);
+            var intersection = new List<DatatypeCtor>(possibleCtors.Intersect(destructor.EnclosingCtors));
+            if (intersection.Count != 0) {
+              possibleCtors = intersection;
+              updates.Add(destructor, entry.Item3);
             } else {
-              updates.Add(destructor.CorrespondingFormals[0], entry.Item3);
-              ctor = destructor.EnclosingCtors[0];
-              ctorSource = entry;
+              reporter.Error(MessageSource.Resolver, entry.Item1, "updated datatype members must belong to the same constructor " +
+                "(unlike the previously mentioned destructors, '{0}' does not belong to {1})", entry.Item2, DatatypeDestructor.PrintableCtorNameList(possibleCtors, "or"));
+              suppressUniquenessCheck = true;
             }
           }
         }
       }
 
-      if (ctor != null) {
+      if (possibleCtors.Count != 1) {
+        if (!suppressUniquenessCheck) {
+          var which = DatatypeDestructor.PrintableCtorNameList(possibleCtors, "and");
+          string explanation;
+          if (memberUpdates.Count == 1) {
+            explanation = string.Format("destructor '{0}' belongs to constructors {1}", memberUpdates[0].Item2, which);
+          } else {
+            explanation = string.Format("the given destructors all belong to constructors {0}", which);
+          }
+          reporter.Error(MessageSource.Resolver, tok, "the updated datatype members must uniquely determine the resulting constructor ({0})", explanation);
+        }
+      } else {
+        var ctor = possibleCtors[0];
         // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)"
         // Wrapping it in a let expr avoids exponential growth in the size of the expression
         // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" where "E0" is "root" to
         //   "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)"
 
+        // Now that we know which constructor we're talking about, we can pick out the formal corresponding to each destructor
+        var fUpdates = new Dictionary<Formal, Expression>();
+        foreach (var entry in updates) {
+          var i = entry.Key.EnclosingCtors.IndexOf(ctor);
+          Contract.Assert(0 <= i && i < entry.Key.CorrespondingFormals.Count);
+          fUpdates.Add(entry.Key.CorrespondingFormals[i], entry.Value);
+        }
+
         // Create a unique name for d', the variable we introduce in the let expression
         var tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext);
         var tmpVarIdExpr = new IdentifierExpr(new AutoGeneratedToken(tok), tmpName);
@@ -10515,7 +10531,7 @@ Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, L
         var ctor_args = new List<Expression>();
         foreach (Formal d in ctor.Formals) {
           Expression v;
-          if (updates.TryGetValue(d, out v)) {
+          if (fUpdates.TryGetValue(d, out v)) {
             ctor_args.Add(v);
           } else {
             ctor_args.Add(new ExprDotName(tok, tmpVarIdExpr, d.Name, null));

Test/allocated1/dafny0/DatatypeUpdateResolution.dfy.expect

@@ -2,5 +2,6 @@ DatatypeUpdateResolution.dfy(3,8): Error: the included file DatatypeUpdateResolu
 DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType'
 DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType'
 DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool'
-DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor'
-5 resolution/type errors detected in DatatypeUpdateResolution.dfy
+DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor (unlike the previously mentioned destructors, 'otherbool' does not belong to 'MyNumericConstructor')
+DatatypeUpdateResolution.dfy(28,10): Error: member 'Make?' is not a destructor in datatype 'Dt'
+6 resolution/type errors detected in DatatypeUpdateResolution.dfy

Test/dafny0/DatatypeUpdateResolution.dfy.expect

@@ -1,6 +1,6 @@
 DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType'
 DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType'
 DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool'
-DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor')
+DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor (unlike the previously mentioned destructors, 'otherbool' does not belong to 'MyNumericConstructor')
 DatatypeUpdateResolution.dfy(28,10): Error: member 'Make?' is not a destructor in datatype 'Dt'
 5 resolution/type errors detected in DatatypeUpdateResolution.dfy

Test/dafny0/SharedDestructors.dfy

@@ -30,6 +30,9 @@ method M(d: Dt) returns (r: int, s: real)
     var h := d.h;  // error: d might not have a member .h (1 name in error msg)
   case d.B? =>
     var h := d.h;
+  case true =>
+    var n := d.(y := 2.7, x := 3);
+    assert n.A?;
 }
 
 datatype Record = Record(t: int)
@@ -59,19 +62,21 @@ datatype Quirky = PP(id: int, a: int) | QQ(b: int, id: int) | RR(id: int, c: int
 
 method UpdateA(y: Quirky) returns (y': Quirky)
 {
-  // The semantics of datatype field update is somewhat quirky.  It's perhaps a design
-  // bug, but here is what it requires and what it does:
-  // - Each field given must be a non-shared destructor.  That is, each field mentioned
-  //   must be a destructor in a unique constructor.  (An alternative to this design
-  //   would be to just insist that the intersection of the constructors that contain
-  //   the given fields must be a single constructor.)
-  //   This unique constructor is the constructor that will be used for the result.
-  // - Every field "g" of the chosen constructor must either be given in the update
-  //   expression or be available in the source expression.  This does not necessarily
-  //   mean that the source expression must already be of the chosen constructor; it
-  //   suffices that every such "g" is available in all of the constructors.  A special
-  //   case of this is that there is no "g", in which case the value of the source
-  //   expression does not matter at all.
+  // Datatype field update works as follows:
+  // 0- The fields given in the update must uniquely determine a constructor.
+  //    The result will be of this constructor.
+  // 1- For any pair "f := E" given in the update, the field "f" of the result will
+  //    have the value "E".
+  // 2- For any field "f" that is not given in the update "E.(x := X, y := Y, ...)",
+  //    "E" must be a value with an "f" field and the value of "f" in the result will
+  //    be "E.f".
+  // Note, in point 2, the requirement that "E" have an "f" field is satisfied
+  // if "E" is constructed by the same constructor as is determined in point 0.
+  // However, it is also possible to satisfy this requirement if "f" is a shared
+  // destructor and "E" is of a constructor that has that shared field.
+  // Note also, that a degenerate case of the update expression is that all fields
+  // of the by-point-0 determined constructor are given explicitly.  In that case,
+  // the source of the update (that is, the "E" in "E.(...)") can be any value.
   if
   case true =>
     // make a PP, get .id from anywhere
@@ -89,3 +94,20 @@ method UpdateA(y: Quirky) returns (y': Quirky)
     // make an RR, but where does .d come from?
     y' := y.(c := 10);  // error: this would require y to be an RR
 }
+
+datatype Klef =
+  | C0(0: int, 1: int, 2: int, c0: int)
+  | C1(1: int, 2: int, 3: int, c1: int)
+  | C2(2: int, 3: int, 0: int, c2: int)
+  | C3(3: int, 0: int, 1: int, c3: int)
+
+method TroubleKlef(k: Klef) returns (k': Klef)
+  ensures k'.C3?
+{
+  if
+  case k.C1? || k.C3? =>
+    k' := k.(0 := 100, c3 := 200);  // makes a C3
+    assert k' == C3(k.3, 100, k.1, 200);
+  case true =>
+    k' := k.(0 := 100, c3 := 200);  // error (x2): k might not have .1 and .3
+}

Test/dafny0/SharedDestructors.dfy.expect

@@ -1,33 +1,41 @@
 SharedDestructors.dfy(16,11): Error: destructor 'x' can only be applied to datatype values constructed by 'A' or 'B'
 Execution trace:
     (0,0): anon0
-    (0,0): anon13_Then
+    (0,0): anon14_Then
 SharedDestructors.dfy(22,11): Error: destructor 'x' can only be applied to datatype values constructed by 'A' or 'B'
 Execution trace:
     (0,0): anon0
-    (0,0): anon16_Then
+    (0,0): anon17_Then
 SharedDestructors.dfy(24,11): Error: destructor 'y' can only be applied to datatype values constructed by 'A', 'C', or 'D'
 Execution trace:
     (0,0): anon0
-    (0,0): anon17_Then
+    (0,0): anon18_Then
 SharedDestructors.dfy(30,15): Error: destructor 'h' can only be applied to datatype values constructed by 'B'
 Execution trace:
     (0,0): anon0
-    (0,0): anon21_Then
-SharedDestructors.dfy(48,14): Error: destructor 'a' can only be applied to datatype values constructed by 'AA'
+    (0,0): anon22_Then
+SharedDestructors.dfy(51,14): Error: destructor 'a' can only be applied to datatype values constructed by 'AA'
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
     (0,0): anon9_Then
-SharedDestructors.dfy(54,14): Error: destructor 'c' can only be applied to datatype values constructed by 'AA'
+SharedDestructors.dfy(57,14): Error: destructor 'c' can only be applied to datatype values constructed by 'AA'
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
     (0,0): anon9_Else
     (0,0): anon10_Else
-SharedDestructors.dfy(90,12): Error: destructor 'd' can only be applied to datatype values constructed by 'RR'
+SharedDestructors.dfy(95,12): Error: destructor 'd' can only be applied to datatype values constructed by 'RR'
 Execution trace:
     (0,0): anon0
     (0,0): anon11_Then
+SharedDestructors.dfy(112,12): Error: destructor '1' can only be applied to datatype values constructed by 'C0', 'C1', or 'C3'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Then
+SharedDestructors.dfy(112,12): Error: destructor '3' can only be applied to datatype values constructed by 'C1', 'C2', or 'C3'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Then
 
-Dafny program verifier finished with 0 verified, 7 errors
+Dafny program verifier finished with 0 verified, 9 errors

Test/dafny0/SharedDestructorsCompile.dfy

@@ -32,4 +32,20 @@ method Main()
     assert d.x == 71;
     i := i + 1;
   }
+
+  BaseKlef(C1(44, 55, 66, 77));
+}
+
+datatype Klef =
+  | C0(0: int, 1: int, 2: int, c0: int)
+  | C1(1: int, 2: int, 3: int, c1: int)
+  | C2(2: int, 3: int, 0: int, c2: int)
+  | C3(3: int, 0: int, 1: int, c3: int)
+
+method BaseKlef(k: Klef)
+  requires !k.C0? && !k.C2?
+{
+  var k' := k.(0 := 100, c3 := 200);  // makes a C3
+  assert k' == C3(k.3, 100, k.1, 200);
+  print k', "\n";
 }

Test/dafny0/SharedDestructorsCompile.dfy.expect

@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 1 verified, 0 errors
+Dafny program verifier finished with 2 verified, 0 errors
 Program compiled successfully
 Running...
 
@@ -8,3 +8,4 @@ Dt.B(__default.MyClass, 6):  h=__default.MyClass x=6
 Dt.C((314.0 / 100.0)):  y=(314.0 / 100.0)
 Dt.C((314.0 / 100.0))
 Dt.A(71, (1.0 / 10.0))
+Klef.C3(66, 100, 44, 200)

Test/dafny0/SharedDestructorsResolution.dfy

@@ -13,12 +13,37 @@ module Module0 {
   method Update(d: Dt) returns (d': Dt)
   {
     if d.A? {
-      d' := d.(x := 6);  // error: the destructor to be updated must be uniquely named
+      d' := d.(x := 6);  // error: this destructor alone does not uniquely determine a resulting constructor
     } else if d.B? {
       d' := d.(h := null);
     } else {
-      d' := d.(y := 0.0);  // error: the destructor to be updated must be uniquely named
+      d' := d.(y := 0.0);  // error: this destructor alone does not uniquely determine a resulting constructor
     }
+    d' := d.(x := 100, h := null);  // yes, this does unique determine the constructor
+  }
+
+  datatype Klef =
+    | C0(0: int, 1: int, 2: int, c0: int)
+    | C1(1: int, 2: int, 3: int, c1: int)
+    | C2(2: int, 3: int, 0: int, c2: int)
+    | C3(3: int, 0: int, 1: int, c3: int)
+
+  method UK(k: Klef, x: int) returns (k': Klef)
+  {
+    k' := k.(2 := x, 3 := x, 0 := x);  // this makes a C2
+    k' := k.(0 := x, 1 := x);  // error: ambiguous
+    k' := k.(c0 := x, 3 := x);  // error: no constructor has both "c0" and "3"
+    k' := k.(3 := x, c0 := x);  // error: ditto
+    k' := k.(3 := x, 2 := x, c0 := x);  // error: no constructor has all these destructors
+    k' := k.(3 := x, 2 := x, 1 := x, c0 := x);  // error: no constructor has all these destructors
+    k' := k.(3 := x, 1 := x, 0 := x);  // this makes a C3
+    k' := k.(1 := x, c3 := x);  // this makes a C3
+    // multiples errors:
+    k' := k.(C0? := x);  // error: C0? is not a destructor
+    k' := k.(C0? := x, c0 := x);  // error: ditto
+    k' := k.(c0 := x, c0 := x, c2 := x);  // error (2x): c0 duplicate, c2 never with c0
+    k' := k.(c0 := x, c1 := x, c2 := x);  // error (2x): c1 and c2 never with c0
+    k' := k.(0 := x, 0 := x, 1 := x);  // error (2x): c0 duplicate, ambiguous C0 or C3
   }
 }