Skip to content

Commit 344c4cd

Browse files
isovectormergify[bot]
isovector
and
mergify[bot]
authored
Perform name lookup directly in TacticsM (#1924)
* Move IO out of the Parser and into Tactics where it belongs * Remove KnownThings, since we can look it up in IO now * Sort imports Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
1 parent 773452c commit 344c4cd

File tree

15 files changed

+174
-252
lines changed

15 files changed

+174
-252
lines changed

‎plugins/hls-tactics-plugin/src/Wingman/Context.hs

+6-17
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ import Data.Foldable.Extra (allM)
88
import Data.Maybe (fromMaybe, isJust, mapMaybe)
99
import qualified Data.Set as S
1010
import Development.IDE.GHC.Compat
11-
import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env)
11+
import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env, extractModule)
1212
import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
1313
import OccName
1414
import TcRnTypes
@@ -23,11 +23,11 @@ mkContext
2323
:: Config
2424
-> [(OccName, CType)]
2525
-> TcGblEnv
26+
-> HscEnv
2627
-> ExternalPackageState
27-
-> KnownThings
2828
-> [Evidence]
2929
-> Context
30-
mkContext cfg locals tcg eps kt ev = fix $ \ctx ->
30+
mkContext cfg locals tcg hscenv eps ev = fix $ \ctx ->
3131
Context
3232
{ ctxDefiningFuncs
3333
= fmap (second $ coerce $ normalizeType ctx) locals
@@ -46,8 +46,10 @@ mkContext cfg locals tcg eps kt ev = fix $ \ctx ->
4646
(eps_inst_env eps)
4747
(tcg_inst_env tcg)
4848
(tcVisibleOrphanMods tcg)
49-
, ctxKnownThings = kt
5049
, ctxTheta = evidenceToThetaType ev
50+
, ctx_hscEnv = hscenv
51+
, ctx_occEnv = tcg_rdr_env tcg
52+
, ctx_module = extractModule tcg
5153
}
5254

5355

@@ -75,19 +77,6 @@ getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
7577
getCurrentDefinitions = asks ctxDefiningFuncs
7678

7779

78-
------------------------------------------------------------------------------
79-
-- | Extract something from 'KnownThings'.
80-
getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a
81-
getKnownThing f = asks $ f . ctxKnownThings
82-
83-
84-
------------------------------------------------------------------------------
85-
-- | Like 'getInstance', but uses a class from the 'KnownThings'.
86-
getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))
87-
getKnownInstance f tys = do
88-
cls <- getKnownThing f
89-
getInstance cls tys
90-
9180

9281
------------------------------------------------------------------------------
9382
-- | Determine if there is an instance that exists for the given 'Class' at the

‎plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs

-1
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,6 @@ codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
5959
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
6060
let stale a = runStaleIde "codeLensProvider" state nfp a
6161

62-
cfg <- getTacticConfig plId
6362
ccs <- getClientCapabilities
6463
liftIO $ fromMaybeT (Right $ List []) $ do
6564
dflags <- getIdeDynflags state nfp

‎plugins/hls-tactics-plugin/src/Wingman/GHC.hs

+35-38
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,12 @@
44
module Wingman.GHC where
55

