From 032ca664af438ed3c273606f616dadf5117f3ada Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 14:36:13 -0700 Subject: [PATCH 1/6] Perform lookups of terms in scope and context --- .../hls-tactics-plugin/src/Wingman/Context.hs | 23 +++++-- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 2 +- .../src/Wingman/Judgements.hs | 1 + .../src/Wingman/LanguageServer.hs | 47 +++++++++++++- .../src/Wingman/LanguageServer/Metaprogram.hs | 9 +-- .../Wingman/LanguageServer/TacticProviders.hs | 28 ++++---- .../src/Wingman/Machinery.hs | 46 ++++++++++++- .../src/Wingman/Metaprogramming/Lexer.hs | 15 ++++- .../src/Wingman/Metaprogramming/Parser.hs | 65 ++++++++++++++----- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 9 ++- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 34 +++++++++- .../hls-tactics-plugin/src/Wingman/Types.hs | 11 ++++ 12 files changed, 243 insertions(+), 47 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs index 4ca76efb34..55f3920353 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Context.hs @@ -4,10 +4,11 @@ import Bag import Control.Arrow import Control.Monad.Reader import Data.Foldable.Extra (allM) -import Data.Maybe (fromMaybe, isJust) +import Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import Development.IDE.GHC.Compat import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys) +import HsDumpAst import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import OccName import TcRnTypes @@ -27,11 +28,13 @@ mkContext -> Context mkContext cfg locals tcg eps kt ev = Context { ctxDefiningFuncs = locals - , ctxModuleFuncs = fmap splitId - . (getFunBindId =<<) - . fmap unLoc - . bagToList - $ tcg_binds tcg + , ctxModuleFuncs + = fmap splitId + . mappend (locallyDefinedMethods tcg) + . (getFunBindId =<<) + . fmap unLoc + . bagToList + $ tcg_binds tcg , ctxConfig = cfg , ctxInstEnvs = InstEnvs @@ -43,6 +46,14 @@ mkContext cfg locals tcg eps kt ev = Context } +locallyDefinedMethods :: TcGblEnv -> [Id] +locallyDefinedMethods + = foldMap classMethods + . mapMaybe tyConClass_maybe + . tcg_tcs + + + splitId :: Id -> (OccName, CType) splitId = occName &&& CType . idType diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index 30ad63bd57..eefadeb003 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -73,7 +73,7 @@ isFunction _ = True -- context. tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type) tacticsSplitFunTy t - = let (vars, theta, t') = tcSplitSigmaTy t + = let (vars, theta, t') = tcSplitNestedSigmaTys t (args, res) = tcSplitFunTys t' in (vars, theta, args, res) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index 27cc02e953..95a7ed6be2 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs @@ -229,6 +229,7 @@ provAncestryOf (PatternMatchPrv (PatVal mo so _ _)) = provAncestryOf (ClassMethodPrv _) = mempty provAncestryOf UserPrv = mempty provAncestryOf RecursivePrv = mempty +provAncestryOf ImportPrv = mempty provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2 diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index 9c3372a880..cca739d5f6 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -4,6 +4,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE NoMonoLocalBinds #-} +{-# LANGUAGE TupleSections #-} module Wingman.LanguageServer where @@ -16,6 +17,7 @@ import Control.Monad.State (State, evalState) import Control.Monad.Trans.Maybe import Data.Bifunctor (first) import Data.Coerce +import Data.Foldable (toList) import Data.Functor ((<&>)) import Data.Functor.Identity (runIdentity) import qualified Data.HashMap.Strict as Map @@ -43,6 +45,7 @@ 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 @@ -57,13 +60,15 @@ import OccName import Prelude hiding (span) import Retrie (transformA) import SrcLoc (containsSpan) -import TcRnTypes (tcg_binds, TcGblEnv) +import TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env)) import Wingman.Context import Wingman.FeatureSet import Wingman.GHC import Wingman.Judgements import Wingman.Judgements.SYB (everythingContaining, metaprogramQ) import Wingman.Judgements.Theta +import Wingman.Machinery (getOccNameType) +import Wingman.Metaprogramming.Lexer (ParserContext(..)) import Wingman.Range import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax) import Wingman.Types @@ -585,6 +590,7 @@ annotateMetaprograms = everywhereM $ mkM $ \case pure x (x :: LHsExpr GhcPs) -> pure x + getMetaprogramAtSpan :: Tracked age SrcSpan -> Tracked age TcGblEnv @@ -596,3 +602,42 @@ getMetaprogramAtSpan (unTrack -> ss) . tcg_binds . unTrack + +getOccNameTypes + :: Foldable t + => IdeState + -> NormalizedFilePath + -> t OccName + -> MaybeT IO (M.Map OccName Type) +getOccNameTypes state nfp occs = do + let stale a = runStaleIde "getOccNameTypes" 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 + lift $ fmap M.fromList $ + fmap join $ for (toList occs) $ \occ -> + fmap (maybeToList . fmap (occ, )) $ + getOccNameType (hscEnv hscenv) rdrenv modul occ + + +getParserState + :: IdeState + -> NormalizedFilePath + -> Context + -> MaybeT IO ParserContext +getParserState state nfp ctx = do + let stale a = runStaleIde "getOccNameTypes" 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 37e8581928..c54d82973f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs @@ -10,6 +10,7 @@ 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) @@ -30,8 +31,8 @@ import Prelude hiding (span) import TcRnTypes (tcg_binds) import Wingman.GHC import Wingman.Judgements.SYB (metaprogramQ) -import Wingman.Metaprogramming.Parser (attempt_it) import Wingman.LanguageServer +import Wingman.Metaprogramming.Parser (attempt_it) import Wingman.Types @@ -53,12 +54,12 @@ 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 pure $ Hover { _contents = HoverContents $ MarkupContent MkMarkdown - $ either T.pack T.pack - $ attempt_it ctx jdg - $ T.unpack program + $ either T.pack T.pack z , _range = Just $ unTrack tr_range } Nothing -> empty diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index 8c23873726..cad31a0107 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -34,26 +34,28 @@ import Wingman.FeatureSet 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 +import Control.Monad.Reader (runReaderT) ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. -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 +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 ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index d0f5368e47..9db2c19c36 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -23,7 +23,7 @@ import Data.Ord (Down (..), comparing) import Data.Set (Set) import qualified Data.Set as S import Development.IDE.GHC.Compat -import OccName (HasOccName (occName)) +import OccName (HasOccName (occName), OccEnv) import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal @@ -33,6 +33,9 @@ import Unify import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types +import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv) +import Development.IDE.Core.Compile (lookupName) +import Control.Applicative (empty) substCTy :: TCvSubst -> CType -> CType @@ -315,3 +318,44 @@ useNameFromHypothesis f name = do Just hi -> f hi Nothing -> throwError $ NotInScope name +------------------------------------------------------------------------------ +-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to +-- look it up in the hypothesis. +useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a +useNameFromContext f name = do + lookupNameInContext name >>= \case + Just ty -> f $ createImportedHyInfo name ty + Nothing -> throwError $ NotInScope name + + +lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType) +lookupNameInContext name = do + ctx <- asks ctxModuleFuncs + pure $ case find ((== name) . fst) ctx of + Just (_, ty) -> pure ty + Nothing -> empty + + +createImportedHyInfo :: OccName -> CType -> HyInfo CType +createImportedHyInfo on ty = HyInfo + { hi_name = on + , hi_provenance = ImportPrv + , hi_type = ty + } + + +getOccNameType + :: HscEnv + -> OccEnv [GlobalRdrElt] + -> Module + -> OccName + -> IO (Maybe Type) +getOccNameType hscenv rdrenv modul occ = + case lookupOccEnv rdrenv occ of + Just (elt : _) -> do + mvar <- lookupName hscenv modul $ gre_name elt + pure $ case mvar of + Just (AnId v) -> pure $ varType v + _ -> Nothing + _ -> pure Nothing + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs index fb396029a4..15f7d817ea 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs @@ -7,16 +7,29 @@ module Wingman.Metaprogramming.Lexer where import Control.Applicative import Control.Monad +import Control.Monad.Reader (ReaderT) 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) + + +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 lineComment :: Parser () lineComment = L.skipLineComment "--" diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index c9f26aa10a..e462a2ef42 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -7,12 +7,17 @@ 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 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 -import Wingman.Machinery (useNameFromHypothesis) +import Wingman.Context (getCurrentDefinitions) +import Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext) import Wingman.Metaprogramming.Lexer import Wingman.Metaprogramming.ProofState (proofState, layout) import Wingman.Tactics @@ -25,6 +30,9 @@ nullary name tac = identifier name $> tac unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ()) unary_occ name tac = tac <$> (identifier name *> variable) +unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ()) +unary_occM name tac = tac =<< (identifier name *> variable) + variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ()) variadic_occ name tac = tac <$> (identifier name *> P.many variable) @@ -45,12 +53,25 @@ oneTactic = , unary_occ "destruct" $ useNameFromHypothesis destruct , unary_occ "homo" $ useNameFromHypothesis homo , nullary "application" application + , unary_occ "apply_module" $ useNameFromContext apply , unary_occ "apply" $ useNameFromHypothesis apply , nullary "split" split , unary_occ "ctor" userSplit , nullary "obvious" obvious , nullary "auto" auto , nullary "sorry" sorry + , nullary "unary" $ nary 1 + , nullary "binary" $ nary 2 + , nullary "recursion" $ + fmap listToMaybe getCurrentDefinitions >>= \case + Just (self, _) -> useNameFromContext apply self + Nothing -> E.throwError $ TacticPanic "no defining function" + , unary_occM "use" $ \occ -> do + ctx <- asks ps_context + ty <- case lookupNameInContext occ ctx of + Just ty -> pure ty + Nothing -> CType <$> getOccTy occ + pure $ apply $ createImportedHyInfo occ ty ] @@ -83,19 +104,33 @@ wrapError :: String -> String wrapError err = "```\n" <> err <> "\n```\n" -attempt_it :: Context -> Judgement -> String -> Either String String +attempt_it + :: Context + -> Judgement + -> String + -> ReaderT ParserContext IO (Either String String) attempt_it ctx jdg program = - case P.runParser tacticProgram "" $ T.pack program of - 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 -> TacticsM () -parseMetaprogram = either (const $ pure ()) id . P.runParser tacticProgram "" + 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 ()) +parseMetaprogram + = fmap (either (const $ pure ()) id) + . P.runParserT tacticProgram "" + + +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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 9f0c0ecce3..95cb965f7f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -40,6 +40,7 @@ import Wingman.Range import Wingman.StaticPlugin import Wingman.Tactics import Wingman.Types +import Wingman.Metaprogramming.Lexer (ParserContext) descriptor :: PluginId -> PluginDescriptor IdeState @@ -50,7 +51,7 @@ descriptor plId = (defaultPluginDescriptor plId) PluginCommand (tcCommandId tc) (tacticDesc $ tcCommandName tc) - (tacticCmd (commandTactic tc) plId)) + (tacticCmd (flip commandTactic tc) plId)) [minBound .. maxBound] , pure $ PluginCommand @@ -101,7 +102,7 @@ showUserFacingMessage ufm = do tacticCmd - :: (T.Text -> TacticsM ()) + :: (ParserContext -> T.Text -> IO (TacticsM ())) -> PluginId -> CommandFunction IdeState TacticParams tacticCmd tac pId state (TacticParams uri range var_name) @@ -115,9 +116,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 timingOut (cfg_timeout_seconds cfg * seconds) $ join $ - case runTactic hj_ctx hj_jdg $ tac var_name of + case runTactic hj_ctx hj_jdg t of Left _ -> Left TacticErrors Right rtr -> case rtr_extract rtr of diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 6f3d36354b..d6bced521a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -39,6 +39,8 @@ import Wingman.Naming import Wingman.Types import OccName (mkVarOcc) import Wingman.StaticPlugin (pattern MetaprogramSyntax) +import GHC.SourceGen ((@@)) +import TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar) ------------------------------------------------------------------------------ @@ -206,7 +208,7 @@ homoLambdaCase = apply :: HyInfo CType -> TacticsM () -apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do +apply hi = tracing ("apply' " <> show (hi_name hi)) $ do jdg <- goal let g = jGoal jdg ty = unCType $ hi_type hi @@ -394,7 +396,7 @@ auto' n = do try intros choice [ overFunctions $ \fname -> do - apply fname + requireConcreteHole $ apply fname loop , overAlgebraicTerms $ \aname -> do destructAuto aname @@ -437,3 +439,31 @@ applyByName name = do True -> apply hi False -> empty + +applyByType :: Type -> TacticsM () +applyByType ty = tracing ("applyByType " <> show ty) $ do + jdg <- goal + let g = jGoal jdg + ty' <- freshTyvars ty + let (_, _, args, ret) = tacticsSplitFunTy ty' + rule $ \jdg -> do + unify g (CType ret) + app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg + ext + <- fmap unzipTrace + $ traverse ( newSubgoal + . blacklistingDestruct + . flip withNewGoal jdg + . CType + ) args + pure $ + fmap noLoc $ + foldl' (@@) + <$> fmap unLoc app + <*> fmap (fmap unLoc) ext + + +nary :: Int -> TacticsM () +nary n = do + applyByType $ mkInvForAllTys [alphaTyVar, betaTyVar] $ mkFunTys (replicate n alphaTy) betaTy + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index 657b6ad4c8..9665c952e1 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -153,6 +153,12 @@ instance Show TyCon where instance Show ConLike where show = unsafeRender +instance Show (HsBindLR GhcTc GhcTc) where + show = unsafeRender + +instance Show (ABExport GhcTc) where + show = unsafeRender + ------------------------------------------------------------------------------ -- | The state that should be shared between subgoals. Extracts move towards @@ -212,6 +218,8 @@ data Provenance (Uniquely Class) -- ^ Class -- | A binding explicitly written by the user. | UserPrv + -- | A binding explicitly imported by the user. + | ImportPrv -- | The recursive hypothesis. Present only in the context of the recursion -- tactic. | RecursivePrv @@ -326,6 +334,7 @@ data TacticError | UnhelpfulSplit OccName | TooPolymorphic | NotInScope OccName + | TacticPanic String deriving stock (Eq) instance Show TacticError where @@ -364,6 +373,8 @@ instance Show TacticError where "The tactic isn't applicable because the goal is too polymorphic" show (NotInScope name) = "Tried to do something with the out of scope name " <> show name + show (TacticPanic err) = + "PANIC: " <> err ------------------------------------------------------------------------------ From 9b5532f9790c658a2c624fe1ebaf54a8a308b92a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:26:19 -0700 Subject: [PATCH 2/6] Fix imports --- plugins/hls-tactics-plugin/src/Wingman/Context.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs index 55f3920353..dc28198585 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Context.hs @@ -8,7 +8,6 @@ import Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import Development.IDE.GHC.Compat import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys) -import HsDumpAst import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import OccName import TcRnTypes From 53ea1b404a26d4c54546195f941c4c222fc1b6cd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:34:23 -0700 Subject: [PATCH 3/6] Add tests --- .../test/CodeAction/RunMetaprogramSpec.hs | 3 +++ .../test/golden/MetaUseImport.expected.hs | 6 ++++++ .../hls-tactics-plugin/test/golden/MetaUseImport.hs | 6 ++++++ .../test/golden/MetaUseLocal.expected.hs | 7 +++++++ .../hls-tactics-plugin/test/golden/MetaUseLocal.hs | 7 +++++++ .../test/golden/MetaUseMethod.expected.hs | 12 ++++++++++++ .../hls-tactics-plugin/test/golden/MetaUseMethod.hs | 12 ++++++++++++ 7 files changed, 53 insertions(+) create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index 17750c93ca..e2e6c6cca3 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs @@ -28,4 +28,7 @@ spec = do metaTest 2 32 "MetaBindAll" metaTest 2 13 "MetaTry" metaTest 2 74 "MetaChoice" + metaTest 5 40 "MetaUseImport" + metaTest 6 31 "MetaUseLocal" + metaTest 11 11 "MetaUseMethod" diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs new file mode 100644 index 0000000000..c72f18589c --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.expected.hs @@ -0,0 +1,6 @@ +import Data.Char + + +result :: Char -> Bool +result = isAlpha + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs new file mode 100644 index 0000000000..87ac26bbcb --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaUseImport.hs @@ -0,0 +1,6 @@ +import Data.Char + + +result :: Char -> Bool +result = [wingman| intro c, use isAlpha, assume c |] + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs new file mode 100644 index 0000000000..1afee3471a --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.expected.hs @@ -0,0 +1,7 @@ +test :: Int +test = 0 + + +resolve :: Int +resolve = test + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs new file mode 100644 index 0000000000..0f791818d1 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaUseLocal.hs @@ -0,0 +1,7 @@ +test :: Int +test = 0 + + +resolve :: Int +resolve = [wingman| use test |] + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs new file mode 100644 index 0000000000..acf46a75a0 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.expected.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE MultiParamTypeClasses #-} + +class Test where + test :: Int + +instance Test where + test = 10 + + +resolve :: Int +resolve = test + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs new file mode 100644 index 0000000000..4723befd10 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaUseMethod.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE MultiParamTypeClasses #-} + +class Test where + test :: Int + +instance Test where + test = 10 + + +resolve :: Int +resolve = [wingman| use test |] + From f0872f9c22ef6746897972e8aa0aad958a6e0478 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:45:31 -0700 Subject: [PATCH 4/6] Cleanup and haddock --- .../src/Wingman/LanguageServer.hs | 41 +++++++------------ .../src/Wingman/Machinery.hs | 14 +++++-- .../src/Wingman/Metaprogramming/Lexer.hs | 2 + .../src/Wingman/Metaprogramming/Parser.hs | 11 +++++ .../hls-tactics-plugin/src/Wingman/Tactics.hs | 20 ++++++--- .../hls-tactics-plugin/src/Wingman/Types.hs | 6 --- 6 files changed, 52 insertions(+), 42 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index cca739d5f6..c7052a7070 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs @@ -1,10 +1,10 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE NoMonoLocalBinds #-} -{-# LANGUAGE TupleSections #-} module Wingman.LanguageServer where @@ -17,7 +17,6 @@ import Control.Monad.State (State, evalState) import Control.Monad.Trans.Maybe import Data.Bifunctor (first) import Data.Coerce -import Data.Foldable (toList) import Data.Functor ((<&>)) import Data.Functor.Identity (runIdentity) import qualified Data.HashMap.Strict as Map @@ -67,7 +66,6 @@ import Wingman.GHC import Wingman.Judgements import Wingman.Judgements.SYB (everythingContaining, metaprogramQ) import Wingman.Judgements.Theta -import Wingman.Machinery (getOccNameType) import Wingman.Metaprogramming.Lexer (ParserContext(..)) import Wingman.Range import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax) @@ -581,6 +579,10 @@ mkWorkspaceEdits dflags ccs uri pm g = do in first (InfrastructureError . T.pack) response +------------------------------------------------------------------------------ +-- | Add ExactPrint annotations to every metaprogram in the source tree. +-- Usually the ExactPrint module can do this for us, but we've enabled +-- QuasiQuotes, so the round-trip print/parse journey will crash. annotateMetaprograms :: Data a => a -> Transform a annotateMetaprograms = everywhereM $ mkM $ \case L ss (WingmanMetaprogram mp) -> do @@ -591,6 +593,8 @@ annotateMetaprograms = everywhereM $ mkM $ \case (x :: LHsExpr GhcPs) -> pure x +------------------------------------------------------------------------------ +-- | Find the source of a tactic metaprogram at the given span. getMetaprogramAtSpan :: Tracked age SrcSpan -> Tracked age TcGblEnv @@ -603,36 +607,19 @@ getMetaprogramAtSpan (unTrack -> ss) . unTrack -getOccNameTypes - :: Foldable t - => IdeState - -> NormalizedFilePath - -> t OccName - -> MaybeT IO (M.Map OccName Type) -getOccNameTypes state nfp occs = do - let stale a = runStaleIde "getOccNameTypes" 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 - lift $ fmap M.fromList $ - fmap join $ for (toList occs) $ \occ -> - fmap (maybeToList . fmap (occ, )) $ - getOccNameType (hscEnv hscenv) rdrenv modul occ - - +------------------------------------------------------------------------------ +-- | 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 + -> Context -> MaybeT IO ParserContext getParserState state nfp ctx = do - let stale a = runStaleIde "getOccNameTypes" state nfp a + let stale a = runStaleIde "getParserState" state nfp a - TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck + TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps let tcgblenv = tmrTypechecked tcmod diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 9db2c19c36..01d0862164 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -3,6 +3,7 @@ module Wingman.Machinery where import Class (Class (classTyVars)) +import Control.Applicative (empty) import Control.Lens ((<>~)) import Control.Monad.Error.Class import Control.Monad.Reader @@ -22,7 +23,9 @@ 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) import OccName (HasOccName (occName), OccEnv) import Refinery.ProofState import Refinery.Tactic @@ -33,9 +36,6 @@ import Unify import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types -import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv) -import Development.IDE.Core.Compile (lookupName) -import Control.Applicative (empty) substCTy :: TCvSubst -> CType -> CType @@ -328,6 +328,8 @@ useNameFromContext f name = do Nothing -> throwError $ NotInScope name +------------------------------------------------------------------------------ +-- | Find the type of an 'OccName' that is defined in the current module. lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType) lookupNameInContext name = do ctx <- asks ctxModuleFuncs @@ -336,6 +338,8 @@ lookupNameInContext name = do Nothing -> empty +------------------------------------------------------------------------------ +-- | Build a 'HyInfo' for an imported term. createImportedHyInfo :: OccName -> CType -> HyInfo CType createImportedHyInfo on ty = HyInfo { hi_name = on @@ -344,6 +348,10 @@ createImportedHyInfo on ty = HyInfo } +------------------------------------------------------------------------------ +-- | Lookup the type of any 'OccName' that was imported. Necessarily done in +-- 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] diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs index 15f7d817ea..e4d62ca085 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Lexer.hs @@ -20,6 +20,8 @@ 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] diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index e462a2ef42..0eb52007af 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -27,15 +27,21 @@ import Wingman.Types nullary :: T.Text -> TacticsM () -> Parser (TacticsM ()) nullary name tac = identifier name $> tac + unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ()) unary_occ name tac = tac <$> (identifier name *> variable) + +------------------------------------------------------------------------------ +-- | Like 'unary_occ', but runs directly in the 'Parser' monad. unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ()) unary_occM name tac = tac =<< (identifier name *> variable) + variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ()) variadic_occ name tac = tac <$> (identifier name *> P.many variable) + oneTactic :: Parser (TacticsM ()) oneTactic = P.choice @@ -104,6 +110,9 @@ wrapError :: String -> String wrapError err = "```\n" <> err <> "\n```\n" +------------------------------------------------------------------------------ +-- | Attempt to run a metaprogram tactic, returning the proof state, or the +-- errors. attempt_it :: Context -> Judgement @@ -128,6 +137,8 @@ parseMetaprogram . P.runParserT tacticProgram "" +------------------------------------------------------------------------------ +-- | Like 'getOccNameType', but runs in the 'Parser' monad. getOccTy :: OccName -> Parser Type getOccTy occ = do ParserContext hscenv rdrenv modul _ <- ask diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index d6bced521a..8df56bbf26 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -24,23 +24,23 @@ import qualified Data.Set as S import DataCon import Development.IDE.GHC.Compat import GHC.Exts +import GHC.SourceGen ((@@)) import GHC.SourceGen.Expr import Name (occNameString, occName) +import OccName (mkVarOcc) import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) +import TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar) import Wingman.CodeGen import Wingman.Context import Wingman.GHC import Wingman.Judgements import Wingman.Machinery import Wingman.Naming +import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types -import OccName (mkVarOcc) -import Wingman.StaticPlugin (pattern MetaprogramSyntax) -import GHC.SourceGen ((@@)) -import TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar) ------------------------------------------------------------------------------ @@ -440,6 +440,9 @@ applyByName name = do False -> empty +------------------------------------------------------------------------------ +-- | Make a function application where the function being applied itself is +-- a hole. applyByType :: Type -> TacticsM () applyByType ty = tracing ("applyByType " <> show ty) $ do jdg <- goal @@ -463,7 +466,12 @@ applyByType ty = tracing ("applyByType " <> show ty) $ do <*> fmap (fmap unLoc) ext +------------------------------------------------------------------------------ +-- | Make an n-ary function call of the form +-- @(_ :: forall a b. a -> a -> b) _ _@. nary :: Int -> TacticsM () -nary n = do - applyByType $ mkInvForAllTys [alphaTyVar, betaTyVar] $ mkFunTys (replicate n alphaTy) betaTy +nary n = + applyByType $ + mkInvForAllTys [alphaTyVar, betaTyVar] $ + mkFunTys (replicate n alphaTy) betaTy diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index 9665c952e1..bfea1afe4c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -153,12 +153,6 @@ instance Show TyCon where instance Show ConLike where show = unsafeRender -instance Show (HsBindLR GhcTc GhcTc) where - show = unsafeRender - -instance Show (ABExport GhcTc) where - show = unsafeRender - ------------------------------------------------------------------------------ -- | The state that should be shared between subgoals. Extracts move towards From d030befb3da88549743eaf709bb379b82aa838fd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 22:48:54 -0700 Subject: [PATCH 5/6] mkFunTys' --- plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 8df56bbf26..0910968253 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -473,5 +473,5 @@ nary :: Int -> TacticsM () nary n = applyByType $ mkInvForAllTys [alphaTyVar, betaTyVar] $ - mkFunTys (replicate n alphaTy) betaTy + mkFunTys' (replicate n alphaTy) betaTy From 706f4002e7bb543cf182fa588e43d3375f9ecc9a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 22 May 2021 10:16:39 -0700 Subject: [PATCH 6/6] Wrangle some imports for GHC 8.6 --- plugins/hls-tactics-plugin/src/Wingman/Machinery.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 01d0862164..ec6dee3310 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -25,13 +25,13 @@ 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) +import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType) import OccName (HasOccName (occName), OccEnv) import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal import TcType -import Type +import Type (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe) import Unify import Wingman.Judgements import Wingman.Simplify (simplify)