Skip to content

Commit 9bd0928

Browse files
authored
Add kind and preferred flag for all Wingman code actions (#1499)
* Add kind and preferred flag for all Wingman code actions * Shorten lambdacase kinds * destructFuncArgs --> splitFuncArgs * Fix a bug where we'd show wingman CAs on all out of scope variables * Change the CA prefix to 'refactor.wingman.'
1 parent db72348 commit 9bd0928

File tree

2 files changed

+44
-1
lines changed

2 files changed

+44
-1
lines changed

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

+3
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,9 @@ getSpanAndTypeAtHole amapping range hf = do
171171
let info = nodeInfo ast'
172172
ty <- listToMaybe $ nodeType info
173173
guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
174+
-- Ensure we're actually looking at a hole here
175+
guard $ all (either (const False) $ isHole . occName)
176+
$ M.keysSet $ nodeIdentifiers info
174177
pure (nodeSpan ast', ty)
175178

176179

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs

+41-1
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,40 @@ commandTactic UseDataCon = userSplit
5454
commandTactic Refine = const refine
5555

5656

57+
------------------------------------------------------------------------------
58+
-- | The LSP kind
59+
tacticKind :: TacticCommand -> T.Text
60+
tacticKind Auto = "fillHole"
61+
tacticKind Intros = "introduceLambda"
62+
tacticKind Destruct = "caseSplit"
63+
tacticKind Homomorphism = "homomorphicCaseSplit"
64+
tacticKind DestructLambdaCase = "lambdaCase"
65+
tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase"
66+
tacticKind DestructAll = "splitFuncArgs"
67+
tacticKind UseDataCon = "useConstructor"
68+
tacticKind Refine = "refine"
69+
70+
71+
------------------------------------------------------------------------------
72+
-- | Whether or not this code action is preferred -- ostensibly refers to
73+
-- whether or not we can bind it to a key in vs code?
74+
tacticPreferred :: TacticCommand -> Bool
75+
tacticPreferred Auto = True
76+
tacticPreferred Intros = True
77+
tacticPreferred Destruct = True
78+
tacticPreferred Homomorphism = False
79+
tacticPreferred DestructLambdaCase = False
80+
tacticPreferred HomomorphismLambdaCase = False
81+
tacticPreferred DestructAll = True
82+
tacticPreferred UseDataCon = True
83+
tacticPreferred Refine = True
84+
85+
86+
mkTacticKind :: TacticCommand -> CodeActionKind
87+
mkTacticKind =
88+
CodeActionUnknown . mappend "refactor.wingman." . tacticKind
89+
90+
5791
------------------------------------------------------------------------------
5892
-- | Mapping from tactic commands to their contextual providers. See 'provide',
5993
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
@@ -225,7 +259,13 @@ provide tc name _ _ plId uri range _ = do
225259
pure
226260
$ pure
227261
$ InR
228-
$ CodeAction title (Just CodeActionQuickFix) Nothing Nothing Nothing Nothing
262+
$ CodeAction
263+
title
264+
(Just $ mkTacticKind tc)
265+
Nothing
266+
(Just $ tacticPreferred tc)
267+
Nothing
268+
Nothing
229269
$ Just cmd
230270

231271

0 commit comments

Comments
 (0)