Test/dafny0/DatatypeUpdateResolution.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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
}