From 032ca664af438ed3c273606f616dadf5117f3ada Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 14:36:13 -0700 Subject: [PATCH 01/13] 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 1ed89d8d56d6d57180bf895af93bdd206b2865d2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 15:49:58 -0700 Subject: [PATCH 02/13] Cata and collapse --- .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 23 +++++++++++ .../src/Wingman/Judgements.hs | 12 ++++++ .../src/Wingman/Machinery.hs | 12 ++++-- .../src/Wingman/Metaprogramming/Parser.hs | 2 + .../hls-tactics-plugin/src/Wingman/Tactics.hs | 41 ++++++++++++++++++- 5 files changed, 85 insertions(+), 5 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 091c2adc90..5c2a7486c1 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -39,6 +39,7 @@ import Wingman.Judgements.Theta import Wingman.Machinery import Wingman.Naming import Wingman.Types +import GHC.SourceGen (occNameToStr) destructMatches @@ -274,3 +275,25 @@ mkApply occ (lhs : rhs : more) = noLoc $ foldl' (@@) (op lhs (coerceName occ) rhs) more mkApply occ args = noLoc $ foldl' (@@) (var' occ) args + + -- TODO(sandy): it's likely that i've mangled the synthesized from terms +letForEach + :: (OccName -> OccName) + -> (HyInfo CType -> TacticsM ()) + -> Hypothesis CType + -> Judgement + -> RuleM (Synthesized (LHsExpr GhcPs)) +letForEach rename solve hy jdg = do + let g = jGoal jdg + terms <- fmap sequenceA $ for (unHypothesis hy) $ \hi -> do + let name = rename $ hi_name hi + res <- tacticToRule jdg $ solve hi + pure $ fmap (name,) res + let hy' = fmap (g <$) $ syn_val terms + g <- newSubgoal $ introduce (userHypothesis hy') jdg + pure $ g + & #syn_val %~ noLoc + . let' (fmap (\(occ, expr) -> valBind (occNameToStr occ) $ unLoc expr) + $ syn_val terms) + . unLoc + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs index 95a7ed6be2..9cffb87b54 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements.hs @@ -107,6 +107,12 @@ recursiveHypothesis :: [(OccName, a)] -> Hypothesis a recursiveHypothesis = introduceHypothesis $ const $ const RecursivePrv +------------------------------------------------------------------------------ +-- | Introduce a binding in a recursive context. +userHypothesis :: [(OccName, a)] -> Hypothesis a +userHypothesis = introduceHypothesis $ const $ const UserPrv + + ------------------------------------------------------------------------------ -- | Check whether any of the given occnames are an ancestor of the term. hasPositionalAncestry @@ -302,6 +308,12 @@ jLocalHypothesis . jHypothesis +------------------------------------------------------------------------------ +-- | Filter elements from the hypothesis +hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a +hyFilter f = Hypothesis . filter f . unHypothesis + + ------------------------------------------------------------------------------ -- | Given a judgment, return the hypotheses that are acceptable to destruct. -- diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 9db2c19c36..6af8dc284e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -3,11 +3,12 @@ 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 (..)) +import Control.Monad.State.Strict (StateT (..), execStateT) import Data.Bool (bool) import Data.Coerce import Data.Either @@ -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 @@ -55,6 +55,10 @@ newSubgoal j = do $ unsetIsTopHole j +tacticToRule :: Judgement -> TacticsM () -> Rule +tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom + + ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index e462a2ef42..0b48ce2b33 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -62,6 +62,8 @@ oneTactic = , nullary "sorry" sorry , nullary "unary" $ nary 1 , nullary "binary" $ nary 2 + , unary_occ "cata" $ useNameFromHypothesis cata + , nullary "collapse" collapse , nullary "recursion" $ fmap listToMaybe getCurrentDefinitions >>= \case Just (self, _) -> useNameFromContext apply self diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index d6bced521a..3571b7422f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -448,7 +448,6 @@ applyByType ty = tracing ("applyByType " <> show ty) $ do let (_, _, args, ret) = tacticsSplitFunTy ty' rule $ \jdg -> do unify g (CType ret) - app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg ext <- fmap unzipTrace $ traverse ( newSubgoal @@ -456,6 +455,7 @@ applyByType ty = tracing ("applyByType " <> show ty) $ do . flip withNewGoal jdg . CType ) args + app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg pure $ fmap noLoc $ foldl' (@@) @@ -467,3 +467,42 @@ nary :: Int -> TacticsM () nary n = do applyByType $ mkInvForAllTys [alphaTyVar, betaTyVar] $ mkFunTys (replicate n alphaTy) betaTy + +self :: TacticsM () +self = + fmap listToMaybe getCurrentDefinitions >>= \case + Just (self, _) -> useNameFromContext apply self + Nothing -> throwError $ TacticPanic "no defining function" + + +cata :: HyInfo CType -> TacticsM () +cata hi = do + diff <- hyDiff $ destruct hi + rule $ + letForEach + (mkVarOcc . flip mappend "_c" . occNameString) + (\hi -> self >> apply hi) + diff + +collapse :: TacticsM () +collapse = do + g <- goal + let terms = unHypothesis $ hyFilter ((jGoal g ==) . hi_type) $ jLocalHypothesis g + case terms of + [hi] -> assume $ hi_name hi + _ -> nary (length terms) <@> fmap (assume . hi_name) terms + + +------------------------------------------------------------------------------ +-- | Determine the difference in hypothesis due to running a tactic. Also, it +-- runs the tactic. +hyDiff :: TacticsM () -> TacticsM (Hypothesis CType) +hyDiff m = do + g <- unHypothesis . jEntireHypothesis <$> goal + let g_len = length g + m + g' <- unHypothesis . jEntireHypothesis <$> goal + pure $ Hypothesis $ take (length g' - g_len) g' + + + From 8ef64184c53ed49c3a18a5654b8048f7a20c618e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:18:42 -0700 Subject: [PATCH 03/13] Remove unused import --- 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 40213cd01a21f4b4ea534ef46d8530ea4809ddb0 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:18:53 -0700 Subject: [PATCH 04/13] Fix bug in intros wrt forall --- plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 3571b7422f..38504cfca5 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -111,9 +111,9 @@ intros' intros' names = rule $ \jdg -> do let g = jGoal jdg ctx <- ask - case tcSplitFunTys $ unCType g of - ([], _) -> throwError $ GoalMismatch "intros" g - (as, b) -> do + case tacticsSplitFunTy $ unCType g of + (_, _, [], _) -> throwError $ GoalMismatch "intros" g + (_, _, as, b) -> do let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names num_args = length vs top_hole = isTopHole ctx jdg From b7ca9939d56d55638e0bc88ed69fc7d65726f3f0 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:19:02 -0700 Subject: [PATCH 05/13] Assume a value for cata recursion if necessary --- 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 38504cfca5..85763c7461 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -481,7 +481,7 @@ cata hi = do rule $ letForEach (mkVarOcc . flip mappend "_c" . occNameString) - (\hi -> self >> apply hi) + (\hi -> self >> commit (apply hi) assumption) diff collapse :: TacticsM () From 9eac5ac75f92412f559c0e7be39fe35725bb6347 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:24:22 -0700 Subject: [PATCH 06/13] Add tests --- .../test/CodeAction/RunMetaprogramSpec.hs | 2 ++ .../test/golden/MetaCataCollapse.expected.hs | 14 ++++++++++++++ .../test/golden/MetaCataCollapse.hs | 10 ++++++++++ .../test/golden/MetaCataCollapseUnary.expected.hs | 8 ++++++++ .../test/golden/MetaCataCollapseUnary.hs | 8 ++++++++ 5 files changed, 42 insertions(+) create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.hs diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index 17750c93ca..a3d8ab0c8d 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs @@ -28,4 +28,6 @@ spec = do metaTest 2 32 "MetaBindAll" metaTest 2 13 "MetaTry" metaTest 2 74 "MetaChoice" + metaTest 9 38 "MetaCataCollapse" + metaTest 7 16 "MetaCataCollapseUnary" diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs new file mode 100644 index 0000000000..be8310b97f --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE TypeOperators #-} + +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f, Yo g) => Yo (f :*: g) where + yo (fx :*: gx) + = let + fx_c = yo fx + gx_c = yo gx + in _ fx_c gx_c + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.hs new file mode 100644 index 0000000000..14dc163f4d --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE TypeOperators #-} + +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f, Yo g) => Yo (f :*: g) where + yo = [wingman| intros x, cata x, collapse |] + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs new file mode 100644 index 0000000000..b9e7eec00d --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs @@ -0,0 +1,8 @@ +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f) => Yo (M1 _1 _2 f) where + yo (M1 fx) = let fx_c = yo fx in fx_c + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.hs new file mode 100644 index 0000000000..c1abb0acf2 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.hs @@ -0,0 +1,8 @@ +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f) => Yo (M1 _1 _2 f) where + yo = [wingman| intros x, cata x, collapse |] + From 9b5532f9790c658a2c624fe1ebaf54a8a308b92a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:26:19 -0700 Subject: [PATCH 07/13] 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 08/13] 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 09/13] 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 605efe58b63b7584e37fa0c490d014d496a83f56 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 16:53:52 -0700 Subject: [PATCH 10/13] Null case for letForEach --- .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 5c2a7486c1..f242d0c034 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -283,17 +283,20 @@ letForEach -> Hypothesis CType -> Judgement -> RuleM (Synthesized (LHsExpr GhcPs)) -letForEach rename solve hy jdg = do - let g = jGoal jdg - terms <- fmap sequenceA $ for (unHypothesis hy) $ \hi -> do - let name = rename $ hi_name hi - res <- tacticToRule jdg $ solve hi - pure $ fmap (name,) res - let hy' = fmap (g <$) $ syn_val terms - g <- newSubgoal $ introduce (userHypothesis hy') jdg - pure $ g - & #syn_val %~ noLoc - . let' (fmap (\(occ, expr) -> valBind (occNameToStr occ) $ unLoc expr) - $ syn_val terms) - . unLoc +letForEach rename solve (unHypothesis -> hy) jdg = do + case hy of + [] -> newSubgoal jdg + _ -> do + let g = jGoal jdg + terms <- fmap sequenceA $ for hy $ \hi -> do + let name = rename $ hi_name hi + res <- tacticToRule jdg $ solve hi + pure $ fmap (name,) res + let hy' = fmap (g <$) $ syn_val terms + g <- newSubgoal $ introduce (userHypothesis hy') jdg + pure $ g + & #syn_val %~ noLoc + . let' (fmap (\(occ, expr) -> valBind (occNameToStr occ) $ unLoc expr) + $ syn_val terms) + . unLoc From cde1256f907cf7fe7352dfc1c644c82ca68fb196 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 21 May 2021 22:48:29 -0700 Subject: [PATCH 11/13] 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 371e0ab8e3..687956ad81 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -473,7 +473,7 @@ nary :: Int -> TacticsM () nary n = applyByType $ mkInvForAllTys [alphaTyVar, betaTyVar] $ - mkFunTys (replicate n alphaTy) betaTy + mkFunTys' (replicate n alphaTy) betaTy self :: TacticsM () From 934dac0ad7e2c04fbc52847f166328ca861a7400 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 24 May 2021 23:40:09 -0700 Subject: [PATCH 12/13] Simplify away single-use let bindings --- plugins/hls-tactics-plugin/src/Wingman/GHC.hs | 10 ++++++++++ plugins/hls-tactics-plugin/src/Wingman/Simplify.hs | 11 ++++++++++- .../test/golden/MetaCataCollapseUnary.expected.hs | 2 +- 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs index eefadeb003..d79683a55a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs @@ -3,6 +3,7 @@ module Wingman.GHC where +import Bag (bagToList) import ConLike import Control.Applicative (empty) import Control.Monad.State @@ -196,6 +197,15 @@ pattern AMatch ctx pats body <- } +pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs +pattern SingleLet bind pats val expr <- + HsLet _ + (L _ (HsValBinds _ + (ValBinds _ (bagToList -> + [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _))) + (L _ expr) + + ------------------------------------------------------------------------------ -- | A pattern over the otherwise (extremely) messy AST for lambdas. pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs diff --git a/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs b/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs index cbd293715b..882d4dd897 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Simplify.hs @@ -11,7 +11,7 @@ import Development.IDE.GHC.Compat import GHC.SourceGen (var) import GHC.SourceGen.Expr (lambda) import Wingman.CodeGen.Utils -import Wingman.GHC (containsHsVar, fromPatCompat) +import Wingman.GHC (containsHsVar, fromPatCompat, pattern SingleLet) ------------------------------------------------------------------------------ @@ -30,6 +30,7 @@ pattern Lambda pats body <- Lambda pats body = lambda pats body + ------------------------------------------------------------------------------ -- | Simlify an expression. simplify :: LHsExpr GhcPs -> LHsExpr GhcPs @@ -41,6 +42,7 @@ simplify [ simplifyEtaReduce , simplifyRemoveParens , simplifyCompose + , simplifySingleLet ]) @@ -68,6 +70,13 @@ simplifyEtaReduce = mkT $ \case Lambda pats f x -> x +------------------------------------------------------------------------------ +-- | Eliminates the unnecessary binding in @let a = b in a@ +simplifySingleLet :: GenericT +simplifySingleLet = mkT $ \case + SingleLet bind [] val (HsVar _ (L _ a)) | a == bind -> val + x -> x + ------------------------------------------------------------------------------ -- | Perform an eta-reducing function composition. For example, transforms diff --git a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs index b9e7eec00d..e9cef291a3 100644 --- a/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs +++ b/plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs @@ -4,5 +4,5 @@ class Yo f where yo :: f x -> Int instance (Yo f) => Yo (M1 _1 _2 f) where - yo (M1 fx) = let fx_c = yo fx in fx_c + yo (M1 fx) = yo fx From bf3711d0db48717a768fff2e1d77718e0df8d57f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 08:33:53 -0700 Subject: [PATCH 13/13] Use the applicative instance to implement letForEach --- .../hls-tactics-plugin/src/Wingman/CodeGen.hs | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index f242d0c034..8795f14944 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -276,12 +276,14 @@ mkApply occ (lhs : rhs : more) mkApply occ args = noLoc $ foldl' (@@) (var' occ) args - -- TODO(sandy): it's likely that i've mangled the synthesized from terms +------------------------------------------------------------------------------ +-- | Run a tactic over each term in the given 'Hypothesis', binding the results +-- of each in a let expression. letForEach - :: (OccName -> OccName) - -> (HyInfo CType -> TacticsM ()) - -> Hypothesis CType - -> Judgement + :: (OccName -> OccName) -- ^ How to name bound variables + -> (HyInfo CType -> TacticsM ()) -- ^ The tactic to run + -> Hypothesis CType -- ^ Terms to generate bindings for + -> Judgement -- ^ The goal of original hole -> RuleM (Synthesized (LHsExpr GhcPs)) letForEach rename solve (unHypothesis -> hy) jdg = do case hy of @@ -291,12 +293,9 @@ letForEach rename solve (unHypothesis -> hy) jdg = do terms <- fmap sequenceA $ for hy $ \hi -> do let name = rename $ hi_name hi res <- tacticToRule jdg $ solve hi - pure $ fmap (name,) res + pure $ fmap ((name,) . unLoc) res let hy' = fmap (g <$) $ syn_val terms - g <- newSubgoal $ introduce (userHypothesis hy') jdg - pure $ g - & #syn_val %~ noLoc - . let' (fmap (\(occ, expr) -> valBind (occNameToStr occ) $ unLoc expr) - $ syn_val terms) - . unLoc + matches = fmap (fmap (\(occ, expr) -> valBind (occNameToStr occ) expr)) terms + g <- fmap (fmap unLoc) $ newSubgoal $ introduce (userHypothesis hy') jdg + pure $ fmap noLoc $ let' <$> matches <*> g