From b95f9391ed517d3a3ad138203d0a7babfbea4334 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 14 Jun 2021 17:01:05 -0700 Subject: [PATCH 1/3] Move IO out of the Parser and into Tactics where it belongs --- .../hls-tactics-plugin/src/Wingman/Context.hs | 8 ++- .../src/Wingman/LanguageServer.hs | 32 ++---------- .../src/Wingman/LanguageServer/Metaprogram.hs | 4 +- .../Wingman/LanguageServer/TacticProviders.hs | 28 +++++----- .../src/Wingman/Machinery.hs | 34 ++++++------ .../src/Wingman/Metaprogramming/Lexer.hs | 16 +----- .../src/Wingman/Metaprogramming/Parser.hs | 52 ++++++++----------- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 18 +++---- .../hls-tactics-plugin/src/Wingman/Types.hs | 9 +++- .../hls-tactics-plugin/test/AutoTupleSpec.hs | 38 +++++++------- 10 files changed, 99 insertions(+), 140 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs index abe3745118..6afa2575fc 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Context.hs @@ -8,7 +8,7 @@ import Data.Foldable.Extra (allM) import Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import Development.IDE.GHC.Compat -import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env) +import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env, extractModule) import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import OccName import TcRnTypes @@ -23,11 +23,12 @@ mkContext :: Config -> [(OccName, CType)] -> TcGblEnv + -> HscEnv -> ExternalPackageState -> KnownThings -> [Evidence] -> Context -mkContext cfg locals tcg eps kt ev = fix $ \ctx -> +mkContext cfg locals tcg hscenv eps kt ev = fix $ \ctx -> Context { ctxDefiningFuncs = fmap (second $ coerce $ normalizeType ctx) locals @@ -48,6 +49,9 @@ mkContext cfg locals tcg eps kt ev = fix $ \ctx -> (tcVisibleOrphanMods tcg) , ctxKnownThings = kt , ctxTheta = evidenceToThetaType ev + , ctx_hscEnv = hscenv + , ctx_occEnv = tcg_rdr_env tcg + , ctx_module = extractModule tcg } diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index 9b82a97ce0..499a63d180 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -44,7 +44,6 @@ import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi import qualified FastString import GHC.Generics (Generic) import Generics.SYB hiding (Generic) -import GhcPlugins (extractModule) import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS) import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Properties @@ -59,13 +58,12 @@ import OccName import Prelude hiding (span) import Retrie (transformA) import SrcLoc (containsSpan) -import TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env)) +import TcRnTypes (tcg_binds, TcGblEnv) import Wingman.Context import Wingman.GHC import Wingman.Judgements import Wingman.Judgements.SYB (everythingContaining, metaprogramQ) import Wingman.Judgements.Theta -import Wingman.Metaprogramming.Lexer (ParserContext(..)) import Wingman.Range import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax) import Wingman.Types @@ -217,7 +215,7 @@ judgementForHole state nfp range cfg = do eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv kt <- knownThings (untrackedStaleValue tcg) henv - (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt + (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps kt let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t dflags <- getIdeDynflags state nfp @@ -240,10 +238,11 @@ mkJudgementAndContext -> TrackedStale Bindings -> Tracked 'Current RealSrcSpan -> TrackedStale TcGblEnv + -> HscEnv -> ExternalPackageState -> KnownThings -> Maybe (Judgement, Context) -mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do +mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps kt = do binds_rss <- mapAgeFrom bmap rss tcg_rss <- mapAgeFrom tcgmap rss @@ -253,6 +252,7 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm $ unTrack $ getDefiningBindings <$> binds <*> binds_rss) (unTrack tcg) + hscenv eps kt evidence @@ -598,25 +598,3 @@ getMetaprogramAtSpan (unTrack -> ss) . tcg_binds . unTrack - ------------------------------------------------------------------------------- --- | The metaprogram parser needs the ability to lookup terms from the module --- and imports. The 'ParserContext' contains everything we need to find that --- stuff. -getParserState - :: IdeState - -> NormalizedFilePath - -> Context - -> MaybeT IO ParserContext -getParserState state nfp ctx = do - let stale a = runStaleIde "getParserState" state nfp a - - TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck - TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps - - let tcgblenv = tmrTypechecked tcmod - modul = extractModule tcgblenv - rdrenv = tcg_rdr_env tcgblenv - - pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx - diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs index a84d274e24..6b924a8060 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs @@ -10,7 +10,6 @@ module Wingman.LanguageServer.Metaprogram import Control.Applicative (empty) import Control.Monad -import Control.Monad.Reader (runReaderT) import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.List (find) @@ -52,8 +51,7 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr Just (trss, program) -> do let tr_range = fmap realSrcSpanToRange trss HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg - ps <- getParserState state nfp ctx - z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program + z <- liftIO $ attempt_it ctx jdg $ T.unpack program pure $ Hover { _contents = HoverContents $ MarkupContent MkMarkdown diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index a3bcad4c58..414388e79e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -12,7 +12,6 @@ module Wingman.LanguageServer.TacticProviders ) where import Control.Monad -import Control.Monad.Reader (runReaderT) import Data.Aeson import Data.Bool (bool) import Data.Coerce @@ -34,7 +33,6 @@ import Wingman.Auto import Wingman.GHC import Wingman.Judgements import Wingman.Machinery (useNameFromHypothesis) -import Wingman.Metaprogramming.Lexer (ParserContext) import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types @@ -42,19 +40,19 @@ import Wingman.Types ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. -commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ()) -commandTactic _ Auto = pure . const auto -commandTactic _ Intros = pure . const intros -commandTactic _ Destruct = pure . useNameFromHypothesis destruct . mkVarOcc . T.unpack -commandTactic _ DestructPun = pure . useNameFromHypothesis destructPun . mkVarOcc . T.unpack -commandTactic _ Homomorphism = pure . useNameFromHypothesis homo . mkVarOcc . T.unpack -commandTactic _ DestructLambdaCase = pure . const destructLambdaCase -commandTactic _ HomomorphismLambdaCase = pure . const homoLambdaCase -commandTactic _ DestructAll = pure . const destructAll -commandTactic _ UseDataCon = pure . userSplit . mkVarOcc . T.unpack -commandTactic _ Refine = pure . const refine -commandTactic _ BeginMetaprogram = pure . const metaprogram -commandTactic c RunMetaprogram = flip runReaderT c . parseMetaprogram +commandTactic :: TacticCommand -> T.Text -> TacticsM () +commandTactic Auto = const auto +commandTactic Intros = const intros +commandTactic Destruct = useNameFromHypothesis destruct . mkVarOcc . T.unpack +commandTactic DestructPun = useNameFromHypothesis destructPun . mkVarOcc . T.unpack +commandTactic Homomorphism = useNameFromHypothesis homo . mkVarOcc . T.unpack +commandTactic DestructLambdaCase = const destructLambdaCase +commandTactic HomomorphismLambdaCase = const homoLambdaCase +commandTactic DestructAll = const destructAll +commandTactic UseDataCon = userSplit . mkVarOcc . T.unpack +commandTactic Refine = const refine +commandTactic BeginMetaprogram = const metaprogram +commandTactic RunMetaprogram = parseMetaprogram ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 0c26c62449..95b65d40c2 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -26,7 +26,7 @@ import qualified Data.Set as S import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType) -import OccName (HasOccName (occName), OccEnv) +import OccName (HasOccName (occName)) import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal @@ -69,8 +69,8 @@ runTactic :: Context -> Judgement -> TacticsM () -- ^ Tactic to use - -> Either [TacticError] RunTacticResults -runTactic ctx jdg t = + -> IO (Either [TacticError] RunTacticResults) +runTactic ctx jdg t = do let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ (:) (jGoal jdg) @@ -82,10 +82,10 @@ runTactic ctx jdg t = defaultTacticState { ts_skolems = skolems } - in case partitionEithers - . flip runReader ctx - . unExtractM - $ runTacticT t jdg tacticState of + res <- flip runReaderT ctx + . unExtractM + $ runTacticT t jdg tacticState + pure $ case partitionEithers res of (errs, []) -> Left $ take 50 errs (_, fmap assoc23 -> solns) -> do let sorted = @@ -360,17 +360,15 @@ createImportedHyInfo on ty = HyInfo -- IO, so we only expose this functionality to the parser. Internal Haskell -- code that wants to lookup terms should do it via 'KnownThings'. getOccNameType - :: HscEnv - -> OccEnv [GlobalRdrElt] - -> Module - -> OccName - -> IO (Maybe Type) -getOccNameType hscenv rdrenv modul occ = - case lookupOccEnv rdrenv occ of + :: OccName + -> TacticsM Type +getOccNameType occ = do + ctx <- ask + case lookupOccEnv (ctx_occEnv ctx) occ of Just (elt : _) -> do - mvar <- lookupName hscenv modul $ gre_name elt - pure $ case mvar of + mvar <- lift $ ExtractM $ lift $ lookupName (ctx_hscEnv ctx) (ctx_module ctx) $ gre_name elt + case mvar of Just (AnId v) -> pure $ varType v - _ -> Nothing - _ -> pure Nothing + _ -> throwError $ NotInScope occ + _ -> throwError $ NotInScope occ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs index 3c911b7dcb..2c15cee171 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs @@ -7,30 +7,16 @@ module Wingman.Metaprogramming.Lexer where import Control.Applicative import Control.Monad -import Control.Monad.Reader (ReaderT) import Data.Foldable (asum) import Data.Text (Text) import qualified Data.Text as T import Data.Void -import Development.IDE.GHC.Compat (HscEnv, Module) -import GhcPlugins (GlobalRdrElt) import Name import qualified Text.Megaparsec as P import qualified Text.Megaparsec.Char as P import qualified Text.Megaparsec.Char.Lexer as L -import Wingman.Types (Context) - ------------------------------------------------------------------------------- --- | Everything we need in order to call 'Wingman.Machinery.getOccNameType'. -data ParserContext = ParserContext - { ps_hscEnv :: HscEnv - , ps_occEnv :: OccEnv [GlobalRdrElt] - , ps_module :: Module - , ps_context :: Context - } - -type Parser = P.ParsecT Void Text (ReaderT ParserContext IO) +type Parser = P.Parsec Void Text diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index a2f503109d..2fb206009b 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -8,11 +8,10 @@ module Wingman.Metaprogramming.Parser where import qualified Control.Monad.Combinators.Expr as P import qualified Control.Monad.Error.Class as E -import Control.Monad.Reader (ReaderT, ask, MonadIO (liftIO), asks) +import Control.Monad.Reader (ask) import Data.Functor import Data.Maybe (listToMaybe) import qualified Data.Text as T -import GhcPlugins (occNameString) import qualified Refinery.Tactic as R import qualified Text.Megaparsec as P import Wingman.Auto @@ -298,12 +297,12 @@ commands = , command "use" Deterministic (Ref One) "Apply the given function from *module* scope." - ( \occ -> do - ctx <- asks ps_context + ( \occ -> pure $ do + ctx <- ask ty <- case lookupNameInContext occ ctx of Just ty -> pure ty - Nothing -> CType <$> getOccTy occ - pure $ apply $ createImportedHyInfo occ ty + Nothing -> CType <$> getOccNameType occ + apply $ createImportedHyInfo occ ty ) [ Example (Just "`import Data.Char (isSpace)`") @@ -392,33 +391,24 @@ attempt_it :: Context -> Judgement -> String - -> ReaderT ParserContext IO (Either String String) + -> IO (Either String String) attempt_it ctx jdg program = - P.runParserT tacticProgram "" (T.pack program) <&> \case - Left peb -> Left $ wrapError $ P.errorBundlePretty peb - Right tt -> do - case runTactic - ctx - jdg - tt - of - Left tes -> Left $ wrapError $ show tes - Right rtr -> Right $ layout $ proofState rtr - - -parseMetaprogram :: T.Text -> ReaderT ParserContext IO (TacticsM ()) + case P.runParser tacticProgram "" (T.pack program) of + Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty peb + Right tt -> do + res <- runTactic + ctx + jdg + tt + pure $ case res of + Left tes -> Left $ wrapError $ show tes + Right rtr -> Right $ layout $ proofState rtr + + +parseMetaprogram :: T.Text -> TacticsM () parseMetaprogram - = fmap (either (const $ pure ()) id) - . P.runParserT tacticProgram "" - - ------------------------------------------------------------------------------- --- | Like 'getOccNameType', but runs in the 'Parser' monad. -getOccTy :: OccName -> Parser Type -getOccTy occ = do - ParserContext hscenv rdrenv modul _ <- ask - mty <- liftIO $ getOccNameType hscenv rdrenv modul occ - maybe (fail $ occNameString occ <> " is not in scope") pure mty + = either (const $ pure ()) id + . P.runParser tacticProgram "" ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 6967f5ac5a..24cfe13352 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -8,7 +8,6 @@ module Wingman.Plugin , TacticCommand (..) ) where -import Control.Exception (evaluate) import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe @@ -40,7 +39,6 @@ import Wingman.Range import Wingman.StaticPlugin import Wingman.Tactics import Wingman.Types -import Wingman.Metaprogramming.Lexer (ParserContext) descriptor :: PluginId -> PluginDescriptor IdeState @@ -51,7 +49,7 @@ descriptor plId = (defaultPluginDescriptor plId) PluginCommand (tcCommandId tc) (tacticDesc $ tcCommandName tc) - (tacticCmd (flip commandTactic tc) plId)) + (tacticCmd (commandTactic tc) plId)) [minBound .. maxBound] , pure $ PluginCommand @@ -102,7 +100,7 @@ showUserFacingMessage ufm = do tacticCmd - :: (ParserContext -> T.Text -> IO (TacticsM ())) + :: (T.Text -> TacticsM ()) -> PluginId -> CommandFunction IdeState TacticParams tacticCmd tac pId state (TacticParams uri range var_name) @@ -116,11 +114,11 @@ tacticCmd tac pId state (TacticParams uri range var_name) let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range TrackedStale pm pmmap <- stale GetAnnotatedParsedSource pm_span <- liftMaybe $ mapAgeFrom pmmap span - pc <- getParserState state nfp hj_ctx - t <- liftIO $ tac pc var_name + let t = tac var_name - timingOut (cfg_timeout_seconds cfg * seconds) $ join $ - case runTactic hj_ctx hj_jdg t of + timingOut (cfg_timeout_seconds cfg * seconds) $ do + res <- liftIO $ runTactic hj_ctx hj_jdg t + pure $ join $ case res of Left errs -> do traceMX "errs" errs Left TacticErrors @@ -153,9 +151,9 @@ seconds = 1e6 timingOut :: Int -- ^ Time in microseconds - -> a -- ^ Computation to run + -> IO a -- ^ Computation to run -> MaybeT IO a -timingOut t m = MaybeT $ timeout t $ evaluate m +timingOut t m = MaybeT $ timeout t m mkErr :: ErrorCode -> T.Text -> ResponseError diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index 4c4c424600..698c647e05 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -33,6 +33,7 @@ import Development.IDE.GHC.Orphans () import FamInstEnv (FamInstEnvs) import GHC.Generics import GHC.SourceGen (var) +import GhcPlugins (GlobalRdrElt) import InstEnv (InstEnvs(..)) import OccName import Refinery.Tactic @@ -302,7 +303,7 @@ data Judgement' a = Judgement type Judgement = Judgement' CType -newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } +newtype ExtractM a = ExtractM { unExtractM :: ReaderT Context IO a } deriving newtype (Functor, Applicative, Monad, MonadReader Context) ------------------------------------------------------------------------------ @@ -422,6 +423,9 @@ data Context = Context , ctxInstEnvs :: InstEnvs , ctxFamInstEnvs :: FamInstEnvs , ctxTheta :: Set CType + , ctx_hscEnv :: HscEnv + , ctx_occEnv :: OccEnv [GlobalRdrElt] + , ctx_module :: Module } instance Show Context where @@ -454,6 +458,9 @@ emptyContext , ctxFamInstEnvs = mempty , ctxInstEnvs = InstEnvs mempty mempty mempty , ctxTheta = mempty + , ctx_hscEnv = error "empty hsc env from emptyContext" + , ctx_occEnv = emptyOccEnv + , ctx_module = error "empty module from emptyContext" } diff --git a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs index a2c7caec7c..a617683d6e 100644 --- a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs +++ b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs @@ -2,17 +2,18 @@ module AutoTupleSpec where -import Data.Either (isRight) -import Wingman.Judgements (mkFirstJudgement) -import Wingman.Machinery -import Wingman.Tactics (auto') -import Wingman.Types -import OccName (mkVarOcc) -import Test.Hspec -import Test.QuickCheck -import Type (mkTyVarTy) -import TysPrim (alphaTyVars) -import TysWiredIn (mkBoxedTupleTy) +import Data.Either (isRight) +import OccName (mkVarOcc) +import System.IO.Unsafe +import Test.Hspec +import Test.QuickCheck +import Type (mkTyVarTy) +import TysPrim (alphaTyVars) +import TysWiredIn (mkBoxedTupleTy) +import Wingman.Judgements (mkFirstJudgement) +import Wingman.Machinery +import Wingman.Tactics (auto') +import Wingman.Types spec :: Spec @@ -33,14 +34,15 @@ spec = describe "auto for tuple" $ do <$> randomGroups vars pure $ -- We should always be able to find a solution - runTactic - emptyContext - (mkFirstJudgement + unsafePerformIO + (runTactic emptyContext - (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type) - True - out_type) - (auto' $ n * 2) `shouldSatisfy` isRight + (mkFirstJudgement + emptyContext + (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type) + True + out_type) + (auto' $ n * 2)) `shouldSatisfy` isRight randomGroups :: [a] -> Gen [[a]] From 865a4959061626b29060e1cea3eca6b3b1b4b575 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 14 Jun 2021 17:31:09 -0700 Subject: [PATCH 2/3] Remove KnownThings, since we can look it up in IO now --- .../hls-tactics-plugin/src/Wingman/Context.hs | 17 +--- .../src/Wingman/EmptyCase.hs | 1 - plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 73 ++++++++-------- .../src/Wingman/Judgements/Theta.hs | 2 +- .../src/Wingman/KnownStrategies.hs | 12 ++- .../src/Wingman/LanguageServer.hs | 7 +- .../src/Wingman/Machinery.hs | 83 +++++++++---------- .../hls-tactics-plugin/src/Wingman/Types.hs | 10 --- .../test/UnificationSpec.hs | 2 +- 9 files changed, 84 insertions(+), 123 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs index 6afa2575fc..64b81631da 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Context.hs @@ -25,10 +25,9 @@ mkContext -> TcGblEnv -> HscEnv -> ExternalPackageState - -> KnownThings -> [Evidence] -> Context -mkContext cfg locals tcg hscenv eps kt ev = fix $ \ctx -> +mkContext cfg locals tcg hscenv eps ev = fix $ \ctx -> Context { ctxDefiningFuncs = fmap (second $ coerce $ normalizeType ctx) locals @@ -47,7 +46,6 @@ mkContext cfg locals tcg hscenv eps kt ev = fix $ \ctx -> (eps_inst_env eps) (tcg_inst_env tcg) (tcVisibleOrphanMods tcg) - , ctxKnownThings = kt , ctxTheta = evidenceToThetaType ev , ctx_hscEnv = hscenv , ctx_occEnv = tcg_rdr_env tcg @@ -79,19 +77,6 @@ getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)] getCurrentDefinitions = asks ctxDefiningFuncs ------------------------------------------------------------------------------- --- | Extract something from 'KnownThings'. -getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a -getKnownThing f = asks $ f . ctxKnownThings - - ------------------------------------------------------------------------------- --- | Like 'getInstance', but uses a class from the 'KnownThings'. -getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType)) -getKnownInstance f tys = do - cls <- getKnownThing f - getInstance cls tys - ------------------------------------------------------------------------------ -- | Determine if there is an instance that exists for the given 'Class' at the diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 4ffc0e6c7a..bcaac35207 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -59,7 +59,6 @@ codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri)) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do let stale a = runStaleIde "codeLensProvider" state nfp a - cfg <- getTacticConfig plId ccs <- getClientCapabilities liftIO $ fromMaybeT (Right $ List []) $ do dflags <- getIdeDynflags state nfp diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index b823b6333f..20a869c1e7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -5,10 +5,10 @@ module Wingman.GHC where import Bag (bagToList) import ConLike -import Control.Applicative (empty) import Control.Monad.State import Control.Monad.Trans.Maybe (MaybeT(..)) import CoreUtils (exprType) +import Data.Bool (bool) import Data.Function (on) import Data.Functor ((<&>)) import Data.List (isPrefixOf) @@ -18,8 +18,6 @@ import Data.Set (Set) import qualified Data.Set as S import Data.Traversable import DataCon -import Development.IDE (HscEnvEq (hscEnv)) -import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat hiding (exprType) import DsExpr (dsExpr) import DsMonad (initDs) @@ -27,16 +25,18 @@ import FamInst (tcLookupDataFamInst_maybe) import FamInstEnv (normaliseType) import GHC.SourceGen (lambda) import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT) -import GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal)) +import GhcPlugins (Role (Nominal)) import OccName import TcRnMonad import TcType import TyCoRep import Type import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon) +import Unify import Unique import Var import Wingman.Types +import Class (classTyVars) tcTyVar_maybe :: Type -> Maybe Var @@ -323,40 +323,6 @@ unXPat (XPat (L _ pat)) = unXPat pat unXPat pat = pat ------------------------------------------------------------------------------- --- | Build a 'KnownThings'. -knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings -knownThings tcg hscenv= do - let cls = knownClass tcg hscenv - KnownThings - <$> cls (mkClsOcc "Semigroup") - <*> cls (mkClsOcc "Monoid") - - ------------------------------------------------------------------------------- --- | Like 'knownThing' but specialized to classes. -knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class -knownClass = knownThing $ \case - ATyCon tc -> tyConClass_maybe tc - _ -> Nothing - - ------------------------------------------------------------------------------- --- | Helper function for defining 'knownThings'. -knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a -knownThing f tcg hscenv occ = do - let modul = extractModule tcg - rdrenv = tcg_rdr_env tcg - - case lookupOccEnv rdrenv occ of - Nothing -> empty - Just elts -> do - mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts - case mvar of - Just tt -> liftMaybe $ f tt - _ -> empty - - liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a @@ -396,3 +362,34 @@ expandTyFam :: Context -> Type -> Type expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal +------------------------------------------------------------------------------ +-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of. +tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst +tryUnifyUnivarsButNotSkolems skolems goal inst = + case tcUnifyTysFG + (bool BindMe Skolem . flip S.member skolems) + [unCType inst] + [unCType goal] of + Unifiable subst -> pure subst + _ -> Nothing + + +updateSubst :: TCvSubst -> TacticState -> TacticState +updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) } + + +------------------------------------------------------------------------------ +-- | Get the class methods of a 'PredType', correctly dealing with +-- instantiation of quantified class types. +methodHypothesis :: PredType -> Maybe [HyInfo CType] +methodHypothesis ty = do + (tc, apps) <- splitTyConApp_maybe ty + cls <- tyConClass_maybe tc + let methods = classMethods cls + tvs = classTyVars cls + subst = zipTvSubst tvs apps + pure $ methods <&> \method -> + let (_, _, ty) = tcSplitSigmaTy $ idType method + in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty + ) + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs index d60526ee5b..622eb4584f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs @@ -32,7 +32,7 @@ import TcEvidence import TcType (substTy) import TcType (tcTyConAppTyCon_maybe) import TysPrim (eqPrimTyCon) -import Wingman.Machinery +import Wingman.GHC import Wingman.Types diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs index 2ad926ce74..913fcd5799 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs @@ -1,15 +1,13 @@ module Wingman.KnownStrategies where -import Control.Applicative (empty) import Control.Monad.Error.Class -import Control.Monad.Reader.Class (asks) import Data.Foldable (for_) -import OccName (mkVarOcc) +import OccName (mkVarOcc, mkClsOcc) import Refinery.Tactic -import Wingman.Context (getCurrentDefinitions, getKnownInstance) +import Wingman.Context (getCurrentDefinitions) import Wingman.Judgements (jGoal) import Wingman.KnownStrategies.QuickCheck (deriveArbitrary) -import Wingman.Machinery (tracing) +import Wingman.Machinery (tracing, getKnownInstance) import Wingman.Tactics import Wingman.Types @@ -57,7 +55,7 @@ deriveMappend = do destructAll split g <- goal - minst <- getKnownInstance kt_semigroup + minst <- getKnownInstance (mkClsOcc "Semigroup") . pure . unCType $ jGoal g @@ -79,7 +77,7 @@ deriveMempty :: TacticsM () deriveMempty = do split g <- goal - minst <- getKnownInstance kt_monoid [unCType $ jGoal g] + minst <- getKnownInstance (mkClsOcc "Monoid") [unCType $ jGoal g] for_ minst $ \(cls, df) -> do applyMethod cls df $ mkVarOcc "mempty" try assumption diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index 499a63d180..125995e992 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -213,9 +213,8 @@ judgementForHole state nfp range cfg = do -- involved, so it's not crucial to track ages. let henv = untrackedStaleValue $ hscenv eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv - kt <- knownThings (untrackedStaleValue tcg) henv - (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps kt + (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t dflags <- getIdeDynflags state nfp @@ -240,9 +239,8 @@ mkJudgementAndContext -> TrackedStale TcGblEnv -> HscEnv -> ExternalPackageState - -> KnownThings -> Maybe (Judgement, Context) -mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps kt = do +mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps = do binds_rss <- mapAgeFrom bmap rss tcg_rss <- mapAgeFrom tcgmap rss @@ -254,7 +252,6 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm (unTrack tcg) hscenv eps - kt evidence top_provs = getRhsPosVals tcg_rss tcs already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 95b65d40c2..f29036a135 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -2,14 +2,13 @@ module Wingman.Machinery where -import Class (Class (classTyVars)) import Control.Applicative (empty) import Control.Lens ((<>~)) import Control.Monad.Error.Class import Control.Monad.Reader import Control.Monad.State.Class (gets, modify) import Control.Monad.State.Strict (StateT (..), execStateT) -import Data.Bool (bool) +import Control.Monad.Trans.Maybe import Data.Coerce import Data.Either import Data.Foldable @@ -21,18 +20,17 @@ import qualified Data.Map as M import Data.Maybe (mapMaybe) import Data.Monoid (getSum) import Data.Ord (Down (..), comparing) -import Data.Set (Set) import qualified Data.Set as S import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType) -import OccName (HasOccName (occName)) import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal import TcType -import Type (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe) -import Unify +import Type (tyCoVarsOfTypeWellScoped) +import Wingman.Context (getInstance) +import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types @@ -204,21 +202,6 @@ newtype Reward a = Reward a deriving (Eq, Ord, Show) via a ------------------------------------------------------------------------------- --- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of. -tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst -tryUnifyUnivarsButNotSkolems skolems goal inst = - case tcUnifyTysFG - (bool BindMe Skolem . flip S.member skolems) - [unCType inst] - [unCType goal] of - Unifiable subst -> pure subst - _ -> Nothing - - -updateSubst :: TCvSubst -> TacticState -> TacticState -updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) } - ------------------------------------------------------------------------------ @@ -244,22 +227,6 @@ attemptWhen _ t2 False = t2 attemptWhen t1 t2 True = commit t1 t2 ------------------------------------------------------------------------------- --- | Get the class methods of a 'PredType', correctly dealing with --- instantiation of quantified class types. -methodHypothesis :: PredType -> Maybe [HyInfo CType] -methodHypothesis ty = do - (tc, apps) <- splitTyConApp_maybe ty - cls <- tyConClass_maybe tc - let methods = classMethods cls - tvs = classTyVars cls - subst = zipTvSubst tvs apps - pure $ methods <&> \method -> - let (_, _, ty) = tcSplitSigmaTy $ idType method - in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty - ) - - ------------------------------------------------------------------------------ -- | Mystical time-traveling combinator for inspecting the extracts produced by -- a tactic. We can use it to guard that extracts match certain predicates, for @@ -355,6 +322,39 @@ createImportedHyInfo on ty = HyInfo } +getTyThing + :: OccName + -> TacticsM (Maybe TyThing) +getTyThing occ = do + ctx <- ask + case lookupOccEnv (ctx_occEnv ctx) occ of + Just (elt : _) -> do + mvar <- lift + $ ExtractM + $ lift + $ lookupName (ctx_hscEnv ctx) (ctx_module ctx) + $ gre_name elt + pure mvar + _ -> pure Nothing + + +------------------------------------------------------------------------------ +-- | Like 'getTyThing' but specialized to classes. +knownClass :: OccName -> TacticsM (Maybe Class) +knownClass occ = + getTyThing occ <&> \case + Just (ATyCon tc) -> tyConClass_maybe tc + _ -> Nothing + + +------------------------------------------------------------------------------ +-- | Like 'getInstance', but uses a class that it just looked up. +getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType)) +getKnownInstance f tys = runMaybeT $ do + cls <- MaybeT $ knownClass f + MaybeT $ getInstance cls tys + + ------------------------------------------------------------------------------ -- | Lookup the type of any 'OccName' that was imported. Necessarily done in -- IO, so we only expose this functionality to the parser. Internal Haskell @@ -363,12 +363,7 @@ getOccNameType :: OccName -> TacticsM Type getOccNameType occ = do - ctx <- ask - case lookupOccEnv (ctx_occEnv ctx) occ of - Just (elt : _) -> do - mvar <- lift $ ExtractM $ lift $ lookupName (ctx_hscEnv ctx) (ctx_module ctx) $ gre_name elt - case mvar of - Just (AnId v) -> pure $ varType v - _ -> throwError $ NotInScope occ + getTyThing occ >>= \case + Just (AnId v) -> pure $ varType v _ -> throwError $ NotInScope occ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index 698c647e05..df61ba50d5 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -419,7 +419,6 @@ data Context = Context , ctxModuleFuncs :: [(OccName, CType)] -- ^ Everything defined in the current module , ctxConfig :: Config - , ctxKnownThings :: KnownThings , ctxInstEnvs :: InstEnvs , ctxFamInstEnvs :: FamInstEnvs , ctxTheta :: Set CType @@ -438,14 +437,6 @@ instance Show Context where ] ------------------------------------------------------------------------------- --- | Things we'd like to look up, that don't exist in TysWiredIn. -data KnownThings = KnownThings - { kt_semigroup :: Class - , kt_monoid :: Class - } - - ------------------------------------------------------------------------------ -- | An empty context emptyContext :: Context @@ -454,7 +445,6 @@ emptyContext { ctxDefiningFuncs = mempty , ctxModuleFuncs = mempty , ctxConfig = emptyConfig - , ctxKnownThings = error "empty known things from emptyContext" , ctxFamInstEnvs = mempty , ctxInstEnvs = InstEnvs mempty mempty mempty , ctxTheta = mempty diff --git a/plugins/hls-tactics-plugin/test/UnificationSpec.hs b/plugins/hls-tactics-plugin/test/UnificationSpec.hs index 7d8d2abd26..c5ce611ec3 100644 --- a/plugins/hls-tactics-plugin/test/UnificationSpec.hs +++ b/plugins/hls-tactics-plugin/test/UnificationSpec.hs @@ -16,7 +16,7 @@ import Test.QuickCheck import Type (mkTyVarTy) import TysPrim (alphaTyVars) import TysWiredIn (mkBoxedTupleTy) -import Wingman.Machinery +import Wingman.GHC import Wingman.Types From 73f51040cfbc20ddd002fcc73c766d78f22688e1 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 14 Jun 2021 17:36:25 -0700 Subject: [PATCH 3/3] Sort imports --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 20a869c1e7..d39ed21587 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -4,6 +4,7 @@ module Wingman.GHC where import Bag (bagToList) +import Class (classTyVars) import ConLike import Control.Monad.State import Control.Monad.Trans.Maybe (MaybeT(..)) @@ -36,7 +37,6 @@ import Unify import Unique import Var import Wingman.Types -import Class (classTyVars) tcTyVar_maybe :: Type -> Maybe Var