Skip to content

Cleanup the TacticProviders interface #1572

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 1 commit into from
Mar 14, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
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
Original file line number Diff line number Diff line change
@@ -1,10 +1,12 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}

module Wingman.LanguageServer.TacticProviders
( commandProvider
, commandTactic
, tcCommandId
, TacticParams (..)
, TacticProviderData (..)
) where

import Control.Monad
Expand Down Expand Up @@ -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
Expand All @@ -162,38 +168,37 @@ 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 []


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


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


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


------------------------------------------------------------------------------
Expand All @@ -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 []


Expand All @@ -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



Expand All @@ -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
Expand Down
15 changes: 8 additions & 7 deletions plugins/hls-tactics-plugin/src/Wingman/Plugin.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 []

Expand Down