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)

1 files changed, 49 insertions, 1 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);

+  }

+}

+}