Feat at attributes #5807
Feat at attributes #5807
Conversation
| case "Subsumption": { | ||
| return A1("subsumption", bindings); | ||
| } | ||
| case "Synthesize": { |
There was a problem hiding this comment.
Shouldn't the attributes be defined in a .dfy file?
There was a problem hiding this comment.
That can definitely be done in the future, and I already organized the code accordingly. For now, I'll keep the refactoring to a dafny file out of scope so all the code for the definition and the sync is in one place, and no pre-parsing and resolving is needed.
Moreover, two attributes (Induction and Trigger) don't have a typed counterpart so can't be expressed in Dafny.
|
I'm surprised, and concerned, that this PR is adding code completion code that is specific to attributes. I think code completion for attributes would be supported by generic code completion code. |
What is generic code completion code? |
It seems that you mention a need for generic code completion that this PR is not addressing. I think we can achieve all other code completions the same way that I am currently doing. Note that I'm happy to move this auto completion code in another PR if that is too concerning. |
|
About unexpected closing/reopening: I'm trying to write on my mobile device and sometimes the keyboard closes, making me click on buttons I did not intend to. |
Generic code completion is one that works for arbitrary references. I think we can implement that by letting the resolver code explicitly define the resolution of each reference, including the scope at that resolution. When invoking code completion at the reference, the IDE can then lookup the resolution defined for it, and from the attached scope see which identifiers of the right kind and type are available. Having the resolver define the resolution of each reference explicitly would also enable getting code navigation for free.
That'd be nice |
It looks great but seems like a very substantial piece of code. I guess the auto-completion I'm defining could easily be moved there, but at the same time I like it that it works before resolution finished. Auto-completion needs to be fast to be effective.
I added a TODO at the beginning of the description for that. I'll try to extract other PRs once I get something coherent. |
If you can define custom attributes using datatypes, which could be in modules, then I don't see how you could know which attributes are available in a certain location without also doing resolution. However, if you only want completion for a fixed set of attributes, then I think you could do "syntactic" completion, similar to snippets, and provide that before resolution. Could you elaborate on what you're targeting? (Could be in a different PR if that's where the change is) |
|
Closing in favor of #5825 and upcoming PRs |
TODO for review
Description
This PR adds support @- attributes prefixes on all nodes that previously supported attributes usually after their first keyword.
It also adds support for @-attributes prefixes on all expressions and statements
It provides auto-completion for @-attributes via the language server.
It provides a built-in rewriting from new @-attribute syntax to old-style attribute for easy migration
It provides a way for users to define their own attributes via @Attribute for datatypes
It resolves all @-attribute
Fixes:
{: ...}before:|in a VarDeclStatement was parsed but not attached to the AST, so I removed it.Left out of this PR:
How has this been tested?
TODO: Need to migrate at least one test for each attribute to ensure mapping is correct
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.