Skip to content

Commit 11d0d51

Browse files
authored
Refactor the hypothesis type in hls-tactics-plugin (#1347)
* Add name to HyInfo * Use a newtype for Hypotheses * Use a set for tracking names in scope * Remove the internal Map OccName representation of Hypothesis * Remove most spurious uses of hyByName * Stop looking up things by name in hyByName; use hi directly * Cleanup imports * Add test for invoking methods at different types * Improve generated names for tyvar applications * Minor formatting and haddocks * Minor styling * Fix test
1 parent e99be7d commit 11d0d51

File tree

12 files changed

+188
-122
lines changed

12 files changed

+188
-122
lines changed

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs

Lines changed: 27 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ module Ide.Plugin.Tactic
1717

1818
import Control.Arrow
1919
import Control.Monad
20+
import Control.Monad.Error.Class (MonadError(throwError))
2021
import Control.Monad.Trans
2122
import Control.Monad.Trans.Maybe
2223
import Data.Aeson
@@ -38,6 +39,7 @@ import Development.IDE.Core.Service (runAction)
3839
import Development.IDE.Core.Shake (useWithStale, IdeState (..))
3940
import Development.IDE.GHC.Compat
4041
import Development.IDE.GHC.Error (realSrcSpanToRange)
42+
import Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource)
4143
import Development.IDE.Spans.LocalBindings (getDefiningBindings)
4244
import Development.Shake (Action)
4345
import DynFlags (xopt)
@@ -53,11 +55,11 @@ import Ide.Plugin.Tactic.Tactics
5355
import Ide.Plugin.Tactic.TestTypes
5456
import Ide.Plugin.Tactic.Types
5557
import Ide.PluginUtils
56-
import Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource)
5758
import Ide.Types
5859
import Language.Haskell.LSP.Core (clientCapabilities)
5960
import Language.Haskell.LSP.Types
6061
import OccName
62+
import Refinery.Tactic (goal)
6163
import SrcLoc (containsSpan)
6264
import System.Timeout
6365
import TcRnTypes (tcg_binds)
@@ -124,12 +126,24 @@ commandProvider HomomorphismLambdaCase =
124126
commandTactic :: TacticCommand -> OccName -> TacticsM ()
125127
commandTactic Auto = const auto
126128
commandTactic Intros = const intros
127-
commandTactic Destruct = destruct
128-
commandTactic Homomorphism = homo
129+
commandTactic Destruct = useNameFromHypothesis destruct
130+
commandTactic Homomorphism = useNameFromHypothesis homo
129131
commandTactic DestructLambdaCase = const destructLambdaCase
130132
commandTactic HomomorphismLambdaCase = const homoLambdaCase
131133

132134

135+
------------------------------------------------------------------------------
136+
-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
137+
-- look it up in the hypothesis.
138+
useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
139+
useNameFromHypothesis f name = do
140+
hy <- jHypothesis <$> goal
141+
case M.lookup name $ hyByName hy of
142+
Just hi -> f hi
143+
Nothing -> throwError $ NotInScope name
144+
145+
146+
133147
------------------------------------------------------------------------------
134148
-- | We should show homos only when the goal type is the same as the binding
135149
-- type, and that both are usual algebraic types.
@@ -216,10 +230,11 @@ filterBindingType
216230
filterBindingType p tp dflags plId uri range jdg =
217231
let hy = jHypothesis jdg
218232
g = jGoal jdg
219-
in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) ->
220-
case p (unCType g) ty of
221-
True -> tp occ ty dflags plId uri range jdg
222-
False -> pure []
233+
in fmap join $ for (unHypothesis hy) $ \hi ->
234+
let ty = unCType $ hi_type hi
235+
in case p (unCType g) ty of
236+
True -> tp (hi_name hi) ty dflags plId uri range jdg
237+
False -> pure []
223238

224239

225240
data TacticParams = TacticParams
@@ -287,11 +302,11 @@ judgementForHole state nfp range = do
287302

