Merge commit 'df5c5f5'

1 files changed, 20 insertions, 0 deletions

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

+}