66
import Bag (bagToList)
7+
import Class (classTyVars)
78
import ConLike
8-
import Control.Applicative (empty)
99
import Control.Monad.State
1010
import Control.Monad.Trans.Maybe (MaybeT(..))
1111
import CoreUtils (exprType)
12+
import Data.Bool (bool)
1213
import Data.Function (on)
1314
import Data.Functor ((<&>))
1415
import Data.List (isPrefixOf)
@@ -18,22 +19,21 @@ import Data.Set (Set)
1819
import qualified Data.Set as S
1920
import Data.Traversable
2021
import DataCon
21-
import Development.IDE (HscEnvEq (hscEnv))
22-
import Development.IDE.Core.Compile (lookupName)
2322
import Development.IDE.GHC.Compat hiding (exprType)
2423
import DsExpr (dsExpr)
2524
import DsMonad (initDs)
2625
import FamInst (tcLookupDataFamInst_maybe)
2726
import FamInstEnv (normaliseType)
2827
import GHC.SourceGen (lambda)
2928
import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
30-
import GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal))
29+
import GhcPlugins (Role (Nominal))
3130
import OccName
3231
import TcRnMonad
3332
import TcType
3433
import TyCoRep
3534
import Type
3635
import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
36+
import Unify
3737
import Unique
3838
import Var
3939
import Wingman.Types
@@ -323,40 +323,6 @@ unXPat (XPat (L _ pat)) = unXPat pat
323323
unXPat pat = pat
324324

325325

326-
------------------------------------------------------------------------------
327-
-- | Build a 'KnownThings'.
328-
knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings
329-
knownThings tcg hscenv= do
330-
let cls = knownClass tcg hscenv
331-
KnownThings
332-
<$> cls (mkClsOcc "Semigroup")
333-
<*> cls (mkClsOcc "Monoid")
334-
335-
336-
------------------------------------------------------------------------------
337-
-- | Like 'knownThing' but specialized to classes.
338-
knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class
339-
knownClass = knownThing $ \case
340-
ATyCon tc -> tyConClass_maybe tc
341-
_ -> Nothing
342-
343-
344-
------------------------------------------------------------------------------
345-
-- | Helper function for defining 'knownThings'.
346-
knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a
347-
knownThing f tcg hscenv occ = do
348-
let modul = extractModule tcg
349-
rdrenv = tcg_rdr_env tcg
350-
351-
case lookupOccEnv rdrenv occ of
352-
Nothing -> empty
353-
Just elts -> do
354-
mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts
355-
case mvar of
356-
Just tt -> liftMaybe $ f tt
357-
_ -> empty
358-
359-
360326
liftMaybe :: Monad m => Maybe a -> MaybeT m a
361327
liftMaybe a = MaybeT $ pure a
362328

@@ -396,3 +362,34 @@ expandTyFam :: Context -> Type -> Type
396362
expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal
397363

398364

365+
------------------------------------------------------------------------------
366+
-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
367+
tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
368+
tryUnifyUnivarsButNotSkolems skolems goal inst =
369+
case tcUnifyTysFG
370+
(bool BindMe Skolem . flip S.member skolems)
371+
[unCType inst]
372+
[unCType goal] of
373+
Unifiable subst -> pure subst
374+
_ -> Nothing
375+
376+
377+
updateSubst :: TCvSubst -> TacticState -> TacticState
378+
updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) }
379+
380+
381+
------------------------------------------------------------------------------
382+
-- | Get the class methods of a 'PredType', correctly dealing with
383+
-- instantiation of quantified class types.
384+
methodHypothesis :: PredType -> Maybe [HyInfo CType]
385+
methodHypothesis ty = do
386+
(tc, apps) <- splitTyConApp_maybe ty
387+
cls <- tyConClass_maybe tc
388+
let methods = classMethods cls
389+
tvs = classTyVars cls
390+
subst = zipTvSubst tvs apps
391+
pure $ methods <&> \method ->
392+
let (_, _, ty) = tcSplitSigmaTy $ idType method
393+
in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
394+
)
395+

‎plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ import TcEvidence
3232
import TcType (substTy)
3333
import TcType (tcTyConAppTyCon_maybe)
3434
import TysPrim (eqPrimTyCon)
35-
import Wingman.Machinery
35+
import Wingman.GHC
3636
import Wingman.Types
3737

3838

‎plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs

+5-5
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ module Wingman.KnownStrategies where
22

