From 6deff15fb735bc998c48931de7d0fea39c1ce5d7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 12 Aug 2021 12:21:08 -0700 Subject: [PATCH 01/26] WIP abstract LSP, take the pain out of writing LSP stuff --- .../src/Wingman/AbstractLSP.hs | 226 ++++++++++++++++++ 1 file changed, 226 insertions(+) create mode 100644 plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs new file mode 100644 index 0000000000..54661dbfb6 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -0,0 +1,226 @@ +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +-- | A plugin that uses tactics to synthesize code +module Wingman.AbstractLSP where + +import Control.Monad (void) +import Control.Monad.IO.Class +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT (MaybeT), mapMaybeT) +import qualified Data.Aeson as A +import Data.Foldable (traverse_) +import Data.Text (Text) +import Development.IDE (IdeState) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.Compat hiding (Target) +import GHC.Generics (Generic) +import qualified Ide.Plugin.Config as Plugin +import Ide.Types +import Language.LSP.Server (LspM, sendRequest) +import qualified Language.LSP.Types as LSP +import Language.LSP.Types hiding (CodeLens, CodeAction) +import Wingman.EmptyCase (fromMaybeT) +import Wingman.LanguageServer (judgementForHole, getTacticConfig, getIdeDynflags) +import Wingman.LanguageServer.TacticProviders +import Wingman.Types + +-- STILL TO DO: +-- +-- generalize c_makeCommand so that it produces a 'b' and a 'Metadata' +-- or maybe attach metadata directly to the continuation +-- +-- implement code lenses +-- +-- and then wire it all up! + + +data Metadata + = CodeActionMetadata + { md_title :: Text + , md_kind :: Text + , md_preferred :: Bool + } + | CodeLensMetadata + { md_title :: Text + } + deriving stock (Eq, Ord, Show) + + +newtype Interaction node = Interaction + { getInteractions :: + LHsBinds GhcTc -> [(Metadata, Continuation node (IO ()))] + } + +data InteractionSort + = CodeAction + | CodeLens + deriving stock (Eq, Ord, Show, Enum, Bounded) + +-- TODO(sandy): a is the data we want to fetch on both sides +-- b is the data we share when synthesizing commands to running them +data Continuation (a :: Target) b = Continuation + { c_interactionSort :: InteractionSort + , c_makeCommand + :: LspEnv + -> TargetArgs a + -- TODO(sandy): wrong type. should be more structured, and then call + -- a high-level function to actually build the command + -- + -- should produce a 'b' + -> IO [Command |? LSP.CodeAction] + , c_runCommand + :: LspEnv + -> TargetArgs a + -> FileContext + -> b + -> MaybeT (LspM Plugin.Config) + (Either [UserFacingMessage] WorkspaceEdit) + } + +data Target = HoleTarget | EmptyCaseTarget + deriving stock (Eq, Ord, Show, Enum, Bounded) + +data FileContext = FileContext + { fc_uri :: Uri + , fc_nfp :: NormalizedFilePath + , fc_range :: Maybe (Tracked 'Current Range) + } + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (A.ToJSON, A.FromJSON) + +deriving anyclass instance A.ToJSON NormalizedFilePath +deriving anyclass instance A.FromJSON NormalizedFilePath +deriving anyclass instance A.ToJSON NormalizedUri +deriving anyclass instance A.FromJSON NormalizedUri + +data LspEnv = LspEnv + { le_ideState :: IdeState + , le_pluginId :: PluginId + , le_dflags :: DynFlags + , le_config :: Config + , le_fileContext :: FileContext + } + +class IsTarget (t :: Target) where + type TargetArgs t + fetchTargetArgs + :: LspEnv + -> MaybeT (LspM Plugin.Config) (TargetArgs t) + +contToCommand :: Continuation a b -> PluginCommand IdeState +contToCommand = undefined + +buildHandlers + :: IsTarget a + => [Continuation a b] + -> PluginHandlers IdeState +buildHandlers cs = + flip foldMap cs $ \c -> + case c_interactionSort c of + CodeAction -> mkPluginHandler STextDocumentCodeAction $ codeActionProvider c + CodeLens -> mkPluginHandler STextDocumentCodeLens $ undefined + +instance IsTarget 'HoleTarget where + type TargetArgs 'HoleTarget = HoleJudgment + fetchTargetArgs LspEnv{..} = do + let FileContext{..} = le_fileContext + range <- MaybeT $ pure fc_range + mapMaybeT liftIO $ judgementForHole le_ideState fc_nfp range le_config + + +runCodeAction + :: forall a b + . IsTarget a + => PluginId + -> Continuation a b + -> CommandFunction IdeState (FileContext, b) +runCodeAction plId cont state (fc, b) = + fromMaybeT (Left undefined) $ do + env <- buildEnv state plId fc + args <- fetchTargetArgs @a env + c_runCommand cont env args fc b >>= \case + Left errs -> + traverse_ showUserFacingMessage errs + Right edits -> + void $ lift $ + sendRequest + SWorkspaceApplyEdit + (ApplyWorkspaceEditParams Nothing edits) + (const $ pure ()) + pure $ Right A.Null + + +showUserFacingMessage :: UserFacingMessage -> MaybeT (LspM Plugin.Config) () +showUserFacingMessage = error "not implemented" + + +buildEnv + :: IdeState + -> PluginId + -> FileContext + -> MaybeT (LspM Plugin.Config) LspEnv +buildEnv state plId fc = do + cfg <- lift $ getTacticConfig plId + dflags <- mapMaybeT liftIO $ getIdeDynflags state $ fc_nfp fc + pure $ LspEnv + { le_ideState = state + , le_pluginId = plId + , le_dflags = dflags + , le_config = cfg + , le_fileContext = fc + } + +codeActionProvider + :: forall target b + . IsTarget target + => Continuation target b + -> PluginMethodHandler IdeState TextDocumentCodeAction +codeActionProvider + c state plId + (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + fromMaybeT (Right $ List []) $ do + let fc = FileContext + { fc_uri = uri + , fc_nfp = nfp + , fc_range = Just $ unsafeMkCurrent range + } + env <- buildEnv state plId fc + args <- fetchTargetArgs @target env + actions <- lift $ liftIO $ c_makeCommand c env args + pure $ Right $ List actions +codeActionProvider _ _ _ _ = pure $ Right $ List [] + + +makeTacticCodeAction + :: TacticCommand + -> Continuation 'HoleTarget b +makeTacticCodeAction cmd = + Continuation CodeAction + (\LspEnv{..} hj -> do + let FileContext{..} = le_fileContext + case fc_range of + Nothing -> do + traceM "Tried to run makeTacticCodeAction but no range was given" + pure [] + Just range -> do + commandProvider cmd $ + -- TODO(sandy): this is stupid. just use the same env + TacticProviderData + { tpd_dflags = le_dflags + , tpd_config = le_config + , tpd_plid = le_pluginId + , tpd_uri = fc_uri + , tpd_range = range + , tpd_jdg = hj_jdg hj + , tpd_hole_sort = hj_hole_sort hj + } + ) undefined + From dc27a6cfb426def392710c7708aa1b320647cd64 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 12 Aug 2021 21:29:36 -0700 Subject: [PATCH 02/26] Finish making commands --- .../src/Wingman/AbstractLSP.hs | 133 +++++++++++------- 1 file changed, 80 insertions(+), 53 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 54661dbfb6..05ead9b562 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -1,10 +1,11 @@ -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + {-# OPTIONS_GHC -Wno-orphans #-} -- | A plugin that uses tactics to synthesize code @@ -28,8 +29,8 @@ import qualified Language.LSP.Types as LSP import Language.LSP.Types hiding (CodeLens, CodeAction) import Wingman.EmptyCase (fromMaybeT) import Wingman.LanguageServer (judgementForHole, getTacticConfig, getIdeDynflags) -import Wingman.LanguageServer.TacticProviders import Wingman.Types +import qualified Data.Text as T -- STILL TO DO: -- @@ -44,19 +45,14 @@ import Wingman.Types data Metadata = CodeActionMetadata { md_title :: Text - , md_kind :: Text + , md_kind :: CodeActionKind , md_preferred :: Bool } | CodeLensMetadata { md_title :: Text } - deriving stock (Eq, Ord, Show) - + deriving stock (Eq, Show) -newtype Interaction node = Interaction - { getInteractions :: - LHsBinds GhcTc -> [(Metadata, Continuation node (IO ()))] - } data InteractionSort = CodeAction @@ -65,8 +61,9 @@ data InteractionSort -- TODO(sandy): a is the data we want to fetch on both sides -- b is the data we share when synthesizing commands to running them -data Continuation (a :: Target) b = Continuation - { c_interactionSort :: InteractionSort +data Continuation sort (a :: Target) b = Continuation + { c_sort :: sort + , c_interactionSort :: InteractionSort , c_makeCommand :: LspEnv -> TargetArgs a @@ -74,7 +71,7 @@ data Continuation (a :: Target) b = Continuation -- a high-level function to actually build the command -- -- should produce a 'b' - -> IO [Command |? LSP.CodeAction] + -> MaybeT (LspM Plugin.Config) [(Metadata, b)] , c_runCommand :: LspEnv -> TargetArgs a @@ -114,18 +111,18 @@ class IsTarget (t :: Target) where :: LspEnv -> MaybeT (LspM Plugin.Config) (TargetArgs t) -contToCommand :: Continuation a b -> PluginCommand IdeState +contToCommand :: Continuation sort a b -> PluginCommand IdeState contToCommand = undefined buildHandlers - :: IsTarget a - => [Continuation a b] + :: (Show sort, IsTarget a, A.ToJSON b ) + => [Continuation sort a b] -> PluginHandlers IdeState buildHandlers cs = flip foldMap cs $ \c -> case c_interactionSort c of CodeAction -> mkPluginHandler STextDocumentCodeAction $ codeActionProvider c - CodeLens -> mkPluginHandler STextDocumentCodeLens $ undefined + CodeLens -> mkPluginHandler STextDocumentCodeLens $ undefined instance IsTarget 'HoleTarget where type TargetArgs 'HoleTarget = HoleJudgment @@ -136,10 +133,10 @@ instance IsTarget 'HoleTarget where runCodeAction - :: forall a b + :: forall sort a b . IsTarget a => PluginId - -> Continuation a b + -> Continuation sort a b -> CommandFunction IdeState (FileContext, b) runCodeAction plId cont state (fc, b) = fromMaybeT (Left undefined) $ do @@ -178,9 +175,9 @@ buildEnv state plId fc = do } codeActionProvider - :: forall target b - . IsTarget target - => Continuation target b + :: forall sort target b + . (Show sort, A.ToJSON b, IsTarget target) + => Continuation sort target b -> PluginMethodHandler IdeState TextDocumentCodeAction codeActionProvider c state plId @@ -194,33 +191,63 @@ codeActionProvider } env <- buildEnv state plId fc args <- fetchTargetArgs @target env - actions <- lift $ liftIO $ c_makeCommand c env args - pure $ Right $ List actions + actions <- c_makeCommand c env args + pure $ Right $ List $ fmap (uncurry $ makeCommands plId $ c_sort c) actions codeActionProvider _ _ _ _ = pure $ Right $ List [] -makeTacticCodeAction - :: TacticCommand - -> Continuation 'HoleTarget b -makeTacticCodeAction cmd = - Continuation CodeAction - (\LspEnv{..} hj -> do - let FileContext{..} = le_fileContext - case fc_range of - Nothing -> do - traceM "Tried to run makeTacticCodeAction but no range was given" - pure [] - Just range -> do - commandProvider cmd $ - -- TODO(sandy): this is stupid. just use the same env - TacticProviderData - { tpd_dflags = le_dflags - , tpd_config = le_config - , tpd_plid = le_pluginId - , tpd_uri = fc_uri - , tpd_range = range - , tpd_jdg = hj_jdg hj - , tpd_hole_sort = hj_hole_sort hj - } - ) undefined +makeCommands + :: (A.ToJSON b, Show sort) + => PluginId + -> sort + -> Metadata + -> b + -> Command |? LSP.CodeAction +makeCommands plId sort (CodeActionMetadata title kind preferred) b = + let cmd_id = CommandId $ T.pack $ show sort + cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] + in InR + $ LSP.CodeAction + { _title = title + , _kind = Just kind + , _diagnostics = Nothing + , _isPreferred = Just preferred + , _disabled = Nothing + , _edit = Nothing + , _command = Just cmd + , _xdata = Nothing + } +makeCommands plId sort (CodeLensMetadata title) b = + let cmd_id = undefined + cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] + range = undefined + -- TODO(sandy): omfg LSP is such an asshole + in undefined -- InR $ LSP.CodeLens range (Just cmd) Nothing + + +-- makeTacticCodeAction +-- :: TacticCommand +-- -> Continuation 'HoleTarget b +-- makeTacticCodeAction cmd = +-- Continuation CodeAction +-- (\LspEnv{..} hj -> do +-- let FileContext{..} = le_fileContext +-- case fc_range of +-- Nothing -> do +-- traceM "Tried to run makeTacticCodeAction but no range was given" +-- pure [] +-- Just range -> do +-- undefined +-- lift $ liftIO $ commandProvider cmd $ +-- -- TODO(sandy): this is stupid. just use the same env +-- TacticProviderData +-- { tpd_dflags = le_dflags +-- , tpd_config = le_config +-- , tpd_plid = le_pluginId +-- , tpd_uri = fc_uri +-- , tpd_range = range +-- , tpd_jdg = hj_jdg hj +-- , tpd_hole_sort = hj_hole_sort hj +-- } +-- ) undefined From bdd7f18260a4ad3909954d91528c902e76fdcb30 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 12 Aug 2021 21:53:13 -0700 Subject: [PATCH 03/26] Separate code lenses and actions --- .../src/Wingman/AbstractLSP.hs | 144 +++++++++++++----- 1 file changed, 103 insertions(+), 41 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 05ead9b562..7181e7a1aa 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -31,26 +31,26 @@ import Wingman.EmptyCase (fromMaybeT) import Wingman.LanguageServer (judgementForHole, getTacticConfig, getIdeDynflags) import Wingman.Types import qualified Data.Text as T +import Data.Tuple.Extra (uncurry3) -- STILL TO DO: --- --- generalize c_makeCommand so that it produces a 'b' and a 'Metadata' --- or maybe attach metadata directly to the continuation --- --- implement code lenses --- --- and then wire it all up! + +-- wire it all up! + + +data Interaction where + Interaction + :: (IsTarget target, Show sort, A.ToJSON b, A.FromJSON b) + => Continuation sort target b + -> Interaction data Metadata - = CodeActionMetadata + = Metadata { md_title :: Text , md_kind :: CodeActionKind , md_preferred :: Bool } - | CodeLensMetadata - { md_title :: Text - } deriving stock (Eq, Show) @@ -59,19 +59,25 @@ data InteractionSort | CodeLens deriving stock (Eq, Ord, Show, Enum, Bounded) +data SynthesizeCommand a b + = SynthesizeCodeAction + ( LspEnv + -> TargetArgs a + -> MaybeT (LspM Plugin.Config) [(Metadata, b)] + ) + | SynthesizeCodeLens + ( LspEnv + -> TargetArgs a + -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] + ) + + + -- TODO(sandy): a is the data we want to fetch on both sides -- b is the data we share when synthesizing commands to running them data Continuation sort (a :: Target) b = Continuation { c_sort :: sort - , c_interactionSort :: InteractionSort - , c_makeCommand - :: LspEnv - -> TargetArgs a - -- TODO(sandy): wrong type. should be more structured, and then call - -- a high-level function to actually build the command - -- - -- should produce a 'b' - -> MaybeT (LspM Plugin.Config) [(Metadata, b)] + , c_makeCommand :: SynthesizeCommand a b , c_runCommand :: LspEnv -> TargetArgs a @@ -115,14 +121,17 @@ contToCommand :: Continuation sort a b -> PluginCommand IdeState contToCommand = undefined buildHandlers - :: (Show sort, IsTarget a, A.ToJSON b ) - => [Continuation sort a b] + :: forall target sort b + . (Show sort, IsTarget target, A.ToJSON b ) + => [Continuation sort target b] -> PluginHandlers IdeState buildHandlers cs = flip foldMap cs $ \c -> - case c_interactionSort c of - CodeAction -> mkPluginHandler STextDocumentCodeAction $ codeActionProvider c - CodeLens -> mkPluginHandler STextDocumentCodeLens $ undefined + case c_makeCommand c of + SynthesizeCodeAction k -> + mkPluginHandler STextDocumentCodeAction $ codeActionProvider @target (c_sort c) k + SynthesizeCodeLens k -> + mkPluginHandler STextDocumentCodeLens $ codeLensProvider @target (c_sort c) k instance IsTarget 'HoleTarget where type TargetArgs 'HoleTarget = HoleJudgment @@ -175,12 +184,16 @@ buildEnv state plId fc = do } codeActionProvider - :: forall sort target b + :: forall target sort b . (Show sort, A.ToJSON b, IsTarget target) - => Continuation sort target b + => sort + -> ( LspEnv + -> TargetArgs target + -> MaybeT (LspM Plugin.Config) [(Metadata, b)] + ) -> PluginMethodHandler IdeState TextDocumentCodeAction codeActionProvider - c state plId + sort k state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do fromMaybeT (Right $ List []) $ do @@ -191,23 +204,54 @@ codeActionProvider } env <- buildEnv state plId fc args <- fetchTargetArgs @target env - actions <- c_makeCommand c env args - pure $ Right $ List $ fmap (uncurry $ makeCommands plId $ c_sort c) actions -codeActionProvider _ _ _ _ = pure $ Right $ List [] + actions <- k env args + pure + $ Right + $ List + $ fmap (InR . uncurry (makeCodeAction plId sort)) actions +codeActionProvider _ _ _ _ _ = pure $ Right $ List [] + + +codeLensProvider + :: forall target sort b + . (Show sort, A.ToJSON b, IsTarget target) + => sort + -> ( LspEnv + -> TargetArgs target + -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] + ) + -> PluginMethodHandler IdeState TextDocumentCodeLens +codeLensProvider + sort k state plId + (CodeLensParams _ _ (TextDocumentIdentifier uri)) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + fromMaybeT (Right $ List []) $ do + let fc = FileContext + { fc_uri = uri + , fc_nfp = nfp + , fc_range = Nothing + } + env <- buildEnv state plId fc + args <- fetchTargetArgs @target env + actions <- k env args + pure + $ Right + $ List + $ fmap (uncurry3 $ makeCodeLens plId sort) actions +codeLensProvider _ _ _ _ _ = pure $ Right $ List [] -makeCommands +makeCodeAction :: (A.ToJSON b, Show sort) => PluginId -> sort -> Metadata -> b - -> Command |? LSP.CodeAction -makeCommands plId sort (CodeActionMetadata title kind preferred) b = + -> LSP.CodeAction +makeCodeAction plId sort (Metadata title kind preferred) b = let cmd_id = CommandId $ T.pack $ show sort cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] - in InR - $ LSP.CodeAction + in LSP.CodeAction { _title = title , _kind = Just kind , _diagnostics = Nothing @@ -217,12 +261,30 @@ makeCommands plId sort (CodeActionMetadata title kind preferred) b = , _command = Just cmd , _xdata = Nothing } -makeCommands plId sort (CodeLensMetadata title) b = - let cmd_id = undefined + +makeCodeLens + :: (A.ToJSON b, Show sort) + => PluginId + -> sort + -> Range + -> Metadata + -> b + -> LSP.CodeLens +makeCodeLens plId sort range (Metadata title _ _) b = + let cmd_id = CommandId $ T.pack $ show sort cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] - range = undefined - -- TODO(sandy): omfg LSP is such an asshole - in undefined -- InR $ LSP.CodeLens range (Just cmd) Nothing + in LSP.CodeLens + { _range = range + , _command = Just cmd + , _xdata = Nothing + } + +-- makeCodeAction plId sort (CodeLensMetadata title) b = +-- let cmd_id = undefined +-- cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] +-- range = undefined +-- -- TODO(sandy): omfg LSP is such an asshole +-- in undefined -- InR $ LSP.CodeLens range (Just cmd) Nothing -- makeTacticCodeAction From f95a9c98cbbc8a5bd11550dded14ddd6bba70be5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 12 Aug 2021 22:07:56 -0700 Subject: [PATCH 04/26] Pull out types --- .../src/Wingman/AbstractLSP.hs | 122 +----------------- .../src/Wingman/AbstractLSP/Types.hs | 106 +++++++++++++++ 2 files changed, 112 insertions(+), 116 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 7181e7a1aa..90aedc0e5c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -1,124 +1,28 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} -{-# OPTIONS_GHC -Wno-orphans #-} - --- | A plugin that uses tactics to synthesize code module Wingman.AbstractLSP where import Control.Monad (void) import Control.Monad.IO.Class import Control.Monad.Trans (lift) -import Control.Monad.Trans.Maybe (MaybeT (MaybeT), mapMaybeT) +import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT) import qualified Data.Aeson as A import Data.Foldable (traverse_) -import Data.Text (Text) +import qualified Data.Text as T +import Data.Tuple.Extra (uncurry3) import Development.IDE (IdeState) import Development.IDE.Core.UseStale -import Development.IDE.GHC.Compat hiding (Target) -import GHC.Generics (Generic) import qualified Ide.Plugin.Config as Plugin import Ide.Types import Language.LSP.Server (LspM, sendRequest) import qualified Language.LSP.Types as LSP import Language.LSP.Types hiding (CodeLens, CodeAction) +import Wingman.AbstractLSP.Types import Wingman.EmptyCase (fromMaybeT) -import Wingman.LanguageServer (judgementForHole, getTacticConfig, getIdeDynflags) +import Wingman.LanguageServer (getTacticConfig, getIdeDynflags) import Wingman.Types -import qualified Data.Text as T -import Data.Tuple.Extra (uncurry3) - --- STILL TO DO: - --- wire it all up! - - -data Interaction where - Interaction - :: (IsTarget target, Show sort, A.ToJSON b, A.FromJSON b) - => Continuation sort target b - -> Interaction - - -data Metadata - = Metadata - { md_title :: Text - , md_kind :: CodeActionKind - , md_preferred :: Bool - } - deriving stock (Eq, Show) - - -data InteractionSort - = CodeAction - | CodeLens - deriving stock (Eq, Ord, Show, Enum, Bounded) - -data SynthesizeCommand a b - = SynthesizeCodeAction - ( LspEnv - -> TargetArgs a - -> MaybeT (LspM Plugin.Config) [(Metadata, b)] - ) - | SynthesizeCodeLens - ( LspEnv - -> TargetArgs a - -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] - ) - - - --- TODO(sandy): a is the data we want to fetch on both sides --- b is the data we share when synthesizing commands to running them -data Continuation sort (a :: Target) b = Continuation - { c_sort :: sort - , c_makeCommand :: SynthesizeCommand a b - , c_runCommand - :: LspEnv - -> TargetArgs a - -> FileContext - -> b - -> MaybeT (LspM Plugin.Config) - (Either [UserFacingMessage] WorkspaceEdit) - } - -data Target = HoleTarget | EmptyCaseTarget - deriving stock (Eq, Ord, Show, Enum, Bounded) - -data FileContext = FileContext - { fc_uri :: Uri - , fc_nfp :: NormalizedFilePath - , fc_range :: Maybe (Tracked 'Current Range) - } - deriving stock (Eq, Ord, Show, Generic) - deriving anyclass (A.ToJSON, A.FromJSON) -deriving anyclass instance A.ToJSON NormalizedFilePath -deriving anyclass instance A.FromJSON NormalizedFilePath -deriving anyclass instance A.ToJSON NormalizedUri -deriving anyclass instance A.FromJSON NormalizedUri - -data LspEnv = LspEnv - { le_ideState :: IdeState - , le_pluginId :: PluginId - , le_dflags :: DynFlags - , le_config :: Config - , le_fileContext :: FileContext - } - -class IsTarget (t :: Target) where - type TargetArgs t - fetchTargetArgs - :: LspEnv - -> MaybeT (LspM Plugin.Config) (TargetArgs t) - -contToCommand :: Continuation sort a b -> PluginCommand IdeState -contToCommand = undefined buildHandlers :: forall target sort b @@ -133,13 +37,6 @@ buildHandlers cs = SynthesizeCodeLens k -> mkPluginHandler STextDocumentCodeLens $ codeLensProvider @target (c_sort c) k -instance IsTarget 'HoleTarget where - type TargetArgs 'HoleTarget = HoleJudgment - fetchTargetArgs LspEnv{..} = do - let FileContext{..} = le_fileContext - range <- MaybeT $ pure fc_range - mapMaybeT liftIO $ judgementForHole le_ideState fc_nfp range le_config - runCodeAction :: forall sort a b @@ -183,6 +80,7 @@ buildEnv state plId fc = do , le_fileContext = fc } + codeActionProvider :: forall target sort b . (Show sort, A.ToJSON b, IsTarget target) @@ -279,14 +177,6 @@ makeCodeLens plId sort range (Metadata title _ _) b = , _xdata = Nothing } --- makeCodeAction plId sort (CodeLensMetadata title) b = --- let cmd_id = undefined --- cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] --- range = undefined --- -- TODO(sandy): omfg LSP is such an asshole --- in undefined -- InR $ LSP.CodeLens range (Just cmd) Nothing - - -- makeTacticCodeAction -- :: TacticCommand -- -> Continuation 'HoleTarget b diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs new file mode 100644 index 0000000000..43f1224635 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -Wno-orphans #-} + +module Wingman.AbstractLSP.Types where + +import Control.Monad.IO.Class +import Control.Monad.Trans.Maybe (MaybeT (MaybeT), mapMaybeT) +import qualified Data.Aeson as A +import Data.Text (Text) +import Development.IDE (IdeState) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.Compat hiding (Target) +import GHC.Generics (Generic) +import qualified Ide.Plugin.Config as Plugin +import Ide.Types +import Language.LSP.Server (LspM) +import Language.LSP.Types hiding (CodeLens, CodeAction) +import Wingman.LanguageServer (judgementForHole) +import Wingman.Types + + +data Interaction where + Interaction + :: (IsTarget target, Show sort, A.ToJSON b, A.FromJSON b) + => Continuation sort target b + -> Interaction + + +data Metadata + = Metadata + { md_title :: Text + , md_kind :: CodeActionKind + , md_preferred :: Bool + } + deriving stock (Eq, Show) + + +data SynthesizeCommand a b + = SynthesizeCodeAction + ( LspEnv + -> TargetArgs a + -> MaybeT (LspM Plugin.Config) [(Metadata, b)] + ) + | SynthesizeCodeLens + ( LspEnv + -> TargetArgs a + -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] + ) + + +data Continuation sort (a :: Target) b = Continuation + { c_sort :: sort + , c_makeCommand :: SynthesizeCommand a b + , c_runCommand + :: LspEnv + -> TargetArgs a + -> FileContext + -> b + -> MaybeT (LspM Plugin.Config) + (Either [UserFacingMessage] WorkspaceEdit) + } + + +data Target = HoleTarget | EmptyCaseTarget + deriving stock (Eq, Ord, Show, Enum, Bounded) + + +data FileContext = FileContext + { fc_uri :: Uri + , fc_nfp :: NormalizedFilePath + , fc_range :: Maybe (Tracked 'Current Range) + } + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (A.ToJSON, A.FromJSON) + +deriving anyclass instance A.ToJSON NormalizedFilePath +deriving anyclass instance A.FromJSON NormalizedFilePath +deriving anyclass instance A.ToJSON NormalizedUri +deriving anyclass instance A.FromJSON NormalizedUri + + +data LspEnv = LspEnv + { le_ideState :: IdeState + , le_pluginId :: PluginId + , le_dflags :: DynFlags + , le_config :: Config + , le_fileContext :: FileContext + } + +class IsTarget (t :: Target) where + type TargetArgs t + fetchTargetArgs + :: LspEnv + -> MaybeT (LspM Plugin.Config) (TargetArgs t) + +instance IsTarget 'HoleTarget where + type TargetArgs 'HoleTarget = HoleJudgment + fetchTargetArgs LspEnv{..} = do + let FileContext{..} = le_fileContext + range <- MaybeT $ pure fc_range + mapMaybeT liftIO $ judgementForHole le_ideState fc_nfp range le_config + From 07763e10749f48dfb6f7201a5e08df8ccabf46cd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 12 Aug 2021 22:34:56 -0700 Subject: [PATCH 05/26] Finalize the abstract API --- .../src/Wingman/AbstractLSP.hs | 49 ++++++++++++------- .../src/Wingman/AbstractLSP/Types.hs | 18 +++---- 2 files changed, 41 insertions(+), 26 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 90aedc0e5c..43dcdaef23 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -25,12 +25,10 @@ import Wingman.Types buildHandlers - :: forall target sort b - . (Show sort, IsTarget target, A.ToJSON b ) - => [Continuation sort target b] + :: [Interaction] -> PluginHandlers IdeState buildHandlers cs = - flip foldMap cs $ \c -> + flip foldMap cs $ \(Interaction (c :: Continuation sort target b)) -> case c_makeCommand c of SynthesizeCodeAction k -> mkPluginHandler STextDocumentCodeAction $ codeActionProvider @target (c_sort c) k @@ -38,6 +36,18 @@ buildHandlers cs = mkPluginHandler STextDocumentCodeLens $ codeLensProvider @target (c_sort c) k +buildCommand + :: PluginId + -> Interaction + -> PluginCommand IdeState +buildCommand plId (Interaction (c :: Continuation sort target b)) = + PluginCommand + { commandId = CommandId $ T.pack $ show (c_sort c) + , commandDesc = T.pack "" + , commandFunc = runCodeAction plId c + } + + runCodeAction :: forall sort a b . IsTarget a @@ -45,19 +55,24 @@ runCodeAction -> Continuation sort a b -> CommandFunction IdeState (FileContext, b) runCodeAction plId cont state (fc, b) = - fromMaybeT (Left undefined) $ do - env <- buildEnv state plId fc - args <- fetchTargetArgs @a env - c_runCommand cont env args fc b >>= \case - Left errs -> - traverse_ showUserFacingMessage errs - Right edits -> - void $ lift $ - sendRequest - SWorkspaceApplyEdit - (ApplyWorkspaceEditParams Nothing edits) - (const $ pure ()) - pure $ Right A.Null + fromMaybeT + (Left $ ResponseError + { _code = InternalError + , _message = T.pack "TODO(sandy)" + , _xdata = Nothing + } ) $ do + env <- buildEnv state plId fc + args <- fetchTargetArgs @a env + c_runCommand cont env args fc b >>= \case + Left errs -> + traverse_ showUserFacingMessage errs + Right edits -> + void $ lift $ + sendRequest + SWorkspaceApplyEdit + (ApplyWorkspaceEditParams Nothing edits) + (const $ pure ()) + pure $ Right A.Null showUserFacingMessage :: UserFacingMessage -> MaybeT (LspM Plugin.Config) () diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs index 43f1224635..4fc1e3614d 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs @@ -1,7 +1,7 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -52,7 +52,7 @@ data SynthesizeCommand a b ) -data Continuation sort (a :: Target) b = Continuation +data Continuation sort a b = Continuation { c_sort :: sort , c_makeCommand :: SynthesizeCommand a b , c_runCommand @@ -65,7 +65,7 @@ data Continuation sort (a :: Target) b = Continuation } -data Target = HoleTarget | EmptyCaseTarget +data HoleTarget = HoleTarget deriving stock (Eq, Ord, Show, Enum, Bounded) @@ -91,14 +91,14 @@ data LspEnv = LspEnv , le_fileContext :: FileContext } -class IsTarget (t :: Target) where +class IsTarget t where type TargetArgs t fetchTargetArgs :: LspEnv -> MaybeT (LspM Plugin.Config) (TargetArgs t) -instance IsTarget 'HoleTarget where - type TargetArgs 'HoleTarget = HoleJudgment +instance IsTarget HoleTarget where + type TargetArgs HoleTarget = HoleJudgment fetchTargetArgs LspEnv{..} = do let FileContext{..} = le_fileContext range <- MaybeT $ pure fc_range From 63816b11a5a0e12e348deadf39dce53e3a5b000a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 12 Aug 2021 23:05:29 -0700 Subject: [PATCH 06/26] Bug fix in JSON; first connected abstract handler --- .../hls-tactics-plugin.cabal | 2 ++ .../src/Wingman/AbstractLSP.hs | 35 ++++++++++++++++--- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 5 ++- 3 files changed, 37 insertions(+), 5 deletions(-) diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index 3d62a50c1e..c1aa501ab9 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -27,6 +27,8 @@ library hs-source-dirs: src exposed-modules: Ide.Plugin.Tactic + Wingman.AbstractLSP + Wingman.AbstractLSP.Types Wingman.Auto Wingman.CaseSplit Wingman.CodeGen diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 43dcdaef23..5a164a333e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -1,7 +1,9 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# OPTIONS_GHC -Wno-orphans #-} -module Wingman.AbstractLSP where +module Wingman.AbstractLSP (buildHandlers, buildCommand, testInteraction) where import Control.Monad (void) import Control.Monad.IO.Class @@ -22,6 +24,8 @@ import Wingman.AbstractLSP.Types import Wingman.EmptyCase (fromMaybeT) import Wingman.LanguageServer (getTacticConfig, getIdeDynflags) import Wingman.Types +import Data.Functor ((<&>)) +import Data.Maybe (fromJust) buildHandlers @@ -121,7 +125,7 @@ codeActionProvider pure $ Right $ List - $ fmap (InR . uncurry (makeCodeAction plId sort)) actions + $ fmap (InR . uncurry (makeCodeAction plId fc sort)) actions codeActionProvider _ _ _ _ _ = pure $ Right $ List [] @@ -157,13 +161,14 @@ codeLensProvider _ _ _ _ _ = pure $ Right $ List [] makeCodeAction :: (A.ToJSON b, Show sort) => PluginId + -> FileContext -> sort -> Metadata -> b -> LSP.CodeAction -makeCodeAction plId sort (Metadata title kind preferred) b = +makeCodeAction plId fc sort (Metadata title kind preferred) b = let cmd_id = CommandId $ T.pack $ show sort - cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] + cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON (fc, b)] in LSP.CodeAction { _title = title , _kind = Just kind @@ -192,6 +197,28 @@ makeCodeLens plId sort range (Metadata title _ _) b = , _xdata = Nothing } +testInteraction :: Continuation String HoleTarget Int +testInteraction = + Continuation + { c_sort = "tactics.test" + , c_makeCommand = SynthesizeCodeAction $ \_ hj -> do + pure $ [0..2] <&> \ix -> (Metadata (T.pack $ "Hello from AbstractLSP: " <> show (_jGoal $ hj_jdg hj)) (CodeActionUnknown $ T.pack "some-kind") False, ix) + , c_runCommand = \_ _ fc n -> do + pure $ Right $ WorkspaceEdit + { _changes = Nothing + , _documentChanges = pure $ pure $ InL $ TextDocumentEdit + { _textDocument = VersionedTextDocumentIdentifier {_uri = fc_uri fc, _version = Just 0} + , _edits = pure $ InL TextEdit + { _range = unTrack $ fromJust $ fc_range fc + , _newText = T.pack $ "yo" <> show n + } + } + , _changeAnnotations = Nothing + } + } + +deriving newtype instance Applicative List + -- makeTacticCodeAction -- :: TacticCommand -- -> Continuation 'HoleTarget b diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 8cd6fa1c9d..257c85fa94 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -33,6 +33,7 @@ import Wingman.EmptyCase import Wingman.GHC import Wingman.Judgements (jNeedsToBindArgs) import Wingman.LanguageServer +import Wingman.AbstractLSP import Wingman.LanguageServer.Metaprogram (hoverProvider) import Wingman.LanguageServer.TacticProviders import Wingman.Machinery (scoreSolution) @@ -40,6 +41,7 @@ import Wingman.Range import Wingman.StaticPlugin import Wingman.Tactics import Wingman.Types +import Wingman.AbstractLSP.Types (Interaction(Interaction)) descriptor :: PluginId -> PluginDescriptor IdeState @@ -57,12 +59,13 @@ descriptor plId = (defaultPluginDescriptor plId) emptyCaseLensCommandId "Complete the empty case" workspaceEditHandler + , pure $ buildCommand plId $ Interaction testInteraction ] , pluginHandlers = mconcat [ mkPluginHandler STextDocumentCodeAction codeActionProvider , mkPluginHandler STextDocumentCodeLens codeLensProvider , mkPluginHandler STextDocumentHover hoverProvider - ] + ] <> buildHandlers [Interaction testInteraction] , pluginRules = wingmanRules plId , pluginConfigDescriptor = defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties} From af54591eba1e093b8057ae236e1bb86836bb5085 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 10:39:21 -0700 Subject: [PATCH 07/26] Add ContinuationResult for better control over how edits work --- .../src/Wingman/AbstractLSP.hs | 73 +++++++++++-------- .../src/Wingman/AbstractLSP/Types.hs | 15 +++- 2 files changed, 56 insertions(+), 32 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 5a164a333e..8fe002b0aa 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -1,7 +1,9 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} + +{-# LANGUAGE NoMonoLocalBinds #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Wingman.AbstractLSP (buildHandlers, buildCommand, testInteraction) where @@ -17,15 +19,17 @@ import Development.IDE (IdeState) import Development.IDE.Core.UseStale import qualified Ide.Plugin.Config as Plugin import Ide.Types -import Language.LSP.Server (LspM, sendRequest) +import Language.LSP.Server (LspM, sendRequest, getClientCapabilities) import qualified Language.LSP.Types as LSP import Language.LSP.Types hiding (CodeLens, CodeAction) import Wingman.AbstractLSP.Types import Wingman.EmptyCase (fromMaybeT) -import Wingman.LanguageServer (getTacticConfig, getIdeDynflags) +import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde) import Wingman.Types import Data.Functor ((<&>)) import Data.Maybe (fromJust) +import Development.IDE.GHC.ExactPrint (GetAnnotatedParsedSource(GetAnnotatedParsedSource)) +import Control.Applicative (empty) buildHandlers @@ -46,7 +50,7 @@ buildCommand -> PluginCommand IdeState buildCommand plId (Interaction (c :: Continuation sort target b)) = PluginCommand - { commandId = CommandId $ T.pack $ show (c_sort c) + { commandId = toCommandId $ c_sort c , commandDesc = T.pack "" , commandFunc = runCodeAction plId c } @@ -58,27 +62,39 @@ runCodeAction => PluginId -> Continuation sort a b -> CommandFunction IdeState (FileContext, b) -runCodeAction plId cont state (fc, b) = +runCodeAction plId cont state (fc, b) = do fromMaybeT (Left $ ResponseError { _code = InternalError , _message = T.pack "TODO(sandy)" , _xdata = Nothing } ) $ do - env <- buildEnv state plId fc + env@LspEnv{..} <- buildEnv state plId fc + let stale a = runStaleIde "runCodeAction" state (fc_nfp le_fileContext) a args <- fetchTargetArgs @a env c_runCommand cont env args fc b >>= \case - Left errs -> + ErrorMessages errs -> traverse_ showUserFacingMessage errs - Right edits -> - void $ lift $ - sendRequest - SWorkspaceApplyEdit - (ApplyWorkspaceEditParams Nothing edits) - (const $ pure ()) + RawEdit edits -> sendEdits edits + GraftEdit gr -> do + ccs <- lift getClientCapabilities + TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of + -- TODO(sandy): fixme + Left _errs -> empty + Right edits -> sendEdits edits pure $ Right A.Null +sendEdits :: WorkspaceEdit -> MaybeT (LspM Plugin.Config) () +sendEdits edits = + void $ lift $ + sendRequest + SWorkspaceApplyEdit + (ApplyWorkspaceEditParams Nothing edits) + (const $ pure ()) + + showUserFacingMessage :: UserFacingMessage -> MaybeT (LspM Plugin.Config) () showUserFacingMessage = error "not implemented" @@ -102,16 +118,15 @@ buildEnv state plId fc = do codeActionProvider :: forall target sort b - . (Show sort, A.ToJSON b, IsTarget target) + . (IsContinuationSort sort, A.ToJSON b, IsTarget target) => sort -> ( LspEnv -> TargetArgs target -> MaybeT (LspM Plugin.Config) [(Metadata, b)] ) -> PluginMethodHandler IdeState TextDocumentCodeAction -codeActionProvider - sort k state plId - (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) +codeActionProvider sort k state plId + (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do fromMaybeT (Right $ List []) $ do let fc = FileContext @@ -131,16 +146,15 @@ codeActionProvider _ _ _ _ _ = pure $ Right $ List [] codeLensProvider :: forall target sort b - . (Show sort, A.ToJSON b, IsTarget target) + . (IsContinuationSort sort, A.ToJSON b, IsTarget target) => sort -> ( LspEnv -> TargetArgs target -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] ) -> PluginMethodHandler IdeState TextDocumentCodeLens -codeLensProvider - sort k state plId - (CodeLensParams _ _ (TextDocumentIdentifier uri)) +codeLensProvider sort k state plId + (CodeLensParams _ _ (TextDocumentIdentifier uri)) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do fromMaybeT (Right $ List []) $ do let fc = FileContext @@ -159,7 +173,7 @@ codeLensProvider _ _ _ _ _ = pure $ Right $ List [] makeCodeAction - :: (A.ToJSON b, Show sort) + :: (A.ToJSON b, IsContinuationSort sort) => PluginId -> FileContext -> sort @@ -167,7 +181,7 @@ makeCodeAction -> b -> LSP.CodeAction makeCodeAction plId fc sort (Metadata title kind preferred) b = - let cmd_id = CommandId $ T.pack $ show sort + let cmd_id = toCommandId sort cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON (fc, b)] in LSP.CodeAction { _title = title @@ -181,7 +195,7 @@ makeCodeAction plId fc sort (Metadata title kind preferred) b = } makeCodeLens - :: (A.ToJSON b, Show sort) + :: (A.ToJSON b, IsContinuationSort sort) => PluginId -> sort -> Range @@ -189,7 +203,7 @@ makeCodeLens -> b -> LSP.CodeLens makeCodeLens plId sort range (Metadata title _ _) b = - let cmd_id = CommandId $ T.pack $ show sort + let cmd_id = toCommandId sort cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] in LSP.CodeLens { _range = range @@ -204,7 +218,7 @@ testInteraction = , c_makeCommand = SynthesizeCodeAction $ \_ hj -> do pure $ [0..2] <&> \ix -> (Metadata (T.pack $ "Hello from AbstractLSP: " <> show (_jGoal $ hj_jdg hj)) (CodeActionUnknown $ T.pack "some-kind") False, ix) , c_runCommand = \_ _ fc n -> do - pure $ Right $ WorkspaceEdit + pure $ RawEdit $ WorkspaceEdit { _changes = Nothing , _documentChanges = pure $ pure $ InL $ TextDocumentEdit { _textDocument = VersionedTextDocumentIdentifier {_uri = fc_uri fc, _version = Just 0} @@ -219,6 +233,7 @@ testInteraction = deriving newtype instance Applicative List + -- makeTacticCodeAction -- :: TacticCommand -- -> Continuation 'HoleTarget b diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs index 4fc1e3614d..2f06c6b127 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs @@ -12,6 +12,7 @@ import Control.Monad.Trans.Maybe (MaybeT (MaybeT), mapMaybeT) import qualified Data.Aeson as A import Data.Text (Text) import Development.IDE (IdeState) +import Development.IDE.GHC.ExactPrint (Graft) import Development.IDE.Core.UseStale import Development.IDE.GHC.Compat hiding (Target) import GHC.Generics (Generic) @@ -25,7 +26,7 @@ import Wingman.Types data Interaction where Interaction - :: (IsTarget target, Show sort, A.ToJSON b, A.FromJSON b) + :: (IsTarget target, IsContinuationSort sort, A.ToJSON b, A.FromJSON b) => Continuation sort target b -> Interaction @@ -52,6 +53,15 @@ data SynthesizeCommand a b ) +class IsContinuationSort a where + toCommandId :: a -> CommandId + +data ContinuationResult + = ErrorMessages [UserFacingMessage] + | RawEdit WorkspaceEdit + | GraftEdit (Graft (Either String) ParsedSource) + + data Continuation sort a b = Continuation { c_sort :: sort , c_makeCommand :: SynthesizeCommand a b @@ -60,8 +70,7 @@ data Continuation sort a b = Continuation -> TargetArgs a -> FileContext -> b - -> MaybeT (LspM Plugin.Config) - (Either [UserFacingMessage] WorkspaceEdit) + -> MaybeT (LspM Plugin.Config) ContinuationResult } From e644a1f32e96fa1795c55fe8010e00df058f47b5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 11:51:41 -0700 Subject: [PATCH 08/26] Remove IO from TacticProviders; use LspEnv instead --- .../Wingman/LanguageServer/TacticProviders.hs | 42 +++++++++---------- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 28 ++++++++----- 2 files changed, 36 insertions(+), 34 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index ebc460f6d3..d384eada1e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -27,10 +27,7 @@ import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.PluginUtils import Ide.Types -import Language.LSP.Types hiding - (SemanticTokenAbsolute (length, line), - SemanticTokenRelative (length), - SemanticTokensEdit (_start)) +import Language.LSP.Types hiding (SemanticTokenAbsolute (..), SemanticTokenRelative (..)) import OccName import Prelude hiding (span) import Wingman.Auto @@ -40,6 +37,7 @@ import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons) import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types +import Wingman.AbstractLSP.Types ------------------------------------------------------------------------------ @@ -192,15 +190,11 @@ guardLength f as = bool [] as $ f $ length as -- UI. type TacticProvider = TacticProviderData - -> IO [Command |? CodeAction] + -> [Command |? CodeAction] data TacticProviderData = TacticProviderData - { tpd_dflags :: DynFlags - , tpd_config :: Config - , tpd_plid :: PluginId - , tpd_uri :: Uri - , tpd_range :: Tracked 'Current Range + { tpd_lspEnv :: LspEnv , tpd_jdg :: Judgement , tpd_hole_sort :: HoleSort } @@ -219,13 +213,13 @@ requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider requireHoleSort p tp tpd = case p $ tpd_hole_sort tpd of True -> tp tpd - False -> pure [] + False -> [] withMetaprogram :: (T.Text -> TacticProvider) -> TacticProvider withMetaprogram tp tpd = case tpd_hole_sort tpd of Metaprogram mp -> tp mp tpd - _ -> pure [] + _ -> [] ------------------------------------------------------------------------------ @@ -233,9 +227,9 @@ withMetaprogram tp tpd = -- predicate holds for the goal. requireExtension :: Extension -> TacticProvider -> TacticProvider requireExtension ext tp tpd = - case xopt ext $ tpd_dflags tpd of + case xopt ext $ le_dflags $ tpd_lspEnv tpd of True -> tp tpd - False -> pure [] + False -> [] ------------------------------------------------------------------------------ @@ -245,7 +239,7 @@ filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider filterGoalType p tp tpd = case p $ unCType $ jGoal $ tpd_jdg tpd of True -> tp tpd - False -> pure [] + False -> [] ------------------------------------------------------------------------------ @@ -266,11 +260,11 @@ filterBindingType p tp tpd = let jdg = tpd_jdg tpd hy = jLocalHypothesis jdg g = jGoal jdg - in fmap join $ for (unHypothesis hy) $ \hi -> + in join $ for (unHypothesis hy) $ \hi -> let ty = unCType $ hi_type hi in case p (unCType g) ty of True -> tp (hi_name hi) ty tpd - False -> pure [] + False -> [] ------------------------------------------------------------------------------ @@ -281,14 +275,14 @@ filterTypeProjection -> (a -> TacticProvider) -> TacticProvider filterTypeProjection p tp tpd = - fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a -> + join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a -> tp a tpd ------------------------------------------------------------------------------ -- | Get access to the 'Config' when building a 'TacticProvider'. withConfig :: (Config -> TacticProvider) -> TacticProvider -withConfig tp tpd = tp (tpd_config tpd) tpd +withConfig tp tpd = tp (le_config $ tpd_lspEnv tpd) tpd ------------------------------------------------------------------------------ @@ -296,11 +290,13 @@ withConfig tp tpd = tp (tpd_config tpd) tpd -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider provide tc name TacticProviderData{..} = do - let title = tacticTitle tc name - params = TacticParams { tp_file = tpd_uri , tp_range = tpd_range , tp_var_name = name } - cmd = mkLspCommand tpd_plid (tcCommandId tc) title (Just [toJSON params]) + let LspEnv{..} = tpd_lspEnv + FileContext{..} = le_fileContext + title = tacticTitle tc name + -- TODO(sandy): fromJust + params = TacticParams { tp_file = fc_uri , tp_range = fromJust fc_range , tp_var_name = name } + cmd = mkLspCommand le_pluginId (tcCommandId tc) title (Just [toJSON params]) pure - $ pure $ InR $ CodeAction { _title = title diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 257c85fa94..bf3e9d7285 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -79,17 +79,23 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) cfg <- getTacticConfig plId liftIO $ fromMaybeT (Right $ List []) $ do HoleJudgment{..} <- judgementForHole state nfp range cfg - actions <- lift $ - -- This foldMap is over the function monoid. - foldMap commandProvider [minBound .. maxBound] $ TacticProviderData - { tpd_dflags = hj_dflags - , tpd_config = cfg - , tpd_plid = plId - , tpd_uri = uri - , tpd_range = range - , tpd_jdg = hj_jdg - , tpd_hole_sort = hj_hole_sort - } + let actions = + -- This foldMap is over the function monoid. + foldMap commandProvider [minBound .. maxBound] $ TacticProviderData + { tpd_lspEnv = LspEnv + { le_ideState = state + , le_pluginId = plId + , le_dflags = hj_dflags + , le_config = cfg + , le_fileContext = FileContext + { fc_uri = uri + , fc_nfp = nfp + , fc_range = Just range + } + } + , tpd_jdg = hj_jdg + , tpd_hole_sort = hj_hole_sort + } pure $ Right $ List actions codeActionProvider _ _ _ = pure $ Right $ List [] From 149b6c5f87d3b19fd34e47aba5d091d799d1f95d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 11:58:12 -0700 Subject: [PATCH 09/26] installInteractions --- .../src/Wingman/AbstractLSP.hs | 50 ++++++----------- .../src/Wingman/AbstractLSP/Types.hs | 7 +++ .../hls-tactics-plugin/src/Wingman/Plugin.hs | 56 ++++++++++--------- 3 files changed, 52 insertions(+), 61 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 8fe002b0aa..252c10295c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -5,18 +5,22 @@ {-# LANGUAGE NoMonoLocalBinds #-} {-# OPTIONS_GHC -Wno-orphans #-} -module Wingman.AbstractLSP (buildHandlers, buildCommand, testInteraction) where +module Wingman.AbstractLSP (installInteractions, testInteraction) where +import Control.Applicative (empty) import Control.Monad (void) import Control.Monad.IO.Class import Control.Monad.Trans (lift) import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT) import qualified Data.Aeson as A import Data.Foldable (traverse_) +import Data.Functor ((<&>)) +import Data.Maybe (fromJust) import qualified Data.Text as T import Data.Tuple.Extra (uncurry3) import Development.IDE (IdeState) import Development.IDE.Core.UseStale +import Development.IDE.GHC.ExactPrint (GetAnnotatedParsedSource(GetAnnotatedParsedSource)) import qualified Ide.Plugin.Config as Plugin import Ide.Types import Language.LSP.Server (LspM, sendRequest, getClientCapabilities) @@ -26,10 +30,15 @@ import Wingman.AbstractLSP.Types import Wingman.EmptyCase (fromMaybeT) import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde) import Wingman.Types -import Data.Functor ((<&>)) -import Data.Maybe (fromJust) -import Development.IDE.GHC.ExactPrint (GetAnnotatedParsedSource(GetAnnotatedParsedSource)) -import Control.Applicative (empty) + + +installInteractions :: [Interaction] -> PluginDescriptor IdeState -> PluginDescriptor IdeState +installInteractions is desc = + let plId = pluginId desc + in desc + { pluginCommands = pluginCommands desc <> fmap (buildCommand plId) is + , pluginHandlers = pluginHandlers desc <> buildHandlers is + } buildHandlers @@ -211,10 +220,10 @@ makeCodeLens plId sort range (Metadata title _ _) b = , _xdata = Nothing } -testInteraction :: Continuation String HoleTarget Int +testInteraction :: Continuation T.Text HoleTarget Int testInteraction = Continuation - { c_sort = "tactics.test" + { c_sort = T.pack "tactics.test" , c_makeCommand = SynthesizeCodeAction $ \_ hj -> do pure $ [0..2] <&> \ix -> (Metadata (T.pack $ "Hello from AbstractLSP: " <> show (_jGoal $ hj_jdg hj)) (CodeActionUnknown $ T.pack "some-kind") False, ix) , c_runCommand = \_ _ fc n -> do @@ -233,30 +242,3 @@ testInteraction = deriving newtype instance Applicative List - --- makeTacticCodeAction --- :: TacticCommand --- -> Continuation 'HoleTarget b --- makeTacticCodeAction cmd = --- Continuation CodeAction --- (\LspEnv{..} hj -> do --- let FileContext{..} = le_fileContext --- case fc_range of --- Nothing -> do --- traceM "Tried to run makeTacticCodeAction but no range was given" --- pure [] --- Just range -> do --- undefined --- lift $ liftIO $ commandProvider cmd $ --- -- TODO(sandy): this is stupid. just use the same env --- TacticProviderData --- { tpd_dflags = le_dflags --- , tpd_config = le_config --- , tpd_plid = le_pluginId --- , tpd_uri = fc_uri --- , tpd_range = range --- , tpd_jdg = hj_jdg hj --- , tpd_hole_sort = hj_hole_sort hj --- } --- ) undefined - diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs index 2f06c6b127..bb21e723c7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs @@ -56,6 +56,13 @@ data SynthesizeCommand a b class IsContinuationSort a where toCommandId :: a -> CommandId + +instance IsContinuationSort CommandId where + toCommandId = id + +instance IsContinuationSort Text where + toCommandId = CommandId + data ContinuationResult = ErrorMessages [UserFacingMessage] | RawEdit WorkspaceEdit diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index bf3e9d7285..b7b92df186 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -28,12 +28,13 @@ import Language.LSP.Types.Capabilities import OccName import Prelude hiding (span) import System.Timeout +import Wingman.AbstractLSP +import Wingman.AbstractLSP.Types (Interaction(Interaction), LspEnv (..), FileContext (..)) import Wingman.CaseSplit import Wingman.EmptyCase import Wingman.GHC import Wingman.Judgements (jNeedsToBindArgs) import Wingman.LanguageServer -import Wingman.AbstractLSP import Wingman.LanguageServer.Metaprogram (hoverProvider) import Wingman.LanguageServer.TacticProviders import Wingman.Machinery (scoreSolution) @@ -41,36 +42,37 @@ import Wingman.Range import Wingman.StaticPlugin import Wingman.Tactics import Wingman.Types -import Wingman.AbstractLSP.Types (Interaction(Interaction)) descriptor :: PluginId -> PluginDescriptor IdeState -descriptor plId = (defaultPluginDescriptor plId) - { pluginCommands - = mconcat - [ fmap (\tc -> - PluginCommand - (tcCommandId tc) - (tacticDesc $ tcCommandName tc) - (tacticCmd (commandTactic tc) plId)) - [minBound .. maxBound] - , pure $ - PluginCommand - emptyCaseLensCommandId - "Complete the empty case" - workspaceEditHandler - , pure $ buildCommand plId $ Interaction testInteraction +descriptor plId + = installInteractions + [Interaction testInteraction] + $ (defaultPluginDescriptor plId) + { pluginCommands + = mconcat + [ fmap (\tc -> + PluginCommand + (tcCommandId tc) + (tacticDesc $ tcCommandName tc) + (tacticCmd (commandTactic tc) plId)) + [minBound .. maxBound] + , pure $ + PluginCommand + emptyCaseLensCommandId + "Complete the empty case" + workspaceEditHandler + ] + , pluginHandlers = mconcat + [ mkPluginHandler STextDocumentCodeAction codeActionProvider + , mkPluginHandler STextDocumentCodeLens codeLensProvider + , mkPluginHandler STextDocumentHover hoverProvider ] - , pluginHandlers = mconcat - [ mkPluginHandler STextDocumentCodeAction codeActionProvider - , mkPluginHandler STextDocumentCodeLens codeLensProvider - , mkPluginHandler STextDocumentHover hoverProvider - ] <> buildHandlers [Interaction testInteraction] - , pluginRules = wingmanRules plId - , pluginConfigDescriptor = - defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties} - , pluginModifyDynflags = staticPlugin - } + , pluginRules = wingmanRules plId + , pluginConfigDescriptor = + defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties} + , pluginModifyDynflags = staticPlugin + } codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction From ee6b73ce15f3f7adedae3d7ccf82ef58329d6a4a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 12:42:55 -0700 Subject: [PATCH 10/26] Pull TacticCodeActions into their own file --- .../hls-tactics-plugin.cabal | 1 + .../src/Wingman/AbstractLSP.hs | 1 + .../src/Wingman/AbstractLSP/TacticActions.hs | 166 +++++++++++++++ .../Wingman/LanguageServer/TacticProviders.hs | 35 +-- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 199 +----------------- 5 files changed, 186 insertions(+), 216 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index c1aa501ab9..f4d11fd892 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -28,6 +28,7 @@ library exposed-modules: Ide.Plugin.Tactic Wingman.AbstractLSP + Wingman.AbstractLSP.TacticActions Wingman.AbstractLSP.Types Wingman.Auto Wingman.CaseSplit diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 252c10295c..7b6941cc43 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -242,3 +242,4 @@ testInteraction = deriving newtype instance Applicative List + diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs new file mode 100644 index 0000000000..be2d8ef0e7 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE RecordWildCards #-} + +{-# LANGUAGE NoMonoLocalBinds #-} + +module Wingman.AbstractLSP.TacticActions where + +import Data.Foldable +import qualified Data.Text as T +import Development.IDE hiding (rangeToRealSrcSpan) +import Development.IDE.Core.UseStale +import Ide.Types (PluginId, CommandFunction) +import Wingman.AbstractLSP.Types +import Wingman.LanguageServer.TacticProviders +import Wingman.Types +import Development.IDE.GHC.Compat +import Wingman.LanguageServer (runStaleIde) +import System.Timeout (timeout) +import Control.Monad.Trans (lift) +import Wingman.GHC (liftMaybe, isHole, pattern AMatch, unXPat) +import Development.IDE.GHC.ExactPrint +import Control.Monad.Trans.Maybe (mapMaybeT) +import Control.Monad.IO.Class (liftIO) +import Wingman.Range +import Wingman.Machinery (runTactic, scoreSolution) +import GhcPlugins (occName) +import Language.Haskell.GHC.ExactPrint +import Data.Proxy +import Control.Monad (when) +import Wingman.CaseSplit +import Data.Maybe (listToMaybe) +import Wingman.Judgements (jNeedsToBindArgs) +import Generics.SYB.GHC (mkBindListT, everywhereM') + + +makeTacticCodeAction + :: TacticCommand + -> Continuation TacticCommand HoleTarget T.Text +makeTacticCodeAction cmd = + Continuation cmd + (SynthesizeCodeAction $ \env@LspEnv{..} hj -> do + pure $ commandProvider cmd $ + TacticProviderData + { tpd_lspEnv = env + , tpd_jdg = hj_jdg hj + , tpd_hole_sort = hj_hole_sort hj + } + ) + $ \LspEnv{..} HoleJudgment{..} FileContext{..} var_name -> do + let stale a = runStaleIde "tacticCmd" le_ideState fc_nfp a + + let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath fc_nfp)) hj_range + TrackedStale _ pmmap <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + pm_span <- liftMaybe $ mapAgeFrom pmmap span + let t = commandTactic cmd var_name + + res <- liftIO $ timeout (cfg_timeout_seconds le_config * seconds) $ do + runTactic hj_ctx hj_jdg t >>= \case + Left err -> pure $ ErrorMessages $ pure $ mkUserFacingMessage err + Right rtr -> + case rtr_extract rtr of + L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> + pure $ ErrorMessages [NothingToDo] + _ -> do + for_ (rtr_other_solns rtr) $ \soln -> do + traceMX "other solution" $ syn_val soln + traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] + traceMX "solution" $ rtr_extract rtr + pure $ GraftEdit $ graftHole (RealSrcSpan $ unTrack pm_span) rtr + + case res of + Nothing -> do + -- showUserFacingMessage TimedOut + undefined + Just c -> pure c + +------------------------------------------------------------------------------ +-- | The number of microseconds in a second +seconds :: Num a => a +seconds = 1e6 + +mkUserFacingMessage :: [TacticError] -> UserFacingMessage +mkUserFacingMessage errs + | elem OutOfGas errs = NotEnoughGas +mkUserFacingMessage _ = TacticErrors + +------------------------------------------------------------------------------ +-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly +-- deals with top-level holes, in which we might need to fiddle with the +-- 'Match's that bind variables. +graftHole + :: SrcSpan + -> RunTacticResults + -> Graft (Either String) ParsedSource +graftHole span rtr + | _jIsTopHole (rtr_jdg rtr) + = genericGraftWithSmallestM + (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span + $ \dflags matches -> + everywhereM' + $ mkBindListT $ \ix -> + graftDecl dflags span ix $ \name pats -> + splitToDecl + (case not $ jNeedsToBindArgs (rtr_jdg rtr) of + -- If the user has explicitly bound arguments, use the + -- fixity they wrote. + True -> matchContextFixity . m_ctxt . unLoc + =<< listToMaybe matches + -- Otherwise, choose based on the name of the function. + False -> Nothing + ) + (occName name) + $ iterateSplit + $ mkFirstAgda (fmap unXPat pats) + $ unLoc + $ rtr_extract rtr +graftHole span rtr + = graft span + $ rtr_extract rtr + + +matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity +matchContextFixity (FunRhs _ l _) = Just l +matchContextFixity _ = Nothing + + +------------------------------------------------------------------------------ +-- | Helper function to route 'mergeFunBindMatches' into the right place in an +-- AST --- correctly dealing with inserting into instance declarations. +graftDecl + :: DynFlags + -> SrcSpan + -> Int + -> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs) + -> LMatch GhcPs (LHsExpr GhcPs) + -> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)] +graftDecl dflags dst ix make_decl (L src (AMatch (FunRhs (L _ name) _ _) pats _)) + | dst `isSubspanOf` src = do + L _ dec <- annotateDecl dflags $ make_decl name pats + case dec of + ValD _ (FunBind { fun_matches = MG { mg_alts = L _ alts@(first_match : _)} + }) -> do + -- For whatever reason, ExactPrint annotates newlines to the ends of + -- case matches and type signatures, but only allows us to insert + -- them at the beginning of those things. Thus, we need want to + -- insert a preceeding newline (done in 'annotateDecl') on all + -- matches, except for the first one --- since it gets its newline + -- from the line above. + when (ix == 0) $ + setPrecedingLinesT first_match 0 0 + pure alts + _ -> lift $ Left "annotateDecl didn't produce a funbind" +graftDecl _ _ _ _ x = pure $ pure x + + +-- tacticCmd +-- :: (T.Text -> TacticsM ()) +-- -> PluginId +-- -> CommandFunction IdeState TacticParams +-- tacticCmd tac pId state (TacticParams uri range var_name) +-- | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do +-- let stale a = runStaleIde "tacticCmd" state nfp a + +-- ccs <- getClientCapabilities +-- cfg <- getTacticConfig pId +-- res <- liftIO $ runMaybeT $ do +-- HoleJudgment{..} <- judgementForHole state nfp range cfg diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index d384eada1e..c138369daf 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -1,6 +1,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Wingman.LanguageServer.TacticProviders ( commandProvider @@ -25,11 +26,11 @@ import Development.IDE.Core.UseStale (Tracked, Age(..)) import Development.IDE.GHC.Compat import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) -import Ide.PluginUtils import Ide.Types import Language.LSP.Types hiding (SemanticTokenAbsolute (..), SemanticTokenRelative (..)) import OccName import Prelude hiding (span) +import Wingman.AbstractLSP.Types import Wingman.Auto import Wingman.GHC import Wingman.Judgements @@ -37,7 +38,6 @@ import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons) import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types -import Wingman.AbstractLSP.Types ------------------------------------------------------------------------------ @@ -190,7 +190,7 @@ guardLength f as = bool [] as $ f $ length as -- UI. type TacticProvider = TacticProviderData - -> [Command |? CodeAction] + -> [(Metadata, T.Text)] data TacticProviderData = TacticProviderData @@ -289,25 +289,8 @@ withConfig tp tpd = tp (le_config $ tpd_lspEnv tpd) tpd -- | Terminal constructor for providing context-sensitive tactics. Tactics -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider -provide tc name TacticProviderData{..} = do - let LspEnv{..} = tpd_lspEnv - FileContext{..} = le_fileContext - title = tacticTitle tc name - -- TODO(sandy): fromJust - params = TacticParams { tp_file = fc_uri , tp_range = fromJust fc_range , tp_var_name = name } - cmd = mkLspCommand le_pluginId (tcCommandId tc) title (Just [toJSON params]) - pure - $ InR - $ CodeAction - { _title = title - , _kind = Just $ mkTacticKind tc - , _diagnostics = Nothing - , _isPreferred = Just $ tacticPreferred tc - , _disabled = Nothing - , _edit = Nothing - , _command = Just cmd - , _xdata = Nothing - } +provide tc name _ = + pure $ (Metadata (tacticTitle tc name) (mkTacticKind tc) (tacticPreferred tc), name) ------------------------------------------------------------------------------ @@ -341,7 +324,7 @@ liftLambdaCase nil f t = -- algebraic types. destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True -destructFilter _ _ = False +destructFilter _ _ = False ------------------------------------------------------------------------------ @@ -350,5 +333,9 @@ destructFilter _ _ = False destructPunFilter :: Type -> Type -> Bool destructPunFilter _ (algebraicTyCon -> Just tc) = any (not . null . dataConFieldLabels) $ tyConDataCons tc -destructPunFilter _ _ = False +destructPunFilter _ _ = False + + +instance IsContinuationSort TacticCommand where + toCommandId = tcCommandId diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index b7b92df186..0c34a71709 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -9,63 +9,42 @@ module Wingman.Plugin ) where import Control.Monad -import Control.Monad.Trans import Control.Monad.Trans.Maybe -import Data.Aeson -import Data.Data -import Data.Foldable (for_) import Data.Maybe import qualified Data.Text as T import Development.IDE.Core.Shake (IdeState (..)) -import Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent) -import Development.IDE.GHC.Compat -import Development.IDE.GHC.ExactPrint -import Generics.SYB.GHC import Ide.Types import Language.LSP.Server import Language.LSP.Types -import Language.LSP.Types.Capabilities -import OccName import Prelude hiding (span) import System.Timeout import Wingman.AbstractLSP -import Wingman.AbstractLSP.Types (Interaction(Interaction), LspEnv (..), FileContext (..)) -import Wingman.CaseSplit +import Wingman.AbstractLSP.TacticActions (makeTacticCodeAction) +import Wingman.AbstractLSP.Types (Interaction(Interaction)) import Wingman.EmptyCase -import Wingman.GHC -import Wingman.Judgements (jNeedsToBindArgs) import Wingman.LanguageServer import Wingman.LanguageServer.Metaprogram (hoverProvider) -import Wingman.LanguageServer.TacticProviders -import Wingman.Machinery (scoreSolution) -import Wingman.Range import Wingman.StaticPlugin -import Wingman.Tactics import Wingman.Types descriptor :: PluginId -> PluginDescriptor IdeState descriptor plId = installInteractions - [Interaction testInteraction] + ( Interaction testInteraction + : fmap (Interaction . makeTacticCodeAction) [minBound .. maxBound] + ) $ (defaultPluginDescriptor plId) { pluginCommands = mconcat - [ fmap (\tc -> - PluginCommand - (tcCommandId tc) - (tacticDesc $ tcCommandName tc) - (tacticCmd (commandTactic tc) plId)) - [minBound .. maxBound] - , pure $ + [ pure $ PluginCommand emptyCaseLensCommandId "Complete the empty case" workspaceEditHandler ] , pluginHandlers = mconcat - [ mkPluginHandler STextDocumentCodeAction codeActionProvider - , mkPluginHandler STextDocumentCodeLens codeLensProvider + [ mkPluginHandler STextDocumentCodeLens codeLensProvider , mkPluginHandler STextDocumentHover hoverProvider ] , pluginRules = wingmanRules plId @@ -75,33 +54,6 @@ descriptor plId } -codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction -codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - cfg <- getTacticConfig plId - liftIO $ fromMaybeT (Right $ List []) $ do - HoleJudgment{..} <- judgementForHole state nfp range cfg - let actions = - -- This foldMap is over the function monoid. - foldMap commandProvider [minBound .. maxBound] $ TacticProviderData - { tpd_lspEnv = LspEnv - { le_ideState = state - , le_pluginId = plId - , le_dflags = hj_dflags - , le_config = cfg - , le_fileContext = FileContext - { fc_uri = uri - , fc_nfp = nfp - , fc_range = Just range - } - } - , tpd_jdg = hj_jdg - , tpd_hole_sort = hj_hole_sort - } - pure $ Right $ List actions -codeActionProvider _ _ _ = pure $ Right $ List [] - - showUserFacingMessage :: MonadLsp cfg m => UserFacingMessage @@ -111,56 +63,6 @@ showUserFacingMessage ufm = do pure $ Left $ mkErr InternalError $ T.pack $ show ufm -mkUserFacingMessage :: [TacticError] -> UserFacingMessage -mkUserFacingMessage errs - | elem OutOfGas errs = NotEnoughGas -mkUserFacingMessage _ = TacticErrors - - -tacticCmd - :: (T.Text -> TacticsM ()) - -> PluginId - -> CommandFunction IdeState TacticParams -tacticCmd tac pId state (TacticParams uri range var_name) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - let stale a = runStaleIde "tacticCmd" state nfp a - - ccs <- getClientCapabilities - cfg <- getTacticConfig pId - res <- liftIO $ runMaybeT $ do - HoleJudgment{..} <- judgementForHole state nfp range cfg - let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range - TrackedStale pm pmmap <- stale GetAnnotatedParsedSource - pm_span <- liftMaybe $ mapAgeFrom pmmap span - let t = tac var_name - - timingOut (cfg_timeout_seconds cfg * seconds) $ do - res <- liftIO $ runTactic hj_ctx hj_jdg t - pure $ join $ case res of - Left errs -> do - traceMX "errs" errs - Left $ mkUserFacingMessage errs - Right rtr -> - case rtr_extract rtr of - L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> - Left NothingToDo - _ -> pure $ mkTacticResultEdits pm_span hj_dflags ccs uri pm rtr - - case res of - 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" - - ------------------------------------------------------------------------------ -- | The number of microseconds in a second seconds :: Num a => a @@ -178,90 +80,3 @@ mkErr :: ErrorCode -> T.Text -> ResponseError mkErr code err = ResponseError code err Nothing ------------------------------------------------------------------------------- --- | Turn a 'RunTacticResults' into concrete edits to make in the source --- document. -mkTacticResultEdits - :: Tracked age RealSrcSpan - -> DynFlags - -> ClientCapabilities - -> Uri - -> Tracked age (Annotated ParsedSource) - -> RunTacticResults - -> Either UserFacingMessage WorkspaceEdit -mkTacticResultEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do - for_ (rtr_other_solns rtr) $ \soln -> do - traceMX "other solution" $ syn_val soln - traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] - traceMX "solution" $ rtr_extract rtr - mkWorkspaceEdits dflags ccs uri pm $ graftHole (RealSrcSpan span) rtr - - ------------------------------------------------------------------------------- --- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly --- deals with top-level holes, in which we might need to fiddle with the --- 'Match's that bind variables. -graftHole - :: SrcSpan - -> RunTacticResults - -> Graft (Either String) ParsedSource -graftHole span rtr - | _jIsTopHole (rtr_jdg rtr) - = genericGraftWithSmallestM - (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span - $ \dflags matches -> - everywhereM' - $ mkBindListT $ \ix -> - graftDecl dflags span ix $ \name pats -> - splitToDecl - (case not $ jNeedsToBindArgs (rtr_jdg rtr) of - -- If the user has explicitly bound arguments, use the - -- fixity they wrote. - True -> matchContextFixity . m_ctxt . unLoc - =<< listToMaybe matches - -- Otherwise, choose based on the name of the function. - False -> Nothing - ) - (occName name) - $ iterateSplit - $ mkFirstAgda (fmap unXPat pats) - $ unLoc - $ rtr_extract rtr -graftHole span rtr - = graft span - $ rtr_extract rtr - - -matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity -matchContextFixity (FunRhs _ l _) = Just l -matchContextFixity _ = Nothing - - ------------------------------------------------------------------------------- --- | Helper function to route 'mergeFunBindMatches' into the right place in an --- AST --- correctly dealing with inserting into instance declarations. -graftDecl - :: DynFlags - -> SrcSpan - -> Int - -> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs) - -> LMatch GhcPs (LHsExpr GhcPs) - -> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)] -graftDecl dflags dst ix make_decl (L src (AMatch (FunRhs (L _ name) _ _) pats _)) - | dst `isSubspanOf` src = do - L _ dec <- annotateDecl dflags $ make_decl name pats - case dec of - ValD _ (FunBind { fun_matches = MG { mg_alts = L _ alts@(first_match : _)} - }) -> do - -- For whatever reason, ExactPrint annotates newlines to the ends of - -- case matches and type signatures, but only allows us to insert - -- them at the beginning of those things. Thus, we need want to - -- insert a preceeding newline (done in 'annotateDecl') on all - -- matches, except for the first one --- since it gets its newline - -- from the line above. - when (ix == 0) $ - setPrecedingLinesT first_match 0 0 - pure alts - _ -> lift $ Left "annotateDecl didn't produce a funbind" -graftDecl _ _ _ _ x = pure $ pure x - From 69ec486cc6db2e2d292acc4c9e8043dfb43fc852 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 13:47:02 -0700 Subject: [PATCH 11/26] Misc cleanup --- .../src/Ide/Plugin/Tactic.hs | 6 +- .../src/Wingman/AbstractLSP.hs | 36 ++-------- .../src/Wingman/AbstractLSP/TacticActions.hs | 67 +++++++------------ .../Wingman/LanguageServer/TacticProviders.hs | 20 +----- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 63 ++++------------- 5 files changed, 49 insertions(+), 143 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index 35ecf0dcfe..de93d03ed0 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -1,9 +1,5 @@ -- | A plugin that uses tactics to synthesize code -module Ide.Plugin.Tactic - ( descriptor - , tacticTitle - , TacticCommand (..) - ) where +module Ide.Plugin.Tactic (descriptor) where import Wingman.Plugin diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 7b6941cc43..8a474b3326 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -5,7 +5,7 @@ {-# LANGUAGE NoMonoLocalBinds #-} {-# OPTIONS_GHC -Wno-orphans #-} -module Wingman.AbstractLSP (installInteractions, testInteraction) where +module Wingman.AbstractLSP (installInteractions) where import Control.Applicative (empty) import Control.Monad (void) @@ -14,8 +14,6 @@ import Control.Monad.Trans (lift) import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT) import qualified Data.Aeson as A import Data.Foldable (traverse_) -import Data.Functor ((<&>)) -import Data.Maybe (fromJust) import qualified Data.Text as T import Data.Tuple.Extra (uncurry3) import Development.IDE (IdeState) @@ -28,7 +26,7 @@ import qualified Language.LSP.Types as LSP import Language.LSP.Types hiding (CodeLens, CodeAction) import Wingman.AbstractLSP.Types import Wingman.EmptyCase (fromMaybeT) -import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde) +import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde, showLspMessage, mkShowMessageParams) import Wingman.Types @@ -104,8 +102,11 @@ sendEdits edits = (const $ pure ()) -showUserFacingMessage :: UserFacingMessage -> MaybeT (LspM Plugin.Config) () -showUserFacingMessage = error "not implemented" +showUserFacingMessage + :: UserFacingMessage + -> MaybeT (LspM Plugin.Config) () +showUserFacingMessage ufm = + void $ lift $ showLspMessage $ mkShowMessageParams ufm buildEnv @@ -220,26 +221,3 @@ makeCodeLens plId sort range (Metadata title _ _) b = , _xdata = Nothing } -testInteraction :: Continuation T.Text HoleTarget Int -testInteraction = - Continuation - { c_sort = T.pack "tactics.test" - , c_makeCommand = SynthesizeCodeAction $ \_ hj -> do - pure $ [0..2] <&> \ix -> (Metadata (T.pack $ "Hello from AbstractLSP: " <> show (_jGoal $ hj_jdg hj)) (CodeActionUnknown $ T.pack "some-kind") False, ix) - , c_runCommand = \_ _ fc n -> do - pure $ RawEdit $ WorkspaceEdit - { _changes = Nothing - , _documentChanges = pure $ pure $ InL $ TextDocumentEdit - { _textDocument = VersionedTextDocumentIdentifier {_uri = fc_uri fc, _version = Just 0} - , _edits = pure $ InL TextEdit - { _range = unTrack $ fromJust $ fc_range fc - , _newText = T.pack $ "yo" <> show n - } - } - , _changeAnnotations = Nothing - } - } - -deriving newtype instance Applicative List - - diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index be2d8ef0e7..6277f96d0f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -4,39 +4,36 @@ module Wingman.AbstractLSP.TacticActions where -import Data.Foldable -import qualified Data.Text as T +import Control.Monad (when) +import Control.Monad.IO.Class (liftIO) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (mapMaybeT) +import Data.Foldable +import Data.Maybe (listToMaybe) +import Data.Proxy import Development.IDE hiding (rangeToRealSrcSpan) import Development.IDE.Core.UseStale -import Ide.Types (PluginId, CommandFunction) +import Development.IDE.GHC.Compat +import Development.IDE.GHC.ExactPrint +import Generics.SYB.GHC (mkBindListT, everywhereM') +import GhcPlugins (occName) +import System.Timeout (timeout) import Wingman.AbstractLSP.Types +import Wingman.CaseSplit +import Wingman.GHC (liftMaybe, isHole, pattern AMatch, unXPat) +import Wingman.Judgements (jNeedsToBindArgs) +import Wingman.LanguageServer (runStaleIde) import Wingman.LanguageServer.TacticProviders +import Wingman.Machinery (runTactic, scoreSolution) +import Wingman.Range import Wingman.Types -import Development.IDE.GHC.Compat -import Wingman.LanguageServer (runStaleIde) -import System.Timeout (timeout) -import Control.Monad.Trans (lift) -import Wingman.GHC (liftMaybe, isHole, pattern AMatch, unXPat) -import Development.IDE.GHC.ExactPrint -import Control.Monad.Trans.Maybe (mapMaybeT) -import Control.Monad.IO.Class (liftIO) -import Wingman.Range -import Wingman.Machinery (runTactic, scoreSolution) -import GhcPlugins (occName) -import Language.Haskell.GHC.ExactPrint -import Data.Proxy -import Control.Monad (when) -import Wingman.CaseSplit -import Data.Maybe (listToMaybe) -import Wingman.Judgements (jNeedsToBindArgs) -import Generics.SYB.GHC (mkBindListT, everywhereM') makeTacticCodeAction :: TacticCommand - -> Continuation TacticCommand HoleTarget T.Text + -> Interaction makeTacticCodeAction cmd = - Continuation cmd + Interaction $ Continuation @_ @HoleTarget cmd (SynthesizeCodeAction $ \env@LspEnv{..} hj -> do pure $ commandProvider cmd $ TacticProviderData @@ -67,22 +64,23 @@ makeTacticCodeAction cmd = traceMX "solution" $ rtr_extract rtr pure $ GraftEdit $ graftHole (RealSrcSpan $ unTrack pm_span) rtr - case res of - Nothing -> do - -- showUserFacingMessage TimedOut - undefined - Just c -> pure c + pure $ case res of + Nothing -> ErrorMessages $ pure TimedOut + Just c -> c + ------------------------------------------------------------------------------ -- | The number of microseconds in a second seconds :: Num a => a seconds = 1e6 + mkUserFacingMessage :: [TacticError] -> UserFacingMessage mkUserFacingMessage errs | elem OutOfGas errs = NotEnoughGas mkUserFacingMessage _ = TacticErrors + ------------------------------------------------------------------------------ -- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly -- deals with top-level holes, in which we might need to fiddle with the @@ -151,16 +149,3 @@ graftDecl dflags dst ix make_decl (L src (AMatch (FunRhs (L _ name) _ _) pats _) _ -> lift $ Left "annotateDecl didn't produce a funbind" graftDecl _ _ _ _ x = pure $ pure x - --- tacticCmd --- :: (T.Text -> TacticsM ()) --- -> PluginId --- -> CommandFunction IdeState TacticParams --- tacticCmd tac pId state (TacticParams uri range var_name) --- | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do --- let stale a = runStaleIde "tacticCmd" state nfp a - --- ccs <- getClientCapabilities --- cfg <- getTacticConfig pId --- res <- liftIO $ runMaybeT $ do --- HoleJudgment{..} <- judgementForHole state nfp range cfg diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index c138369daf..5a0844b73c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -6,25 +6,18 @@ module Wingman.LanguageServer.TacticProviders ( commandProvider , commandTactic - , tcCommandId - , TacticParams (..) , TacticProviderData (..) - , useNameFromHypothesis ) where import Control.Monad -import Data.Aeson import Data.Bool (bool) import Data.Coerce import Data.Maybe import Data.Monoid import qualified Data.Set as S import qualified Data.Text as T -import Data.Traversable import DataCon (dataConName) -import Development.IDE.Core.UseStale (Tracked, Age(..)) import Development.IDE.GHC.Compat -import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Types import Language.LSP.Types hiding (SemanticTokenAbsolute (..), SemanticTokenRelative (..)) @@ -200,15 +193,6 @@ data TacticProviderData = TacticProviderData } -data TacticParams = TacticParams - { tp_file :: Uri -- ^ Uri of the file to fill the hole in - , tp_range :: Tracked 'Current Range -- ^ The range of the hole - , tp_var_name :: T.Text - } - deriving stock (Show, Eq, Generic) - deriving anyclass (ToJSON, FromJSON) - - requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider requireHoleSort p tp tpd = case p $ tpd_hole_sort tpd of @@ -260,7 +244,7 @@ filterBindingType p tp tpd = let jdg = tpd_jdg tpd hy = jLocalHypothesis jdg g = jGoal jdg - in join $ for (unHypothesis hy) $ \hi -> + in unHypothesis hy >>= \hi -> let ty = unCType $ hi_type hi in case p (unCType g) ty of True -> tp (hi_name hi) ty tpd @@ -275,7 +259,7 @@ filterTypeProjection -> (a -> TacticProvider) -> TacticProvider filterTypeProjection p tp tpd = - join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a -> + (p $ unCType $ jGoal $ tpd_jdg tpd) >>= \a -> tp a tpd diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 0c34a71709..805eb29e9c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -2,81 +2,44 @@ {-# LANGUAGE RecordWildCards #-} -- | A plugin that uses tactics to synthesize code -module Wingman.Plugin - ( descriptor - , tacticTitle - , TacticCommand (..) - ) where +module Wingman.Plugin where import Control.Monad -import Control.Monad.Trans.Maybe -import Data.Maybe -import qualified Data.Text as T import Development.IDE.Core.Shake (IdeState (..)) import Ide.Types -import Language.LSP.Server import Language.LSP.Types import Prelude hiding (span) -import System.Timeout import Wingman.AbstractLSP import Wingman.AbstractLSP.TacticActions (makeTacticCodeAction) -import Wingman.AbstractLSP.Types (Interaction(Interaction)) import Wingman.EmptyCase import Wingman.LanguageServer import Wingman.LanguageServer.Metaprogram (hoverProvider) import Wingman.StaticPlugin -import Wingman.Types descriptor :: PluginId -> PluginDescriptor IdeState descriptor plId = installInteractions - ( Interaction testInteraction - : fmap (Interaction . makeTacticCodeAction) [minBound .. maxBound] + ( fmap makeTacticCodeAction [minBound .. maxBound] ) $ (defaultPluginDescriptor plId) - { pluginCommands - = mconcat - [ pure $ - PluginCommand - emptyCaseLensCommandId - "Complete the empty case" - workspaceEditHandler - ] + { pluginCommands = + mconcat + [ pure $ + PluginCommand + emptyCaseLensCommandId + "Complete the empty case" + workspaceEditHandler + ] , pluginHandlers = mconcat [ mkPluginHandler STextDocumentCodeLens codeLensProvider , mkPluginHandler STextDocumentHover hoverProvider ] , pluginRules = wingmanRules plId , pluginConfigDescriptor = - defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties} + defaultConfigDescriptor + { configCustomConfig = mkCustomConfig properties + } , pluginModifyDynflags = staticPlugin } - -showUserFacingMessage - :: MonadLsp cfg m - => UserFacingMessage - -> m (Either ResponseError a) -showUserFacingMessage ufm = do - showLspMessage $ mkShowMessageParams ufm - pure $ Left $ mkErr InternalError $ T.pack $ show ufm - - ------------------------------------------------------------------------------- --- | The number of microseconds in a second -seconds :: Num a => a -seconds = 1e6 - - -timingOut - :: Int -- ^ Time in microseconds - -> IO a -- ^ Computation to run - -> MaybeT IO a -timingOut t m = MaybeT $ timeout t m - - -mkErr :: ErrorCode -> T.Text -> ResponseError -mkErr code err = ResponseError code err Nothing - - From 6b44e4da54cbad0c804c5073f9467c1ea4117f61 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 14:07:16 -0700 Subject: [PATCH 12/26] Haddock --- .../src/Wingman/AbstractLSP.hs | 42 +++++++++-- .../src/Wingman/AbstractLSP/TacticActions.hs | 6 ++ .../src/Wingman/AbstractLSP/Types.hs | 71 ++++++++++++++++--- 3 files changed, 103 insertions(+), 16 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 8a474b3326..ce20c14546 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -30,7 +30,15 @@ import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWork import Wingman.Types -installInteractions :: [Interaction] -> PluginDescriptor IdeState -> PluginDescriptor IdeState +------------------------------------------------------------------------------ +-- | Attact the 'Interaction's to a 'PluginDescriptor'. Interactions are +-- self-contained request/response pairs that abstract over the LSP, and +-- provide a unified interface for doing interesting things, without needing to +-- dive into the underlying API too directly. +installInteractions + :: [Interaction] + -> PluginDescriptor IdeState + -> PluginDescriptor IdeState installInteractions is desc = let plId = pluginId desc in desc @@ -39,6 +47,8 @@ installInteractions is desc = } +------------------------------------------------------------------------------ +-- | Extract 'PluginHandlers' from 'Interaction's. buildHandlers :: [Interaction] -> PluginHandlers IdeState @@ -51,6 +61,8 @@ buildHandlers cs = mkPluginHandler STextDocumentCodeLens $ codeLensProvider @target (c_sort c) k +------------------------------------------------------------------------------ +-- | Extract a 'PluginCommand' from an 'Interaction'. buildCommand :: PluginId -> Interaction @@ -59,17 +71,19 @@ buildCommand plId (Interaction (c :: Continuation sort target b)) = PluginCommand { commandId = toCommandId $ c_sort c , commandDesc = T.pack "" - , commandFunc = runCodeAction plId c + , commandFunc = runContinuation plId c } -runCodeAction +------------------------------------------------------------------------------ +-- | Boilerplate for running a 'Continuation' as part of an LSP command. +runContinuation :: forall sort a b . IsTarget a => PluginId -> Continuation sort a b -> CommandFunction IdeState (FileContext, b) -runCodeAction plId cont state (fc, b) = do +runContinuation plId cont state (fc, b) = do fromMaybeT (Left $ ResponseError { _code = InternalError @@ -77,7 +91,7 @@ runCodeAction plId cont state (fc, b) = do , _xdata = Nothing } ) $ do env@LspEnv{..} <- buildEnv state plId fc - let stale a = runStaleIde "runCodeAction" state (fc_nfp le_fileContext) a + let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a args <- fetchTargetArgs @a env c_runCommand cont env args fc b >>= \case ErrorMessages errs -> @@ -93,6 +107,8 @@ runCodeAction plId cont state (fc, b) = do pure $ Right A.Null +------------------------------------------------------------------------------ +-- | Push a 'WorkspaceEdit' to the client. sendEdits :: WorkspaceEdit -> MaybeT (LspM Plugin.Config) () sendEdits edits = void $ lift $ @@ -102,6 +118,8 @@ sendEdits edits = (const $ pure ()) +------------------------------------------------------------------------------ +-- | Push a 'UserFacingMessage' to the client. showUserFacingMessage :: UserFacingMessage -> MaybeT (LspM Plugin.Config) () @@ -109,6 +127,9 @@ showUserFacingMessage ufm = void $ lift $ showLspMessage $ mkShowMessageParams ufm +------------------------------------------------------------------------------ +-- | Build an 'LspEnv', which contains the majority of things we need to know +-- in a 'Continuation'. buildEnv :: IdeState -> PluginId @@ -126,6 +147,8 @@ buildEnv state plId fc = do } +------------------------------------------------------------------------------ +-- | Lift a 'Continuation' into an LSP CodeAction. codeActionProvider :: forall target sort b . (IsContinuationSort sort, A.ToJSON b, IsTarget target) @@ -154,6 +177,8 @@ codeActionProvider sort k state plId codeActionProvider _ _ _ _ _ = pure $ Right $ List [] +------------------------------------------------------------------------------ +-- | Lift a 'Continuation' into an LSP CodeLens. codeLensProvider :: forall target sort b . (IsContinuationSort sort, A.ToJSON b, IsTarget target) @@ -175,6 +200,7 @@ codeLensProvider sort k state plId env <- buildEnv state plId fc args <- fetchTargetArgs @target env actions <- k env args + -- TODO(sandy): NEED TO STICK THE RANGE INTO HERE pure $ Right $ List @@ -182,6 +208,8 @@ codeLensProvider sort k state plId codeLensProvider _ _ _ _ _ = pure $ Right $ List [] +------------------------------------------------------------------------------ +-- | Build a 'LSP.CodeAction'. makeCodeAction :: (A.ToJSON b, IsContinuationSort sort) => PluginId @@ -204,6 +232,9 @@ makeCodeAction plId fc sort (Metadata title kind preferred) b = , _xdata = Nothing } + +------------------------------------------------------------------------------ +-- | Build a 'LSP.CodeLens'. makeCodeLens :: (A.ToJSON b, IsContinuationSort sort) => PluginId @@ -214,6 +245,7 @@ makeCodeLens -> LSP.CodeLens makeCodeLens plId sort range (Metadata title _ _) b = let cmd_id = toCommandId sort + -- TODO(sandy): BUG HERE. NEED TO PUSH THE FILE CONTEXT TOO cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] in LSP.CodeLens { _range = range diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index 6277f96d0f..bc46b57a6c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -29,6 +29,8 @@ import Wingman.Range import Wingman.Types +------------------------------------------------------------------------------ +-- | An 'Interaction' for a 'TacticCommand'. makeTacticCodeAction :: TacticCommand -> Interaction @@ -75,6 +77,8 @@ seconds :: Num a => a seconds = 1e6 +------------------------------------------------------------------------------ +-- | Transform some tactic errors into a 'UserFacingMessage'. mkUserFacingMessage :: [TacticError] -> UserFacingMessage mkUserFacingMessage errs | elem OutOfGas errs = NotEnoughGas @@ -116,6 +120,8 @@ graftHole span rtr $ rtr_extract rtr +------------------------------------------------------------------------------ +-- | Keep a fixity if one was present in the 'HsMatchContext'. matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity matchContextFixity (FunRhs _ l _) = Just l matchContextFixity _ = Nothing diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs index bb21e723c7..8b00f0b021 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs @@ -24,6 +24,9 @@ import Wingman.LanguageServer (judgementForHole) import Wingman.Types +------------------------------------------------------------------------------ +-- | An 'Interaction' is an existential 'Continuation', which handles both +-- sides of the request/response interaction for LSP. data Interaction where Interaction :: (IsTarget target, IsContinuationSort sort, A.ToJSON b, A.FromJSON b) @@ -31,6 +34,9 @@ data Interaction where -> Interaction +------------------------------------------------------------------------------ +-- | Metadata for a command. Used by both code actions and lenses, though for +-- lenses, only 'md_title' is currently used. data Metadata = Metadata { md_title :: Text @@ -40,6 +46,8 @@ data Metadata deriving stock (Eq, Show) +------------------------------------------------------------------------------ +-- | Whether we're defining a CodeAction or CodeLens. data SynthesizeCommand a b = SynthesizeCodeAction ( LspEnv @@ -53,52 +61,82 @@ data SynthesizeCommand a b ) +------------------------------------------------------------------------------ +-- | Transform a "continuation sort" into a 'CommandId'. class IsContinuationSort a where toCommandId :: a -> CommandId - instance IsContinuationSort CommandId where toCommandId = id instance IsContinuationSort Text where toCommandId = CommandId + +------------------------------------------------------------------------------ +-- | Ways a 'Continuation' can resolve. data ContinuationResult - = ErrorMessages [UserFacingMessage] + = -- | Produce some error messages. + ErrorMessages [UserFacingMessage] + -- | Produce an explicit 'WorkspaceEdit'. | RawEdit WorkspaceEdit + -- | Produce a 'Graft', corresponding to a transformation of the current + -- AST. | GraftEdit (Graft (Either String) ParsedSource) -data Continuation sort a b = Continuation +------------------------------------------------------------------------------ +-- | A 'Continuation' is a single object corresponding to an action that users +-- can take via LSP. It generalizes codeactions and codelenses, allowing for +-- a significant amount of code reuse. +-- +-- Given @Continuation sort target payload@: +-- +-- the @sort@ corresponds to a 'CommandId', allowing you to namespace actions +-- rather than working directly with text. This functionality is driven via +-- 'IsContinuationSort'. +-- +-- the @target@ is used to fetch data from LSP on both sides of the +-- request/response barrier. For example, you can use it to resolve what node +-- in the AST the incoming range refers to. This functionality is driven via +-- 'IsTarget'. +-- +-- the @payload@ is used for data you'd explicitly like to send from the +-- request to the response. It's like @target@, but only gets computed once. +-- This is beneficial if you can do it, but requires that your data is +-- serializable via JSON. +data Continuation sort target payload = Continuation { c_sort :: sort - , c_makeCommand :: SynthesizeCommand a b + , c_makeCommand :: SynthesizeCommand target payload , c_runCommand :: LspEnv - -> TargetArgs a + -> TargetArgs target -> FileContext - -> b + -> payload -> MaybeT (LspM Plugin.Config) ContinuationResult } -data HoleTarget = HoleTarget - deriving stock (Eq, Ord, Show, Enum, Bounded) - - +------------------------------------------------------------------------------ +-- | What file are we looking at, and what bit of it? data FileContext = FileContext { fc_uri :: Uri , fc_nfp :: NormalizedFilePath , fc_range :: Maybe (Tracked 'Current Range) + -- ^ For code actions, this is 'Just'. For code lenses, you'll get + -- a 'Nothing' in the request, and a 'Just' in the response. } deriving stock (Eq, Ord, Show, Generic) deriving anyclass (A.ToJSON, A.FromJSON) deriving anyclass instance A.ToJSON NormalizedFilePath -deriving anyclass instance A.FromJSON NormalizedFilePath deriving anyclass instance A.ToJSON NormalizedUri +deriving anyclass instance A.FromJSON NormalizedFilePath deriving anyclass instance A.FromJSON NormalizedUri +------------------------------------------------------------------------------ +-- | Everything we need to resolve continuations. data LspEnv = LspEnv { le_ideState :: IdeState , le_pluginId :: PluginId @@ -107,12 +145,23 @@ data LspEnv = LspEnv , le_fileContext :: FileContext } + +------------------------------------------------------------------------------ +-- | Extract some information from LSP, so it can be passed to the requests and +-- responses of a 'Continuation'. class IsTarget t where type TargetArgs t fetchTargetArgs :: LspEnv -> MaybeT (LspM Plugin.Config) (TargetArgs t) +------------------------------------------------------------------------------ +-- | A 'HoleTarget' is a target (see 'IsTarget') which succeeds if the given +-- range is an HsExpr hole. It gives continuations access to the resulting +-- tactic judgement. +data HoleTarget = HoleTarget + deriving stock (Eq, Ord, Show, Enum, Bounded) + instance IsTarget HoleTarget where type TargetArgs HoleTarget = HoleJudgment fetchTargetArgs LspEnv{..} = do From cefbbe797cc85714ec7ff99daf6195a302b7fdcd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 14:14:40 -0700 Subject: [PATCH 13/26] Fix bug in codelens --- .../src/Wingman/AbstractLSP.hs | 34 ++++++++++++------- 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index ce20c14546..0baf96a6d3 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -3,11 +3,11 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE NoMonoLocalBinds #-} + {-# OPTIONS_GHC -Wno-orphans #-} module Wingman.AbstractLSP (installInteractions) where -import Control.Applicative (empty) import Control.Monad (void) import Control.Monad.IO.Class import Control.Monad.Trans (lift) @@ -94,17 +94,25 @@ runContinuation plId cont state (fc, b) = do let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a args <- fetchTargetArgs @a env c_runCommand cont env args fc b >>= \case - ErrorMessages errs -> + ErrorMessages errs -> do traverse_ showUserFacingMessage errs - RawEdit edits -> sendEdits edits + pure $ Right A.Null + RawEdit edits -> do + sendEdits edits + pure $ Right A.Null GraftEdit gr -> do ccs <- lift getClientCapabilities TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of - -- TODO(sandy): fixme - Left _errs -> empty - Right edits -> sendEdits edits - pure $ Right A.Null + Left errs -> + pure $ Left $ ResponseError + { _code = InternalError + , _message = T.pack $ show errs + , _xdata = Nothing + } + Right edits -> do + sendEdits edits + pure $ Right A.Null ------------------------------------------------------------------------------ @@ -200,11 +208,10 @@ codeLensProvider sort k state plId env <- buildEnv state plId fc args <- fetchTargetArgs @target env actions <- k env args - -- TODO(sandy): NEED TO STICK THE RANGE INTO HERE pure $ Right $ List - $ fmap (uncurry3 $ makeCodeLens plId sort) actions + $ fmap (uncurry3 $ makeCodeLens plId sort fc) actions codeLensProvider _ _ _ _ _ = pure $ Right $ List [] @@ -239,14 +246,15 @@ makeCodeLens :: (A.ToJSON b, IsContinuationSort sort) => PluginId -> sort + -> FileContext -> Range -> Metadata -> b -> LSP.CodeLens -makeCodeLens plId sort range (Metadata title _ _) b = - let cmd_id = toCommandId sort - -- TODO(sandy): BUG HERE. NEED TO PUSH THE FILE CONTEXT TOO - cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON b] +makeCodeLens plId sort fc range (Metadata title _ _) b = + let fc' = fc { fc_range = Just $ unsafeMkCurrent range } + cmd_id = toCommandId sort + cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON (fc', b)] in LSP.CodeLens { _range = range , _command = Just cmd From cdfcedc25f88588204f745764621276bee4f21ca Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 14:46:57 -0700 Subject: [PATCH 14/26] Port EmptyCase to Interaction --- .../src/Wingman/EmptyCase.hs | 102 +++++++++--------- .../hls-tactics-plugin/src/Wingman/Plugin.hs | 16 +-- 2 files changed, 51 insertions(+), 67 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 8335642a4e..568ca69ca1 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -1,4 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE NoMonoLocalBinds #-} @@ -9,7 +11,6 @@ import Control.Monad import Control.Monad.Except (runExcept) import Control.Monad.Trans import Control.Monad.Trans.Maybe -import Data.Aeson import Data.Generics.Aliases (mkQ, GenericQ) import Data.Generics.Schemes (everything) import Data.Maybe @@ -31,6 +32,7 @@ import OccName import Prelude hiding (span) import Prelude hiding (span) import TcRnTypes (tcg_binds) +import Wingman.AbstractLSP.Types import Wingman.CodeGen (destructionFor) import Wingman.GHC import Wingman.Judgements @@ -38,59 +40,51 @@ import Wingman.LanguageServer import Wingman.Types ------------------------------------------------------------------------------- --- | The 'CommandId' for the empty case completion. -emptyCaseLensCommandId :: CommandId -emptyCaseLensCommandId = CommandId "wingman.emptyCase" - - ------------------------------------------------------------------------------- --- | A command function that just applies a 'WorkspaceEdit'. -workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit -workspaceEditHandler _ideState wedit = do - _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ()) - return $ Right Null - - ------------------------------------------------------------------------------- --- | Provide the "empty case completion" code lens -codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens -codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri)) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - let stale a = runStaleIde "codeLensProvider" state nfp a - - ccs <- getClientCapabilities - liftIO $ fromMaybeT (Right $ List []) $ do - dflags <- getIdeDynflags state nfp - TrackedStale pm _ <- stale GetAnnotatedParsedSource - TrackedStale binds bind_map <- stale GetBindings - holes <- emptyCaseScrutinees state nfp - - fmap (Right . List) $ for holes $ \(ss, ty) -> do - binds_ss <- liftMaybe $ mapAgeFrom bind_map ss - let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss - range = realSrcSpanToRange $ unTrack ss - matches <- - liftMaybe $ - destructionFor - (foldMap (hySingleton . occName . fst) bindings) - ty - edits <- liftMaybe $ hush $ - mkWorkspaceEdits dflags ccs uri (unTrack pm) $ - graftMatchGroup (RealSrcSpan $ unTrack ss) $ - noLoc matches - - pure $ - CodeLens range - (Just - $ mkLspCommand - plId - emptyCaseLensCommandId - (mkEmptyCaseLensDesc ty) - $ Just $ pure $ toJSON $ edits - ) - Nothing -codeLensProvider _ _ _ = pure $ Right $ List [] +data EmptyCaseT = EmptyCaseT + +instance IsContinuationSort EmptyCaseT where + toCommandId _ = CommandId "wingman.emptyCase" + +instance IsTarget EmptyCaseT where + type TargetArgs EmptyCaseT = () + fetchTargetArgs _ = pure () + +emptyCaseInteraction :: Interaction +emptyCaseInteraction = Interaction $ + Continuation @EmptyCaseT @EmptyCaseT @WorkspaceEdit EmptyCaseT + (SynthesizeCodeLens $ \LspEnv{..} _ -> do + let FileContext{..} = le_fileContext + + let stale a = runStaleIde "codeLensProvider" le_ideState fc_nfp a + + ccs <- lift getClientCapabilities + TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + TrackedStale binds bind_map <- mapMaybeT liftIO $ stale GetBindings + holes <- mapMaybeT liftIO $ emptyCaseScrutinees le_ideState fc_nfp + + for holes $ \(ss, ty) -> do + binds_ss <- liftMaybe $ mapAgeFrom bind_map ss + let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss + range = realSrcSpanToRange $ unTrack ss + matches <- + liftMaybe $ + destructionFor + (foldMap (hySingleton . occName . fst) bindings) + ty + edits <- liftMaybe $ hush $ + mkWorkspaceEdits le_dflags ccs fc_uri (unTrack pm) $ + graftMatchGroup (RealSrcSpan $ unTrack ss) $ + noLoc matches + pure + ( range + , Metadata + (mkEmptyCaseLensDesc ty) + (CodeActionUnknown "refactor.wingman.completeEmptyCase") + False + , edits + ) + ) + $ (\ _ _ _ we -> pure $ RawEdit we) scrutinzedType :: EmptyCaseSort Type -> Maybe Type diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index 805eb29e9c..f5b0da3488 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -20,21 +20,11 @@ import Wingman.StaticPlugin descriptor :: PluginId -> PluginDescriptor IdeState descriptor plId = installInteractions - ( fmap makeTacticCodeAction [minBound .. maxBound] + ( emptyCaseInteraction + : fmap makeTacticCodeAction [minBound .. maxBound] ) $ (defaultPluginDescriptor plId) - { pluginCommands = - mconcat - [ pure $ - PluginCommand - emptyCaseLensCommandId - "Complete the empty case" - workspaceEditHandler - ] - , pluginHandlers = mconcat - [ mkPluginHandler STextDocumentCodeLens codeLensProvider - , mkPluginHandler STextDocumentHover hoverProvider - ] + { pluginHandlers = mkPluginHandler STextDocumentHover hoverProvider , pluginRules = wingmanRules plId , pluginConfigDescriptor = defaultConfigDescriptor From a552896cce58bd49f75e410e0d44d344256326a0 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 14:53:10 -0700 Subject: [PATCH 15/26] Rename makeTacticCodeAction -> makeTacticInteraction --- .../src/Wingman/AbstractLSP/TacticActions.hs | 4 ++-- plugins/hls-tactics-plugin/src/Wingman/Plugin.hs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index bc46b57a6c..62f51f7a34 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -31,10 +31,10 @@ import Wingman.Types ------------------------------------------------------------------------------ -- | An 'Interaction' for a 'TacticCommand'. -makeTacticCodeAction +makeTacticInteraction :: TacticCommand -> Interaction -makeTacticCodeAction cmd = +makeTacticInteraction cmd = Interaction $ Continuation @_ @HoleTarget cmd (SynthesizeCodeAction $ \env@LspEnv{..} hj -> do pure $ commandProvider cmd $ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index f5b0da3488..909ee6c26e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs @@ -10,7 +10,7 @@ import Ide.Types import Language.LSP.Types import Prelude hiding (span) import Wingman.AbstractLSP -import Wingman.AbstractLSP.TacticActions (makeTacticCodeAction) +import Wingman.AbstractLSP.TacticActions (makeTacticInteraction) import Wingman.EmptyCase import Wingman.LanguageServer import Wingman.LanguageServer.Metaprogram (hoverProvider) @@ -21,7 +21,7 @@ descriptor :: PluginId -> PluginDescriptor IdeState descriptor plId = installInteractions ( emptyCaseInteraction - : fmap makeTacticCodeAction [minBound .. maxBound] + : fmap makeTacticInteraction [minBound .. maxBound] ) $ (defaultPluginDescriptor plId) { pluginHandlers = mkPluginHandler STextDocumentHover hoverProvider From 2aedbe71c2b634cb0a5050a896aa3200f88afd71 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 13 Aug 2021 19:45:27 -0700 Subject: [PATCH 16/26] Support for partial timeouts in upcoming refinery v5 --- .../hls-tactics-plugin.cabal | 1 + .../src/Wingman/AbstractLSP/TacticActions.hs | 12 +-- .../src/Wingman/Machinery.hs | 89 +++++++++++++------ .../src/Wingman/Metaprogramming/Parser.hs | 5 +- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 24 ++--- .../hls-tactics-plugin/src/Wingman/Types.hs | 1 + 6 files changed, 81 insertions(+), 51 deletions(-) diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index f4d11fd892..3c0a809287 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -93,6 +93,7 @@ library , refinery ^>=0.4 , retrie >=0.1.1.0 , syb + , unagi-chan , text , transformers , unordered-containers diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index 62f51f7a34..4f66e0eb43 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -17,7 +17,6 @@ import Development.IDE.GHC.Compat import Development.IDE.GHC.ExactPrint import Generics.SYB.GHC (mkBindListT, everywhereM') import GhcPlugins (occName) -import System.Timeout (timeout) import Wingman.AbstractLSP.Types import Wingman.CaseSplit import Wingman.GHC (liftMaybe, isHole, pattern AMatch, unXPat) @@ -52,8 +51,8 @@ makeTacticInteraction cmd = pm_span <- liftMaybe $ mapAgeFrom pmmap span let t = commandTactic cmd var_name - res <- liftIO $ timeout (cfg_timeout_seconds le_config * seconds) $ do - runTactic hj_ctx hj_jdg t >>= \case + res <- + liftIO $ runTactic (cfg_timeout_seconds le_config * seconds) hj_ctx hj_jdg t >>= \case Left err -> pure $ ErrorMessages $ pure $ mkUserFacingMessage err Right rtr -> case rtr_extract rtr of @@ -66,9 +65,10 @@ makeTacticInteraction cmd = traceMX "solution" $ rtr_extract rtr pure $ GraftEdit $ graftHole (RealSrcSpan $ unTrack pm_span) rtr - pure $ case res of - Nothing -> ErrorMessages $ pure TimedOut - Just c -> c + pure res +-- pure $ case res of +-- Nothing -> ErrorMessages $ pure TimedOut +-- Just c -> c ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 9eb6e1dc62..b9553d94a6 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -1,5 +1,6 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} module Wingman.Machinery where @@ -16,7 +17,7 @@ import Data.Generics (everything, gcount, mkQ) import Data.Generics.Product (field') import Data.List (sortBy) import qualified Data.Map as M -import Data.Maybe (mapMaybe) +import Data.Maybe (mapMaybe, isJust) import Data.Monoid (getSum) import Data.Ord (Down (..), comparing) import qualified Data.Set as S @@ -34,6 +35,8 @@ import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tactics import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types +import Control.Concurrent.Chan.Unagi.NoBlocking (newChan, writeChan, OutChan, tryRead, tryReadChan) +import System.Timeout (timeout) substCTy :: TCvSubst -> CType -> CType @@ -71,15 +74,39 @@ tacticToRule :: Judgement -> TacticsM () -> Rule tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom +hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a +hoistElem _ Done = Done +hoistElem f (Next a lt) = Next a $ hoistListT f lt + + +hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a +hoistListT f t = ListT $ f $ fmap (hoistElem f) $ unListT t + + +consume :: Monad m => ListT m a -> (a -> m ()) -> m () +consume lt f = unListT lt >>= \case + Done -> pure () + Next a lt' -> f a >> consume lt' f + + +consumeChan :: OutChan (Maybe a) -> IO [a] +consumeChan chan = do + tryReadChan chan >>= tryRead >>= \case + Nothing -> pure [] + Just (Just a) -> (:) <$> pure a <*> consumeChan chan + Just Nothing -> pure [] + + ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. runTactic - :: Context + :: Int -- ^ Timeout + -> Context -> Judgement - -> TacticsM () -- ^ Tactic to use + -> TacticsM () -- ^ Tactic to use -> IO (Either [TacticError] RunTacticResults) -runTactic ctx jdg t = do +runTactic duration ctx jdg t = do let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ (:) (jGoal jdg) @@ -91,31 +118,35 @@ runTactic ctx jdg t = do defaultTacticState { ts_skolems = skolems } - res <- flip runReaderT ctx - . unExtractM - $ runTacticT t jdg tacticState - pure $ case res of - (Left errs) -> Left $ take 50 errs - (Right solns) -> do - let sorted = - flip sortBy solns $ comparing $ \(Proof ext _ holes) -> - Down $ scoreSolution ext jdg $ fmap snd holes - case sorted of - ((Proof syn _ subgoals) : _) -> - Right $ - RunTacticResults - { rtr_trace = syn_trace syn - , rtr_extract = simplify $ syn_val syn - , rtr_subgoals = fmap snd subgoals - , rtr_other_solns = reverse . fmap pf_extract $ sorted - , rtr_jdg = jdg - , rtr_ctx = ctx - } - -- guaranteed to not be empty - _ -> Left [] - -assoc23 :: (a, b, c) -> (a, (b, c)) -assoc23 (a, b, c) = (a, (b, c)) + + let stream = hoistListT (flip runReaderT ctx . unExtractM) + $ runStreamingTacticT t jdg tacticState + (in_chan, out_chan) <- newChan + timed_out <- + fmap isJust $ timeout duration $ consume stream $ \case + Left _ -> pure () + Right proof -> writeChan in_chan $ Just proof + writeChan in_chan Nothing + + solns <- consumeChan out_chan + pure $ do + let sorted = + flip sortBy solns $ comparing $ \(Proof ext _ holes) -> + Down $ scoreSolution ext jdg $ fmap snd holes + case sorted of + ((Proof syn _ subgoals) : _) -> + Right $ + RunTacticResults + { rtr_trace = syn_trace syn + , rtr_extract = simplify $ syn_val syn + , rtr_subgoals = fmap snd subgoals + , rtr_other_solns = reverse . fmap pf_extract $ sorted + , rtr_jdg = jdg + , rtr_ctx = ctx + , rtr_timed_out = timed_out + } + -- guaranteed to not be empty + _ -> Left [] tracePrim :: String -> Trace diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index 8277603faf..d22c20363e 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -447,10 +447,7 @@ attempt_it rsl ctx jdg program = case P.runParser tacticProgram "" (T.pack program) of Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb Right tt -> do - res <- runTactic - ctx - jdg - tt + res <- runTactic 2e6 ctx jdg tt pure $ case res of Left tes -> Left $ wrapError $ show tes Right rtr -> Right diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 44e996c8c7..71ec1bbd07 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -6,7 +6,7 @@ module Wingman.Tactics ) where import ConLike (ConLike(RealDataCon)) -import Control.Applicative (Alternative(empty)) +import Control.Applicative (Alternative(empty), (<|>)) import Control.Lens ((&), (%~), (<>~)) import Control.Monad (filterM) import Control.Monad (unless) @@ -465,17 +465,17 @@ auto' 0 = failure OutOfGas auto' n = do let loop = auto' (n - 1) try intros - choice - [ overFunctions $ \fname -> do - requireConcreteHole $ apply Saturated fname - loop - , overAlgebraicTerms $ \aname -> do - destructAuto aname - loop - , splitAuto >> loop - , assumption >> loop - , recursion - ] + assumption <|> + choice + [ overFunctions $ \fname -> do + requireConcreteHole $ apply Saturated fname + loop + , overAlgebraicTerms $ \aname -> do + destructAuto aname + loop + , splitAuto >> loop + , recursion + ] overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM () overFunctions = diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index 0ccee7b977..ca28e53177 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -530,6 +530,7 @@ data RunTacticResults = RunTacticResults , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)] , rtr_jdg :: Judgement , rtr_ctx :: Context + , rtr_timed_out :: Bool } deriving Show From d80fc2c5fd2b2006b3d34138e9256bfe7c4f06af Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 16 Aug 2021 08:39:37 -0700 Subject: [PATCH 17/26] asum instead of choice for assumption --- plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 71ec1bbd07..0e63e03ccf 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -48,6 +48,8 @@ import Wingman.Types -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () assumption = attemptOn (S.toList . allNames) assume + where + attemptOn getNames tac = matching (asum . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------ From 7ec618b32804e5e994a42d77e776013aa98aa534 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 16 Aug 2021 10:05:46 -0700 Subject: [PATCH 18/26] Don't count it as using a term if you only destruct it --- plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs | 1 - plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 4 ++-- plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs | 1 + .../test/golden/AutoUnusedPatternMatch.expected.hs | 2 ++ .../hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.hs | 2 ++ 5 files changed, 7 insertions(+), 3 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index ab3e266abd..57afba70e9 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs @@ -225,7 +225,6 @@ destruct' use_field_puns f hi jdg = do $ disallowing AlreadyDestructed (S.singleton term) jdg pure $ ext & #syn_trace %~ rose ("destruct " <> show term) . pure - & #syn_used_vals %~ S.insert term & #syn_val %~ noLoc . case' (var' term) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 44e996c8c7..8805ae2c99 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -63,7 +63,7 @@ assume name = rule $ \jdg -> do -- reasonable for a default value. (pure (noLoc $ var' name)) { syn_trace = tracePrim $ "assume " <> occNameString name - , syn_used_vals = S.singleton name + , syn_used_vals = S.singleton name <> getAncestry jdg name } Nothing -> cut @@ -298,7 +298,7 @@ apply (Unsaturated n) hi = tracing ("apply' " <> show (hi_name hi)) $ do ) saturated_args pure $ ext - & #syn_used_vals %~ S.insert func + & #syn_used_vals %~ (\x -> S.insert func x <> getAncestry jdg func) & #syn_val %~ mkApply func . fmap unLoc application :: TacticsM () diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index 413f33ad5c..cc97666a2a 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs @@ -49,6 +49,7 @@ spec = do autoTest 2 25 "AutoInfixInfix" autoTest 19 12 "AutoTypeLevel" autoTest 11 9 "AutoForallClassMethod" + autoTest 2 8 "AutoUnusedPatternMatch" failing "flaky in CI" $ autoTest 2 11 "GoldenApplicativeThen" diff --git a/plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.expected.hs b/plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.expected.hs new file mode 100644 index 0000000000..2885a1ca05 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.expected.hs @@ -0,0 +1,2 @@ +test :: Bool -> () +test _ = () diff --git a/plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.hs b/plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.hs new file mode 100644 index 0000000000..5345192969 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoUnusedPatternMatch.hs @@ -0,0 +1,2 @@ +test :: Bool -> () +test = _ From 1755392d667ae3dda1b5b2b0d97b0e99f06da16e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 16 Aug 2021 16:25:13 -0700 Subject: [PATCH 19/26] Let interactions return multiple results --- aka also info messages --- .../src/Wingman/AbstractLSP.hs | 47 +++++++++++-------- .../src/Wingman/AbstractLSP/TacticActions.hs | 45 +++++++++++------- .../src/Wingman/AbstractLSP/Types.hs | 2 +- .../src/Wingman/EmptyCase.hs | 2 +- .../src/Wingman/Machinery.hs | 2 +- .../hls-tactics-plugin/src/Wingman/Types.hs | 2 +- 6 files changed, 58 insertions(+), 42 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs index 0baf96a6d3..a7b83f0fd4 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP.hs @@ -13,8 +13,11 @@ import Control.Monad.IO.Class import Control.Monad.Trans (lift) import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT) import qualified Data.Aeson as A +import Data.Coerce import Data.Foldable (traverse_) +import Data.Monoid (Last (..)) import qualified Data.Text as T +import Data.Traversable (for) import Data.Tuple.Extra (uncurry3) import Development.IDE (IdeState) import Development.IDE.Core.UseStale @@ -93,26 +96,30 @@ runContinuation plId cont state (fc, b) = do env@LspEnv{..} <- buildEnv state plId fc let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a args <- fetchTargetArgs @a env - c_runCommand cont env args fc b >>= \case - ErrorMessages errs -> do - traverse_ showUserFacingMessage errs - pure $ Right A.Null - RawEdit edits -> do - sendEdits edits - pure $ Right A.Null - GraftEdit gr -> do - ccs <- lift getClientCapabilities - TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource - case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of - Left errs -> - pure $ Left $ ResponseError - { _code = InternalError - , _message = T.pack $ show errs - , _xdata = Nothing - } - Right edits -> do - sendEdits edits - pure $ Right A.Null + res <- c_runCommand cont env args fc b + + -- This block returns a maybe error. + fmap (maybe (Right $ A.Null) Left . coerce . foldMap Last) $ + for res $ \case + ErrorMessages errs -> do + traverse_ showUserFacingMessage errs + pure Nothing + RawEdit edits -> do + sendEdits edits + pure Nothing + GraftEdit gr -> do + ccs <- lift getClientCapabilities + TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of + Left errs -> + pure $ Just $ ResponseError + { _code = InternalError + , _message = T.pack $ show errs + , _xdata = Nothing + } + Right edits -> do + sendEdits edits + pure $ Nothing ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index 4f66e0eb43..542b2620e1 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -51,24 +51,33 @@ makeTacticInteraction cmd = pm_span <- liftMaybe $ mapAgeFrom pmmap span let t = commandTactic cmd var_name - res <- - liftIO $ runTactic (cfg_timeout_seconds le_config * seconds) hj_ctx hj_jdg t >>= \case - Left err -> pure $ ErrorMessages $ pure $ mkUserFacingMessage err - Right rtr -> - case rtr_extract rtr of - L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> - pure $ ErrorMessages [NothingToDo] - _ -> do - for_ (rtr_other_solns rtr) $ \soln -> do - traceMX "other solution" $ syn_val soln - traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] - traceMX "solution" $ rtr_extract rtr - pure $ GraftEdit $ graftHole (RealSrcSpan $ unTrack pm_span) rtr - - pure res --- pure $ case res of --- Nothing -> ErrorMessages $ pure TimedOut --- Just c -> c + liftIO $ runTactic (cfg_timeout_seconds le_config * seconds) hj_ctx hj_jdg t >>= \case + Left err -> pure $ pure $ ErrorMessages $ pure $ mkUserFacingMessage err + Right rtr -> + case rtr_extract rtr of + L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> + pure + $ addTimeoutMessage rtr + $ pure + $ ErrorMessages + $ pure NothingToDo + _ -> do + for_ (rtr_other_solns rtr) $ \soln -> do + traceMX "other solution" $ syn_val soln + traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] + traceMX "solution" $ rtr_extract rtr + pure + $ addTimeoutMessage rtr + $ pure + $ GraftEdit + $ graftHole (RealSrcSpan $ unTrack pm_span) rtr + + +addTimeoutMessage :: RunTacticResults -> [ContinuationResult] -> [ContinuationResult] +addTimeoutMessage rtr = mappend + [ ErrorMessages $ pure TimedOut + | rtr_timed_out rtr + ] ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs index 8b00f0b021..8555b880d2 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/Types.hs @@ -113,7 +113,7 @@ data Continuation sort target payload = Continuation -> TargetArgs target -> FileContext -> payload - -> MaybeT (LspM Plugin.Config) ContinuationResult + -> MaybeT (LspM Plugin.Config) [ContinuationResult] } diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 568ca69ca1..93deee4e3a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -84,7 +84,7 @@ emptyCaseInteraction = Interaction $ , edits ) ) - $ (\ _ _ _ we -> pure $ RawEdit we) + $ (\ _ _ _ we -> pure $ pure $ RawEdit we) scrutinzedType :: EmptyCaseSort Type -> Maybe Type diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index b9553d94a6..7ad9ef157a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -123,7 +123,7 @@ runTactic duration ctx jdg t = do $ runStreamingTacticT t jdg tacticState (in_chan, out_chan) <- newChan timed_out <- - fmap isJust $ timeout duration $ consume stream $ \case + fmap (not. isJust) $ timeout duration $ consume stream $ \case Left _ -> pure () Right proof -> writeChan in_chan $ Just proof writeChan in_chan Nothing diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index ca28e53177..491ff9724a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -552,7 +552,7 @@ data UserFacingMessage instance Show UserFacingMessage where show NotEnoughGas = "Wingman ran out of gas when trying to find a solution. \nTry increasing the `auto_gas` setting." show TacticErrors = "Wingman couldn't find a solution" - show TimedOut = "Wingman timed out while trying to find a solution" + show TimedOut = "Wingman timed out while finding a solution. \nYou might get a better result if you increase the timeout duration." show NothingToDo = "Nothing to do" show (InfrastructureError t) = "Internal error: " <> T.unpack t From 53199b3b781884d7bd85ac8fb3efa1d2da915ea6 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 16 Aug 2021 16:27:48 -0700 Subject: [PATCH 20/26] Update refinery lower bounds --- plugins/hls-tactics-plugin/hls-tactics-plugin.cabal | 2 +- stack-8.10.2.yaml | 2 +- stack-8.10.3.yaml | 2 +- stack-8.10.4.yaml | 2 +- stack-8.10.5.yaml | 2 +- stack-8.6.4.yaml | 2 +- stack-8.6.5.yaml | 2 +- stack-8.8.3.yaml | 2 +- stack-8.8.4.yaml | 2 +- stack-9.0.1.yaml | 2 +- stack.yaml | 2 +- 11 files changed, 11 insertions(+), 11 deletions(-) diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index 3c0a809287..df457d0d2b 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -90,7 +90,7 @@ library , mtl , parser-combinators , prettyprinter - , refinery ^>=0.4 + , refinery ^>=0.5 , retrie >=0.1.1.0 , syb , unagi-chan diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index 893a340c60..46c103cfe3 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -50,7 +50,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-0.1.1.1 - shake-0.19.4 - stylish-haskell-0.12.2.0 diff --git a/stack-8.10.3.yaml b/stack-8.10.3.yaml index c0d360d3f6..5f813b05f9 100644 --- a/stack-8.10.3.yaml +++ b/stack-8.10.3.yaml @@ -50,7 +50,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-0.1.1.1 - shake-0.19.4 - stylish-haskell-0.12.2.0 diff --git a/stack-8.10.4.yaml b/stack-8.10.4.yaml index b4c06fc578..ea861e26bc 100644 --- a/stack-8.10.4.yaml +++ b/stack-8.10.4.yaml @@ -47,7 +47,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-0.1.1.1 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 diff --git a/stack-8.10.5.yaml b/stack-8.10.5.yaml index 1e9b4281a3..50f07fa2d0 100644 --- a/stack-8.10.5.yaml +++ b/stack-8.10.5.yaml @@ -49,7 +49,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-1.0.0.0 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml index b37a0503b6..8036d50512 100644 --- a/stack-8.6.4.yaml +++ b/stack-8.6.4.yaml @@ -76,7 +76,7 @@ extra-deps: - ormolu-0.1.4.1 - parser-combinators-1.2.1 - primitive-0.7.1.0 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index f012979944..ea0215901b 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -77,7 +77,7 @@ extra-deps: - ormolu-0.1.4.1 - parser-combinators-1.2.1 - primitive-0.7.1.0 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml index c202d21c82..87995b1a4a 100644 --- a/stack-8.8.3.yaml +++ b/stack-8.8.3.yaml @@ -63,7 +63,7 @@ extra-deps: - opentelemetry-0.6.1 - opentelemetry-extra-0.6.1 - ormolu-0.1.4.1 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 - shake-0.19.4 diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml index 33c01989a6..18fd206453 100644 --- a/stack-8.8.4.yaml +++ b/stack-8.8.4.yaml @@ -62,7 +62,7 @@ extra-deps: - monad-dijkstra-0.1.1.2 - opentelemetry-0.6.1 - opentelemetry-extra-0.6.1 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 - shake-0.19.4 diff --git a/stack-9.0.1.yaml b/stack-9.0.1.yaml index 112dada930..3b18d18bdb 100644 --- a/stack-9.0.1.yaml +++ b/stack-9.0.1.yaml @@ -51,7 +51,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - lens-5.0.1 - profunctors-5.6.2 -- refinery-0.4.0.0 +- refinery-0.5.0.0 - retrie-1.0.0.0 - some-1.0.2@sha256:3d460998df32ad7b93bf55657aeae988d97070155e71718b4bc75d0997ce9d62,2244 - lsp-1.2.0.1 diff --git a/stack.yaml b/stack.yaml index b9ded8b709..645e4fbd39 100644 --- a/stack.yaml +++ b/stack.yaml @@ -44,7 +44,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.4.0.0 + - refinery-0.5.0.0 - retrie-0.1.1.1 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 From 436bf46de7afb2591d0ed7407932cc3ba1163e9d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 18 Aug 2021 20:06:08 -0700 Subject: [PATCH 21/26] Revert "Update refinery lower bounds" This reverts commit 53199b3b781884d7bd85ac8fb3efa1d2da915ea6. --- plugins/hls-tactics-plugin/hls-tactics-plugin.cabal | 2 +- stack-8.10.2.yaml | 2 +- stack-8.10.3.yaml | 2 +- stack-8.10.4.yaml | 2 +- stack-8.10.5.yaml | 2 +- stack-8.6.4.yaml | 2 +- stack-8.6.5.yaml | 2 +- stack-8.8.3.yaml | 2 +- stack-8.8.4.yaml | 2 +- stack-9.0.1.yaml | 2 +- stack.yaml | 2 +- 11 files changed, 11 insertions(+), 11 deletions(-) diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index df457d0d2b..3c0a809287 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -90,7 +90,7 @@ library , mtl , parser-combinators , prettyprinter - , refinery ^>=0.5 + , refinery ^>=0.4 , retrie >=0.1.1.0 , syb , unagi-chan diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index 46c103cfe3..893a340c60 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -50,7 +50,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-0.1.1.1 - shake-0.19.4 - stylish-haskell-0.12.2.0 diff --git a/stack-8.10.3.yaml b/stack-8.10.3.yaml index 5f813b05f9..c0d360d3f6 100644 --- a/stack-8.10.3.yaml +++ b/stack-8.10.3.yaml @@ -50,7 +50,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-0.1.1.1 - shake-0.19.4 - stylish-haskell-0.12.2.0 diff --git a/stack-8.10.4.yaml b/stack-8.10.4.yaml index ea861e26bc..b4c06fc578 100644 --- a/stack-8.10.4.yaml +++ b/stack-8.10.4.yaml @@ -47,7 +47,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-0.1.1.1 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 diff --git a/stack-8.10.5.yaml b/stack-8.10.5.yaml index 50f07fa2d0..1e9b4281a3 100644 --- a/stack-8.10.5.yaml +++ b/stack-8.10.5.yaml @@ -49,7 +49,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-1.0.0.0 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml index 8036d50512..b37a0503b6 100644 --- a/stack-8.6.4.yaml +++ b/stack-8.6.4.yaml @@ -76,7 +76,7 @@ extra-deps: - ormolu-0.1.4.1 - parser-combinators-1.2.1 - primitive-0.7.1.0 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index ea0215901b..f012979944 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -77,7 +77,7 @@ extra-deps: - ormolu-0.1.4.1 - parser-combinators-1.2.1 - primitive-0.7.1.0 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml index 87995b1a4a..c202d21c82 100644 --- a/stack-8.8.3.yaml +++ b/stack-8.8.3.yaml @@ -63,7 +63,7 @@ extra-deps: - opentelemetry-0.6.1 - opentelemetry-extra-0.6.1 - ormolu-0.1.4.1 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 - shake-0.19.4 diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml index 18fd206453..33c01989a6 100644 --- a/stack-8.8.4.yaml +++ b/stack-8.8.4.yaml @@ -62,7 +62,7 @@ extra-deps: - monad-dijkstra-0.1.1.2 - opentelemetry-0.6.1 - opentelemetry-extra-0.6.1 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 - shake-0.19.4 diff --git a/stack-9.0.1.yaml b/stack-9.0.1.yaml index 3b18d18bdb..112dada930 100644 --- a/stack-9.0.1.yaml +++ b/stack-9.0.1.yaml @@ -51,7 +51,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - lens-5.0.1 - profunctors-5.6.2 -- refinery-0.5.0.0 +- refinery-0.4.0.0 - retrie-1.0.0.0 - some-1.0.2@sha256:3d460998df32ad7b93bf55657aeae988d97070155e71718b4bc75d0997ce9d62,2244 - lsp-1.2.0.1 diff --git a/stack.yaml b/stack.yaml index 645e4fbd39..b9ded8b709 100644 --- a/stack.yaml +++ b/stack.yaml @@ -44,7 +44,7 @@ extra-deps: - implicit-hie-cradle-0.3.0.5 - implicit-hie-0.1.2.6 - monad-dijkstra-0.1.1.2 - - refinery-0.5.0.0 + - refinery-0.4.0.0 - retrie-0.1.1.1 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 From 602205debc2694a6f0af670a8f3d4afc20c746d8 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 18 Aug 2021 20:16:59 -0700 Subject: [PATCH 22/26] Pull refinery from the future --- .../hls-tactics-plugin.cabal | 1 + .../hls-tactics-plugin/src/Refinery/Future.hs | 140 ++++++++++++++++++ .../src/Wingman/Machinery.hs | 20 +-- 3 files changed, 144 insertions(+), 17 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Refinery/Future.hs diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index 3c0a809287..161f7e2613 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -27,6 +27,7 @@ library hs-source-dirs: src exposed-modules: Ide.Plugin.Tactic + Refinery.Future Wingman.AbstractLSP Wingman.AbstractLSP.TacticActions Wingman.AbstractLSP.Types diff --git a/plugins/hls-tactics-plugin/src/Refinery/Future.hs b/plugins/hls-tactics-plugin/src/Refinery/Future.hs new file mode 100644 index 0000000000..51d844b3b4 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Refinery/Future.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE RankNTypes #-} + +------------------------------------------------------------------------------ +-- | Things that belong in the future release of refinery v5. +module Refinery.Future + ( runStreamingTacticT + , hoistListT + , consume + ) where + +import Control.Applicative +import Control.Monad (ap, (>=>)) +import Control.Monad.State.Lazy (runStateT) +import Control.Monad.Trans +import Data.Either (isRight) +import Data.Functor ((<&>)) +import Data.Tuple (swap) +import Refinery.ProofState +import Refinery.Tactic.Internal + + + +hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a +hoistElem _ Done = Done +hoistElem f (Next a lt) = Next a $ hoistListT f lt + + +hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a +hoistListT f t = ListT $ f $ fmap (hoistElem f) $ unListT t + + +consume :: Monad m => ListT m a -> (a -> m ()) -> m () +consume lt f = unListT lt >>= \case + Done -> pure () + Next a lt' -> f a >> consume lt' f + + +newHole :: MonadExtract meta ext err s m => s -> m (s, (meta, ext)) +newHole = fmap swap . runStateT hole + +runStreamingTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> ListT m (Either err (Proof s meta jdg ext)) +runStreamingTacticT t j s = streamProofs s $ fmap snd $ proofState t j + +data Elem m a + = Done + | Next a (ListT m a) + deriving stock Functor + + +point :: Applicative m => a -> Elem m a +point a = Next a $ ListT $ pure Done + +newtype ListT m a = ListT { unListT :: m (Elem m a) } + +cons :: (Applicative m) => a -> ListT m a -> ListT m a +cons x xs = ListT $ pure $ Next x xs + +instance Functor m => Functor (ListT m) where + fmap f (ListT xs) = ListT $ xs <&> \case + Done -> Done + Next a xs -> Next (f a) (fmap f xs) + +instance (Monad m) => Applicative (ListT m) where + pure = return + (<*>) = ap + +instance (Monad m) => Alternative (ListT m) where + empty = ListT $ pure Done + (ListT xs) <|> (ListT ys) = + ListT $ xs >>= \case + Done -> ys + Next x xs -> pure (Next x (xs <|> ListT ys)) + +instance (Monad m) => Monad (ListT m) where + return a = cons a empty + (ListT xs) >>= k = + ListT $ xs >>= \case + Done -> pure Done + Next x xs -> unListT $ k x <|> (xs >>= k) + + +instance MonadTrans ListT where + lift m = ListT $ fmap (\x -> Next x empty) m + + +interleaveT :: (Monad m) => Elem m a -> Elem m a -> Elem m a +interleaveT xs ys = + case xs of + Done -> ys + Next x xs -> Next x $ ListT $ fmap (interleaveT ys) $ unListT xs + +-- ys <&> \case +-- Done -> Next x xs +-- Next y ys -> Next x (cons y (interleaveT xs ys)) + +force :: (Monad m) => Elem m a -> m [a] +force = \case + Done -> pure [] + Next x xs' -> (x:) <$> (unListT xs' >>= force) + +ofList :: Monad m => [a] -> Elem m a +ofList [] = Done +ofList (x:xs) = Next x $ ListT $ pure $ ofList xs + +streamProofs :: forall ext err s m goal meta. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> ListT m (Either err (Proof s meta goal ext)) +streamProofs s p = ListT $ go s [] pure p + where + go :: s -> [(meta, goal)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Elem m (Either err (Proof s meta goal ext))) + go s goals _ (Subgoal goal k) = do + (s', (meta, h)) <- newHole s + -- Note [Handler Reset]: + -- We reset the handler stack to avoid the handlers leaking across subgoals. + -- This would happen when we had a handler that wasn't followed by an error call. + -- pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error" + -- We would see the "Handling a" message when solving for b. + (go s' (goals ++ [(meta, goal)]) pure $ k h) + go s goals handlers (Effect m) = m >>= go s goals handlers + go s goals handlers (Stateful f) = + let (s', p) = f s + in go s' goals handlers p + go s goals handlers (Alt p1 p2) = + unListT $ ListT (go s goals handlers p1) <|> ListT (go s goals handlers p2) + go s goals handlers (Interleave p1 p2) = + interleaveT <$> (go s goals handlers p1) <*> (go s goals handlers p2) + go s goals handlers (Commit p1 p2) = do + solns <- force =<< go s goals handlers p1 + if (any isRight solns) then pure $ ofList solns else go s goals handlers p2 + go _ _ _ Empty = pure Done + go _ _ handlers (Failure err _) = do + annErr <- handlers err + pure $ point $ Left annErr + go s goals handlers (Handle p h) = + -- Note [Handler ordering]: + -- If we have multiple handlers in scope, then we want the handlers closer to the error site to + -- run /first/. This allows the handlers up the stack to add their annotations on top of the + -- ones lower down, which is the behavior that we desire. + -- IE: for @handler f >> handler g >> failure err@, @g@ ought to be run before @f@. + go s goals (h >=> handlers) p + go s goals _ (Axiom ext) = pure $ point $ Right (Proof ext s goals) + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 7ad9ef157a..e2fa307d15 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -5,6 +5,7 @@ module Wingman.Machinery where import Control.Applicative (empty) +import Control.Concurrent.Chan.Unagi.NoBlocking (newChan, writeChan, OutChan, tryRead, tryReadChan) import Control.Lens ((<>~)) import Control.Monad.Reader import Control.Monad.State.Class (gets, modify, MonadState) @@ -25,9 +26,11 @@ import Data.Traversable (for) import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType) +import Refinery.Future import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal +import System.Timeout (timeout) import TcType import Type (tyCoVarsOfTypeWellScoped) import Wingman.Context (getInstance) @@ -35,8 +38,6 @@ import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tactics import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types -import Control.Concurrent.Chan.Unagi.NoBlocking (newChan, writeChan, OutChan, tryRead, tryReadChan) -import System.Timeout (timeout) substCTy :: TCvSubst -> CType -> CType @@ -74,21 +75,6 @@ tacticToRule :: Judgement -> TacticsM () -> Rule tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom -hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a -hoistElem _ Done = Done -hoistElem f (Next a lt) = Next a $ hoistListT f lt - - -hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a -hoistListT f t = ListT $ f $ fmap (hoistElem f) $ unListT t - - -consume :: Monad m => ListT m a -> (a -> m ()) -> m () -consume lt f = unListT lt >>= \case - Done -> pure () - Next a lt' -> f a >> consume lt' f - - consumeChan :: OutChan (Maybe a) -> IO [a] consumeChan chan = do tryReadChan chan >>= tryRead >>= \case From 278310066c677c352a801d72dbf0b90108ce72a0 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 18 Aug 2021 23:09:01 -0700 Subject: [PATCH 23/26] Fix tests --- plugins/hls-tactics-plugin/test/AutoTupleSpec.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs index a617683d6e..88eb862611 100644 --- a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs +++ b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs @@ -36,6 +36,7 @@ spec = describe "auto for tuple" $ do -- We should always be able to find a solution unsafePerformIO (runTactic + 2e6 emptyContext (mkFirstJudgement emptyContext From 063987dfedd2031a1f3a883bb5c2e20256029c72 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 19 Aug 2021 08:37:40 -0700 Subject: [PATCH 24/26] Add -XNumDecimals --- plugins/hls-tactics-plugin/test/AutoTupleSpec.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs index 88eb862611..38306e55c7 100644 --- a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs +++ b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE NumDecimals #-} + {-# OPTIONS_GHC -fno-warn-orphans #-} module AutoTupleSpec where From cf3a941e425c524f048a1fe4c7f1bbbbc264a720 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 20 Aug 2021 17:17:09 -0500 Subject: [PATCH 25/26] Fix AutoTypeLevel test --- plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 2 -- 1 file changed, 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index d59e5cbbe6..a853335e35 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -48,8 +48,6 @@ import Wingman.Types -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () assumption = attemptOn (S.toList . allNames) assume - where - attemptOn getNames tac = matching (asum . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------ From 54469b53925608a36a608fe0806aaf71bb041c92 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 20 Aug 2021 17:39:14 -0500 Subject: [PATCH 26/26] Continue to emit errors --- .../src/Wingman/AbstractLSP/TacticActions.hs | 8 +++- .../src/Wingman/Machinery.hs | 47 +++++++++---------- 2 files changed, 30 insertions(+), 25 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs index 71a6e7927c..89769ae8aa 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/AbstractLSP/TacticActions.hs @@ -53,7 +53,12 @@ makeTacticInteraction cmd = let t = commandTactic cmd var_name liftIO $ runTactic (cfg_timeout_seconds le_config * seconds) hj_ctx hj_jdg t >>= \case - Left err -> pure $ pure $ ErrorMessages $ pure $ mkUserFacingMessage err + Left err -> + pure + $ pure + $ ErrorMessages + $ pure + $ mkUserFacingMessage err Right rtr -> case rtr_extract rtr of L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> @@ -92,6 +97,7 @@ seconds = 1e6 mkUserFacingMessage :: [TacticError] -> UserFacingMessage mkUserFacingMessage errs | elem OutOfGas errs = NotEnoughGas +mkUserFacingMessage [] = NothingToDo mkUserFacingMessage _ = TacticErrors diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index e2fa307d15..0cebec94b7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -107,32 +107,31 @@ runTactic duration ctx jdg t = do let stream = hoistListT (flip runReaderT ctx . unExtractM) $ runStreamingTacticT t jdg tacticState - (in_chan, out_chan) <- newChan + (in_proofs, out_proofs) <- newChan + (in_errs, out_errs) <- newChan timed_out <- fmap (not. isJust) $ timeout duration $ consume stream $ \case - Left _ -> pure () - Right proof -> writeChan in_chan $ Just proof - writeChan in_chan Nothing - - solns <- consumeChan out_chan - pure $ do - let sorted = - flip sortBy solns $ comparing $ \(Proof ext _ holes) -> - Down $ scoreSolution ext jdg $ fmap snd holes - case sorted of - ((Proof syn _ subgoals) : _) -> - Right $ - RunTacticResults - { rtr_trace = syn_trace syn - , rtr_extract = simplify $ syn_val syn - , rtr_subgoals = fmap snd subgoals - , rtr_other_solns = reverse . fmap pf_extract $ sorted - , rtr_jdg = jdg - , rtr_ctx = ctx - , rtr_timed_out = timed_out - } - -- guaranteed to not be empty - _ -> Left [] + Left err -> writeChan in_errs $ Just err + Right proof -> writeChan in_proofs $ Just proof + writeChan in_proofs Nothing + + solns <- consumeChan out_proofs + let sorted = + flip sortBy solns $ comparing $ \(Proof ext _ holes) -> + Down $ scoreSolution ext jdg $ fmap snd holes + case sorted of + ((Proof syn _ subgoals) : _) -> + pure $ Right $ + RunTacticResults + { rtr_trace = syn_trace syn + , rtr_extract = simplify $ syn_val syn + , rtr_subgoals = fmap snd subgoals + , rtr_other_solns = reverse . fmap pf_extract $ sorted + , rtr_jdg = jdg + , rtr_ctx = ctx + , rtr_timed_out = timed_out + } + _ -> fmap Left $ consumeChan out_errs tracePrim :: String -> Trace