From ff9a18208ce4d621d6acb90426d0b5f5cf2f6d52 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 19 Feb 2021 11:02:57 -0800 Subject: [PATCH] Implement Tactic Featuresets (#1398) * Implement featuresets * Make Tactics tests run with a full feature set * Respond to feedback from @wz1000 * Cleanup imports in Types Co-authored-by: Javier Neira Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- haskell-language-server.cabal | 1 + .../hls-tactics-plugin.cabal | 1 + .../src/Ide/Plugin/Tactic.hs | 10 +- .../src/Ide/Plugin/Tactic/Context.hs | 8 +- .../src/Ide/Plugin/Tactic/FeatureSet.hs | 92 +++++++++++++++++++ .../src/Ide/Plugin/Tactic/LanguageServer.hs | 32 +++++-- .../Tactic/LanguageServer/TacticProviders.hs | 27 ++++-- .../src/Ide/Plugin/Tactic/TestTypes.hs | 23 +++++ .../src/Ide/Plugin/Tactic/Types.hs | 14 +-- test/functional/Tactic.hs | 26 +++++- 10 files changed, 206 insertions(+), 28 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 8f9e89bf4b..3104936787 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -462,6 +462,7 @@ test-suite func-test Splice HaddockComments Ide.Plugin.Splice.Types + Ide.Plugin.Tactic.FeatureSet Ide.Plugin.Tactic.TestTypes Ide.Plugin.Eval.Types diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index 1712df5dd2..04e4038877 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -29,6 +29,7 @@ library Ide.Plugin.Tactic.CodeGen.Utils Ide.Plugin.Tactic.Context Ide.Plugin.Tactic.Debug + Ide.Plugin.Tactic.FeatureSet Ide.Plugin.Tactic.GHC Ide.Plugin.Tactic.Judgements Ide.Plugin.Tactic.KnownStrategies diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index e17d3c727e..eff9e5efab 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -33,6 +33,7 @@ import Development.IDE.GHC.Compat import Development.IDE.GHC.ExactPrint import Development.Shake.Classes import Ide.Plugin.Tactic.CaseSplit +import Ide.Plugin.Tactic.FeatureSet (hasFeature, Feature (..)) import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.LanguageServer import Ide.Plugin.Tactic.LanguageServer.TacticProviders @@ -66,13 +67,15 @@ descriptor plId = (defaultPluginDescriptor plId) codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + features <- getFeatureSet liftIO $ fromMaybeT (Right $ List []) $ do - (_, jdg, _, dflags) <- judgementForHole state nfp range + (_, jdg, _, dflags) <- judgementForHole state nfp range features actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider [minBound .. maxBound] dflags + features plId uri range @@ -84,9 +87,10 @@ 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 ccs <- getClientCapabilities res <- liftIO $ fromMaybeT (Right Nothing) $ do - (range', jdg, ctx, dflags) <- judgementForHole state nfp range + (range', jdg, ctx, dflags) <- judgementForHole state nfp range features let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs index ad5f937f6f..c67ec8c7bc 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs @@ -7,8 +7,6 @@ import Bag import Control.Arrow import Control.Monad.Reader import Data.List -import Data.Map (Map) -import qualified Data.Map as M import Data.Maybe (mapMaybe) import Data.Set (Set) import qualified Data.Set as S @@ -20,16 +18,18 @@ import OccName import TcRnTypes import TcType (substTy, tcSplitSigmaTy) import Unify (tcUnifyTy) +import Ide.Plugin.Tactic.FeatureSet (FeatureSet) -mkContext :: [(OccName, CType)] -> TcGblEnv -> Context -mkContext locals tcg = Context +mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context +mkContext features locals tcg = Context { ctxDefiningFuncs = locals , ctxModuleFuncs = fmap splitId . (getFunBindId =<<) . fmap unLoc . bagToList $ tcg_binds tcg + , ctxFeatureSet = features } diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs new file mode 100644 index 0000000000..96008a4778 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.FeatureSet + ( Feature (..) + , FeatureSet + , hasFeature + , defaultFeatures + , allFeatures + , parseFeatureSet + , prettyFeatureSet + ) where + +import Data.List (intercalate) +import Data.Maybe (mapMaybe, listToMaybe) +import Data.Set (Set) +import qualified Data.Set as S +import qualified Data.Text as T + + +------------------------------------------------------------------------------ +-- | All the available features. A 'FeatureSet' describes the ones currently +-- available to the user. +data Feature = CantHaveAnEmptyDataType + deriving (Eq, Ord, Show, Read, Enum, Bounded) + + +------------------------------------------------------------------------------ +-- | A collection of enabled features. +type FeatureSet = Set Feature + + +------------------------------------------------------------------------------ +-- | Parse a feature set. +parseFeatureSet :: T.Text -> FeatureSet +parseFeatureSet + = mappend defaultFeatures + . S.fromList + . mapMaybe (readMaybe . mappend featurePrefix . rot13 . T.unpack) + . T.split (== '/') + + +------------------------------------------------------------------------------ +-- | Features that are globally enabled for all users. +defaultFeatures :: FeatureSet +defaultFeatures = S.fromList + [ + ] + + +------------------------------------------------------------------------------ +-- | All available features. +allFeatures :: FeatureSet +allFeatures = S.fromList $ enumFromTo minBound maxBound + + +------------------------------------------------------------------------------ +-- | Pretty print a feature set. +prettyFeatureSet :: FeatureSet -> String +prettyFeatureSet + = intercalate "/" + . fmap (rot13 . drop (length featurePrefix) . show) + . S.toList + + +------------------------------------------------------------------------------ +-- | Is a given 'Feature' currently enabled? +hasFeature :: Feature -> FeatureSet -> Bool +hasFeature = S.member + + +------------------------------------------------------------------------------ +-- | Like 'read', but not partial. +readMaybe :: Read a => String -> Maybe a +readMaybe = fmap fst . listToMaybe . reads + + +featurePrefix :: String +featurePrefix = "Feature" + + +rot13 :: String -> String +rot13 = fmap (toEnum . rot13int . fromEnum) + + +rot13int :: Integral a => a -> a +rot13int x + | (fromIntegral x :: Word) - 97 < 26 = 97 + rem (x - 84) 26 + | (fromIntegral x :: Word) - 65 < 26 = 65 + rem (x - 52) 26 + | otherwise = x + 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 d130410091..c81ccf549d 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} @@ -8,6 +9,8 @@ module Ide.Plugin.Tactic.LanguageServer where import Control.Arrow import Control.Monad import Control.Monad.Trans.Maybe +import Data.Aeson (Value(Object), fromJSON) +import Data.Aeson.Types (Result(Success, Error)) import Data.Coerce import Data.Functor ((<&>)) import Data.Generics.Aliases (mkQ) @@ -29,12 +32,17 @@ import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi import Development.Shake (RuleResult, Action) import Development.Shake.Classes import qualified FastString +import Ide.Plugin.Config (PluginConfig(plcConfig)) +import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Tactic.Context +import Ide.Plugin.Tactic.FeatureSet import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range -import Ide.Plugin.Tactic.TestTypes (TacticCommand) +import Ide.Plugin.Tactic.TestTypes (cfg_feature_set, TacticCommand) import Ide.Plugin.Tactic.Types +import Ide.PluginUtils (getPluginConfig) +import Language.LSP.Server (MonadLsp) import Language.LSP.Types import OccName import Prelude hiding (span) @@ -69,6 +77,16 @@ runStaleIde runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp +------------------------------------------------------------------------------ +-- | Get the current feature set from the plugin config. +getFeatureSet :: MonadLsp Plugin.Config m => m FeatureSet +getFeatureSet = do + pcfg <- getPluginConfig "tactics" + pure $ case fromJSON $ Object $ plcConfig pcfg of + Success cfg -> cfg_feature_set cfg + Error _ -> defaultFeatures + + getIdeDynflags :: IdeState -> NormalizedFilePath @@ -87,8 +105,9 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range + -> FeatureSet -> MaybeT IO (Range, Judgement, Context, DynFlags) -judgementForHole state nfp range = do +judgementForHole state nfp range features = do (asts, amapping) <- runStaleIde state nfp GetHieAst case asts of HAR _ _ _ _ (HieFromDisk _) -> fail "Need a fresh hie file" @@ -97,21 +116,22 @@ judgementForHole state nfp range = do (tcmod, _) <- runStaleIde state nfp TypeCheck (rss, g) <- liftMaybe $ getSpanAndTypeAtHole amapping range hf resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss - let (jdg, ctx) = mkJudgementAndContext g binds rss tcmod + let (jdg, ctx) = mkJudgementAndContext features g binds rss tcmod dflags <- getIdeDynflags state nfp pure (resulting_range, jdg, ctx, dflags) mkJudgementAndContext - :: Type + :: FeatureSet + -> Type -> Bindings -> RealSrcSpan -> TcModuleResult -> (Judgement, Context) -mkJudgementAndContext g binds rss tcmod = do +mkJudgementAndContext features g binds rss tcmod = do let tcg = tmrTypechecked tcmod tcs = tcg_binds tcg - ctx = mkContext + ctx = mkContext features (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings binds rss) tcg 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 c66c4d7bd7..f564df2ba2 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 @@ -21,9 +21,10 @@ import Data.Monoid import qualified Data.Text as T import Data.Traversable import Development.IDE.GHC.Compat -import GHC.Generics (Generic) +import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Plugin.Tactic.Auto +import Ide.Plugin.Tactic.FeatureSet import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Tactics @@ -77,6 +78,7 @@ commandProvider HomomorphismLambdaCase = -- UI. type TacticProvider = DynFlags + -> FeatureSet -> PluginId -> Uri -> Range @@ -93,13 +95,22 @@ data TacticParams = TacticParams deriving anyclass (ToJSON, FromJSON) +------------------------------------------------------------------------------ +-- | 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 + + ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. requireExtension :: Extension -> TacticProvider -> TacticProvider -requireExtension ext tp dflags plId uri range jdg = +requireExtension ext tp dflags fs plId uri range jdg = case xopt ext dflags of - True -> tp dflags plId uri range jdg + True -> tp dflags fs plId uri range jdg False -> pure [] @@ -107,9 +118,9 @@ requireExtension ext tp dflags 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 plId uri range jdg = +filterGoalType p tp dflags fs plId uri range jdg = case p $ unCType $ jGoal jdg of - True -> tp dflags plId uri range jdg + True -> tp dflags fs plId uri range jdg False -> pure [] @@ -120,13 +131,13 @@ filterBindingType :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider -filterBindingType p tp dflags plId uri range jdg = +filterBindingType p tp dflags fs 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 plId uri range jdg + True -> tp (hi_name hi) ty dflags fs plId uri range jdg False -> pure [] @@ -146,7 +157,7 @@ useNameFromHypothesis f name = do -- | Terminal constructor for providing context-sensitive tactics. Tactics -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider -provide tc name _ plId uri range _ = do +provide tc name _ _ plId uri range _ = do let title = tacticTitle tc name params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name } cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params]) 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 2ea4b8d06c..972ac4a35b 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs @@ -3,6 +3,8 @@ module Ide.Plugin.Tactic.TestTypes where import qualified Data.Text as T +import Data.Aeson +import Ide.Plugin.Tactic.FeatureSet ------------------------------------------------------------------------------ -- | The list of tactics exposed to the outside world. These are attached to @@ -25,3 +27,24 @@ 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" + + +------------------------------------------------------------------------------ +-- | Plugin configuration for tactics +newtype Config = Config + { cfg_feature_set :: FeatureSet + } + +emptyConfig :: Config +emptyConfig = Config defaultFeatures + +instance ToJSON Config where + toJSON (Config features) = object + [ "features" .= prettyFeatureSet features + ] + +instance FromJSON Config where + parseJSON = withObject "Config" $ \obj -> do + features <- parseFeatureSet <$> obj .: "features" + pure $ Config features + diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index c9744bab78..413b0f69b7 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -1,11 +1,12 @@ -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Ide.Plugin.Tactic.Types @@ -19,13 +20,12 @@ module Ide.Plugin.Tactic.Types , Range ) where -import Control.Lens hiding (Context) +import Control.Lens hiding (Context, (.=)) import Control.Monad.Reader import Control.Monad.State import Data.Coerce import Data.Function import Data.Generics.Product (field) -import Data.Map (Map) import Data.Set (Set) import Data.Tree import Development.IDE.GHC.Compat hiding (Node) @@ -33,6 +33,7 @@ import Development.IDE.GHC.Orphans () import Development.IDE.Types.Location import GHC.Generics import Ide.Plugin.Tactic.Debug +import Ide.Plugin.Tactic.FeatureSet (FeatureSet) import OccName import Refinery.Tactic import System.IO.Unsafe (unsafePerformIO) @@ -336,6 +337,7 @@ data Context = Context -- ^ The functions currently being defined , ctxModuleFuncs :: [(OccName, CType)] -- ^ Everything defined in the current module + , ctxFeatureSet :: FeatureSet } deriving stock (Eq, Ord, Show) @@ -343,7 +345,7 @@ data Context = Context ------------------------------------------------------------------------------ -- | An empty context emptyContext :: Context -emptyContext = Context mempty mempty +emptyContext = Context mempty mempty mempty newtype Rose a = Rose (Tree a) diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 6bac33728f..59835755c8 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -15,12 +15,16 @@ import Control.Lens hiding ((<.>)) import Control.Monad (unless) import Control.Monad.IO.Class import Data.Aeson +import Data.Default (Default(def)) import Data.Either (isLeft) import Data.Foldable +import qualified Data.Map as M import Data.Maybe 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 @@ -154,10 +158,30 @@ mkTest name fp line col ts = @? ("Expected a code action with title " <> T.unpack title) +setFeatureSet :: FeatureSet -> Session () +setFeatureSet features = do + let unObject (Object obj) = obj + unObject _ = undefined + def_config = def :: Plugin.Config + config = + def_config + { Plugin.plugins = M.fromList [("tactics", + def { Plugin.plcConfig = unObject $ toJSON $ + emptyConfig { cfg_feature_set = features }} + )] <> Plugin.plugins def_config } + + sendNotification SWorkspaceDidChangeConfiguration $ + DidChangeConfigurationParams $ + toJSON config + goldenTest :: FilePath -> Int -> Int -> TacticCommand -> Text -> TestTree -goldenTest input line col tc occ = +goldenTest = goldenTest' allFeatures + +goldenTest' :: FeatureSet -> FilePath -> Int -> Int -> TacticCommand -> Text -> TestTree +goldenTest' features input line col tc occ = testCase (input <> " (golden)") $ do runSession hlsCommand fullCaps tacticPath $ do + setFeatureSet features doc <- openDoc input "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col