diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index 6978dcc4348..2f0918cad5d 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -4677,26 +4677,53 @@ public void ResolveParameterDefaultValues(List formals, ResolutionContex 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(); - var allowMoreRequiredParameters = true; - var allowNamelessParameters = true; + string nameOfMostRecentNameonlyParameter = null; + var previousParametersWithDefaultValue = new HashSet(); 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(); diff --git a/Test/dafny0/ParameterResolution.dfy b/Test/dafny0/ParameterResolution.dfy index 5e0db7bc1a7..bc07ac66885 100644 --- a/Test/dafny0/ParameterResolution.dfy +++ b/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); + } } diff --git a/Test/dafny0/ParameterResolution.dfy.expect b/Test/dafny0/ParameterResolution.dfy.expect index 25b3fe38b80..ebd0c81519d 100644 --- a/Test/dafny0/ParameterResolution.dfy.expect +++ b/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 diff --git a/docs/dev/news/3864.fix b/docs/dev/news/3864.fix new file mode 100644 index 00000000000..5284870ff43 --- /dev/null +++ b/docs/dev/news/3864.fix @@ -0,0 +1 @@ +Improved rules for nameonly parameters and parameter default-value expressions