Open isovector opened 3 years ago
from bgamari:
{-# LANGUAGE CPP #-}
module Plugin where
#if MIN_VERSION_ghc(9,0,0)
import GHC.Tc.Utils.Monad
import GHC.ThToHs (convertToHsExpr)
import GHC.Types.Basic (Origin(..))
import GHC.Utils.Error (MsgDoc)
#elif MIN_VERSION_ghc(8,10,0)
import TcRnMonad as GHC.Tc.Utils.Monad
import GHC.ThToHs (convertToHsExpr)
import RnEnv (lookupOccRn)
import Plugins (Plugin)
import BasicTypes (Origin(..))
import ErrUtils (MsgDoc)
import TcEnv (tcLookupId)
import Annotations
#endif
import GHC
import Language.Haskell.TH.Syntax as TH
resolveTHName :: TypecheckedModule -> TH.Name -> RealSrcSpan -> Ghc (Maybe Id)
resolveTHName tcm th_name src_span = do
hsc_env <- getSession
let (gbl_env, _) = tm_internals_ tcm
(msgs, mb_id) <- liftIO $ GHC.Tc.Utils.Monad.initTcWithGbl hsc_env gbl_env src_span $ do
Right rdr <- pure $ cvtName FromSource undefined th_name
name <- lookupOccRn (unLoc rdr)
tcLookupId (unLoc name)
return mb_id
cvtName :: Origin -> SrcSpan -> TH.Name -> Either MsgDoc (Located GHC.RdrName)
cvtName origin span v =
fmap (f . unLoc) (convertToHsExpr origin span (VarE v))
where
f (HsVar _ v') = v'
f _ = error "this shouldn't happen"
Inspiration could also be taken from Tritlos work - e.g. writing names in holes (this is also how you "add names to scope" for Agdas auto
)?
Also this mr - https://gitlab.haskell.org/ghc/ghc/-/merge_requests/1766, which is unfortunately not ready yet.
Inspiration could also be taken from Tritlos work - e.g. writing names in holes (this is also how you "add names to scope" for Agdas
auto
)?Also this mr - https://gitlab.haskell.org/ghc/ghc/-/merge_requests/1766, which is unfortunately not ready yet.
Yes! Unfortunately, that MR requires a change in syntax, which means going through the whole GHC proposal process first. Though I've since worked on hole-fit plugins and now have a running use case, so I'll pick this thread up again soon!
Let users decide which functions are in scope when running auto.
Maybe we could use a module level annotation with TH names?