Resolve ambiguity in export least predicate
#3291
Conversation
Source/DafnyCore/Dafny.atg
Outdated
| [ ExportId<out exportId> ] | ||
| [ IF(IsIdentifier(la.kind) || la.kind==_digits) ExportId<out exportId> // If the next token is 'least' or 'greatest' use it as the export id, | ||
| // not the beginning of a subsequent extreme predicate declaration | ||
| (. if (startToken.line != exportId.line) errors.Warning(exportId, "the id for the export declaration is on a different line than the 'export' keyword -- this looks suspicious or confusing"); |
There was a problem hiding this comment.
I'm puzzled about that. I've seen people writing
export
name
provides X
reveals Y
which seems adequate.
I think the error message could be more appropriate - but I don't have a strong opinion, your warning is already great - if the token before the start of a predicate on the same line was "least" or "greatest" and this predicate itself is not "least" or "greatest".
That way, export names could be on a different line.
There was a problem hiding this comment.
I suggest that if the input includes export least predicate, then we should given an error if least and predicate are on the same line (not if export and least are on different lines).
There was a problem hiding this comment.
OK. Now there is a warning if the token is least or greatest, it is in a export declaration, the next token is 'predicate', and 'predicate' is on the same line as 'least or 'greatest'.
Or, Rustan, did you really mean 'error' instead of 'warn ing' in your comment?
There was a problem hiding this comment.
Sorry, I meant warning. Good fix.
| @@ -2445,6 +2449,9 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f> | |||
| MethodFunctionName<out id> | |||
| ( | |||
| [ GenericParameters<typeArgs, false> ] | |||
| [ KType<ref kType> | |||
| (. SemErr(t, "a formal [ ] declaration is only allowed for least and greatest predicates"); .) | |||
There was a problem hiding this comment.
Great proactive error reporting
docs/DafnyRef/Modules.md
Outdated
| @@ -453,6 +453,25 @@ in `B` nor as `Z.a` in C would be valid, because `a` is not in `Z`. | |||
| The default export set is important in the resolution of qualified | |||
| names, as described in [Section 4.8](#sec-name-resolution). | |||
|
|
|||
| There are a few unusual cases to be noted: | |||
| - an export set can be completely empty, as in `export Nothing` | |||
| - an anonymous export set can be completely empty, as in `export` | |||
There was a problem hiding this comment.
Is this a way to make the module entirely private? If so, you could mention it.
There was a problem hiding this comment.
I don't like the term "anonymous export set". It does have a name, even if you don't give the name explicitly. (This is unlike a constructor in a class, which can indeed be anonymous.) If you omit the name of the export set, the name of the export set defaults to the name of the module. Therefore, "eponymous export set" is more appropriate.
For example, consider
module Module {
export
provides F
export Friends extends Module
provides G
function F(): int
function G(): int
}Here, the Friends export set extends the eponymous export set. Here, it is important that the first export set does have a name.
A client can use any of these import declarations:
import Module
import Module`Module
import Module`Friendswhere the first two mean the same thing. (Each one of these three introduces the local name Module, so if a client wants to use more than one of these imports, the client needs to provide an explicit local name.)
docs/DafnyRef/Modules.md
Outdated
| In this case the `least` (or `greatest`) is the identifier naming the export set. | ||
| Consequently, `export least predicate[nat]() { true }` is illegal because `[nat]` cannot be part of a non-extreme predicate. | ||
| Also, it is not possible to declare an anonymous, empty export set immediately prior to a declaration of an extreme predicate, | ||
| because the `least` or `greatest` is parsed as the export set identifier. The workaround for this situation is to reorder the declarations. |
There was a problem hiding this comment.
I just thought of a better or more natural workaround: Don't omit the name of the eponymous export set, but instead give its name explicitly. That is, change export to export M if this declaration is placed inside a module named M. (Alright, you still have to reorder the declarations inside the module if your module happens to be called least.)
There was a problem hiding this comment.
Revised accordingly.
This PR is a follow-up to PR #3291, making a few small corrections. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Fixes #3288
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.