Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve rules for nameonly/positional/nameless and required/optional … #3864

Merged
merged 5 commits into from
Apr 24, 2023

Conversation

RustanLeino
Copy link
Collaborator

Fixes #3859

This PR allows more parameter declarations (for example, as suggested in #3859, a nameonly parameter with a default value can now be follow by other nameonly parameters), clarifies some error messages, and gives new errors for useless situations (for example, a parameter's default value can not be used if it is followed by a positional-only parameter).

The new rules

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 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

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@RustanLeino RustanLeino marked this pull request as ready for review April 12, 2023 17:33
seebees
seebees previously approved these changes Apr 12, 2023
Copy link

@seebees seebees left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

// * 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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

does not a => does not allow a

//
// 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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

be passed

// "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");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

a default-value expression

@@ -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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we should come up with a testing file format where you can specify the expected error messages inline : )

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I do like being able to read the expected outcome in the test file itself. Therefore, I always put such "error" comments in the tests. But these comments aren't the exact error messages, don't capture column information, and in some cases are even placed only on a nearby line. It's plausible that we could turn these into a formally recognized testing file format.

@keyboardDrummer
Copy link
Member

Such a nice quality of life improvement, thanks !

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) April 24, 2023 18:28
@keyboardDrummer keyboardDrummer merged commit 385b3f2 into dafny-lang:master Apr 24, 2023
19 checks passed
@RustanLeino RustanLeino deleted the issue-3859 branch April 25, 2023 00:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

nameonly should not constrain default values
3 participants