search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

Need a way to pattern match datatypes without referencing all nameonly parameters #5907

Open robin-aws opened 2 weeks ago

robin-aws commented 2 weeks ago

Part of the motivation for supporting nameonly parameters and default arguments was enabling backwards compatibility:

datatype Foo = Foo(
  nameonly a: Option<int> := None,
  nameonly b: Option<int> := None
)

..

var f := Foo(a := Some(42));   // b defaults to None
// Adding a similar `c` parameter later doesn't break the statement above

However, there's currently no way to deconstruct such datatypes in match statements/expressions that isn't broken when more optional nameonly parameters are added:

var Foo(a, b) := f;    // breaks when `c` is added

(This has been hit in the past in smithy-dafny, when picking up AWS service model changes that should be backwards compatible but aren't because of this)

We need to support syntax similar to var Foo(a, b, ...) := ..., or more pessimistically not allow deconstructing datatypes with any nameonly parameters.