From 628acc07a07bd5516551dc2caa2c4612f70d2688 Mon Sep 17 00:00:00 2001 From: leino 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 ++++++++++++++++++++++++- Test/dafny0/DatatypeUpdate.dfy.expect | 13 ++++++- Test/dafny0/DatatypeUpdateResolution.dfy | 20 ++++++++++ Test/dafny0/DatatypeUpdateResolution.dfy.expect | 5 +++ 4 files changed, 86 insertions(+), 2 deletions(-) create mode 100644 Test/dafny0/DatatypeUpdateResolution.dfy create mode 100644 Test/dafny0/DatatypeUpdateResolution.dfy.expect (limited to 'Test/dafny0') 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); + } +} +} diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect index 790f6509..9a924214 100644 --- a/Test/dafny0/DatatypeUpdate.dfy.expect +++ b/Test/dafny0/DatatypeUpdate.dfy.expect @@ -1,2 +1,13 @@ +DatatypeUpdate.dfy(10,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(11,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(12,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(12,34): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(14,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(17,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(20,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(22,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(22,45): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(29,3): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) +DatatypeUpdate.dfy(36,10): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E) -Dafny program verifier finished with 5 verified, 0 errors +Dafny program verifier finished with 12 verified, 0 errors 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 +} diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy.expect b/Test/dafny0/DatatypeUpdateResolution.dfy.expect new file mode 100644 index 00000000..db3e1fe2 --- /dev/null +++ b/Test/dafny0/DatatypeUpdateResolution.dfy.expect @@ -0,0 +1,5 @@ +DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType' +DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType' +DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool' +DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor' +4 resolution/type errors detected in DatatypeUpdateResolution.dfy -- cgit v1.2.3