-
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
Idea: replace attributes with arbitrary expressions #3149
Comments
@MikaelMayer also suggested using opaque predicates to solve the same problems. Perhaps that's a good reason to support arbitrary expressions as I've suggested, as uninterpreted calls to opaque predicates might end up having benefits over datatype values (although I haven't thought deeply enough to see them yet) |
Regardless of exactly what expressions we support in the end, having the parser accept arbitrary expressions and having the type checker sort out which ones are allowed seems like a good design approach. |
I love that proposal, especially the meta-attribute :-) I think this will be a huge leap forward. It would also enable us to rethink about annotations, for the same way we rethought about the new CLI over the previous one. I would be thrilled to see, for example down the road. assert @Error("Unexpected unitary x") x != 1
assert @AssumeOthers X by {
// Let's focus on this proof
} I don't think datatypes or opaque predicates would make a difference, except if we enable pre-computing annotations, then datatypes would rock. For example, could we consider this: function method ErrorAbout(name: string): string {
Error("Unexpected unitary " + name)
}
const nameOfX := "first coordinate X";
method Test(x: int)
requires @ErrorAbout(nameOfX) x != 1
}
method Main() {
Test(1); // Error: Unexpected unitary first coordinate X
} |
A nice side-effect of being able to implement traits with datatypes now (with |
Summary
Replace the current unchecked attribute syntax with arbitrary expressions, most often datatype values.
Background and Motivation
A common pain point is mis-spelling an attribute name and having the intended effect silently fail. For example adding
{:tailrecursive}
instead of{:tailrecursion}
on a function or method has no effect and raises no errors.Attributes are also not as self-documenting as other elements that can be referenced in a Dafny program: if you see a call to
FooBar(42)
, you can hover over it to see its declaration, or select "Go To Definition" to inspect it in detail. There is no such help for attributes in any tooling to date.Proposed Feature
Instead of the current
{:<name>, <argument>*}
syntax, we would add syntax for attaching an arbitrary expression as metadata to the same places within the AST. By requiring that these expressions resolve and type check successfully, we ensure that typos and other misuse results in errors. This appears to be a very nice solution for Dafny specifically because it already has an extremely rich sub-language for side-effect free expressions, and static evaluation of fairly sophisticated expressions is highly feasible and already present to a degree in the pipeline.As a straw-person argument I'd suggest following the lead of C#, Java, Python, and other languages and using
@
. For example:(I fully admit supporting arbitrary expressions rather than only datatype values may be too much power and complexity, but I'd like to start from this clean and general solution and be argued back to something more restrictive if necessary. It's likely that the general constant folding necessary for this feature could support arbitrary expressions, but that there are no solid use cases for it.)
Alternatives
We can address some of the requirements by an alternate mechanisms for registering supported attributes, their documentation, their valid use and argument types, and so on. We would also want plugins to participate in this mechanism.
The text was updated successfully, but these errors were encountered: