Introduced new datatype update syntax: D.(f := E)

The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated.
The new syntax also supports multiple updates:  D.(f := E0, g := E1, h := E2)

4 files changed, 86 insertions, 2 deletions

diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 76cce5ce..b7905928 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -1,6 +1,6 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-

+module OldSyntax {

 datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

                     | MyOtherConstructor(otherbool:bool) 

                     | MyNumericConstructor(42:int)

@@ -35,3 +35,51 @@ method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)
 {

   pp := nn[010 := y];  // not to be confused with a field name 10

 }

+}

+

+module NewSyntax {

+datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

+                    | MyOtherConstructor(otherbool:bool) 

+                    | MyNumericConstructor(42:int)

+

+method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)

+    requires foo.MyConstructor?;

+    ensures abc == foo.(myint := x + 2);

+    ensures def == foo.(otherbool := !foo.mybool);

+    ensures ghi == foo.(myint := 2).(mybool := false);

+    //ensures jkl == foo.(non_destructor := 5);      // Resolution error: no non_destructor in MyDataType

+    ensures jkl == foo.(42 := 7);

+{

+    abc := MyConstructor(x + 2, foo.mybool); 

+    abc := foo.(myint := x + 2);

+    def := MyOtherConstructor(!foo.mybool);

+    ghi := MyConstructor(2, false);

+    jkl := foo.(42 := 7);

+

+    assert abc.(myint := abc.myint - 2) == foo.(myint := x);

+}

+

+// regression test (for a previous bug in the Translator.Substituter):

+datatype Dt = Ctor(x: int, y: bool)

+function F(d: Dt): Dt

+{

+  d.(x := 5)

+}

+

+datatype NumericNames = NumNam(010: int, 10: real, f: bool)

+

+method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)

+{

+  pp := nn.(010 := y);  // not to be confused with a field name 10

+}

+

+method MultipleUpdates(nn: NumericNames, y: int) returns (pp: NumericNames)

+  ensures pp.010 == y

+{

+  if * {

+    pp := nn.(10 := 0.10, 010 := y);

+  } else {

+    pp := nn.(010 := y, f := true, 10 := 0.10);

+  }

+}

+}

diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 790f6509..9a924214 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,13 @@
+DatatypeUpdate.dfy(10,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(11,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(12,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(12,34): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(14,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(17,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(20,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(22,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(22,45): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(29,3): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(36,10): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

 

-Dafny program verifier finished with 5 verified, 0 errors

+Dafny program verifier finished with 12 verified, 0 errors

diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy b/Test/dafny0/DatatypeUpdateResolution.dfy
new file mode 100644
index 00000000..26142fa8
--- /dev/null
+++ b/Test/dafny0/DatatypeUpdateResolution.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

+                    | MyOtherConstructor(otherbool:bool) 

+                    | MyNumericConstructor(42:int)

+datatype SomeOtherType = S_O_T(non_destructor: int)

+

+method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)

+  requires foo.MyConstructor?

+  ensures abc == foo.(myint := x + 2)

+  ensures jkl == foo.(non_destructor := 5)      // error: 'non_destructor' is not a destructor in MyDataType

+  ensures jkl == foo.(mybool := true, 40 := 100, myint := 200)  // error: '40' is not a destructor

+{

+  abc := MyConstructor(x + 2, foo.mybool).(myint := x + 3);

+  abc := foo.(myint := x + 2, mybool := true).(mybool := false);  // allowed

+  def := MyOtherConstructor(!foo.mybool).(otherbool := true, otherbool := true);  // error: duplicated member

+  ghi := MyConstructor(2, false).(otherbool := true);  // allowed, and will generate verification error

+  jkl := foo.(42 := 7, otherbool := true);  // error: members are from different constructors

+}

diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy.expect b/Test/dafny0/DatatypeUpdateResolution.dfy.expect
new file mode 100644
index 00000000..db3e1fe2
--- /dev/null
+++ b/Test/dafny0/DatatypeUpdateResolution.dfy.expect
@@ -0,0 +1,5 @@
+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'

+4 resolution/type errors detected in DatatypeUpdateResolution.dfy