Skip to content

Implement Tactic Featuresets #1398

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 7 commits into from
Feb 19, 2021
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make Tactics tests run with a full feature set
  • Loading branch information
isovector committed Feb 18, 2021
commit d77f6884e8d358abb4b4c4f0c718d7ade9186b17
1 change: 1 addition & 0 deletions haskell-language-server.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module Ide.Plugin.Tactic.FeatureSet
, FeatureSet
, hasFeature
, defaultFeatures
, allFeatures
, parseFeatureSet
, prettyFeatureSet
) where
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,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)
Expand All @@ -30,24 +32,22 @@ 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)
import SrcLoc (containsSpan)
import TcRnTypes (tcg_binds)
import Ide.Plugin.Config (PluginConfig(plcConfig))
import qualified Ide.Plugin.Config as Plugin
import Data.Aeson (Value(Object), fromJSON)
import Data.Aeson.Types (Result(Success, Error))
import Language.LSP.Server (MonadLsp)


tacticDesc :: T.Text -> T.Text
Expand Down
23 changes: 23 additions & 0 deletions plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

20 changes: 0 additions & 20 deletions plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -388,23 +388,3 @@ data AgdaMatch = AgdaMatch
}
deriving (Show)


------------------------------------------------------------------------------
-- | 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

26 changes: 25 additions & 1 deletion test/functional/Tactic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down