From b37f8fcae22e93e1baafdde75a52ad60c80ad7fb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 14:32:16 -0800 Subject: [PATCH 1/4] Add DestructAll tactic --- .../src/Ide/Plugin/Tactic/Judgements.hs | 9 +++++++++ .../Tactic/LanguageServer/TacticProviders.hs | 15 +++++++++++++++ .../src/Ide/Plugin/Tactic/Tactics.hs | 16 ++++++++++++++++ .../src/Ide/Plugin/Tactic/TestTypes.hs | 2 ++ 4 files changed, 42 insertions(+) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs index c865f53650..dc368274bf 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs @@ -295,6 +295,15 @@ hyNamesInScope :: Hypothesis a -> Set OccName hyNamesInScope = M.keysSet . hyByName +jHasBoundArgs :: Judgement' a -> Bool +jHasBoundArgs + = not + . null + . filter (isTopLevel . hi_provenance) + . unHypothesis + . jLocalHypothesis + + ------------------------------------------------------------------------------ -- | Fold a hypothesis into a single mapping from name to info. This -- unavoidably will cause duplicate names (things like methods) to shadow one 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 d495bb8d37..6cacb3e54b 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 @@ -3,6 +3,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wall #-} module Ide.Plugin.Tactic.LanguageServer.TacticProviders ( commandProvider @@ -47,6 +48,7 @@ commandTactic Destruct = useNameFromHypothesis destruct commandTactic Homomorphism = useNameFromHypothesis homo commandTactic DestructLambdaCase = const destructLambdaCase commandTactic HomomorphismLambdaCase = const homoLambdaCase +commandTactic DestructAll = const destructAll ------------------------------------------------------------------------------ @@ -71,6 +73,11 @@ commandProvider HomomorphismLambdaCase = requireExtension LambdaCase $ filterGoalType ((== Just True) . lambdaCaseable) $ provide HomomorphismLambdaCase "" +commandProvider DestructAll = + withJudgement $ \jdg -> + case _jIsTopHole jdg && jHasBoundArgs jdg of + True -> provide DestructAll "" + False -> mempty ------------------------------------------------------------------------------ @@ -124,6 +131,14 @@ filterGoalType p tp dflags fs plId uri range jdg = False -> pure [] +------------------------------------------------------------------------------ +-- | Restrict a 'TacticProvider', making sure it appears only when the given +-- predicate holds for the goal. +withJudgement :: (Judgement -> TacticProvider) -> TacticProvider +withJudgement tp dflags fs plId uri range jdg = + tp jdg dflags fs plId uri range jdg + + ------------------------------------------------------------------------------ -- | Multiply a 'TacticProvider' for each binding, making sure it appears only -- when the given predicate holds over the goal and binding types. diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index ae1eda428c..60d16ef9fa 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -234,6 +234,22 @@ splitDataCon dc = Nothing -> throwError $ GoalMismatch "splitDataCon" g +destructAll :: TacticsM () +destructAll = do + jdg <- goal + let args = fmap fst + $ sortOn (Down . snd) + $ mapMaybe (\(hi, prov) -> + case prov of + TopLevelArgPrv _ idx _ -> pure (hi, idx) + _ -> Nothing + ) + $ fmap (\hi -> (hi, hi_provenance hi)) + $ unHypothesis + $ jHypothesis jdg + for_ args destruct + + ------------------------------------------------------------------------------ -- | @matching f@ takes a function from a judgement to a @Tactic@, and -- then applies the resulting @Tactic@. diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs index 970e7b6671..d2a23d22d6 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs @@ -17,6 +17,7 @@ data TacticCommand | Homomorphism | DestructLambdaCase | HomomorphismLambdaCase + | DestructAll deriving (Eq, Ord, Show, Enum, Bounded) -- | Generate a title for the command. @@ -27,6 +28,7 @@ tacticTitle Destruct var = "Case split on " <> var tacticTitle Homomorphism var = "Homomorphic case split on " <> var tacticTitle DestructLambdaCase _ = "Lambda case split" tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split" +tacticTitle DestructAll _ = "Split all function arguments" ------------------------------------------------------------------------------ From 1b347bbc38930ec70ea3ae9ee4227d5322a133ba Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 12:08:18 -0800 Subject: [PATCH 2/4] Don't use guard in IO Missing features were accidentally blocking all code actions --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 2 +- .../src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index 3fb774d4d1..2a6cc9ef41 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -90,7 +90,7 @@ codeActionProvider _ _ _ = pure $ Right $ List [] tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams tacticCmd tac state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - features <- getFeatureSet (shakeExtras state) + features <- getFeatureSet $ shakeExtras state ccs <- getClientCapabilities res <- liftIO $ fromMaybeT (Right Nothing) $ do (range', jdg, ctx, dflags) <- judgementForHole state nfp range features 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 6cacb3e54b..341d462966 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 @@ -107,8 +107,9 @@ data TacticParams = TacticParams -- 'Feature' is in the feature set. requireFeature :: Feature -> TacticProvider -> TacticProvider requireFeature f tp dflags fs plId uri range jdg = do - guard $ hasFeature f fs - tp dflags fs plId uri range jdg + case hasFeature f fs of + True -> tp dflags fs plId uri range jdg + False -> pure [] ------------------------------------------------------------------------------ From 48703bbf232aeff64783174d19670383cdb91ccc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 15:06:02 -0800 Subject: [PATCH 3/4] Write a better provider and add tests --- .../src/Ide/Plugin/Tactic/FeatureSet.hs | 3 +- .../Tactic/LanguageServer/TacticProviders.hs | 9 +++--- plugins/hls-tactics-plugin/test/GoldenSpec.hs | 29 +++++++++++++++++++ .../test/golden/DestructAllAnd.hs | 2 ++ .../test/golden/DestructAllAnd.hs.expected | 5 ++++ .../test/golden/DestructAllMany.hs | 4 +++ .../test/golden/DestructAllMany.hs.expected | 27 +++++++++++++++++ .../test/golden/DestructAllProvider.hs | 12 ++++++++ 8 files changed, 86 insertions(+), 5 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs.expected create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs.expected create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllProvider.hs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs index a5bf4b53c8..ddebabd9d0 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs @@ -21,7 +21,8 @@ import qualified Data.Text as T ------------------------------------------------------------------------------ -- | All the available features. A 'FeatureSet' describes the ones currently -- available to the user. -data Feature = CantHaveAnEmptyDataType +data Feature + = FeatureDestructAll deriving (Eq, Ord, Show, Read, Enum, Bounded) 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 341d462966..686be51baf 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 @@ -74,10 +74,11 @@ commandProvider HomomorphismLambdaCase = filterGoalType ((== Just True) . lambdaCaseable) $ provide HomomorphismLambdaCase "" commandProvider DestructAll = - withJudgement $ \jdg -> - case _jIsTopHole jdg && jHasBoundArgs jdg of - True -> provide DestructAll "" - False -> mempty + requireFeature FeatureDestructAll $ + withJudgement $ \jdg -> + case _jIsTopHole jdg && jHasBoundArgs jdg of + True -> provide DestructAll "" + False -> mempty ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs index 7a8b63e0d8..61f180cd85 100644 --- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs +++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs @@ -73,6 +73,34 @@ spec = do [ (not, DestructLambdaCase, "") ] + + -- test via: + -- stack test hls-tactics-plugin --test-arguments '--match "Golden/destruct all/"' + describe "destruct all" $ do + let destructAllTest = mkGoldenTest allFeatures DestructAll "" + describe "provider" $ do + mkTest + "Requires args on lhs of =" + "DestructAllProvider.hs" 3 21 + [ (not, DestructAll, "") + ] + mkTest + "Can't be a non-top-hole" + "DestructAllProvider.hs" 8 19 + [ (not, DestructAll, "") + , (id, Destruct, "a") + , (id, Destruct, "b") + ] + mkTest + "Provides a destruct all otherwise" + "DestructAllProvider.hs" 12 22 + [ (id, DestructAll, "") + ] + + describe "golden" $ do + destructAllTest "DestructAllAnd.hs" 2 11 + destructAllTest "DestructAllMany.hs" 4 23 + describe "golden tests" $ do let goldenTest = mkGoldenTest allFeatures autoTest = mkGoldenTest allFeatures Auto "" @@ -150,6 +178,7 @@ mkTest -> SpecWith (Arg Bool) mkTest name fp line col ts = it name $ do runSession testCommand fullCaps tacticPath $ do + setFeatureSet allFeatures doc <- openDoc fp "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs new file mode 100644 index 0000000000..892eab679c --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs @@ -0,0 +1,2 @@ +and :: Bool -> Bool -> Bool +and x y = _ diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs.expected b/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs.expected new file mode 100644 index 0000000000..0559503178 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllAnd.hs.expected @@ -0,0 +1,5 @@ +and :: Bool -> Bool -> Bool +and False False = _ +and True False = _ +and False True = _ +and True True = _ diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs new file mode 100644 index 0000000000..ab0a4dccb9 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs @@ -0,0 +1,4 @@ +data ABC = A | B | C + +many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> () +many u e b mabc abc = _ diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs.expected b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs.expected new file mode 100644 index 0000000000..95dd543773 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllMany.hs.expected @@ -0,0 +1,27 @@ +data ABC = A | B | C + +many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> () +many () (Left a) False Nothing A = _ +many () (Right b5) False Nothing A = _ +many () (Left a) True Nothing A = _ +many () (Right b5) True Nothing A = _ +many () (Left a6) False (Just a) A = _ +many () (Right b6) False (Just a) A = _ +many () (Left a6) True (Just a) A = _ +many () (Right b6) True (Just a) A = _ +many () (Left a) False Nothing B = _ +many () (Right b5) False Nothing B = _ +many () (Left a) True Nothing B = _ +many () (Right b5) True Nothing B = _ +many () (Left a6) False (Just a) B = _ +many () (Right b6) False (Just a) B = _ +many () (Left a6) True (Just a) B = _ +many () (Right b6) True (Just a) B = _ +many () (Left a) False Nothing C = _ +many () (Right b5) False Nothing C = _ +many () (Left a) True Nothing C = _ +many () (Right b5) True Nothing C = _ +many () (Left a6) False (Just a) C = _ +many () (Right b6) False (Just a) C = _ +many () (Left a6) True (Just a) C = _ +many () (Right b6) True (Just a) C = _ diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllProvider.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllProvider.hs new file mode 100644 index 0000000000..8d115e828d --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllProvider.hs @@ -0,0 +1,12 @@ +-- we need to name the args ourselves first +nothingToDestruct :: [a] -> [a] -> [a] +nothingToDestruct = _ + + +-- can't destruct all for non-top-level holes +notTop :: Bool -> Bool -> Bool +notTop a b = a && _ + +-- destruct all is ok +canDestructAll :: Bool -> Bool -> Bool +canDestructAll a b = _ From e4d321ce32316cd30b7f63a85e80a0c09d3fe0fc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 15:09:05 -0800 Subject: [PATCH 4/4] Haddock --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs | 2 ++ plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs | 3 +++ 2 files changed, 5 insertions(+) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs index dc368274bf..a691441d86 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs @@ -295,6 +295,8 @@ hyNamesInScope :: Hypothesis a -> Set OccName hyNamesInScope = M.keysSet . hyByName +------------------------------------------------------------------------------ +-- | Are there any top-level function argument bindings in this judgement? jHasBoundArgs :: Judgement' a -> Bool jHasBoundArgs = not diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 60d16ef9fa..8a718bc27f 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -234,6 +234,9 @@ splitDataCon dc = Nothing -> throwError $ GoalMismatch "splitDataCon" g +------------------------------------------------------------------------------ +-- | Perform a case split on each top-level argument. Used to implement the +-- "Destruct all function arguments" action. destructAll :: TacticsM () destructAll = do jdg <- goal