288303
spliceProvenance
289304
:: Map OccName Provenance
290-
-> Map OccName (HyInfo a)
291-
-> Map OccName (HyInfo a)
292-
spliceProvenance provs =
293-
M.mapWithKey $ \name hi ->
294-
overProvenance (maybe id const $ M.lookup name provs) hi
305+
-> Hypothesis a
306+
-> Hypothesis a
307+
spliceProvenance provs x =
308+
Hypothesis $ flip fmap (unHypothesis x) $ \hi ->
309+
overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi
295310

296311

297312
tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ import Type hiding (Var)
3535
useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
3636
useOccName jdg name =
3737
-- Only score points if this is in the local hypothesis
38-
case M.lookup name $ jLocalHypothesis jdg of
38+
case M.lookup name $ hyByName $ jLocalHypothesis jdg of
3939
Just{} -> modify
4040
$ (withUsedVals $ S.insert name)
4141
. (field @"ts_unused_top_vals" %~ S.delete name)
@@ -75,7 +75,7 @@ destructMatches f scrut t jdg = do
7575
[] -> throwError $ GoalMismatch "destruct" g
7676
_ -> fmap unzipTrace $ for dcs $ \dc -> do
7777
let args = dataConInstOrigArgTys' dc apps
78-
names <- mkManyGoodNames hy args
78+
names <- mkManyGoodNames (hyNamesInScope hy) args
7979
let hy' = zip names $ coerce args
8080
j = introducingPat scrut dc hy'
8181
$ withNewGoal g jdg
@@ -150,23 +150,20 @@ dataConInstOrigArgTys' con uniTys =
150150
-- | Combinator for performing case splitting, and running sub-rules on the
151151
-- resulting matches.
152152

153-
destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
154-
destruct' f term jdg = do
153+
destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
154+
destruct' f hi jdg = do
155155
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
156-
let hy = jHypothesis jdg
157-
case M.lookup term hy of
158-
Nothing -> throwError $ UndefinedHypothesis term
159-
Just (hi_type -> t) -> do
160-
useOccName jdg term
161-
(tr, ms)
162-
<- destructMatches
163-
f
164-
(Just term)
165-
t
166-
$ disallowing AlreadyDestructed [term] jdg
167-
pure ( rose ("destruct " <> show term) $ pure tr
168-
, noLoc $ case' (var' term) ms
169-
)
156+
let term = hi_name hi
157+
useOccName jdg term
158+
(tr, ms)
159+
<- destructMatches
160+
f
161+
(Just term)
162+
(hi_type hi)
163+
$ disallowing AlreadyDestructed [term] jdg
164+
pure ( rose ("destruct " <> show term) $ pure tr
165+
, noLoc $ case' (var' term) ms
166+
)
170167

171168

172169
------------------------------------------------------------------------------

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,9 @@ mkContext locals tcg = Context
3535

3636
------------------------------------------------------------------------------
3737
-- | Find all of the class methods that exist from the givens in the context.
38-
contextMethodHypothesis :: Context -> Map OccName (HyInfo CType)
38+
contextMethodHypothesis :: Context -> Hypothesis CType
3939
contextMethodHypothesis ctx
40-
= M.fromList
40+
= Hypothesis
4141
. excludeForbiddenMethods
4242
. join
4343
. concatMap
@@ -54,8 +54,8 @@ contextMethodHypothesis ctx
5454
-- | Many operations are defined in typeclasses for performance reasons, rather
5555
-- than being a true part of the class. This function filters out those, in
5656
-- order to keep our hypothesis space small.
57-
excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)]
58-
excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . fst)
57+
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
58+
excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
5959
where
6060
forbiddenMethods :: Set OccName
6161
forbiddenMethods = S.map mkVarOcc $ S.fromList

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs

Lines changed: 52 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,11 @@ module Ide.Plugin.Tactic.Judgements
2626
, mkFirstJudgement
2727
, hypothesisFromBindings
2828
, isTopLevel
29+
, hyNamesInScope
30+
, hyByName
2931
) where
3032