33
import Control.Monad.Error.Class
44
import Data.Foldable (for_)
5-
import OccName (mkVarOcc)
5+
import OccName (mkVarOcc, mkClsOcc)
66
import Refinery.Tactic
7-
import Wingman.Context (getCurrentDefinitions, getKnownInstance)
7+
import Wingman.Context (getCurrentDefinitions)
88
import Wingman.Judgements (jGoal)
99
import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)
10-
import Wingman.Machinery (tracing)
10+
import Wingman.Machinery (tracing, getKnownInstance)
1111
import Wingman.Tactics
1212
import Wingman.Types
1313

@@ -55,7 +55,7 @@ deriveMappend = do
5555
destructAll
5656
split
5757
g <- goal
58-
minst <- getKnownInstance kt_semigroup
58+
minst <- getKnownInstance (mkClsOcc "Semigroup")
5959
. pure
6060
. unCType
6161
$ jGoal g
@@ -77,7 +77,7 @@ deriveMempty :: TacticsM ()
7777
deriveMempty = do
7878
split
7979
g <- goal
80-
minst <- getKnownInstance kt_monoid [unCType $ jGoal g]
80+
minst <- getKnownInstance (mkClsOcc "Monoid") [unCType $ jGoal g]
8181
for_ minst $ \(cls, df) -> do
8282
applyMethod cls df $ mkVarOcc "mempty"
8383
try assumption

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

+5-30
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,6 @@ import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
4444
import qualified FastString
4545
import GHC.Generics (Generic)
4646
import Generics.SYB hiding (Generic)
47-
import GhcPlugins (extractModule)
4847
import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
4948
import qualified Ide.Plugin.Config as Plugin
5049
import Ide.Plugin.Properties
@@ -59,13 +58,12 @@ import OccName
5958
import Prelude hiding (span)
6059
import Retrie (transformA)
6160
import SrcLoc (containsSpan)
62-
import TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env))
61+
import TcRnTypes (tcg_binds, TcGblEnv)
6362
import Wingman.Context
6463
import Wingman.GHC
6564
import Wingman.Judgements
6665
import Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
6766
import Wingman.Judgements.Theta
68-
import Wingman.Metaprogramming.Lexer (ParserContext(..))
6967
import Wingman.Range
7068
import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
7169
import Wingman.Types
@@ -215,9 +213,8 @@ judgementForHole state nfp range cfg = do
215213
-- involved, so it's not crucial to track ages.
216214
let henv = untrackedStaleValue $ hscenv
217215
eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
218-
kt <- knownThings (untrackedStaleValue tcg) henv
219216

