Skip to content

Commit 032ca66

Browse files
isovectorisovector
committed
Perform lookups of terms in scope and context
1 parent cc4dea6 commit 032ca66

File tree

12 files changed

+243
-47
lines changed

12 files changed

+243
-47
lines changed

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

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,11 @@ import Bag
44
import Control.Arrow
55
import Control.Monad.Reader
66
import Data.Foldable.Extra (allM)
7-
import Data.Maybe (fromMaybe, isJust)
7+
import Data.Maybe (fromMaybe, isJust, mapMaybe)
88
import qualified Data.Set as S
99
import Development.IDE.GHC.Compat
1010
import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)
11+
import HsDumpAst
1112
import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
1213
import OccName
1314
import TcRnTypes
@@ -27,11 +28,13 @@ mkContext
2728
-> Context
2829
mkContext cfg locals tcg eps kt ev = Context
2930
{ ctxDefiningFuncs = locals
30-
, ctxModuleFuncs = fmap splitId
31-
. (getFunBindId =<<)
32-
. fmap unLoc
33-
. bagToList
34-
$ tcg_binds tcg
31+
, ctxModuleFuncs
32+
= fmap splitId
33+
. mappend (locallyDefinedMethods tcg)
34+
. (getFunBindId =<<)
35+
. fmap unLoc
36+
. bagToList
37+
$ tcg_binds tcg
3538
, ctxConfig = cfg
3639
, ctxInstEnvs =
3740
InstEnvs
@@ -43,6 +46,14 @@ mkContext cfg locals tcg eps kt ev = Context
4346
}
4447

4548

