-
Notifications
You must be signed in to change notification settings - Fork 268
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
Feat: Predicates can name their return parameter #2454
Conversation
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.
Thanks for suggesting this addition. This design of allowing an optional : (x: bool)
in predicate declarations (and not allowing just : bool
in predicate declarations) looks good to me.
@@ -6094,9 +6094,10 @@ public enum BodyOriginKind { | |||
public readonly BodyOriginKind BodyOrigin; | |||
public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isGhost, | |||
List<TypeParameter> typeArgs, List<Formal> formals, | |||
Formal result, |
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.
Printer.cs
also needs to be updated.
Source/Dafny/Dafny.atg
Outdated
[ ":" Type<out returnType> (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .) | ||
[ | ||
":" | ||
( IF(FollowedByColon()) |
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.
The FollowedByColon()
method (which was already in the source before this PR) is mis-named (something like IsParenIdentColon()
seems more to the point) and its implementation is too liberal. For example, the input
function F(): :
gives the error message openparen expected
, which seems less than ideal. I suggest changing its implementation to returning true
if the next three things in the input are (in order) (
Ident
:
.
Source/Dafny/Dafny.atg
Outdated
"(" | ||
GIdentType<false, false, false, false, out var resultId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder> | ||
(. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder); | ||
if(ty is not BoolType) { |
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.
This is probably the right design, but an alternative would be to accept any type here and to, in the resolver, check that the type is bool
. A difference between these two designs is that the latter could allow
type MyBoolSynonym = bool
predicate P(): (result: MyBoolSynonym)
I don't know if that's valuable, consistent with other things, or just plain confusing.
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 understand the more permissive alternative. Here is my reasoning to not allow it (for now)
(result: MyBoolSynonym)
enables strictly more syntax than this PR, so if we decided it's useless, we would not be able to remove it if we added it.- I see another benefit using
(result: MyBoolSynonym)
: to use a subset type. But a subset type of bool is not very interesting. If the subset type constrained the value to true, we could simplyensures result
, and if it contrained the value to false, we could simplyensures !result
. - Despite these workarounds, even if there was some benefit doing
(result: MyBoolSynonym)
(e.g. for special ad-hoc compilation purposes liketype Wrapped<T>=T
that has a special meaning in the target, that could not nicely be implemented with attributes), we could implement it in a follow-up PR after carefully reviewing the need of someone asking for that. - Despite this, someone could still convert the predicate to a function for future purposes - this is what people would have done before this PR when trying to name the result.
So, after consideration, I think we can stick to this simpler PR.
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.
Sounds good. For now, if someone wants something different than the exact type bool
, then they can redeclare the predicate as a function
.
(Btw, there is one other place where Dafny accepts only two very specific types, namely in the optional square brackets that follow an extreme predicate or extreme lemma. The two types accepted are nat
and ORDINAL
. I have at times wanted to use a type synonym for them, so that I can easily experiment with changing a whole bunch of declarations from nat
to ORDINAL
or vice versa. I hope we'll allow type synonyms there in the future.)
Source/Dafny/Dafny.atg
Outdated
GIdentType<false, false, false, false, out var resultId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder> | ||
(. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder); | ||
if(ty is not BoolType) { | ||
SemErr(t, $"least predicates return type should be bool, got {ty}"); | ||
} | ||
result = new Formal(resultId, resultId.val, ty, false, false, null, false); | ||
.) | ||
")" | ||
| Type<out returnType> (. SemErr(t, "least predicates do not have an explicitly declared return type; it is always bool. Unless you want to name the result: ': (result: bool)'"); .) |
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.
This is mostly repeated 3 times (predicates, extreme predicates, and two-state predicates). Can it be refactored into one place?
@@ -0,0 +1,14 @@ | |||
// RUN: %dafny_0 /compile:0 "%s" > "%t" | |||
// RUN: %diff "%s.expect" "%t" | |||
|
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 suggest adding the MyBoolSynonym
example from my comments above (and recording that this does generate an error, or, if the design is ever changed, that it is allowed). Another test could be to define a subset type on top of bool
--I think that should not be allowed.
Just here to say nice job :) |
…-lang/dafny into feat-predicate-return-name
RELEASE_NOTES.md
Outdated
@@ -11,6 +11,7 @@ | |||
- fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (https://github.com/dafny-lang/dafny/pull/2437) | |||
- fix: Check extreme predicates and constants in all types, not just classes | |||
(https://github.com/dafny-lang/dafny/pull/2515) | |||
- feat: `predicate P(x: Int): (y: bool) ...` is now a valid syntax (https://github.com/dafny-lang/dafny/pull/2454) |
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.
- feat: `predicate P(x: Int): (y: bool) ...` is now a valid syntax (https://github.com/dafny-lang/dafny/pull/2454) | |
- feat: `predicate P(x: int): (y: bool) ...` is now a valid syntax (https://github.com/dafny-lang/dafny/pull/2454) |
Source/Dafny/Dafny.atg
Outdated
return false; | ||
} | ||
x = scanner.Peek(); | ||
var oneIdentifier = false; |
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.
This means oneOrMoreIdentifiers
, right?
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.
It also means that yes, although technically speaking, if you have one or many identifiers, it implies that you have one identifier for sure.
But I used your name.
…-lang/dafny into feat-predicate-return-name
Fixes #2453
Added two tests to verify the behavior.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.