33+
import Control.Arrow
3134
import Control.Lens hiding (Context)
3235
import Data.Bool
3336
import Data.Char
@@ -48,20 +51,20 @@ import Type
4851

4952
------------------------------------------------------------------------------
5053
-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
51-
hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)
54+
hypothesisFromBindings :: RealSrcSpan -> Bindings -> Hypothesis CType
5255
hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span
5356

5457

5558
------------------------------------------------------------------------------
5659
-- | Convert a @Set Id@ into a hypothesis.
57-
buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType)
60+
buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
5861
buildHypothesis
59-
= M.fromList
62+
= Hypothesis
6063
. mapMaybe go
6164
where
6265
go (occName -> occ, t)
6366
| Just ty <- t
64-
, isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty)
67+
, isAlpha . head . occNameString $ occ = Just $ HyInfo occ UserPrv $ CType ty
6568
| otherwise = Nothing
6669

6770

@@ -96,8 +99,8 @@ introducing
9699
-> Judgement' a
97100
-> Judgement' a
98101
introducing f ns =
99-
field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>
100-
\(pos, (name, ty)) -> (name, HyInfo (f pos) ty))
102+
field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&>
103+
\(pos, (name, ty)) -> HyInfo name (f pos) ty)
101104

102105

103106
------------------------------------------------------------------------------
@@ -149,7 +152,7 @@ filterAncestry
149152
-> Judgement
150153
-> Judgement
151154
filterAncestry ancestry reason jdg =
152-
disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg
155+
disallowing reason (M.keys $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg
153156
where
154157
go name _
155158
= not
@@ -172,7 +175,7 @@ findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
172175
findPositionVal jdg defn pos = listToMaybe $ do
173176
-- It's important to inspect the entire hypothesis here, as we need to trace
174177
-- ancstry through potentially disallowed terms in the hypothesis.
175-
(name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg
178+
(name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg
176179
case hi_provenance hi of
177180
TopLevelArgPrv defn' pos'
178181
| defn == defn'
@@ -188,7 +191,7 @@ findPositionVal jdg defn pos = listToMaybe $ do
188191
-- 'filterSameTypeFromOtherPositions'.
189192
findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]
190193
findDconPositionVals jdg dcon pos = do
191-
(name, hi) <- M.toList $ jHypothesis jdg
194+
(name, hi) <- M.toList $ hyByName $ jHypothesis jdg
192195
case hi_provenance hi of
193196
PatternMatchPrv pv
194197
| pv_datacon pv == Uniquely dcon
@@ -203,14 +206,15 @@ findDconPositionVals jdg dcon pos = do
203206
-- other term which might match.
204207
filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement
205208
filterSameTypeFromOtherPositions dcon pos jdg =
206-
let hy = jHypothesis
209+
let hy = hyByName
210+
. jHypothesis
207211
$ filterAncestry
208212
(findDconPositionVals jdg dcon pos)
209213
(WrongBranch pos)
210214
jdg
211215
tys = S.fromList $ hi_type <$> M.elems hy
212216
to_remove =
213-
M.filter (flip S.member tys . hi_type) (jHypothesis jdg)
217+
M.filter (flip S.member tys . hi_type) (hyByName $ jHypothesis jdg)
214218
M.\\ hy
215219
in disallowing Shadowed (M.keys to_remove) jdg
216220

@@ -267,8 +271,8 @@ introducingPat scrutinee dc ns jdg
267271
-- them from 'jHypothesis', but not from 'jEntireHypothesis'.
268272
disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
269273
disallowing reason (S.fromList -> ns) =
270-
field @"_jHypothesis" %~ (M.mapWithKey $ \name hi ->
271-
case S.member name ns of
274+
field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->
275+
case S.member (hi_name hi) ns of
272276
True -> overProvenance (DisallowedPrv reason) hi
273277
False -> hi
274278
)
@@ -277,20 +281,28 @@ disallowing reason (S.fromList -> ns) =
277281
------------------------------------------------------------------------------
278282
-- | The hypothesis, consisting of local terms and the ambient environment
279283
-- (impors and class methods.) Hides disallowed values.
280-
jHypothesis :: Judgement' a -> Map OccName (HyInfo a)
281-
jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis
284+
jHypothesis :: Judgement' a -> Hypothesis a
285+
jHypothesis
286+
= Hypothesis
287+
. filter (not . isDisallowed . hi_provenance)
288+
. unHypothesis
289+
. jEntireHypothesis
282290

283291

284292
------------------------------------------------------------------------------
285293
-- | The whole hypothesis, including things disallowed.
286-
jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)
294+
jEntireHypothesis :: Judgement' a -> Hypothesis a
287295
jEntireHypothesis = _jHypothesis
288296

289297

290298
------------------------------------------------------------------------------
291299
-- | Just the local hypothesis.
292-
jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)
293-
jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis
300+
jLocalHypothesis :: Judgement' a -> Hypothesis a
301+
jLocalHypothesis
302+
= Hypothesis
303+
. filter (isLocalHypothesis . hi_provenance)
304+
. unHypothesis
305+
. jHypothesis
294306

