@@ -12,6 +12,7 @@ module Wingman.LanguageServer.TacticProviders
1212 ) where
1313
1414import Control.Monad
15+ import Control.Monad.Reader (runReaderT )
1516import Data.Aeson
1617import Data.Bool (bool )
1718import Data.Coerce
@@ -30,15 +31,13 @@ import Language.LSP.Types
3031import OccName
3132import Prelude hiding (span )
3233import Wingman.Auto
33- import Wingman.FeatureSet
3434import Wingman.GHC
3535import Wingman.Judgements
3636import Wingman.Machinery (useNameFromHypothesis )
3737import Wingman.Metaprogramming.Lexer (ParserContext )
3838import Wingman.Metaprogramming.Parser (parseMetaprogram )
3939import Wingman.Tactics
4040import Wingman.Types
41- import Control.Monad.Reader (runReaderT )
4241
4342
4443------------------------------------------------------------------------------
@@ -115,7 +114,6 @@ commandProvider Destruct =
115114 provide Destruct $ T. pack $ occNameString occ
116115commandProvider DestructPun =
117116 requireHoleSort (== Hole ) $
118- requireFeature FeatureDestructPun $
119117 filterBindingType destructPunFilter $ \ occ _ ->
120118 provide DestructPun $ T. pack $ occNameString occ
121119commandProvider Homomorphism =
@@ -134,38 +132,33 @@ commandProvider HomomorphismLambdaCase =
134132 provide HomomorphismLambdaCase " "
135133commandProvider DestructAll =
136134 requireHoleSort (== Hole ) $
137- requireFeature FeatureDestructAll $
138135 withJudgement $ \ jdg ->
139136 case _jIsTopHole jdg && jHasBoundArgs jdg of
140137 True -> provide DestructAll " "
141138 False -> mempty
142139commandProvider UseDataCon =
143140 requireHoleSort (== Hole ) $
144141 withConfig $ \ cfg ->
145- requireFeature FeatureUseDataCon $
146- filterTypeProjection
147- ( guardLength (<= cfg_max_use_ctor_actions cfg)
148- . fromMaybe []
149- . fmap fst
150- . tacticsGetDataCons
151- ) $ \ dcon ->
152- provide UseDataCon
153- . T. pack
154- . occNameString
155- . occName
156- $ dataConName dcon
142+ filterTypeProjection
143+ ( guardLength (<= cfg_max_use_ctor_actions cfg)
144+ . fromMaybe []
145+ . fmap fst
146+ . tacticsGetDataCons
147+ ) $ \ dcon ->
148+ provide UseDataCon
149+ . T. pack
150+ . occNameString
151+ . occName
152+ $ dataConName dcon
157153commandProvider Refine =
158154 requireHoleSort (== Hole ) $
159- requireFeature FeatureRefineHole $
160155 provide Refine " "
161156commandProvider BeginMetaprogram =
162157 requireGHC88OrHigher $
163- requireFeature FeatureMetaprogram $
164158 requireHoleSort (== Hole ) $
165159 provide BeginMetaprogram " "
166160commandProvider RunMetaprogram =
167161 requireGHC88OrHigher $
168- requireFeature FeatureMetaprogram $
169162 withMetaprogram $ \ mp ->
170163 provide RunMetaprogram mp
171164
@@ -213,16 +206,6 @@ data TacticParams = TacticParams
213206 deriving anyclass (ToJSON , FromJSON )
214207
215208
216- ------------------------------------------------------------------------------
217- -- | Restrict a 'TacticProvider', making sure it appears only when the given
218- -- 'Feature' is in the feature set.
219- requireFeature :: Feature -> TacticProvider -> TacticProvider
220- requireFeature f tp tpd =
221- case hasFeature f $ cfg_feature_set $ tpd_config tpd of
222- True -> tp tpd
223- False -> pure []
224-
225-
226209requireHoleSort :: (HoleSort -> Bool ) -> TacticProvider -> TacticProvider
227210requireHoleSort p tp tpd =
228211 case p $ tpd_hole_sort tpd of
0 commit comments