From 425953d5a1ac59477c5f998276b2ee13d6e02214 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 10:26:10 -0800 Subject: [PATCH 1/8] Implement "use constructor" code action --- .../src/Ide/Plugin/Tactic/FeatureSet.hs | 2 +- .../src/Ide/Plugin/Tactic/GHC.hs | 30 +++++++---- .../Tactic/LanguageServer/TacticProviders.hs | 27 ++++++++++ .../src/Ide/Plugin/Tactic/Tactics.hs | 31 ++++++++--- .../src/Ide/Plugin/Tactic/TestTypes.hs | 2 + plugins/hls-tactics-plugin/test/GoldenSpec.hs | 53 +++++++++++++------ .../test/golden/ConProviders.hs | 10 ++++ .../test/golden/UseConLeft.hs | 3 ++ .../test/golden/UseConLeft.hs.expected | 3 ++ .../test/golden/UseConPair.hs | 2 + .../test/golden/UseConPair.hs.expected | 2 + .../test/golden/UseConRight.hs | 3 ++ .../test/golden/UseConRight.hs.expected | 3 ++ 13 files changed, 137 insertions(+), 34 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/ConProviders.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConLeft.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConPair.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConRight.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected 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..394e688f73 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,7 @@ 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 = FeatureUseDataCon deriving (Eq, Ord, Show, Read, Enum, Bounded) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs index b05952b1af..c3f05d9ad7 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs @@ -9,26 +9,25 @@ module Ide.Plugin.Tactic.GHC where +import Control.Arrow import Control.Monad.State -import Data.Function (on) -import Data.List (isPrefixOf) -import qualified Data.Map as M -import Data.Maybe (isJust) -import Data.Set (Set) -import qualified Data.Set as S +import Data.Function (on) +import Data.List (isPrefixOf) +import qualified Data.Map as M +import Data.Maybe (isJust) +import Data.Set (Set) +import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat -import GHC.SourceGen (case', lambda, match) -import Generics.SYB (Data, everything, everywhere, - listify, mkQ, mkT) +import GHC.SourceGen (case', lambda, match) +import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT) import Ide.Plugin.Tactic.Types import OccName import TcType import TyCoRep import Type -import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, - intTyCon) +import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon) import Unique import Var @@ -81,6 +80,12 @@ tacticsThetaTy :: Type -> ThetaType tacticsThetaTy (tcSplitSigmaTy -> (_, theta, _)) = theta +------------------------------------------------------------------------------ +-- | Get the data cons of a type, if it has any. +tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type]) +tacticsGetDataCons = + fmap (first tyConDataCons) . splitTyConApp_maybe + ------------------------------------------------------------------------------ -- | Instantiate all of the quantified type variables in a type with fresh -- skolems. @@ -131,6 +136,9 @@ algebraicTyCon _ = Nothing eqRdrName :: RdrName -> RdrName -> Bool eqRdrName = (==) `on` occNameString . occName +sloppyEqOccName :: OccName -> OccName -> Bool +sloppyEqOccName = (==) `on` occNameString + ------------------------------------------------------------------------------ -- | Does this thing contain any references to 'HsVar's with the given 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..b661e42985 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 @@ -14,12 +15,14 @@ module Ide.Plugin.Tactic.LanguageServer.TacticProviders import Control.Monad import Control.Monad.Error.Class (MonadError (throwError)) import Data.Aeson +import Data.Bool (bool) import Data.Coerce import qualified Data.Map as M import Data.Maybe import Data.Monoid import qualified Data.Text as T import Data.Traversable +import DataCon (dataConName) import Development.IDE.GHC.Compat import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) @@ -47,6 +50,7 @@ commandTactic Destruct = useNameFromHypothesis destruct commandTactic Homomorphism = useNameFromHypothesis homo commandTactic DestructLambdaCase = const destructLambdaCase commandTactic HomomorphismLambdaCase = const homoLambdaCase +commandTactic UseDataCon = userSplit ------------------------------------------------------------------------------ @@ -71,6 +75,22 @@ commandProvider HomomorphismLambdaCase = requireExtension LambdaCase $ filterGoalType ((== Just True) . lambdaCaseable) $ provide HomomorphismLambdaCase "" +commandProvider UseDataCon = + requireFeature FeatureUseDataCon $ + filterTypeProjection + ( guardLength (<= 5) + . fromMaybe [] + . fmap fst + . tacticsGetDataCons + ) $ \dcon -> + provide UseDataCon + . T.pack + . occNameString + . occName + $ dataConName dcon + +guardLength :: (Int -> Bool) -> [a] -> [a] +guardLength f as = bool [] as $ f $ length as ------------------------------------------------------------------------------ @@ -140,6 +160,13 @@ filterBindingType p tp dflags fs plId uri range jdg = True -> tp (hi_name hi) ty dflags fs plId uri range jdg False -> pure [] +filterTypeProjection + :: (Type -> [a]) -- ^ Features of the goal to look into further + -> (a -> TacticProvider) + -> TacticProvider +filterTypeProjection p tp dflags fs plId uri range jdg = + fmap join $ for ( p $ unCType $ jGoal jdg) $ \a -> + tp a dflags fs plId uri range jdg ------------------------------------------------------------------------------ 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..c85b4104f3 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -31,7 +31,7 @@ import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Types -import Name (occNameString) +import Name (occNameString, occName) import Refinery.Tactic import Refinery.Tactic.Internal import TcType @@ -197,10 +197,9 @@ splitAuto :: TacticsM () splitAuto = requireConcreteHole $ tracing "split(auto)" $ do jdg <- goal let g = jGoal jdg - case splitTyConApp_maybe $ unCType g of + case tacticsGetDataCons $ unCType g of Nothing -> throwError $ GoalMismatch "split" g - Just (tc, _) -> do - let dcs = tyConDataCons tc + Just (dcs, _) -> do case isSplitWhitelisted jdg of True -> choice $ fmap splitDataCon dcs False -> do @@ -222,18 +221,36 @@ requireNewHoles m = do ------------------------------------------------------------------------------ -- | Attempt to instantiate the given data constructor to solve the goal. +-- +-- INVARIANT: Assumes the give datacon is appropriate to construct the type +-- with. splitDataCon :: DataCon -> TacticsM () splitDataCon dc = requireConcreteHole $ tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do let g = jGoal jdg case splitTyConApp_maybe $ unCType g of Just (tc, apps) -> do - case elem dc $ tyConDataCons tc of - True -> buildDataCon (unwhitelistingSplit jdg) dc apps - False -> throwError $ IncorrectDataCon dc + buildDataCon (unwhitelistingSplit jdg) dc apps Nothing -> throwError $ GoalMismatch "splitDataCon" g +------------------------------------------------------------------------------ +-- | User-facing tactic to implement "Use constructor " +userSplit :: OccName -> TacticsM () +userSplit occ = do + jdg <- goal + let g = jGoal jdg + -- TODO(sandy): It's smelly that we need to find the datacon to generate the + -- code action, send it as a string, and then look it up again. Can we push + -- this over LSP somehow instead? + case splitTyConApp_maybe $ unCType g of + Just (tc, apps) -> do + case find (sloppyEqOccName occ . occName . dataConName) + $ tyConDataCons tc of + Just dc -> splitDataCon dc + Nothing -> throwError $ NotInScope occ + + ------------------------------------------------------------------------------ -- | @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..641c1b1d28 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 + | UseDataCon 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 UseDataCon dcon = "Use constructor " <> dcon ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs index 7a8b63e0d8..d3082831b7 100644 --- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs +++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs @@ -8,26 +8,24 @@ module GoldenSpec where import Control.Applicative.Combinators (skipManyTill) -import Control.Lens hiding (failing, (<.>)) -import Control.Monad (unless) +import Control.Lens hiding (failing, (<.>)) +import Control.Monad (unless) import Control.Monad.IO.Class import Data.Aeson -import Data.Default (Default (def)) +import Data.Default (Default (def)) import Data.Foldable -import qualified Data.Map as M +import qualified Data.Map as M import Data.Maybe -import Data.Text (Text) -import qualified Data.Text.IO as T -import qualified Ide.Plugin.Config as Plugin -import Ide.Plugin.Tactic.FeatureSet (FeatureSet, allFeatures) +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text.IO as T +import qualified Ide.Plugin.Config as Plugin +import Ide.Plugin.Tactic.FeatureSet (FeatureSet, allFeatures) import Ide.Plugin.Tactic.TestTypes import Language.LSP.Test import Language.LSP.Types -import Language.LSP.Types.Lens hiding (actions, applyEdit, - capabilities, executeCommand, - id, line, message, name, - rename, title) -import System.Directory (doesFileExist) +import Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title) +import System.Directory (doesFileExist) import System.FilePath import Test.Hspec @@ -73,9 +71,33 @@ spec = do [ (not, DestructLambdaCase, "") ] + let goldenTest = mkGoldenTest allFeatures + + describe "use constructor" $ do + let useTest = mkGoldenTest allFeatures UseDataCon + describe "provider" $ do + mkTest + "Suggests all data cons for Either" + "ConProviders.hs" 3 6 + [ (id, UseDataCon, "Left") + , (id, UseDataCon, "Right") + , (not, UseDataCon, ":") + , (not, UseDataCon, "[]") + , (not, UseDataCon, "C1") + ] + mkTest + "Suggests no data cons for big types" + "ConProviders.hs" 9 17 $ do + c <- [1 :: Int .. 10] + pure $ (not, UseDataCon, T.pack $ show c) + + describe "golden" $ do + useTest "(,)" "UseConPair.hs" 2 8 + useTest "Left" "UseConLeft.hs" 2 8 + useTest "Right" "UseConRight.hs" 2 8 + describe "golden tests" $ do - let goldenTest = mkGoldenTest allFeatures - autoTest = mkGoldenTest allFeatures Auto "" + let autoTest = mkGoldenTest allFeatures Auto "" goldenTest Intros "" "GoldenIntros.hs" 2 8 autoTest "GoldenEitherAuto.hs" 2 11 @@ -150,6 +172,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/ConProviders.hs b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs new file mode 100644 index 0000000000..d3124fecd5 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs @@ -0,0 +1,10 @@ +-- Should suggest Left and Right, but not [] +t1 :: Either a b +t1 = _ + + +data ManyConstructors = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10 + +noCtorsIfMany :: ManyConstructors +noCtorsIfMany = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs new file mode 100644 index 0000000000..59d03ae7d0 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs @@ -0,0 +1,3 @@ +test :: Either a b +test = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected new file mode 100644 index 0000000000..cd04697d6a --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected @@ -0,0 +1,3 @@ +test :: Either a b +test = Left _ + diff --git a/plugins/hls-tactics-plugin/test/golden/UseConPair.hs b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs new file mode 100644 index 0000000000..2d15fe3500 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs @@ -0,0 +1,2 @@ +test :: (a, b) +test = _ diff --git a/plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected new file mode 100644 index 0000000000..130c3dd7c9 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected @@ -0,0 +1,2 @@ +test :: (a, b) +test = (_, _) diff --git a/plugins/hls-tactics-plugin/test/golden/UseConRight.hs b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs new file mode 100644 index 0000000000..59d03ae7d0 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs @@ -0,0 +1,3 @@ +test :: Either a b +test = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected new file mode 100644 index 0000000000..beaecf28c5 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected @@ -0,0 +1,3 @@ +test :: Either a b +test = Right _ + From 82cdc8babebb075f37a705669c00e68b572dcca2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 10:33:34 -0800 Subject: [PATCH 2/8] Haddock --- .../hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs | 7 +++++-- .../Plugin/Tactic/LanguageServer/TacticProviders.hs | 10 ++++++++-- plugins/hls-tactics-plugin/test/GoldenSpec.hs | 2 ++ 3 files changed, 15 insertions(+), 4 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs index c3f05d9ad7..f385d6085a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs @@ -131,11 +131,14 @@ algebraicTyCon _ = Nothing ------------------------------------------------------------------------------ --- | We can't compare 'RdrName' for equality directly. Instead, compare them by --- their 'OccName's. +-- | We can't compare 'RdrName' for equality directly. Instead, sloppily +-- compare them by their 'OccName's. eqRdrName :: RdrName -> RdrName -> Bool eqRdrName = (==) `on` occNameString . occName + +------------------------------------------------------------------------------ +-- | Compare two 'OccName's for unqualified equality. sloppyEqOccName :: OccName -> OccName -> Bool sloppyEqOccName = (==) `on` occNameString 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 b661e42985..db08508940 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 @@ -89,6 +89,9 @@ commandProvider UseDataCon = . occName $ dataConName dcon + +------------------------------------------------------------------------------ +-- | Return an empty list if the given predicate doesn't hold over the length guardLength :: (Int -> Bool) -> [a] -> [a] guardLength f as = bool [] as $ f $ length as @@ -160,12 +163,16 @@ filterBindingType p tp dflags fs plId uri range jdg = True -> tp (hi_name hi) ty dflags fs plId uri range jdg False -> pure [] + +------------------------------------------------------------------------------ +-- | Multiply a 'TacticProvider' by some feature projection out of the goal +-- type. Used e.g. to crete a code action for every data constructor. filterTypeProjection :: (Type -> [a]) -- ^ Features of the goal to look into further -> (a -> TacticProvider) -> TacticProvider filterTypeProjection p tp dflags fs plId uri range jdg = - fmap join $ for ( p $ unCType $ jGoal jdg) $ \a -> + fmap join $ for (p $ unCType $ jGoal jdg) $ \a -> tp a dflags fs plId uri range jdg @@ -201,7 +208,6 @@ tcCommandId :: TacticCommand -> CommandId tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" - ------------------------------------------------------------------------------ -- | We should show homos only when the goal type is the same as the binding -- type, and that both are usual algebraic types. diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs index d3082831b7..9b4a8ca119 100644 --- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs +++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs @@ -73,6 +73,8 @@ spec = do let goldenTest = mkGoldenTest allFeatures + -- test via: + -- stack test hls-tactics-plugin --test-arguments '--match "Golden/use constructor/"' describe "use constructor" $ do let useTest = mkGoldenTest allFeatures UseDataCon describe "provider" $ do From b73cf83e06117fd666917b78dd4fa38ee52a37a0 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 11:04:42 -0800 Subject: [PATCH 3/8] Make use ctor actions configurable --- .../src/Ide/Plugin/Tactic.hs | 30 +++++----- .../src/Ide/Plugin/Tactic/LanguageServer.hs | 18 ++++-- .../Tactic/LanguageServer/TacticProviders.hs | 56 +++++++++++-------- .../src/Ide/Plugin/Tactic/TestTypes.hs | 18 +++--- 4 files changed, 69 insertions(+), 53 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..5a0a8e0156 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -13,30 +13,28 @@ module Ide.Plugin.Tactic , TacticCommand (..) ) where -import Bag (bagToList, - listToBag) -import Control.Exception (evaluate) +import Bag (bagToList, listToBag) +import Control.Exception (evaluate) import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.Aeson -import Data.Bifunctor (Bifunctor (bimap)) -import Data.Bool (bool) -import Data.Data (Data) +import Data.Bifunctor (Bifunctor (bimap)) +import Data.Bool (bool) +import Data.Data (Data) import Data.Foldable (for_) -import Data.Generics.Aliases (mkQ) -import Data.Generics.Schemes (everything) +import Data.Generics.Aliases (mkQ) +import Data.Generics.Schemes (everything) import Data.Maybe import Data.Monoid -import qualified Data.Text as T +import qualified Data.Text as T import Data.Traversable -import Development.IDE.Core.Shake (IdeState (..)) +import Development.IDE.Core.Shake (IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.ExactPrint import Development.Shake.Classes import Ide.Plugin.Tactic.CaseSplit -import Ide.Plugin.Tactic.FeatureSet (Feature (..), - hasFeature) +import Ide.Plugin.Tactic.FeatureSet (Feature (..), hasFeature) import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.LanguageServer import Ide.Plugin.Tactic.LanguageServer.TacticProviders @@ -49,7 +47,7 @@ import Language.LSP.Server import Language.LSP.Types import Language.LSP.Types.Capabilities import OccName -import Prelude hiding (span) +import Prelude hiding (span) import System.Timeout @@ -71,14 +69,14 @@ descriptor plId = (defaultPluginDescriptor plId) codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - features <- getFeatureSet (shakeExtras state) + cfg <- getTacticConfig $ shakeExtras state liftIO $ fromMaybeT (Right $ List []) $ do - (_, jdg, _, dflags) <- judgementForHole state nfp range features + (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider [minBound .. maxBound] dflags - features + cfg plId uri range 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 4fcbdabd5a..bd8c5e8038 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -44,7 +44,7 @@ import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.TestTypes (TacticCommand, - cfg_feature_set) + cfg_feature_set, emptyConfig, Config) import Ide.Plugin.Tactic.Types import Language.LSP.Server (MonadLsp) import Language.LSP.Types @@ -82,13 +82,19 @@ runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp ------------------------------------------------------------------------------ --- | Get the current feature set from the plugin config. -getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet -getFeatureSet extras = do +-- | Get the the plugin config +getTacticConfig :: MonadLsp Plugin.Config m => ShakeExtras -> m Config +getTacticConfig extras = do pcfg <- getPluginConfig extras "tactics" pure $ case fromJSON $ Object $ plcConfig pcfg of - Success cfg -> cfg_feature_set cfg - Error _ -> defaultFeatures + Success cfg -> cfg + Error _ -> emptyConfig + + +------------------------------------------------------------------------------ +-- | Get the current feature set from the plugin config. +getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet +getFeatureSet = fmap cfg_feature_set . getTacticConfig getIdeDynflags 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 db08508940..140be14eee 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 @@ -76,18 +76,19 @@ commandProvider HomomorphismLambdaCase = filterGoalType ((== Just True) . lambdaCaseable) $ provide HomomorphismLambdaCase "" commandProvider UseDataCon = - requireFeature FeatureUseDataCon $ - filterTypeProjection - ( guardLength (<= 5) - . fromMaybe [] - . fmap fst - . tacticsGetDataCons - ) $ \dcon -> - provide UseDataCon - . T.pack - . occNameString - . occName - $ dataConName dcon + withConfig $ \cfg -> + requireFeature FeatureUseDataCon $ + filterTypeProjection + ( guardLength (<= cfg_max_use_ctor_actions cfg) + . fromMaybe [] + . fmap fst + . tacticsGetDataCons + ) $ \dcon -> + provide UseDataCon + . T.pack + . occNameString + . occName + $ dataConName dcon ------------------------------------------------------------------------------ @@ -101,7 +102,7 @@ guardLength f as = bool [] as $ f $ length as -- UI. type TacticProvider = DynFlags - -> FeatureSet + -> Config -> PluginId -> Uri -> Range @@ -122,18 +123,18 @@ data TacticParams = TacticParams -- | Restrict a 'TacticProvider', making sure it appears only when the given -- '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 +requireFeature f tp dflags cfg plId uri range jdg = do + guard $ hasFeature f $ cfg_feature_set cfg + tp dflags cfg plId uri range jdg ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. requireExtension :: Extension -> TacticProvider -> TacticProvider -requireExtension ext tp dflags fs plId uri range jdg = +requireExtension ext tp dflags cfg plId uri range jdg = case xopt ext dflags of - True -> tp dflags fs plId uri range jdg + True -> tp dflags cfg plId uri range jdg False -> pure [] @@ -141,9 +142,9 @@ requireExtension ext tp dflags fs plId uri range jdg = -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider -filterGoalType p tp dflags fs plId uri range jdg = +filterGoalType p tp dflags cfg plId uri range jdg = case p $ unCType $ jGoal jdg of - True -> tp dflags fs plId uri range jdg + True -> tp dflags cfg plId uri range jdg False -> pure [] @@ -154,13 +155,13 @@ filterBindingType :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider -filterBindingType p tp dflags fs plId uri range jdg = +filterBindingType p tp dflags cfg plId uri range jdg = let hy = jHypothesis jdg g = jGoal jdg in fmap join $ for (unHypothesis hy) $ \hi -> let ty = unCType $ hi_type hi in case p (unCType g) ty of - True -> tp (hi_name hi) ty dflags fs plId uri range jdg + True -> tp (hi_name hi) ty dflags cfg plId uri range jdg False -> pure [] @@ -171,9 +172,16 @@ filterTypeProjection :: (Type -> [a]) -- ^ Features of the goal to look into further -> (a -> TacticProvider) -> TacticProvider -filterTypeProjection p tp dflags fs plId uri range jdg = +filterTypeProjection p tp dflags cfg plId uri range jdg = fmap join $ for (p $ unCType $ jGoal jdg) $ \a -> - tp a dflags fs plId uri range jdg + tp a dflags cfg plId uri range jdg + + +------------------------------------------------------------------------------ +-- | Get access to the 'Config' when building a 'TacticProvider'. +withConfig :: (Config -> TacticProvider) -> TacticProvider +withConfig tp dflags cfg plId uri range jdg = tp cfg dflags cfg plId uri range jdg + ------------------------------------------------------------------------------ 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 641c1b1d28..fa97f1b9c9 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} module Ide.Plugin.Tactic.TestTypes where @@ -33,20 +34,23 @@ tacticTitle UseDataCon dcon = "Use constructor " <> dcon ------------------------------------------------------------------------------ -- | Plugin configuration for tactics -newtype Config = Config - { cfg_feature_set :: FeatureSet +data Config = Config + { cfg_feature_set :: FeatureSet + , cfg_max_use_ctor_actions :: Int } emptyConfig :: Config -emptyConfig = Config defaultFeatures +emptyConfig = Config defaultFeatures 5 instance ToJSON Config where - toJSON (Config features) = object - [ "features" .= prettyFeatureSet features + toJSON Config{..} = object + [ "features" .= prettyFeatureSet cfg_feature_set + , "max_use_ctor_actions" .= cfg_max_use_ctor_actions ] instance FromJSON Config where parseJSON = withObject "Config" $ \obj -> do - features <- parseFeatureSet <$> obj .: "features" - pure $ Config features + cfg_feature_set <- parseFeatureSet <$> obj .: "features" + cfg_max_use_ctor_actions <- obj .: "max_use_ctor_actions" + pure $ Config{..} From 9c20a3ab0b983787942de40e9228f4a2012455e1 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 11:07:54 -0800 Subject: [PATCH 4/8] Undo more stupid formatting --- .../Plugin/Tactic/LanguageServer/TacticProviders.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 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 140be14eee..905bf43ecb 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 @@ -13,19 +13,19 @@ module Ide.Plugin.Tactic.LanguageServer.TacticProviders ) where import Control.Monad -import Control.Monad.Error.Class (MonadError (throwError)) +import Control.Monad.Error.Class (MonadError (throwError)) import Data.Aeson import Data.Bool (bool) import Data.Coerce -import qualified Data.Map as M +import qualified Data.Map as M import Data.Maybe import Data.Monoid -import qualified Data.Text as T +import qualified Data.Text as T import Data.Traversable import DataCon (dataConName) import Development.IDE.GHC.Compat import GHC.Generics -import GHC.LanguageExtensions.Type (Extension (LambdaCase)) +import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Plugin.Tactic.Auto import Ide.Plugin.Tactic.FeatureSet import Ide.Plugin.Tactic.GHC @@ -37,8 +37,8 @@ import Ide.PluginUtils import Ide.Types import Language.LSP.Types import OccName -import Prelude hiding (span) -import Refinery.Tactic (goal) +import Prelude hiding (span) +import Refinery.Tactic (goal) ------------------------------------------------------------------------------ From 557432e311e6541a704d6d5410f8d6c4de3c0974 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 11:21:03 -0800 Subject: [PATCH 5/8] Use loose parsing for config --- .../hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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 fa97f1b9c9..219731fbc2 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs @@ -4,6 +4,7 @@ module Ide.Plugin.Tactic.TestTypes where import Data.Aeson +import Data.Maybe (fromMaybe) import qualified Data.Text as T import Ide.Plugin.Tactic.FeatureSet @@ -50,7 +51,9 @@ instance ToJSON Config where instance FromJSON Config where parseJSON = withObject "Config" $ \obj -> do - cfg_feature_set <- parseFeatureSet <$> obj .: "features" - cfg_max_use_ctor_actions <- obj .: "max_use_ctor_actions" + cfg_feature_set <- + parseFeatureSet . fromMaybe "" <$> obj .:? "features" + cfg_max_use_ctor_actions <- + fromMaybe 5 <$> obj .:? "max_use_ctor_actions" pure $ Config{..} From 3d79859f22e6bee41bd6a31e3f7d6bcfcc0b2d10 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 11:30:58 -0800 Subject: [PATCH 6/8] Only show unifiable ctors --- .../Tactic/LanguageServer/TacticProviders.hs | 17 +++++++++++++---- plugins/hls-tactics-plugin/test/GoldenSpec.hs | 11 +++++++++-- .../test/golden/ConProviders.hs | 11 +++++++++++ 3 files changed, 33 insertions(+), 6 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 905bf43ecb..3cd9460cd6 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 @@ -22,7 +22,7 @@ import Data.Maybe import Data.Monoid import qualified Data.Text as T import Data.Traversable -import DataCon (dataConName) +import DataCon (dataConName, dataConCannotMatch) import Development.IDE.GHC.Compat import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) @@ -80,9 +80,7 @@ commandProvider UseDataCon = requireFeature FeatureUseDataCon $ filterTypeProjection ( guardLength (<= cfg_max_use_ctor_actions cfg) - . fromMaybe [] - . fmap fst - . tacticsGetDataCons + . useCtorFilter ) $ \dcon -> provide UseDataCon . T.pack @@ -231,3 +229,14 @@ destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _ = False + +------------------------------------------------------------------------------ +-- | Only show data cons in "Use constructor" if they can unify with the goal +useCtorFilter :: Type -> [DataCon] +useCtorFilter ty + | Just (dcs, apps) <- tacticsGetDataCons ty = do + dc <- dcs + guard $ not $ dataConCannotMatch apps dc + pure dc +useCtorFilter _ = [] + diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs index 9b4a8ca119..5e3fd4b9e5 100644 --- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs +++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs @@ -80,7 +80,7 @@ spec = do describe "provider" $ do mkTest "Suggests all data cons for Either" - "ConProviders.hs" 3 6 + "ConProviders.hs" 5 6 [ (id, UseDataCon, "Left") , (id, UseDataCon, "Right") , (not, UseDataCon, ":") @@ -89,9 +89,16 @@ spec = do ] mkTest "Suggests no data cons for big types" - "ConProviders.hs" 9 17 $ do + "ConProviders.hs" 11 17 $ do c <- [1 :: Int .. 10] pure $ (not, UseDataCon, T.pack $ show c) + mkTest + "Suggests only matching data cons for GADT" + "ConProviders.hs" 20 12 + [ (id, UseDataCon, "IntGADT") + , (id, UseDataCon, "VarGADT") + , (not, UseDataCon, "BoolGADT") + ] describe "golden" $ do useTest "(,)" "UseConPair.hs" 2 8 diff --git a/plugins/hls-tactics-plugin/test/golden/ConProviders.hs b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs index d3124fecd5..19dbc3c6e5 100644 --- a/plugins/hls-tactics-plugin/test/golden/ConProviders.hs +++ b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE GADTs #-} + -- Should suggest Left and Right, but not [] t1 :: Either a b t1 = _ @@ -8,3 +10,12 @@ data ManyConstructors = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10 noCtorsIfMany :: ManyConstructors noCtorsIfMany = _ + +data GADT a where + IntGADT :: GADT Int + BoolGADT :: GADT Bool + VarGADT :: GADT a + +gadtCtor :: GADT Int +gadtCtor = _ + From 94c02b374cc533163b16b0d7f05cf3eaa88db98e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 12:08:18 -0800 Subject: [PATCH 7/8] 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 5a0a8e0156..011315dd8b 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -88,7 +88,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 3cd9460cd6..ea2399e571 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 @@ -122,8 +122,9 @@ data TacticParams = TacticParams -- 'Feature' is in the feature set. requireFeature :: Feature -> TacticProvider -> TacticProvider requireFeature f tp dflags cfg plId uri range jdg = do - guard $ hasFeature f $ cfg_feature_set cfg - tp dflags cfg plId uri range jdg + case hasFeature f $ cfg_feature_set cfg of + True -> tp dflags cfg plId uri range jdg + False -> pure [] ------------------------------------------------------------------------------ From 277bb649b5ba1b2486f64e3ed1da5f94d69938db Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 28 Feb 2021 12:50:54 -0800 Subject: [PATCH 8/8] Push data con matching into tacticsGetDataCons --- .../src/Ide/Plugin/Tactic/GHC.hs | 8 ++++++-- .../Tactic/LanguageServer/TacticProviders.hs | 17 ++++------------- 2 files changed, 10 insertions(+), 15 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs index f385d6085a..e5644cebae 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs @@ -30,6 +30,7 @@ import Type import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon) import Unique import Var +import Data.Functor ((<&>)) tcTyVar_maybe :: Type -> Maybe Var @@ -83,8 +84,11 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta, _)) = theta ------------------------------------------------------------------------------ -- | Get the data cons of a type, if it has any. tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type]) -tacticsGetDataCons = - fmap (first tyConDataCons) . splitTyConApp_maybe +tacticsGetDataCons ty = + splitTyConApp_maybe ty <&> \(tc, apps) -> + ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc + , apps + ) ------------------------------------------------------------------------------ -- | Instantiate all of the quantified type variables in a type with fresh 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 ea2399e571..d082e4441f 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 @@ -22,7 +22,7 @@ import Data.Maybe import Data.Monoid import qualified Data.Text as T import Data.Traversable -import DataCon (dataConName, dataConCannotMatch) +import DataCon (dataConName) import Development.IDE.GHC.Compat import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) @@ -80,7 +80,9 @@ commandProvider UseDataCon = requireFeature FeatureUseDataCon $ filterTypeProjection ( guardLength (<= cfg_max_use_ctor_actions cfg) - . useCtorFilter + . fromMaybe [] + . fmap fst + . tacticsGetDataCons ) $ \dcon -> provide UseDataCon . T.pack @@ -230,14 +232,3 @@ destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _ = False - ------------------------------------------------------------------------------- --- | Only show data cons in "Use constructor" if they can unify with the goal -useCtorFilter :: Type -> [DataCon] -useCtorFilter ty - | Just (dcs, apps) <- tacticsGetDataCons ty = do - dc <- dcs - guard $ not $ dataConCannotMatch apps dc - pure dc -useCtorFilter _ = [] -