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

Feat: Predicates can name their return parameter #2454

Merged
merged 15 commits into from
Aug 3, 2022

Conversation

MikaelMayer
Copy link
Member

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.

@MikaelMayer MikaelMayer marked this pull request as ready for review July 19, 2022 20:43
@MikaelMayer MikaelMayer requested a review from RustanLeino July 20, 2022 17:34
Copy link
Collaborator

@RustanLeino RustanLeino left a 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,
Copy link
Collaborator

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.

[ ":" Type<out returnType> (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
[
":"
( IF(FollowedByColon())
Copy link
Collaborator

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

"("
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) {
Copy link
Collaborator

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.

Copy link
Member Author

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)

  1. (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.
  2. 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 simply ensures result, and if it contrained the value to false, we could simply ensures !result.
  3. Despite these workarounds, even if there was some benefit doing (result: MyBoolSynonym) (e.g. for special ad-hoc compilation purposes like type 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.
  4. 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.

Copy link
Collaborator

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

Comment on lines 2357 to 2365
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)'"); .)
Copy link
Collaborator

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"

Copy link
Collaborator

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.

@MikaelMayer MikaelMayer self-assigned this Jul 21, 2022
@cpitclaudel
Copy link
Member

Just here to say nice job :)

@MikaelMayer MikaelMayer requested a review from RustanLeino August 3, 2022 17:54
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)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
- 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)

return false;
}
x = scanner.Peek();
var oneIdentifier = false;
Copy link
Collaborator

Choose a reason for hiding this comment

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

This means oneOrMoreIdentifiers, right?

Copy link
Member Author

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.

@MikaelMayer MikaelMayer enabled auto-merge (squash) August 3, 2022 20:11
@MikaelMayer MikaelMayer merged commit 9884d56 into master Aug 3, 2022
@MikaelMayer MikaelMayer deleted the feat-predicate-return-name branch August 3, 2022 20:54
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.

Would love to name predicate result
3 participants