From 6a10fc526fa64763ff88dc14c28d036555c16645 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 12 Apr 2023 10:16:16 -0700 Subject: [PATCH 1/3] Improve rules for nameonly/positional/nameless and required/optional parameters Fixes #3859 --- .../NameResolutionAndTypeInference.cs | 45 +++++++++++++++---- Test/dafny0/ParameterResolution.dfy | 42 ++++++++++++----- Test/dafny0/ParameterResolution.dfy.expect | 20 +++++---- 3 files changed, 79 insertions(+), 28 deletions(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index 74866bb2065..b8575e7f671 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -4673,26 +4673,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 value is to name the parameter + // * positional only: these are nameless arguments (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 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 by 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 an 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..3d9505f2e79 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 an 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 an 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 an 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 an 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 an 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 an 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 an 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 an 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 From 5377a3128b237471f48fa87b725c09a612ca6199 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 12 Apr 2023 10:33:04 -0700 Subject: [PATCH 2/3] Add release notes --- Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs | 4 ++-- docs/dev/news/3864.fix | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) create mode 100644 docs/dev/news/3864.fix diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index b8575e7f671..cf6c43744e8 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -4674,8 +4674,8 @@ 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 value is to name the parameter - // * positional only: these are nameless arguments (which are allowed only for datatype constructor parameters) + // * 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 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 From 837505d48622630b2ffff36d905f86326dc39731 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 18 Apr 2023 13:45:07 -0700 Subject: [PATCH 3/3] Act on PR comments --- .../Resolver/NameResolutionAndTypeInference.cs | 6 +++--- Test/dafny0/ParameterResolution.dfy.expect | 16 ++++++++-------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs index cf6c43744e8..e8e1a59b6c1 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs @@ -4681,12 +4681,12 @@ public void ResolveParameterDefaultValues(List formals, ResolutionContex // * 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 a default-value expression, so + // 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 by passed by name or have a default value. That is, if a later + // 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 // @@ -4716,7 +4716,7 @@ public void ResolveParameterDefaultValues(List formals, ResolutionContex // "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 an default-value expression"); + "declare it as nameonly or give it a default-value expression"); } if (formal.IsNameOnly) { nameOfMostRecentNameonlyParameter = formal.Name; diff --git a/Test/dafny0/ParameterResolution.dfy.expect b/Test/dafny0/ParameterResolution.dfy.expect index 3d9505f2e79..ebd0c81519d 100644 --- a/Test/dafny0/ParameterResolution.dfy.expect +++ b/Test/dafny0/ParameterResolution.dfy.expect @@ -68,13 +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(278,33): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'u'); declare it as nameonly or give it an 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 an 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 an 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(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 an 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 an 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 an default-value expression +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 @@ -97,7 +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 -ParameterResolution.dfy(369,73): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it an 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 an default-value expression +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