-
Notifications
You must be signed in to change notification settings - Fork 261
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
Documentation of nameonly and default values for formals #3903
Conversation
docs/DafnyRef/Types.md
Outdated
may be called as either | ||
<!-- %check-resolve %use f.tmp --> | ||
```dafny | ||
const i := f(1,2); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add space after ,
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK
docs/DafnyRef/Types.md
Outdated
const i := f(1,2); | ||
const j := f(1); | ||
``` | ||
where `f(1)` is equivalent to `f(1,10)` in this case. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add space after ,
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK
docs/DafnyRef/Types.md
Outdated
The above function may be called as | ||
<!-- %no-check --> | ||
```dafny | ||
var k := f(y:=10, x:=2); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add a space on both sides of :=
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
docs/DafnyRef/Types.md
Outdated
Formal parameters may also be declared `nameonly`, in which case a call site | ||
must explicitly name the formal when providing its actual argument. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it would be nicer to explain nameonly
after explaining (in lines 4522-2527) that actual parameters may be given by name.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
docs/DafnyRef/Types.md
Outdated
as opposed to _required_. All required parameters must be declared | ||
before any optional parameters. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, this is no longer true (once #3864 is merged). A required parameter is allowed to follow an optional parameter, provided the required parameter is nameonly
. (It may be best to omit the sentence here and explain this below, after nameonly
has been introduced.)
Actually, L4538 says what needs to be said.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Removed the sentence.
docs/DafnyRef/Types.md
Outdated
```dafny | ||
function ff(x: int, nameonly y: int): int | ||
``` | ||
may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"only" here feels a bit confusing. For one, the parameters don't have to be passed in as 0
and 4
. But also, one can call ff
with ff(y := 4, x := 0)
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Right. Fixed.
docs/DafnyRef/Types.md
Outdated
may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. | ||
|
||
Any formals after a `nameonly` formal must either be `nameonly` themselves or have default values. | ||
Otherwise an error will result when an attempt is made to call the function or method with such a formal list. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
L4539 describes the motivation for L4538, from the language-design perspective. If L4538 is violated, Dafny will give an error for the declaration of the formals, so what happens at a call site is a moot point. I suggest keeping just L4538 and deleting L4539.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In this code
function f(x: int, nameonly y: int, z: int): int
const c := f(0, y:=0)
Dafny gives an error on the const declaration, but not on the function.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Apparently, this has been fixed since Dafny 4.0. We now get an error on the function declaration as well.
docs/DafnyRef/Types.md
Outdated
The formals of datatype constructors are not required to have names. Such formals may have default values but | ||
may not be declared `nameonly`. Such nameless formals must be declared before `nameonly` formals. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, a nameless formal is neither allowed to have a default value nor allowed to be declared nameonly
. Also, missing here is the rule that a nameless formal parameter is not allowed to follow an optional parameter. I suggest replacing the second and third sentences with "A nameless parameter is not allowed to follow a parameter with a default value.".
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK, but I would think a default value for a nameless formal to be a perfectly reasonable thing.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree. It would be a perfectly reasonable thing. We could add it in the future.
docs/DafnyRef/Expressions.md
Outdated
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 (in the formal parameter declaration) parameter does not have a default value, it is effectively nameonly. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since this paragraph explains "effectively nameonly", you may want to add a similar paragraph that explains "effectively required" (see #3864).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually, I found the 'effectively' terminology unhelpful -- better is simply stating and enforcing the rules about which formals can be optional and which can be nameonly.
Fixes #
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.