49+
locallyDefinedMethods :: TcGblEnv -> [Id]
50+
locallyDefinedMethods
51+
= foldMap classMethods
52+
. mapMaybe tyConClass_maybe
53+
. tcg_tcs
54+
55+
56+
4657
splitId :: Id -> (OccName, CType)
4758
splitId = occName &&& CType . idType
4859

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ isFunction _ = True
7373
-- context.
7474
tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
7575
tacticsSplitFunTy t
76-
= let (vars, theta, t') = tcSplitSigmaTy t
76+
= let (vars, theta, t') = tcSplitNestedSigmaTys t
7777
(args, res) = tcSplitFunTys t'
7878
in (vars, theta, args, res)
7979

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -229,6 +229,7 @@ provAncestryOf (PatternMatchPrv (PatVal mo so _ _)) =
229229
provAncestryOf (ClassMethodPrv _) = mempty
230230
provAncestryOf UserPrv = mempty
231231
provAncestryOf RecursivePrv = mempty
232+
provAncestryOf ImportPrv = mempty
232233
provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2
233234

234235

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

Lines changed: 46 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
{-# LANGUAGE TypeFamilies #-}
55

66
{-# LANGUAGE NoMonoLocalBinds #-}
7+
{-# LANGUAGE TupleSections #-}
78

89
module Wingman.LanguageServer where
910

@@ -16,6 +17,7 @@ import Control.Monad.State (State, evalState)
1617
import Control.Monad.Trans.Maybe
1718
import Data.Bifunctor (first)
1819
import Data.Coerce
20+
import Data.Foldable (toList)
1921
import Data.Functor ((<&>))
2022
import Data.Functor.Identity (runIdentity)
2123
import qualified Data.HashMap.Strict as Map
@@ -43,6 +45,7 @@ import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
4345
import qualified FastString
4446
import GHC.Generics (Generic)
4547
import Generics.SYB hiding (Generic)
48+
import GhcPlugins (extractModule)
4649
import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
4750
import qualified Ide.Plugin.Config as Plugin
4851
import Ide.Plugin.Properties
@@ -57,13 +60,15 @@ import OccName
5760
import Prelude hiding (span)
5861
import Retrie (transformA)
5962
import SrcLoc (containsSpan)
60-
import TcRnTypes (tcg_binds, TcGblEnv)
63+
import TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env))
6164
import Wingman.Context
6265
import Wingman.FeatureSet
6366
import Wingman.GHC
6467
import Wingman.Judgements
6568
import Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
6669
import Wingman.Judgements.Theta
70+
import Wingman.Machinery (getOccNameType)
71+
import Wingman.Metaprogramming.Lexer (ParserContext(..))
6772
import Wingman.Range
6873
import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
6974
import Wingman.Types
@@ -585,6 +590,7 @@ annotateMetaprograms = everywhereM $ mkM $ \case
585590
pure x
586591
(x :: LHsExpr GhcPs) -> pure x
587592

593+
588594
getMetaprogramAtSpan
589595
:: Tracked age SrcSpan
590596
-> Tracked age TcGblEnv
@@ -596,3 +602,42 @@ getMetaprogramAtSpan (unTrack -> ss)
596602
. tcg_binds
597603
. unTrack
598604

605+
606+
getOccNameTypes
607+
:: Foldable t
608+
=> IdeState
609+
-> NormalizedFilePath
610+
-> t OccName
611+
-> MaybeT IO (M.Map OccName Type)
612+
getOccNameTypes state nfp occs = do
613+
let stale a = runStaleIde "getOccNameTypes" state nfp a
614+
615+
TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck
616+
TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
617+
618+
let tcgblenv = tmrTypechecked tcmod
619+
modul = extractModule tcgblenv
620+
rdrenv = tcg_rdr_env tcgblenv
621+
lift $ fmap M.fromList $
622+
fmap join $ for (toList occs) $ \occ ->
623+
fmap (maybeToList . fmap (occ, )) $
624+
getOccNameType (hscEnv hscenv) rdrenv modul occ
625+
626+
627+
getParserState
628+
:: IdeState
629+
-> NormalizedFilePath
630+
-> Context
631+
-> MaybeT IO ParserContext
632+
getParserState state nfp ctx = do
633+
let stale a = runStaleIde "getOccNameTypes" state nfp a
634+
635+
TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck
636+
TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
637+
638+
let tcgblenv = tmrTypechecked tcmod
639+
modul = extractModule tcgblenv
640+
rdrenv = tcg_rdr_env tcgblenv
641+
642+
pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx
643+

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ module Wingman.LanguageServer.Metaprogram
1010

1111
import Control.Applicative (empty)
1212
import Control.Monad
13+
import Control.Monad.Reader (runReaderT)
1314
import Control.Monad.Trans
1415
import Control.Monad.Trans.Maybe
1516
import Data.List (find)
@@ -30,8 +31,8 @@ import Prelude hiding (span)
3031
import TcRnTypes (tcg_binds)
3132
import Wingman.GHC
3233
import Wingman.Judgements.SYB (metaprogramQ)
33-
import Wingman.Metaprogramming.Parser (attempt_it)
3434
import Wingman.LanguageServer
35+
import Wingman.Metaprogramming.Parser (attempt_it)
3536
import Wingman.Types
3637

3738

@@ -53,12 +54,12 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
5354
Just (trss, program) -> do
5455
let tr_range = fmap realSrcSpanToRange trss
5556
HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
57+
ps <- getParserState state nfp ctx
58+
z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program
5659
pure $ Hover
5760
{ _contents = HoverContents
5861
$ MarkupContent MkMarkdown
59-
$ either T.pack T.pack
60-
$ attempt_it ctx jdg
61-
$ T.unpack program
62+
$ either T.pack T.pack z
6263
, _range = Just $ unTrack tr_range
6364
}
6465
Nothing -> empty

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

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -34,26 +34,28 @@ import Wingman.FeatureSet
3434
import Wingman.GHC
3535
import Wingman.Judgements
3636
import Wingman.Machinery (useNameFromHypothesis)
37+
import Wingman.Metaprogramming.Lexer (ParserContext)
3738
import Wingman.Metaprogramming.Parser (parseMetaprogram)
3839
import Wingman.Tactics
3940
import Wingman.Types
41+
import Control.Monad.Reader (runReaderT)
4042

4143

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

5860

5961
------------------------------------------------------------------------------

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

Lines changed: 45 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ import Data.Ord (Down (..), comparing)
2323
import Data.Set (Set)
2424
import qualified Data.Set as S
2525
import Development.IDE.GHC.Compat
26-
import OccName (HasOccName (occName))
26+
import OccName (HasOccName (occName), OccEnv)
2727
import Refinery.ProofState
2828
import Refinery.Tactic
2929
import Refinery.Tactic.Internal
@@ -33,6 +33,9 @@ import Unify
3333
import Wingman.Judgements
3434
import Wingman.Simplify (simplify)
3535
import Wingman.Types
36+
import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv)
37+
import Development.IDE.Core.Compile (lookupName)
38+
import Control.Applicative (empty)
3639

3740

3841
substCTy :: TCvSubst -> CType -> CType
@@ -315,3 +318,44 @@ useNameFromHypothesis f name = do
315318
Just hi -> f hi
316319
Nothing -> throwError $ NotInScope name
317320

321+
------------------------------------------------------------------------------
322+
-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
323+
-- look it up in the hypothesis.
324+
useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
325+
useNameFromContext f name = do
326+
lookupNameInContext name >>= \case
327+
Just ty -> f $ createImportedHyInfo name ty
328+
Nothing -> throwError $ NotInScope name
329+
330+
331+
lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)
332+
lookupNameInContext name = do
333+
ctx <- asks ctxModuleFuncs
334+
pure $ case find ((== name) . fst) ctx of
335+
Just (_, ty) -> pure ty
336+
Nothing -> empty
337+
338+
339+
createImportedHyInfo :: OccName -> CType -> HyInfo CType
340+
createImportedHyInfo on ty = HyInfo
341+
{ hi_name = on
342+
, hi_provenance = ImportPrv
343+
, hi_type = ty
344+
}
345+
346+
347+
getOccNameType
348+
:: HscEnv
349+
-> OccEnv [GlobalRdrElt]
350+
-> Module
351+
-> OccName
352+
-> IO (Maybe Type)
353+
getOccNameType hscenv rdrenv modul occ =
354+
case lookupOccEnv rdrenv occ of
355+
Just (elt : _) -> do
356+
mvar <- lookupName hscenv modul $ gre_name elt
357+
pure $ case mvar of
358+
Just (AnId v) -> pure $ varType v
359+
_ -> Nothing
360+
_ -> pure Nothing
361+

‎plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,16 +7,29 @@ module Wingman.Metaprogramming.Lexer where
77

88
import Control.Applicative
99
import Control.Monad
10+
import Control.Monad.Reader (ReaderT)
1011
import Data.Text (Text)
1112
import qualified Data.Text as T
1213
import Data.Void
14+
import Development.IDE.GHC.Compat (HscEnv, Module)
15+
import GhcPlugins (GlobalRdrElt)
1316
import Name
1417
import qualified Text.Megaparsec as P
1518
import qualified Text.Megaparsec.Char as P
1619
import qualified Text.Megaparsec.Char.Lexer as L
20+
import Wingman.Types (Context)
21+
22+
23+
data ParserContext = ParserContext
24+
{ ps_hscEnv :: HscEnv
25+
, ps_occEnv :: OccEnv [GlobalRdrElt]
26+
, ps_module :: Module
27+
, ps_context :: Context
28+
}
29+
30+
type Parser = P.ParsecT Void Text (ReaderT ParserContext IO)
1731

1832

19-
type Parser = P.Parsec Void Text
2033

2134
lineComment :: Parser ()
2235
lineComment = L.skipLineComment "--"

0 commit comments

Comments
 (0)