Improve rules for nameonly/positional/nameless and required/optional … (

#3864)

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

@@ -4677,26 +4677,53 @@ public XConstraint_EquatableArg(IToken tok, Type a, Type b, bool allowSuperSub,
 
  Contract.Assume(AllTypeConstraints.Count == 0);
 
+ // Formal parameters have three ways to indicate how they are to be passed in:
+ // * nameonly: the only way to give a specific argument value is to name the parameter
+ // * positional only: these are nameless parameters (which are allowed only for datatype constructor parameters)
+ // * either positional or by name: this is the most common parameter
+ // A parameter is either required or optional:
+ // * required: a caller has to supply an argument
+ // * optional: the parameter has a default value that is used if a caller omits passing a specific argument
+ //
+ // The syntax for giving a positional-only (i.e., nameless) parameter does not allow a default-value expression, so
+ // a positional-only parameter is always required.
+ //
+ // At a call site, positional arguments are not allowed to follow named arguments. Therefore, if "x" is
+ // a nameonly parameter, then there is no way to supply the parameters after "x" by position. Thus, any
+ // parameter that follows "x" must either be passed by name or have a default value. That is, if a later
+ // parameter does not have a default value, it is _effectively_ nameonly. We impose the rule that
+ // * an effectively nameonly parameter must be declared as nameonly
+ //
+ // For a positional-only parameter "x", every parameter preceding "x" is _effectively_ required. We impose
+ // the rule that
+ // * an effectively required parameter must not have a default-value expression
  var dependencies = new Graph<IVariable>();
- var allowMoreRequiredParameters = true;
- var allowNamelessParameters = true;
+ string nameOfMostRecentNameonlyParameter = null;
+ var previousParametersWithDefaultValue = new HashSet<Formal>();
  foreach (var formal in formals) {
+ if (!formal.HasName) {
+ foreach (var previousFormal in previousParametersWithDefaultValue) {
+ reporter.Error(MessageSource.Resolver, previousFormal.DefaultValue.tok,
+ $"because of a later nameless parameter, this default value is never used; remove it or name all subsequent parameters");
+ }
+ previousParametersWithDefaultValue.Clear();
+ }
  var d = formal.DefaultValue;
  if (d != null) {
- allowMoreRequiredParameters = false;
  ResolveExpression(d, resolutionContext);
  AddAssignableConstraint(d.tok, formal.Type, d.Type, "default-value expression (of type '{1}') is not assignable to formal (of type '{0}')");
  foreach (var v in FreeVariables(d)) {
  dependencies.AddEdge(formal, v);
  }
- } else if (!allowMoreRequiredParameters) {
- reporter.Error(MessageSource.Resolver, formal.tok, "a required parameter must precede all optional parameters");
- }
- if (!allowNamelessParameters && !formal.HasName) {
- reporter.Error(MessageSource.Resolver, formal.tok, "a nameless parameter must precede all nameonly parameters");
+ previousParametersWithDefaultValue.Add(formal);
+ } else if (nameOfMostRecentNameonlyParameter != null && !formal.IsNameOnly) {
+ // "formal" is preceded by a nameonly parameter, but itself is neither nameonly nor has a default value
+ reporter.Error(MessageSource.Resolver, formal.tok,
+ $"this parameter is effectively nameonly (because of the earlier nameonly parameter '{nameOfMostRecentNameonlyParameter}'); " +
+ "declare it as nameonly or give it a default-value expression");
  }
  if (formal.IsNameOnly) {
- allowNamelessParameters = false;
+ nameOfMostRecentNameonlyParameter = formal.Name;
  }
  }
  SolveAllTypeConstraints();

Test/dafny0/ParameterResolution.dfy

@@ -198,11 +198,11 @@ module TypesAreDetermined {
  datatype Record = Record(y: int := F()) // error: type parameter X not determined
 }
 
-module RequiresBeforeOptional {
- datatype Color = Blue(x: int := y, y: int) // error: required parameters must precede optional parameters
- iterator Iter(x: int := y, y: int) // error: required parameters must precede optional parameters (reported twice)
- lemma Lemma(x: int := y, y: int) // error: required parameters must precede optional parameters
- least predicate Least(x: int := y, y: int) // error: required parameters must precede optional parameters
+module RequiredBeforeOptional {
+ datatype Color = Blue(x: int := y, y: int)
+ iterator Iter(x: int := y, y: int)
+ lemma Lemma(x: int := y, y: int)
+ least predicate Least(x: int := y, y: int)
 }
 
 module TwoState {
@@ -275,15 +275,15 @@ module NameOnlyParameters {
  least predicate LP(a: int, nameonly b: int, c: int := 100)
  static greatest predicate GP(a: int, nameonly b: int := 75, c: int := 100)
  }
- iterator Iter(nameonly u: int, x: int)
+ iterator Iter(nameonly u: int, x: int) // error (x2, because of the desugaring of iterators): x is effectively nameonly, but not declared as such
  datatype D =
  | DD(a: int, nameonly b: int)
- | DE(int, 0: int, real, nameonly 1: int, c: int)
+ | DE(int, 0: int, real, nameonly 1: int, c: int) // error: c is effective nameonly, but not declared as such
  | DF(800: int, nameonly 900: int, 9_0_0: int := 100)
  datatype E =
- | E0(a: int, b: int := 6, int) // error: required parameters must preceded optional parameters
- | E1(a: int, nameonly b: int := 6, u: int) // error: required parameters must preceded optional parameters
- | E2(a: int, nameonly b: int, int) // error: after a 'nameonly' parameter, all remaining parameters must have names
+ | E0(a: int, b: int := 6, int) // error: there is no way for the default value of 'b' to be used
+ | E1(a: int, nameonly b: int := 6, u: int) // u is effectively nameonly
+ | E2(a: int, nameonly b: int, int) // error: after a 'nameonly' parameter, all remaining parameters must be nameonly or have a default value
 
  method Test() {
  var c: C;
@@ -355,4 +355,26 @@ module NameOnlyParameters {
  d := DF(2, 0900 := 3, 9_0_0 := 4); // error (x2): no parameter is named '0900'; no argument passed for parameter '900'
  d := DF(2, 900 := 3, 90_0 := 4); // error: no parameter is named '90_0'
  }
+
+ // Issue 3859
+ datatype Foo = Foo(nameonly bar: string := "", nameonly baz: string, qux: int := 8)
+ function FooF(nameonly bar: string := "", nameonly baz: string, qux: int := 8): int
+ method FooM(nameonly bar: string := "", nameonly baz: string, qux: int := 8)
+
+ datatype XFoo = XFoo(bar: string := "", nameonly baz: string, qux: int := 8)
+ function XFooF(bar: string := "", nameonly baz: string, qux: int := 8): int
+ method XFooM(bar: string := "", nameonly baz: string, qux: int := 8)
+
+ datatype YFoo = YFoo(bar: string := "", nameonly baz: string, qux: int := 8, ohno: int, quux: real := 2.0) // error: onho is effectively nameonly, but not declared as such
+ function YFooF(bar: string := "", nameonly baz: string, qux: int := 8, ohno: int, quux: real := 2.0): int // error: onho is effectively nameonly, but not declared as such
+ method YFooM(bar: string := "", nameonly baz: string, qux: int := 8, ohno: int, quux: real := 2.0) // error: onho is effectively nameonly, but not declared as such
+
+ method FooUse() {
+ var f := Foo(baz := "yeah");
+ f := Foo(baz := "yeah", bar := "fun");
+ f := Foo(bar := "fun", baz := "yeah", qux := 10);
+ f := Foo(qux := 10, baz := "yeah");
+ f := Foo(); // error: baz is missing
+ var y := YFoo(baz := "a", ohno := 21);
+ }
 }

Test/dafny0/ParameterResolution.dfy.expect

@@ -52,11 +52,6 @@ ParameterResolution.dfy(198,37): Error: type parameter 'X' (inferred to be '?')
 ParameterResolution.dfy(193,21): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
 ParameterResolution.dfy(194,13): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
 ParameterResolution.dfy(196,29): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
-ParameterResolution.dfy(202,37): Error: a required parameter must precede all optional parameters
-ParameterResolution.dfy(203,29): Error: a required parameter must precede all optional parameters
-ParameterResolution.dfy(203,29): Error: a required parameter must precede all optional parameters
-ParameterResolution.dfy(204,27): Error: a required parameter must precede all optional parameters
-ParameterResolution.dfy(205,37): Error: a required parameter must precede all optional parameters
 ParameterResolution.dfy(211,23): Error: old expressions are not allowed in this context
 ParameterResolution.dfy(213,25): Error: old expressions are not allowed in this context
 ParameterResolution.dfy(216,32): Error: old expressions are not allowed in this context
@@ -73,9 +68,13 @@ ParameterResolution.dfy(252,21): Error: Duplicate parameter name: x
 ParameterResolution.dfy(259,11): Error: default-value expressions for parameters contain a cycle: x -> x
 ParameterResolution.dfy(260,35): Error: unresolved identifier: _k
 ParameterResolution.dfy(261,26): Error: unresolved identifier: _k
-ParameterResolution.dfy(284,30): Error: a required parameter must precede all optional parameters
-ParameterResolution.dfy(285,39): Error: a required parameter must precede all optional parameters
-ParameterResolution.dfy(286,34): Error: a nameless parameter must precede all nameonly parameters
+ParameterResolution.dfy(278,33): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'u'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(278,33): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'u'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(281,45): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter '1'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(284,27): Error: because of a later nameless parameter, this default value is never used; remove it or name all subsequent parameters
+ParameterResolution.dfy(285,39): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'b'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(286,34): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'b'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(368,79): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it a default-value expression
 ParameterResolution.dfy(290,21): Error: nameonly parameter 'c' must be passed using a name binding; it cannot be passed positionally
 ParameterResolution.dfy(297,26): Error: nameonly parameter 'c' must be passed using a name binding; it cannot be passed positionally
 ParameterResolution.dfy(301,34): Error: a positional argument is not allowed to follow named arguments
@@ -98,4 +97,7 @@ ParameterResolution.dfy(351,15): Error: nameonly parameter '900' must be passed
 ParameterResolution.dfy(355,15): Error: the binding named '0900' does not correspond to any formal parameter
 ParameterResolution.dfy(355,9): Error: datatype constructor parameter '900' at index 1 requires an argument of type int
 ParameterResolution.dfy(356,25): Error: the binding named '90_0' does not correspond to any formal parameter
-100 resolution/type errors detected in ParameterResolution.dfy
+ParameterResolution.dfy(369,73): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(370,71): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it a default-value expression
+ParameterResolution.dfy(377,9): Error: wrong number of arguments (got 0, but datatype constructor 'Foo' expects at least 1: (bar: string, baz: string, qux: int))
+102 resolution/type errors detected in ParameterResolution.dfy

docs/dev/news/3864.fix

@@ -0,0 +1 @@
+Improved rules for nameonly parameters and parameter default-value expressions