diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index 825285ce8c..549af57716 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -1,10 +1,12 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} module Wingman.LanguageServer.TacticProviders ( commandProvider , commandTactic , tcCommandId , TacticParams (..) + , TacticProviderData (..) ) where import Control.Monad @@ -140,14 +142,18 @@ guardLength f as = bool [] as $ f $ length as -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS -- UI. type TacticProvider - = DynFlags - -> Config - -> PluginId - -> Uri - -> Range - -> Judgement + = TacticProviderData -> IO [Command |? CodeAction] +data TacticProviderData = TacticProviderData + { tpd_dflags :: DynFlags + , tpd_config :: Config + , tpd_plid :: PluginId + , tpd_uri :: Uri + , tpd_range :: Range + , tpd_jdg :: Judgement + } + data TacticParams = TacticParams { tp_file :: Uri -- ^ Uri of the file to fill the hole in @@ -162,9 +168,9 @@ 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 cfg plId uri range jdg = do - case hasFeature f $ cfg_feature_set cfg of - True -> tp dflags cfg plId uri range jdg +requireFeature f tp tpd = + case hasFeature f $ cfg_feature_set $ tpd_config tpd of + True -> tp tpd False -> pure [] @@ -172,9 +178,9 @@ requireFeature f tp dflags cfg plId uri range jdg = do -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. requireExtension :: Extension -> TacticProvider -> TacticProvider -requireExtension ext tp dflags cfg plId uri range jdg = - case xopt ext dflags of - True -> tp dflags cfg plId uri range jdg +requireExtension ext tp tpd = + case xopt ext $ tpd_dflags tpd of + True -> tp tpd False -> pure [] @@ -182,9 +188,9 @@ requireExtension ext tp dflags cfg 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 cfg plId uri range jdg = - case p $ unCType $ jGoal jdg of - True -> tp dflags cfg plId uri range jdg +filterGoalType p tp tpd = + case p $ unCType $ jGoal $ tpd_jdg tpd of + True -> tp tpd False -> pure [] @@ -192,8 +198,7 @@ filterGoalType p tp dflags cfg plId uri range jdg = -- | 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 +withJudgement tp tpd = tp (tpd_jdg tpd) tpd ------------------------------------------------------------------------------ @@ -203,13 +208,14 @@ filterBindingType :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider -filterBindingType p tp dflags cfg plId uri range jdg = - let hy = jHypothesis jdg - g = jGoal jdg +filterBindingType p tp tpd = + let jdg = tpd_jdg tpd + 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 cfg plId uri range jdg + True -> tp (hi_name hi) ty tpd False -> pure [] @@ -220,15 +226,15 @@ filterTypeProjection :: (Type -> [a]) -- ^ Features of the goal to look into further -> (a -> TacticProvider) -> TacticProvider -filterTypeProjection p tp dflags cfg plId uri range jdg = - fmap join $ for (p $ unCType $ jGoal jdg) $ \a -> - tp a dflags cfg plId uri range jdg +filterTypeProjection p tp tpd = + fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a -> + tp a tpd ------------------------------------------------------------------------------ -- | 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 +withConfig tp tpd = tp (tpd_config tpd) tpd @@ -247,10 +253,10 @@ 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 TacticProviderData{..} = 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]) + params = TacticParams { tp_file = tpd_uri , tp_range = tpd_range , tp_var_name = name } + cmd = mkLspCommand tpd_plid (tcCommandId tc) title (Just [toJSON params]) pure $ pure $ InR diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 182cb4bb92..d4c2d7a2bd 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -60,13 +60,14 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg actions <- lift $ -- This foldMap is over the function monoid. - foldMap commandProvider [minBound .. maxBound] - dflags - cfg - plId - uri - range - jdg + foldMap commandProvider [minBound .. maxBound] $ TacticProviderData + { tpd_dflags = dflags + , tpd_config = cfg + , tpd_plid = plId + , tpd_uri = uri + , tpd_range = range + , tpd_jdg = jdg + } pure $ Right $ List actions codeActionProvider _ _ _ = pure $ Right $ List []