Skip to content

Add kind and preferred flag for all Wingman code actions #1499

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.

Sign up for GitHub

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

Merged
merged 6 commits into from
Mar 5, 2021
Merged

Add kind and preferred flag for all Wingman code actions #1499

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
43d3790
Add kind and preferred flag for all Wingman code actions
isovector Mar 5, 2021
4e2b179
Shorten lambdacase kinds
isovector Mar 5, 2021
66537a7
destructFuncArgs --> splitFuncArgs
isovector Mar 5, 2021
5df7697
Fix a bug where we'd show wingman CAs on all out of scope variables
isovector Mar 5, 2021
9b87e10
Change the CA prefix to 'refactor.wingman.'
isovector Mar 5, 2021
07bf49f
Merge branch 'master' into tactic-kinds
isovector Mar 5, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,6 +171,9 @@ getSpanAndTypeAtHole amapping range hf = do
let info = nodeInfo ast'
ty <- listToMaybe $ nodeType info
guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
-- Ensure we're actually looking at a hole here
guard $ all (either (const False) $ isHole . occName)
$ M.keysSet $ nodeIdentifiers info
pure (nodeSpan ast', ty)


Expand Down
42 changes: 41 additions & 1 deletion plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,40 @@ commandTactic UseDataCon = userSplit
commandTactic Refine = const refine


------------------------------------------------------------------------------
-- | The LSP kind
tacticKind :: TacticCommand -> T.Text
tacticKind Auto = "fillHole"
tacticKind Intros = "introduceLambda"
tacticKind Destruct = "caseSplit"
tacticKind Homomorphism = "homomorphicCaseSplit"
tacticKind DestructLambdaCase = "lambdaCase"
tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase"
tacticKind DestructAll = "splitFuncArgs"
tacticKind UseDataCon = "useConstructor"
tacticKind Refine = "refine"


------------------------------------------------------------------------------
-- | Whether or not this code action is preferred -- ostensibly refers to
-- whether or not we can bind it to a key in vs code?
tacticPreferred :: TacticCommand -> Bool
tacticPreferred Auto = True
tacticPreferred Intros = True
tacticPreferred Destruct = True
tacticPreferred Homomorphism = False
tacticPreferred DestructLambdaCase = False
tacticPreferred HomomorphismLambdaCase = False
tacticPreferred DestructAll = True
tacticPreferred UseDataCon = True
tacticPreferred Refine = True


mkTacticKind :: TacticCommand -> CodeActionKind
mkTacticKind =
CodeActionUnknown . mappend "refactor.wingman." . tacticKind
Copy link
Member

@Ailrun Ailrun Mar 5, 2021 •
edited
Loading

Choose a reason for hiding this comment

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

I'm not familiar to action kind things, but since tactics plugin resolves (or changes) some errors, it may be better to use quickfix.wingman.. WDYT?

CC: @michaelpj

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Too slow, sorry! Feel free to file a bug if this is terribly worrisome!

Copy link
Collaborator

Choose a reason for hiding this comment

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

They don't seem very quickfix-y to me, and I think a bunch of them work with holes, so they won't actually be fixing errors.

Copy link
Member

Choose a reason for hiding this comment

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

@michaelpj I mean a hole produces a compile error, so... But I'm not strongly inclined to anything :)



------------------------------------------------------------------------------
-- | Mapping from tactic commands to their contextual providers. See 'provide',
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
Expand Down Expand Up @@ -225,7 +259,13 @@ provide tc name _ _ plId uri range _ = do
pure
$ pure
$ InR
$ CodeAction title (Just CodeActionQuickFix) Nothing Nothing Nothing Nothing
$ CodeAction
title
(Just $ mkTacticKind tc)
Nothing
(Just $ tacticPreferred tc)
Nothing
Nothing
$ Just cmd


Expand Down