From b070cd1d66fa887272342ef27e6be98fff388c23 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 5 Mar 2021 10:52:51 -0800 Subject: [PATCH 1/2] Make Wingman produce user-facing error messages --- .../src/Ide/Plugin/Tactic.hs | 74 ++++++++++++------- .../src/Ide/Plugin/Tactic/LanguageServer.hs | 6 +- .../src/Ide/Plugin/Tactic/Types.hs | 9 +++ 3 files changed, 63 insertions(+), 26 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index 69c28c7109..b2afe9c7dd 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -19,8 +19,7 @@ import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.Aeson -import Data.Bifunctor (Bifunctor (bimap)) -import Data.Bool (bool) +import Data.Bifunctor (first) import Data.Data (Data) import Data.Foldable (for_) import Data.Generics.Aliases (mkQ) @@ -32,9 +31,7 @@ import Data.Traversable import Development.IDE.Core.Shake (IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.ExactPrint -import Development.Shake.Classes import Ide.Plugin.Tactic.CaseSplit -import Ide.Plugin.Tactic.FeatureSet (Feature (..), hasFeature) import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.LanguageServer import Ide.Plugin.Tactic.LanguageServer.TacticProviders @@ -85,41 +82,70 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) codeActionProvider _ _ _ = pure $ Right $ List [] +showUserFacingMessage + :: MonadLsp cfg m + => UserFacingMessage + -> m (Either ResponseError a) +showUserFacingMessage ufm = do + let msg = ufmMessage ufm + sev = ufmSeverity ufm + showLspMessage sev msg + pure $ Left $ mkErr InternalError msg + + +ufmMessage :: UserFacingMessage -> T.Text +ufmMessage (TacticErrors _) = "Wingman couldn't find a solution" +ufmMessage TimedOut = "Wingman timed out while trying to find a solution" +ufmMessage NothingToDo = "Nothing to do" +ufmMessage (InfrastructureError t) = "Internal error: " <> t + + +ufmSeverity :: UserFacingMessage -> MessageType +ufmSeverity (TacticErrors _) = MtError +ufmSeverity TimedOut = MtInfo +ufmSeverity NothingToDo = MtInfo +ufmSeverity (InfrastructureError _) = MtError + + tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams tacticCmd tac state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do features <- getFeatureSet $ shakeExtras state ccs <- getClientCapabilities - res <- liftIO $ fromMaybeT (Right Nothing) $ do + res <- liftIO $ runMaybeT $ do (range', jdg, ctx, dflags) <- judgementForHole state nfp range features let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp timingOut 2e8 $ join $ - bimap (mkErr InvalidRequest . T.pack . show) - (mkWorkspaceEdits span dflags ccs uri pm) - $ runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name + case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of + Left errs -> Left $ TacticErrors errs + Right rtr -> + case rtr_extract rtr of + L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> + Left NothingToDo + _ -> pure $ mkWorkspaceEdits span dflags ccs uri pm rtr case res of - Left err -> pure $ Left err - Right medit -> do - forM_ medit $ \edit -> - sendRequest - SWorkspaceApplyEdit - (ApplyWorkspaceEditParams Nothing edit) - (const $ pure ()) + Nothing -> do + showUserFacingMessage TimedOut + Just (Left ufm) -> do + showUserFacingMessage ufm + Just (Right edit) -> do + sendRequest + SWorkspaceApplyEdit + (ApplyWorkspaceEditParams Nothing edit) + (const $ pure ()) pure $ Right Null tacticCmd _ _ _ = pure $ Left $ mkErr InvalidRequest "Bad URI" timingOut - :: Int -- ^ Time in microseconds - -> Either ResponseError a -- ^ Computation to run - -> MaybeT IO (Either ResponseError a) -timingOut t m = do - x <- lift $ timeout t $ evaluate m - pure $ joinNote (mkErr InvalidRequest "timed out") x + :: Int -- ^ Time in microseconds + -> a -- ^ Computation to run + -> MaybeT IO a +timingOut t m = MaybeT $ timeout t $ evaluate m mkErr :: ErrorCode -> T.Text -> ResponseError @@ -141,15 +167,13 @@ mkWorkspaceEdits -> Uri -> Annotated ParsedSource -> RunTacticResults - -> Either ResponseError (Maybe WorkspaceEdit) + -> Either UserFacingMessage WorkspaceEdit mkWorkspaceEdits span dflags ccs uri pm rtr = do for_ (rtr_other_solns rtr) $ traceMX "other solution" traceMX "solution" $ rtr_extract rtr let g = graftHole (RealSrcSpan span) rtr response = transform dflags ccs uri g pm - in case response of - Right res -> Right $ Just res - Left err -> Left $ mkErr InternalError $ T.pack err + in first (InfrastructureError . T.pack) response ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 916aebed53..fd5ad7c3b8 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -47,7 +47,7 @@ import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.TestTypes (TacticCommand, cfg_feature_set, emptyConfig, Config) import Ide.Plugin.Tactic.Types -import Language.LSP.Server (MonadLsp) +import Language.LSP.Server (MonadLsp, sendNotification) import Language.LSP.Types import OccName import Prelude hiding (span) @@ -343,3 +343,7 @@ isRhsHole rss tcs = everything (||) (mkQ False $ \case _ -> False ) tcs + +showLspMessage :: MonadLsp cfg m => MessageType -> T.Text -> m () +showLspMessage level t = sendNotification SWindowShowMessage $ ShowMessageParams level t + diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index 92a1f66c88..8b1eff31e4 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -45,6 +45,7 @@ import System.IO.Unsafe (unsafePerformIO) import Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst) import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) +import Data.Text (Text) ------------------------------------------------------------------------------ @@ -391,3 +392,11 @@ data AgdaMatch = AgdaMatch } deriving (Show) + +data UserFacingMessage + = TacticErrors [TacticError] + | TimedOut + | NothingToDo + | InfrastructureError Text + deriving Eq + From b3963105979901534c90f8e75d300a58f11efb84 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 5 Mar 2021 12:09:41 -0800 Subject: [PATCH 2/2] Add a few tests to check the notifications come up --- .../src/Ide/Plugin/Tactic.hs | 22 +++-------------- .../src/Ide/Plugin/Tactic/LanguageServer.hs | 15 ++++++++++-- .../src/Ide/Plugin/Tactic/Types.hs | 8 ++++++- .../test/CodeAction/AutoSpec.hs | 7 +++++- .../test/CodeAction/RefineSpec.hs | 4 ++++ plugins/hls-tactics-plugin/test/Utils.hs | 24 +++++++++++++++++++ .../test/golden/MessageForallA.hs | 2 ++ 7 files changed, 59 insertions(+), 23 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/MessageForallA.hs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index fb1c4dda5b..5aae79cf97 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -86,24 +86,8 @@ showUserFacingMessage => UserFacingMessage -> m (Either ResponseError a) showUserFacingMessage ufm = do - let msg = ufmMessage ufm - sev = ufmSeverity ufm - showLspMessage sev msg - pure $ Left $ mkErr InternalError msg - - -ufmMessage :: UserFacingMessage -> T.Text -ufmMessage (TacticErrors _) = "Wingman couldn't find a solution" -ufmMessage TimedOut = "Wingman timed out while trying to find a solution" -ufmMessage NothingToDo = "Nothing to do" -ufmMessage (InfrastructureError t) = "Internal error: " <> t - - -ufmSeverity :: UserFacingMessage -> MessageType -ufmSeverity (TacticErrors _) = MtError -ufmSeverity TimedOut = MtInfo -ufmSeverity NothingToDo = MtInfo -ufmSeverity (InfrastructureError _) = MtError + showLspMessage $ mkShowMessageParams ufm + pure $ Left $ mkErr InternalError $ T.pack $ show ufm tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams @@ -118,7 +102,7 @@ tacticCmd tac state (TacticParams uri range var_name) timingOut 2e8 $ join $ case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of - Left errs -> Left $ TacticErrors errs + Left _ -> Left TacticErrors Right rtr -> case rtr_extract rtr of L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 84cbc0e148..671d16bffd 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -346,6 +346,17 @@ isRhsHole rss tcs = everything (||) (mkQ False $ \case ) tcs -showLspMessage :: MonadLsp cfg m => MessageType -> T.Text -> m () -showLspMessage level t = sendNotification SWindowShowMessage $ ShowMessageParams level t +ufmSeverity :: UserFacingMessage -> MessageType +ufmSeverity TacticErrors = MtError +ufmSeverity TimedOut = MtInfo +ufmSeverity NothingToDo = MtInfo +ufmSeverity (InfrastructureError _) = MtError + + +mkShowMessageParams :: UserFacingMessage -> ShowMessageParams +mkShowMessageParams ufm = ShowMessageParams (ufmSeverity ufm) $ T.pack $ show ufm + + +showLspMessage :: MonadLsp cfg m => ShowMessageParams -> m () +showLspMessage = sendNotification SWindowShowMessage diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index a4390b8da8..72e4daa823 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -454,9 +454,15 @@ data AgdaMatch = AgdaMatch data UserFacingMessage - = TacticErrors [TacticError] + = TacticErrors | TimedOut | NothingToDo | InfrastructureError Text deriving Eq +instance Show UserFacingMessage where + show TacticErrors = "Wingman couldn't find a solution" + show TimedOut = "Wingman timed out while trying to find a solution" + show NothingToDo = "Nothing to do" + show (InfrastructureError t) = "Internal error: " <> T.unpack t + diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index 7e01a0a2eb..4ee6564da1 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs @@ -10,13 +10,14 @@ module CodeAction.AutoSpec where import Ide.Plugin.Tactic.Types import Test.Hspec import Utils +import Ide.Plugin.Tactic.FeatureSet (allFeatures) spec :: Spec spec = do let autoTest = goldenTest Auto "" - describe "golden tests" $ do + describe "golden" $ do autoTest 11 8 "AutoSplitGADT.hs" autoTest 2 11 "GoldenEitherAuto.hs" autoTest 4 12 "GoldenJoinCont.hs" @@ -52,3 +53,7 @@ spec = do failing "not enough auto gas" $ autoTest 5 18 "GoldenFish.hs" + + describe "messages" $ do + mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA.hs" TacticErrors + diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RefineSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RefineSpec.hs index f779a21947..813f6d60e6 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RefineSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RefineSpec.hs @@ -10,6 +10,7 @@ module CodeAction.RefineSpec where import Ide.Plugin.Tactic.Types import Test.Hspec import Utils +import Ide.Plugin.Tactic.FeatureSet (allFeatures) spec :: Spec @@ -22,3 +23,6 @@ spec = do refineTest 4 8 "RefineReader.hs" refineTest 8 8 "RefineGADT.hs" + describe "messages" $ do + mkShowMessageTest allFeatures Refine "" 2 8 "MessageForallA.hs" NothingToDo + diff --git a/plugins/hls-tactics-plugin/test/Utils.hs b/plugins/hls-tactics-plugin/test/Utils.hs index f11ecb34c6..d0d4a15335 100644 --- a/plugins/hls-tactics-plugin/test/Utils.hs +++ b/plugins/hls-tactics-plugin/test/Utils.hs @@ -20,6 +20,7 @@ import Data.Text (Text) import qualified Data.Text.IO as T import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Tactic.FeatureSet (FeatureSet, allFeatures) +import Ide.Plugin.Tactic.LanguageServer (mkShowMessageParams) import Ide.Plugin.Tactic.Types import Language.LSP.Test import Language.LSP.Types @@ -118,6 +119,29 @@ mkGoldenTest features tc occ line col input = expected <- liftIO $ T.readFile expected_name liftIO $ edited `shouldBe` expected +mkShowMessageTest + :: FeatureSet + -> TacticCommand + -> Text + -> Int + -> Int + -> FilePath + -> UserFacingMessage + -> SpecWith () +mkShowMessageTest features tc occ line col input ufm = + it (input <> " (golden)") $ do + runSession testCommand fullCaps tacticPath $ do + setFeatureSet features + doc <- openDoc input "haskell" + _ <- waitForDiagnostics + actions <- getCodeActions doc $ pointRange line col + Just (InR CodeAction {_command = Just c}) + <- pure $ find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions + executeCommand c + NotificationMessage _ _ err <- skipManyTill anyMessage (message SWindowShowMessage) + liftIO $ err `shouldBe` mkShowMessageParams ufm + + goldenTest :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith () goldenTest = mkGoldenTest allFeatures diff --git a/plugins/hls-tactics-plugin/test/golden/MessageForallA.hs b/plugins/hls-tactics-plugin/test/golden/MessageForallA.hs new file mode 100644 index 0000000000..1498dfd8e4 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/MessageForallA.hs @@ -0,0 +1,2 @@ +test :: a +test = _