From 43d3790b1ee12159c4344a930166bf746f833c68 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 4 Mar 2021 22:46:04 -0800 Subject: [PATCH 1/5] Add kind and preferred flag for all Wingman code actions --- .../Tactic/LanguageServer/TacticProviders.hs | 42 ++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs index a1a530d55b..0446310409 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs @@ -55,6 +55,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 = "lambdaCaseSplit" +tacticKind HomomorphismLambdaCase = "homomorphicLambdaCaseSplit" +tacticKind DestructAll = "destructFuncArgs" +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.inline.wingman." . tacticKind + + ------------------------------------------------------------------------------ -- | Mapping from tactic commands to their contextual providers. See 'provide', -- 'filterGoalType' and 'filterBindingType' for the nitty gritty. @@ -226,7 +260,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 From 4e2b1795209cf4d29cfba20936782e9c4ef0f410 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 4 Mar 2021 22:51:51 -0800 Subject: [PATCH 2/5] Shorten lambdacase kinds --- .../src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs index 0446310409..849bd53602 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs @@ -62,8 +62,8 @@ tacticKind Auto = "fillHole" tacticKind Intros = "introduceLambda" tacticKind Destruct = "caseSplit" tacticKind Homomorphism = "homomorphicCaseSplit" -tacticKind DestructLambdaCase = "lambdaCaseSplit" -tacticKind HomomorphismLambdaCase = "homomorphicLambdaCaseSplit" +tacticKind DestructLambdaCase = "lambdaCase" +tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase" tacticKind DestructAll = "destructFuncArgs" tacticKind UseDataCon = "useConstructor" tacticKind Refine = "refine" From 66537a744538784a0aaf185c109087d9e6e6582d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 4 Mar 2021 23:35:00 -0800 Subject: [PATCH 3/5] destructFuncArgs --> splitFuncArgs --- .../src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs index 849bd53602..2e9b5027db 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs @@ -64,7 +64,7 @@ tacticKind Destruct = "caseSplit" tacticKind Homomorphism = "homomorphicCaseSplit" tacticKind DestructLambdaCase = "lambdaCase" tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase" -tacticKind DestructAll = "destructFuncArgs" +tacticKind DestructAll = "splitFuncArgs" tacticKind UseDataCon = "useConstructor" tacticKind Refine = "refine" From 5df7697f9acf636a4cb77bab0fe3ac8a2e68c60a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 5 Mar 2021 08:11:33 -0800 Subject: [PATCH 4/5] Fix a bug where we'd show wingman CAs on all out of scope variables --- .../hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 916aebed53..3b34d52dfa 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -172,6 +172,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) From 9b87e109599bdebbf891fe3828d4a5d24cf5ac37 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 5 Mar 2021 08:11:57 -0800 Subject: [PATCH 5/5] Change the CA prefix to 'refactor.wingman.' --- .../src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs index 2e9b5027db..929db0748c 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs @@ -86,7 +86,7 @@ tacticPreferred Refine = True mkTacticKind :: TacticCommand -> CodeActionKind mkTacticKind = - CodeActionUnknown . mappend "refactor.inline.wingman." . tacticKind + CodeActionUnknown . mappend "refactor.wingman." . tacticKind ------------------------------------------------------------------------------