220-
(jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
217+
(jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps
221218
let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t
222219

223220
dflags <- getIdeDynflags state nfp
@@ -240,10 +237,10 @@ mkJudgementAndContext
240237
-> TrackedStale Bindings
241238
-> Tracked 'Current RealSrcSpan
242239
-> TrackedStale TcGblEnv
240+
-> HscEnv
243241
-> ExternalPackageState
244-
-> KnownThings
245242
-> Maybe (Judgement, Context)
246-
mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
243+
mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps = do
247244
binds_rss <- mapAgeFrom bmap rss
248245
tcg_rss <- mapAgeFrom tcgmap rss
249246

@@ -253,8 +250,8 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
253250
$ unTrack
254251
$ getDefiningBindings <$> binds <*> binds_rss)
255252
(unTrack tcg)
253+
hscenv
256254
eps
257-
kt
258255
evidence
259256
top_provs = getRhsPosVals tcg_rss tcs
260257
already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs
@@ -598,25 +595,3 @@ getMetaprogramAtSpan (unTrack -> ss)
598595
. tcg_binds
599596
. unTrack
600597

601-
602-
------------------------------------------------------------------------------
603-
-- | The metaprogram parser needs the ability to lookup terms from the module
604-
-- and imports. The 'ParserContext' contains everything we need to find that
605-
-- stuff.
606-
getParserState
607-
:: IdeState
608-
-> NormalizedFilePath
609-
-> Context
610-
-> MaybeT IO ParserContext
611-
getParserState state nfp ctx = do
612-
let stale a = runStaleIde "getParserState" state nfp a
613-
614-
TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck
615-
TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
616-
617-
let tcgblenv = tmrTypechecked tcmod
618-
modul = extractModule tcgblenv
619-
rdrenv = tcg_rdr_env tcgblenv
620-
621-
pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx
622-

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs

+1-3
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module Wingman.LanguageServer.Metaprogram
1010

1111
import Control.Applicative (empty)
1212
import Control.Monad
13-
import Control.Monad.Reader (runReaderT)
1413
import Control.Monad.Trans
1514
import Control.Monad.Trans.Maybe
1615
import Data.List (find)
@@ -52,8 +51,7 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
5251
Just (trss, program) -> do
5352
let tr_range = fmap realSrcSpanToRange trss
5453
HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
55-
ps <- getParserState state nfp ctx
56-
z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program
54+
z <- liftIO $ attempt_it ctx jdg $ T.unpack program
5755
pure $ Hover
5856
{ _contents = HoverContents
5957
$ MarkupContent MkMarkdown

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs

+13-15
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ module Wingman.LanguageServer.TacticProviders
1212
) where
1313

1414
import Control.Monad
15-
import Control.Monad.Reader (runReaderT)
1615
import Data.Aeson
1716
import Data.Bool (bool)
1817
import Data.Coerce
@@ -34,27 +33,26 @@ import Wingman.Auto
3433
import Wingman.GHC
3534
import Wingman.Judgements
3635
import Wingman.Machinery (useNameFromHypothesis)
37-
import Wingman.Metaprogramming.Lexer (ParserContext)
3836
import Wingman.Metaprogramming.Parser (parseMetaprogram)
3937
import Wingman.Tactics
4038
import Wingman.Types
4139

4240

4341
------------------------------------------------------------------------------
4442
-- | A mapping from tactic commands to actual tactics for refinery.
45-
commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ())
46-
commandTactic _ Auto = pure . const auto
47-
commandTactic _ Intros = pure . const intros
48-
commandTactic _ Destruct = pure . useNameFromHypothesis destruct . mkVarOcc . T.unpack
49-
commandTactic _ DestructPun = pure . useNameFromHypothesis destructPun . mkVarOcc . T.unpack
50-
commandTactic _ Homomorphism = pure . useNameFromHypothesis homo . mkVarOcc . T.unpack
51-
commandTactic _ DestructLambdaCase = pure . const destructLambdaCase
52-
commandTactic _ HomomorphismLambdaCase = pure . const homoLambdaCase
53-
commandTactic _ DestructAll = pure . const destructAll
54-
commandTactic _ UseDataCon = pure . userSplit . mkVarOcc . T.unpack
55-
commandTactic _ Refine = pure . const refine
56-
commandTactic _ BeginMetaprogram = pure . const metaprogram
57-
commandTactic c RunMetaprogram = flip runReaderT c . parseMetaprogram
43+
commandTactic :: TacticCommand -> T.Text -> TacticsM ()
44+
commandTactic Auto = const auto
45+
commandTactic Intros = const intros
46+
commandTactic Destruct = useNameFromHypothesis destruct . mkVarOcc . T.unpack
47+
commandTactic DestructPun = useNameFromHypothesis destructPun . mkVarOcc . T.unpack
48+
commandTactic Homomorphism = useNameFromHypothesis homo . mkVarOcc . T.unpack
49+
commandTactic DestructLambdaCase = const destructLambdaCase
50+
commandTactic HomomorphismLambdaCase = const homoLambdaCase
51+
commandTactic DestructAll = const destructAll
52+
commandTactic UseDataCon = userSplit . mkVarOcc . T.unpack
53+
commandTactic Refine = const refine
54+
commandTactic BeginMetaprogram = const metaprogram
55+
commandTactic RunMetaprogram = parseMetaprogram
5856

5957

6058
------------------------------------------------------------------------------

0 commit comments

Comments
 (0)