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/DatatypeUpdateResolution.dfy | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Test/dafny0/DatatypeUpdateResolution.dfy

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

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