1
1
{-# LANGUAGE OverloadedStrings #-}
2
+ {-# LANGUAGE RecordWildCards #-}
2
3
3
4
module Wingman.LanguageServer.TacticProviders
4
5
( commandProvider
5
6
, commandTactic
6
7
, tcCommandId
7
8
, TacticParams (.. )
9
+ , TacticProviderData (.. )
8
10
) where
9
11
10
12
import Control.Monad
@@ -140,14 +142,18 @@ guardLength f as = bool [] as $ f $ length as
140
142
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
141
143
-- UI.
142
144
type TacticProvider
143
- = DynFlags
144
- -> Config
145
- -> PluginId
146
- -> Uri
147
- -> Range
148
- -> Judgement
145
+ = TacticProviderData
149
146
-> IO [Command |? CodeAction ]
150
147
148
+ data TacticProviderData = TacticProviderData
149
+ { tpd_dflags :: DynFlags
150
+ , tpd_config :: Config
151
+ , tpd_plid :: PluginId
152
+ , tpd_uri :: Uri
153
+ , tpd_range :: Range
154
+ , tpd_jdg :: Judgement
155
+ }
156
+
151
157
152
158
data TacticParams = TacticParams
153
159
{ tp_file :: Uri -- ^ Uri of the file to fill the hole in
@@ -162,38 +168,37 @@ data TacticParams = TacticParams
162
168
-- | Restrict a 'TacticProvider', making sure it appears only when the given
163
169
-- 'Feature' is in the feature set.
164
170
requireFeature :: Feature -> TacticProvider -> TacticProvider
165
- requireFeature f tp dflags cfg plId uri range jdg = do
166
- case hasFeature f $ cfg_feature_set cfg of
167
- True -> tp dflags cfg plId uri range jdg
171
+ requireFeature f tp tpd =
172
+ case hasFeature f $ cfg_feature_set $ tpd_config tpd of
173
+ True -> tp tpd
168
174
False -> pure []
169
175
170
176
171
177
------------------------------------------------------------------------------
172
178
-- | Restrict a 'TacticProvider', making sure it appears only when the given
173
179
-- predicate holds for the goal.
174
180
requireExtension :: Extension -> TacticProvider -> TacticProvider
175
- requireExtension ext tp dflags cfg plId uri range jdg =
176
- case xopt ext dflags of
177
- True -> tp dflags cfg plId uri range jdg
181
+ requireExtension ext tp tpd =
182
+ case xopt ext $ tpd_dflags tpd of
183
+ True -> tp tpd
178
184
False -> pure []
179
185
180
186
181
187
------------------------------------------------------------------------------
182
188
-- | Restrict a 'TacticProvider', making sure it appears only when the given
183
189
-- predicate holds for the goal.
184
190
filterGoalType :: (Type -> Bool ) -> TacticProvider -> TacticProvider
185
- filterGoalType p tp dflags cfg plId uri range jdg =
186
- case p $ unCType $ jGoal jdg of
187
- True -> tp dflags cfg plId uri range jdg
191
+ filterGoalType p tp tpd =
192
+ case p $ unCType $ jGoal $ tpd_jdg tpd of
193
+ True -> tp tpd
188
194
False -> pure []
189
195
190
196
191
197
------------------------------------------------------------------------------
192
198
-- | Restrict a 'TacticProvider', making sure it appears only when the given
193
199
-- predicate holds for the goal.
194
200
withJudgement :: (Judgement -> TacticProvider ) -> TacticProvider
195
- withJudgement tp dflags fs plId uri range jdg =
196
- tp jdg dflags fs plId uri range jdg
201
+ withJudgement tp tpd = tp (tpd_jdg tpd) tpd
197
202
198
203
199
204
------------------------------------------------------------------------------
@@ -203,13 +208,14 @@ filterBindingType
203
208
:: (Type -> Type -> Bool ) -- ^ Goal and then binding types.
204
209
-> (OccName -> Type -> TacticProvider )
205
210
-> TacticProvider
206
- filterBindingType p tp dflags cfg plId uri range jdg =
207
- let hy = jHypothesis jdg
208
- g = jGoal jdg
211
+ filterBindingType p tp tpd =
212
+ let jdg = tpd_jdg tpd
213
+ hy = jHypothesis jdg
214
+ g = jGoal jdg
209
215
in fmap join $ for (unHypothesis hy) $ \ hi ->
210
216
let ty = unCType $ hi_type hi
211
217
in case p (unCType g) ty of
212
- True -> tp (hi_name hi) ty dflags cfg plId uri range jdg
218
+ True -> tp (hi_name hi) ty tpd
213
219
False -> pure []
214
220
215
221
@@ -220,15 +226,15 @@ filterTypeProjection
220
226
:: (Type -> [a ]) -- ^ Features of the goal to look into further
221
227
-> (a -> TacticProvider )
222
228
-> TacticProvider
223
- filterTypeProjection p tp dflags cfg plId uri range jdg =
224
- fmap join $ for (p $ unCType $ jGoal jdg ) $ \ a ->
225
- tp a dflags cfg plId uri range jdg
229
+ filterTypeProjection p tp tpd =
230
+ fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd ) $ \ a ->
231
+ tp a tpd
226
232
227
233
228
234
------------------------------------------------------------------------------
229
235
-- | Get access to the 'Config' when building a 'TacticProvider'.
230
236
withConfig :: (Config -> TacticProvider ) -> TacticProvider
231
- withConfig tp dflags cfg plId uri range jdg = tp cfg dflags cfg plId uri range jdg
237
+ withConfig tp tpd = tp (tpd_config tpd) tpd
232
238
233
239
234
240
@@ -247,10 +253,10 @@ useNameFromHypothesis f name = do
247
253
-- | Terminal constructor for providing context-sensitive tactics. Tactics
248
254
-- given by 'provide' are always available.
249
255
provide :: TacticCommand -> T. Text -> TacticProvider
250
- provide tc name _ _ plId uri range _ = do
256
+ provide tc name TacticProviderData { .. } = do
251
257
let title = tacticTitle tc name
252
- params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }
253
- cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
258
+ params = TacticParams { tp_file = tpd_uri , tp_range = tpd_range , tp_var_name = name }
259
+ cmd = mkLspCommand tpd_plid (tcCommandId tc) title (Just [toJSON params])
254
260
pure
255
261
$ pure
256
262
$ InR
0 commit comments