295307

296308
------------------------------------------------------------------------------
@@ -304,10 +316,30 @@ unsetIsTopHole :: Judgement' a -> Judgement' a
304316
unsetIsTopHole = field @"_jIsTopHole" .~ False
305317

306318

319+
------------------------------------------------------------------------------
320+
-- | What names are currently in scope in the hypothesis?
321+
hyNamesInScope :: Hypothesis a -> Set OccName
322+
hyNamesInScope = M.keysSet . hyByName
323+
324+
325+
------------------------------------------------------------------------------
326+
-- | Fold a hypothesis into a single mapping from name to info. This
327+
-- unavoidably will cause duplicate names (things like methods) to shadow one
328+
-- another.
329+
hyByName :: Hypothesis a -> Map OccName (HyInfo a)
330+
hyByName
331+
= M.fromList
332+
. fmap (hi_name &&& id)
333+
. unHypothesis
334+
335+
307336
------------------------------------------------------------------------------
308337
-- | Only the hypothesis members which are pattern vals
309338
jPatHypothesis :: Judgement' a -> Map OccName PatVal
310-
jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis
339+
jPatHypothesis
340+
= M.mapMaybe (getPatVal . hi_provenance)
341+
. hyByName
342+
. jHypothesis
311343

312344

313345
getPatVal :: Provenance-> Maybe PatVal
@@ -326,7 +358,7 @@ substJdg subst = fmap $ coerce . substTy subst . coerce
326358

327359

328360
mkFirstJudgement
329-
:: M.Map OccName (HyInfo CType)
361+
:: Hypothesis CType
330362
-> Bool -- ^ are we in the top level rhs hole?
331363
-> Type
332364
-> Judgement' CType

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -74,9 +74,11 @@ runTactic ctx jdg t =
7474
$ (:) (jGoal jdg)
7575
$ fmap hi_type
7676
$ toList
77+
$ hyByName
7778
$ jHypothesis jdg
7879
unused_topvals = M.keysSet
7980
$ M.filter (isTopLevel . hi_provenance)
81+
$ hyByName
8082
$ jHypothesis jdg
8183
tacticState =
8284
defaultTacticState
@@ -218,7 +220,7 @@ unify goal inst = do
218220
------------------------------------------------------------------------------
219221
-- | Get the class methods of a 'PredType', correctly dealing with
220222
-- instantiation of quantified class types.
221-
methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]
223+
methodHypothesis :: PredType -> Maybe [HyInfo CType]
222224
methodHypothesis ty = do
223225
(tc, apps) <- splitTyConApp_maybe ty
224226
cls <- tyConClass_maybe tc
@@ -230,8 +232,7 @@ methodHypothesis ty = do
230232
$ classSCTheta cls
231233
pure $ mappend sc_methods $ methods <&> \method ->
232234
let (_, _, ty) = tcSplitSigmaTy $ idType method
233-
in ( occName method
234-
, HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
235+
in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
235236
)
236237

237238

0 commit comments

Comments
 (0)