3
3
{-# LANGUAGE DerivingStrategies #-}
4
4
{-# LANGUAGE OverloadedStrings #-}
5
5
{-# LANGUAGE ViewPatterns #-}
6
+ {-# OPTIONS_GHC -Wall #-}
6
7
7
8
module Ide.Plugin.Tactic.LanguageServer.TacticProviders
8
9
( commandProvider
@@ -12,17 +13,19 @@ module Ide.Plugin.Tactic.LanguageServer.TacticProviders
12
13
) where
13
14
14
15
import Control.Monad
15
- import Control.Monad.Error.Class (MonadError (throwError ))
16
+ import Control.Monad.Error.Class (MonadError (throwError ))
16
17
import Data.Aeson
18
+ import Data.Bool (bool )
17
19
import Data.Coerce
18
- import qualified Data.Map as M
20
+ import qualified Data.Map as M
19
21
import Data.Maybe
20
22
import Data.Monoid
21
- import qualified Data.Text as T
23
+ import qualified Data.Text as T
22
24
import Data.Traversable
25
+ import DataCon (dataConName )
23
26
import Development.IDE.GHC.Compat
24
27
import GHC.Generics
25
- import GHC.LanguageExtensions.Type (Extension (LambdaCase ))
28
+ import GHC.LanguageExtensions.Type (Extension (LambdaCase ))
26
29
import Ide.Plugin.Tactic.Auto
27
30
import Ide.Plugin.Tactic.FeatureSet
28
31
import Ide.Plugin.Tactic.GHC
@@ -34,8 +37,8 @@ import Ide.PluginUtils
34
37
import Ide.Types
35
38
import Language.LSP.Types
36
39
import OccName
37
- import Prelude hiding (span )
38
- import Refinery.Tactic (goal )
40
+ import Prelude hiding (span )
41
+ import Refinery.Tactic (goal )
39
42
40
43
41
44
------------------------------------------------------------------------------
@@ -47,6 +50,7 @@ commandTactic Destruct = useNameFromHypothesis destruct
47
50
commandTactic Homomorphism = useNameFromHypothesis homo
48
51
commandTactic DestructLambdaCase = const destructLambdaCase
49
52
commandTactic HomomorphismLambdaCase = const homoLambdaCase
53
+ commandTactic UseDataCon = userSplit
50
54
51
55
52
56
------------------------------------------------------------------------------
@@ -71,14 +75,34 @@ commandProvider HomomorphismLambdaCase =
71
75
requireExtension LambdaCase $
72
76
filterGoalType ((== Just True ) . lambdaCaseable) $
73
77
provide HomomorphismLambdaCase " "
78
+ commandProvider UseDataCon =
79
+ withConfig $ \ cfg ->
80
+ requireFeature FeatureUseDataCon $
81
+ filterTypeProjection
82
+ ( guardLength (<= cfg_max_use_ctor_actions cfg)
83
+ . fromMaybe []
84
+ . fmap fst
85
+ . tacticsGetDataCons
86
+ ) $ \ dcon ->
87
+ provide UseDataCon
88
+ . T. pack
89
+ . occNameString
90
+ . occName
91
+ $ dataConName dcon
92
+
93
+
94
+ ------------------------------------------------------------------------------
95
+ -- | Return an empty list if the given predicate doesn't hold over the length
96
+ guardLength :: (Int -> Bool ) -> [a ] -> [a ]
97
+ guardLength f as = bool [] as $ f $ length as
74
98
75
99
76
100
------------------------------------------------------------------------------
77
101
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
78
102
-- UI.
79
103
type TacticProvider
80
104
= DynFlags
81
- -> FeatureSet
105
+ -> Config
82
106
-> PluginId
83
107
-> Uri
84
108
-> Range
@@ -99,28 +123,29 @@ data TacticParams = TacticParams
99
123
-- | Restrict a 'TacticProvider', making sure it appears only when the given
100
124
-- 'Feature' is in the feature set.
101
125
requireFeature :: Feature -> TacticProvider -> TacticProvider
102
- requireFeature f tp dflags fs plId uri range jdg = do
103
- guard $ hasFeature f fs
104
- tp dflags fs plId uri range jdg
126
+ requireFeature f tp dflags cfg plId uri range jdg = do
127
+ case hasFeature f $ cfg_feature_set cfg of
128
+ True -> tp dflags cfg plId uri range jdg
129
+ False -> pure []
105
130
106
131
107
132
------------------------------------------------------------------------------
108
133
-- | Restrict a 'TacticProvider', making sure it appears only when the given
109
134
-- predicate holds for the goal.
110
135
requireExtension :: Extension -> TacticProvider -> TacticProvider
111
- requireExtension ext tp dflags fs plId uri range jdg =
136
+ requireExtension ext tp dflags cfg plId uri range jdg =
112
137
case xopt ext dflags of
113
- True -> tp dflags fs plId uri range jdg
138
+ True -> tp dflags cfg plId uri range jdg
114
139
False -> pure []
115
140
116
141
117
142
------------------------------------------------------------------------------
118
143
-- | Restrict a 'TacticProvider', making sure it appears only when the given
119
144
-- predicate holds for the goal.
120
145
filterGoalType :: (Type -> Bool ) -> TacticProvider -> TacticProvider
121
- filterGoalType p tp dflags fs plId uri range jdg =
146
+ filterGoalType p tp dflags cfg plId uri range jdg =
122
147
case p $ unCType $ jGoal jdg of
123
- True -> tp dflags fs plId uri range jdg
148
+ True -> tp dflags cfg plId uri range jdg
124
149
False -> pure []
125
150
126
151
@@ -131,16 +156,34 @@ filterBindingType
131
156
:: (Type -> Type -> Bool ) -- ^ Goal and then binding types.
132
157
-> (OccName -> Type -> TacticProvider )
133
158
-> TacticProvider
134
- filterBindingType p tp dflags fs plId uri range jdg =
159
+ filterBindingType p tp dflags cfg plId uri range jdg =
135
160
let hy = jHypothesis jdg
136
161
g = jGoal jdg
137
162
in fmap join $ for (unHypothesis hy) $ \ hi ->
138
163
let ty = unCType $ hi_type hi
139
164
in case p (unCType g) ty of
140
- True -> tp (hi_name hi) ty dflags fs plId uri range jdg
165
+ True -> tp (hi_name hi) ty dflags cfg plId uri range jdg
141
166
False -> pure []
142
167
143
168
169
+ ------------------------------------------------------------------------------
170
+ -- | Multiply a 'TacticProvider' by some feature projection out of the goal
171
+ -- type. Used e.g. to crete a code action for every data constructor.
172
+ filterTypeProjection
173
+ :: (Type -> [a ]) -- ^ Features of the goal to look into further
174
+ -> (a -> TacticProvider )
175
+ -> TacticProvider
176
+ filterTypeProjection p tp dflags cfg plId uri range jdg =
177
+ fmap join $ for (p $ unCType $ jGoal jdg) $ \ a ->
178
+ tp a dflags cfg plId uri range jdg
179
+
180
+
181
+ ------------------------------------------------------------------------------
182
+ -- | Get access to the 'Config' when building a 'TacticProvider'.
183
+ withConfig :: (Config -> TacticProvider ) -> TacticProvider
184
+ withConfig tp dflags cfg plId uri range jdg = tp cfg dflags cfg plId uri range jdg
185
+
186
+
144
187
145
188
------------------------------------------------------------------------------
146
189
-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
@@ -174,7 +217,6 @@ tcCommandId :: TacticCommand -> CommandId
174
217
tcCommandId c = coerce $ T. pack $ " tactics" <> show c <> " Command"
175
218
176
219
177
-
178
220
------------------------------------------------------------------------------
179
221
-- | We should show homos only when the goal type is the same as the binding
180
222
-- type, and that both are usual algebraic types.
0 commit comments