From 628acc07a07bd5516551dc2caa2c4612f70d2688 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 23 Oct 2015 18:30:11 -0700
Subject: 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)

---
 Test/dafny0/DatatypeUpdate.dfy | 50 +++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 49 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0/DatatypeUpdate.dfy')

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);
+  }
+}
+}
-- 
cgit v1.2.3