Feat at attributes

[MikaelMayer]

TODO for review

• [x] Move auto-completion in a separate PR
• [x] A test for resolution of attributes

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:

• The attribute {: ...} before :| in a VarDeclStatement was parsed but not attached to the AST, so I removed it.

Left out of this PR:

• Auto-complete on the language server
• Attributes on any statement (can be added later if needed)

How has this been tested?

• A test that covers all new built-in @-attributes
• A test that covers all typical mispellings of builtin attributes
• A test that demonstrates user-defined @-attributes
• To minimize the risk of typo, I used hotkeys for 8 redundant constructs in Dafny.atg

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

[keyboardDrummer]

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.

[MikaelMayer]

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?

[MikaelMayer]

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.

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.

[MikaelMayer]

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.

[keyboardDrummer]

What is generic code completion code?

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.

Note that I'm happy to move this auto completion code in another PR if that is too concerning.

That'd be nice

[MikaelMayer]

What is generic code completion code?

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.

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.

Note that I'm happy to move this auto completion code in another PR if that is too concerning.

That'd be nice

I added a TODO at the beginning of the description for that. I'll try to extract other PRs once I get something coherent.

[keyboardDrummer]

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.

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)

[MikaelMayer]

Closing in favor of https://github.com/dafny-lang/dafny/pull/5825 and upcoming PRs