{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Wingman.Plugin
( descriptor
, tacticTitle
, TacticCommand (..)
) 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.CaseSplit
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 :: PluginId -> PluginDescriptor IdeState
descriptor PluginId
plId = (PluginId -> PluginDescriptor IdeState
forall ideState. PluginId -> PluginDescriptor ideState
defaultPluginDescriptor PluginId
plId)
{ pluginCommands :: [PluginCommand IdeState]
pluginCommands
= [[PluginCommand IdeState]] -> [PluginCommand IdeState]
forall a. Monoid a => [a] -> a
mconcat
[ (TacticCommand -> PluginCommand IdeState)
-> [TacticCommand] -> [PluginCommand IdeState]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\TacticCommand
tc ->
CommandId
-> Text
-> CommandFunction IdeState TacticParams
-> PluginCommand IdeState
forall ideState a.
FromJSON a =>
CommandId
-> Text -> CommandFunction ideState a -> PluginCommand ideState
PluginCommand
(TacticCommand -> CommandId
tcCommandId TacticCommand
tc)
(Text -> Text
tacticDesc (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ TacticCommand -> Text
tcCommandName TacticCommand
tc)
((Text -> TacticsM ())
-> PluginId -> CommandFunction IdeState TacticParams
tacticCmd (TacticCommand -> Text -> TacticsM ()
commandTactic TacticCommand
tc) PluginId
plId))
[TacticCommand
forall a. Bounded a => a
minBound .. TacticCommand
forall a. Bounded a => a
maxBound]
, PluginCommand IdeState -> [PluginCommand IdeState]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PluginCommand IdeState -> [PluginCommand IdeState])
-> PluginCommand IdeState -> [PluginCommand IdeState]
forall a b. (a -> b) -> a -> b
$
CommandId
-> Text
-> CommandFunction IdeState WorkspaceEdit
-> PluginCommand IdeState
forall ideState a.
FromJSON a =>
CommandId
-> Text -> CommandFunction ideState a -> PluginCommand ideState
PluginCommand
CommandId
emptyCaseLensCommandId
Text
"Complete the empty case"
CommandFunction IdeState WorkspaceEdit
workspaceEditHandler
]
, pluginHandlers :: PluginHandlers IdeState
pluginHandlers = [PluginHandlers IdeState] -> PluginHandlers IdeState
forall a. Monoid a => [a] -> a
mconcat
[ SClientMethod 'TextDocumentCodeAction
-> PluginMethodHandler IdeState 'TextDocumentCodeAction
-> PluginHandlers IdeState
forall (m :: Method 'FromClient 'Request) ideState.
PluginMethod m =>
SClientMethod m
-> PluginMethodHandler ideState m -> PluginHandlers ideState
mkPluginHandler SClientMethod 'TextDocumentCodeAction
STextDocumentCodeAction PluginMethodHandler IdeState 'TextDocumentCodeAction
codeActionProvider
, SClientMethod 'TextDocumentCodeLens
-> PluginMethodHandler IdeState 'TextDocumentCodeLens
-> PluginHandlers IdeState
forall (m :: Method 'FromClient 'Request) ideState.
PluginMethod m =>
SClientMethod m
-> PluginMethodHandler ideState m -> PluginHandlers ideState
mkPluginHandler SClientMethod 'TextDocumentCodeLens
STextDocumentCodeLens PluginMethodHandler IdeState 'TextDocumentCodeLens
codeLensProvider
, SClientMethod 'TextDocumentHover
-> PluginMethodHandler IdeState 'TextDocumentHover
-> PluginHandlers IdeState
forall (m :: Method 'FromClient 'Request) ideState.
PluginMethod m =>
SClientMethod m
-> PluginMethodHandler ideState m -> PluginHandlers ideState
mkPluginHandler SClientMethod 'TextDocumentHover
STextDocumentHover PluginMethodHandler IdeState 'TextDocumentHover
hoverProvider
]
, pluginRules :: Rules ()
pluginRules = PluginId -> Rules ()
wingmanRules PluginId
plId
, pluginConfigDescriptor :: ConfigDescriptor
pluginConfigDescriptor =
ConfigDescriptor
defaultConfigDescriptor {configCustomConfig :: CustomConfig
configCustomConfig = Properties
'[ 'PropertyKey
"hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
'PropertyKey "max_use_ctor_actions" 'TInteger,
'PropertyKey "timeout_duration" 'TInteger,
'PropertyKey "auto_gas" 'TInteger,
'PropertyKey "proofstate_styling" 'TBoolean]
-> CustomConfig
forall (r :: [PropertyKey]). Properties r -> CustomConfig
mkCustomConfig Properties
'[ 'PropertyKey
"hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
'PropertyKey "max_use_ctor_actions" 'TInteger,
'PropertyKey "timeout_duration" 'TInteger,
'PropertyKey "auto_gas" 'TInteger,
'PropertyKey "proofstate_styling" 'TBoolean]
properties}
, pluginModifyDynflags :: DynFlagsModifications
pluginModifyDynflags = DynFlagsModifications
staticPlugin
}
codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
codeActionProvider :: PluginMethodHandler IdeState 'TextDocumentCodeAction
codeActionProvider IdeState
state PluginId
plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx)
| Just NormalizedFilePath
nfp <- NormalizedUri -> Maybe NormalizedFilePath
uriToNormalizedFilePath (NormalizedUri -> Maybe NormalizedFilePath)
-> NormalizedUri -> Maybe NormalizedFilePath
forall a b. (a -> b) -> a -> b
$ Uri -> NormalizedUri
toNormalizedUri Uri
uri = do
Config
cfg <- PluginId -> LspT Config IO Config
forall (m :: * -> *). MonadLsp Config m => PluginId -> m Config
getTacticConfig PluginId
plId
IO (Either ResponseError (List (Command |? CodeAction)))
-> LspT
Config IO (Either ResponseError (List (Command |? CodeAction)))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either ResponseError (List (Command |? CodeAction)))
-> LspT
Config IO (Either ResponseError (List (Command |? CodeAction))))
-> IO (Either ResponseError (List (Command |? CodeAction)))
-> LspT
Config IO (Either ResponseError (List (Command |? CodeAction)))
forall a b. (a -> b) -> a -> b
$ Either ResponseError (List (Command |? CodeAction))
-> MaybeT IO (Either ResponseError (List (Command |? CodeAction)))
-> IO (Either ResponseError (List (Command |? CodeAction)))
forall (m :: * -> *) a. Functor m => a -> MaybeT m a -> m a
fromMaybeT (List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction))
forall a b. b -> Either a b
Right (List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction)))
-> List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction))
forall a b. (a -> b) -> a -> b
$ [Command |? CodeAction] -> List (Command |? CodeAction)
forall a. [a] -> List a
List []) (MaybeT IO (Either ResponseError (List (Command |? CodeAction)))
-> IO (Either ResponseError (List (Command |? CodeAction))))
-> MaybeT IO (Either ResponseError (List (Command |? CodeAction)))
-> IO (Either ResponseError (List (Command |? CodeAction)))
forall a b. (a -> b) -> a -> b
$ do
HoleJudgment{DynFlags
Tracked 'Current Range
HoleSort
Context
Judgement
hj_hole_sort :: HoleJudgment -> HoleSort
hj_dflags :: HoleJudgment -> DynFlags
hj_ctx :: HoleJudgment -> Context
hj_jdg :: HoleJudgment -> Judgement
hj_range :: HoleJudgment -> Tracked 'Current Range
hj_hole_sort :: HoleSort
hj_dflags :: DynFlags
hj_ctx :: Context
hj_jdg :: Judgement
hj_range :: Tracked 'Current Range
..} <- IdeState
-> NormalizedFilePath
-> Tracked 'Current Range
-> Config
-> MaybeT IO HoleJudgment
judgementForHole IdeState
state NormalizedFilePath
nfp Tracked 'Current Range
range Config
cfg
[Command |? CodeAction]
actions <- IO [Command |? CodeAction] -> MaybeT IO [Command |? CodeAction]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [Command |? CodeAction] -> MaybeT IO [Command |? CodeAction])
-> IO [Command |? CodeAction] -> MaybeT IO [Command |? CodeAction]
forall a b. (a -> b) -> a -> b
$
(TacticCommand -> TacticProvider)
-> [TacticCommand] -> TacticProvider
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TacticCommand -> TacticProvider
commandProvider [TacticCommand
forall a. Bounded a => a
minBound .. TacticCommand
forall a. Bounded a => a
maxBound] TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$ TacticProviderData :: DynFlags
-> Config
-> PluginId
-> Uri
-> Tracked 'Current Range
-> Judgement
-> HoleSort
-> TacticProviderData
TacticProviderData
{ tpd_dflags :: DynFlags
tpd_dflags = DynFlags
hj_dflags
, tpd_config :: Config
tpd_config = Config
cfg
, tpd_plid :: PluginId
tpd_plid = PluginId
plId
, tpd_uri :: Uri
tpd_uri = Uri
uri
, tpd_range :: Tracked 'Current Range
tpd_range = Tracked 'Current Range
range
, tpd_jdg :: Judgement
tpd_jdg = Judgement
hj_jdg
, tpd_hole_sort :: HoleSort
tpd_hole_sort = HoleSort
hj_hole_sort
}
Either ResponseError (List (Command |? CodeAction))
-> MaybeT IO (Either ResponseError (List (Command |? CodeAction)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError (List (Command |? CodeAction))
-> MaybeT IO (Either ResponseError (List (Command |? CodeAction))))
-> Either ResponseError (List (Command |? CodeAction))
-> MaybeT IO (Either ResponseError (List (Command |? CodeAction)))
forall a b. (a -> b) -> a -> b
$ List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction))
forall a b. b -> Either a b
Right (List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction)))
-> List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction))
forall a b. (a -> b) -> a -> b
$ [Command |? CodeAction] -> List (Command |? CodeAction)
forall a. [a] -> List a
List [Command |? CodeAction]
actions
codeActionProvider IdeState
_ PluginId
_ MessageParams 'TextDocumentCodeAction
_ = Either ResponseError (List (Command |? CodeAction))
-> LspT
Config IO (Either ResponseError (List (Command |? CodeAction)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError (List (Command |? CodeAction))
-> LspT
Config IO (Either ResponseError (List (Command |? CodeAction))))
-> Either ResponseError (List (Command |? CodeAction))
-> LspT
Config IO (Either ResponseError (List (Command |? CodeAction)))
forall a b. (a -> b) -> a -> b
$ List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction))
forall a b. b -> Either a b
Right (List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction)))
-> List (Command |? CodeAction)
-> Either ResponseError (List (Command |? CodeAction))
forall a b. (a -> b) -> a -> b
$ [Command |? CodeAction] -> List (Command |? CodeAction)
forall a. [a] -> List a
List []
showUserFacingMessage
:: MonadLsp cfg m
=> UserFacingMessage
-> m (Either ResponseError a)
showUserFacingMessage :: UserFacingMessage -> m (Either ResponseError a)
showUserFacingMessage UserFacingMessage
ufm = do
ShowMessageParams -> m ()
forall cfg (m :: * -> *).
MonadLsp cfg m =>
ShowMessageParams -> m ()
showLspMessage (ShowMessageParams -> m ()) -> ShowMessageParams -> m ()
forall a b. (a -> b) -> a -> b
$ UserFacingMessage -> ShowMessageParams
mkShowMessageParams UserFacingMessage
ufm
Either ResponseError a -> m (Either ResponseError a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError a -> m (Either ResponseError a))
-> Either ResponseError a -> m (Either ResponseError a)
forall a b. (a -> b) -> a -> b
$ ResponseError -> Either ResponseError a
forall a b. a -> Either a b
Left (ResponseError -> Either ResponseError a)
-> ResponseError -> Either ResponseError a
forall a b. (a -> b) -> a -> b
$ ErrorCode -> Text -> ResponseError
mkErr ErrorCode
InternalError (Text -> ResponseError) -> Text -> ResponseError
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ UserFacingMessage -> String
forall a. Show a => a -> String
show UserFacingMessage
ufm
mkUserFacingMessage :: [TacticError] -> UserFacingMessage
mkUserFacingMessage :: [TacticError] -> UserFacingMessage
mkUserFacingMessage [TacticError]
errs
| TacticError -> [TacticError] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem TacticError
OutOfGas [TacticError]
errs = UserFacingMessage
NotEnoughGas
mkUserFacingMessage [TacticError]
_ = UserFacingMessage
TacticErrors
tacticCmd
:: (T.Text -> TacticsM ())
-> PluginId
-> CommandFunction IdeState TacticParams
tacticCmd :: (Text -> TacticsM ())
-> PluginId -> CommandFunction IdeState TacticParams
tacticCmd Text -> TacticsM ()
tac PluginId
pId IdeState
state (TacticParams Uri
uri Tracked 'Current Range
range Text
var_name)
| Just NormalizedFilePath
nfp <- NormalizedUri -> Maybe NormalizedFilePath
uriToNormalizedFilePath (NormalizedUri -> Maybe NormalizedFilePath)
-> NormalizedUri -> Maybe NormalizedFilePath
forall a b. (a -> b) -> a -> b
$ Uri -> NormalizedUri
toNormalizedUri Uri
uri = do
let stale :: GetAnnotatedParsedSource
-> MaybeT IO (TrackedStale (Annotated ParsedSource))
stale GetAnnotatedParsedSource
a = String
-> IdeState
-> NormalizedFilePath
-> GetAnnotatedParsedSource
-> MaybeT IO (TrackedStale (Annotated ParsedSource))
forall a r.
(r ~ RuleResult a, Eq a, Hashable a, Binary a, Show a, Typeable a,
NFData a, Show r, Typeable r, NFData r) =>
String
-> IdeState
-> NormalizedFilePath
-> a
-> MaybeT IO (TrackedStale r)
runStaleIde String
"tacticCmd" IdeState
state NormalizedFilePath
nfp GetAnnotatedParsedSource
a
ClientCapabilities
ccs <- LspT Config IO ClientCapabilities
forall config (m :: * -> *).
MonadLsp config m =>
m ClientCapabilities
getClientCapabilities
Config
cfg <- PluginId -> LspT Config IO Config
forall (m :: * -> *). MonadLsp Config m => PluginId -> m Config
getTacticConfig PluginId
pId
Maybe (Either UserFacingMessage WorkspaceEdit)
res <- IO (Maybe (Either UserFacingMessage WorkspaceEdit))
-> LspT Config IO (Maybe (Either UserFacingMessage WorkspaceEdit))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Either UserFacingMessage WorkspaceEdit))
-> LspT Config IO (Maybe (Either UserFacingMessage WorkspaceEdit)))
-> IO (Maybe (Either UserFacingMessage WorkspaceEdit))
-> LspT Config IO (Maybe (Either UserFacingMessage WorkspaceEdit))
forall a b. (a -> b) -> a -> b
$ MaybeT IO (Either UserFacingMessage WorkspaceEdit)
-> IO (Maybe (Either UserFacingMessage WorkspaceEdit))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO (Either UserFacingMessage WorkspaceEdit)
-> IO (Maybe (Either UserFacingMessage WorkspaceEdit)))
-> MaybeT IO (Either UserFacingMessage WorkspaceEdit)
-> IO (Maybe (Either UserFacingMessage WorkspaceEdit))
forall a b. (a -> b) -> a -> b
$ do
HoleJudgment{DynFlags
Tracked 'Current Range
HoleSort
Context
Judgement
hj_hole_sort :: HoleSort
hj_dflags :: DynFlags
hj_ctx :: Context
hj_jdg :: Judgement
hj_range :: Tracked 'Current Range
hj_hole_sort :: HoleJudgment -> HoleSort
hj_dflags :: HoleJudgment -> DynFlags
hj_ctx :: HoleJudgment -> Context
hj_jdg :: HoleJudgment -> Judgement
hj_range :: HoleJudgment -> Tracked 'Current Range
..} <- IdeState
-> NormalizedFilePath
-> Tracked 'Current Range
-> Config
-> MaybeT IO HoleJudgment
judgementForHole IdeState
state NormalizedFilePath
nfp Tracked 'Current Range
range Config
cfg
let span :: Tracked 'Current RealSrcSpan
span = (Range -> RealSrcSpan)
-> Tracked 'Current Range -> Tracked 'Current RealSrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> Range -> RealSrcSpan
rangeToRealSrcSpan (NormalizedFilePath -> String
fromNormalizedFilePath NormalizedFilePath
nfp)) Tracked 'Current Range
hj_range
TrackedStale Tracked ('Stale s) (Annotated ParsedSource)
pm PositionMap ('Stale s) 'Current
pmmap <- GetAnnotatedParsedSource
-> MaybeT IO (TrackedStale (Annotated ParsedSource))
stale GetAnnotatedParsedSource
GetAnnotatedParsedSource
Tracked ('Stale s) RealSrcSpan
pm_span <- Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan))
-> Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan)
forall a b. (a -> b) -> a -> b
$ PositionMap ('Stale s) 'Current
-> Tracked 'Current RealSrcSpan
-> Maybe (Tracked ('Stale s) RealSrcSpan)
forall a (from :: Age) (to :: Age).
MapAge a =>
PositionMap from to -> Tracked to a -> Maybe (Tracked from a)
mapAgeFrom PositionMap ('Stale s) 'Current
pmmap Tracked 'Current RealSrcSpan
span
let t :: TacticsM ()
t = Text -> TacticsM ()
tac Text
var_name
Int
-> IO (Either UserFacingMessage WorkspaceEdit)
-> MaybeT IO (Either UserFacingMessage WorkspaceEdit)
forall a. Int -> IO a -> MaybeT IO a
timingOut (Config -> Int
cfg_timeout_seconds Config
cfg Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
forall a. Num a => a
seconds) (IO (Either UserFacingMessage WorkspaceEdit)
-> MaybeT IO (Either UserFacingMessage WorkspaceEdit))
-> IO (Either UserFacingMessage WorkspaceEdit)
-> MaybeT IO (Either UserFacingMessage WorkspaceEdit)
forall a b. (a -> b) -> a -> b
$ do
Either [TacticError] RunTacticResults
res <- IO (Either [TacticError] RunTacticResults)
-> IO (Either [TacticError] RunTacticResults)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either [TacticError] RunTacticResults)
-> IO (Either [TacticError] RunTacticResults))
-> IO (Either [TacticError] RunTacticResults)
-> IO (Either [TacticError] RunTacticResults)
forall a b. (a -> b) -> a -> b
$ Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic Context
hj_ctx Judgement
hj_jdg TacticsM ()
t
Either UserFacingMessage WorkspaceEdit
-> IO (Either UserFacingMessage WorkspaceEdit)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UserFacingMessage WorkspaceEdit
-> IO (Either UserFacingMessage WorkspaceEdit))
-> Either UserFacingMessage WorkspaceEdit
-> IO (Either UserFacingMessage WorkspaceEdit)
forall a b. (a -> b) -> a -> b
$ Either UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
-> Either UserFacingMessage WorkspaceEdit
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Either UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
-> Either UserFacingMessage WorkspaceEdit)
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
-> Either UserFacingMessage WorkspaceEdit
forall a b. (a -> b) -> a -> b
$ case Either [TacticError] RunTacticResults
res of
Left [TacticError]
errs -> do
String -> [TacticError] -> Either UserFacingMessage ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"errs" [TacticError]
errs
UserFacingMessage
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
forall a b. a -> Either a b
Left (UserFacingMessage
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit))
-> UserFacingMessage
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
forall a b. (a -> b) -> a -> b
$ [TacticError] -> UserFacingMessage
mkUserFacingMessage [TacticError]
errs
Right RunTacticResults
rtr ->
case RunTacticResults -> LHsExpr GhcPs
rtr_extract RunTacticResults
rtr of
L SrcSpan
_ (HsVar XVar GhcPs
_ (L SrcSpan
_ IdP GhcPs
rdr)) | OccName -> Bool
isHole (RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName IdP GhcPs
RdrName
rdr) ->
UserFacingMessage
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
forall a b. a -> Either a b
Left UserFacingMessage
NothingToDo
LHsExpr GhcPs
_ -> Either UserFacingMessage WorkspaceEdit
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either UserFacingMessage WorkspaceEdit
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit))
-> Either UserFacingMessage WorkspaceEdit
-> Either
UserFacingMessage (Either UserFacingMessage WorkspaceEdit)
forall a b. (a -> b) -> a -> b
$ Tracked ('Stale s) RealSrcSpan
-> DynFlags
-> ClientCapabilities
-> Uri
-> Tracked ('Stale s) (Annotated ParsedSource)
-> RunTacticResults
-> Either UserFacingMessage WorkspaceEdit
forall (age :: Age).
Tracked age RealSrcSpan
-> DynFlags
-> ClientCapabilities
-> Uri
-> Tracked age (Annotated ParsedSource)
-> RunTacticResults
-> Either UserFacingMessage WorkspaceEdit
mkTacticResultEdits Tracked ('Stale s) RealSrcSpan
pm_span DynFlags
hj_dflags ClientCapabilities
ccs Uri
uri Tracked ('Stale s) (Annotated ParsedSource)
pm RunTacticResults
rtr
case Maybe (Either UserFacingMessage WorkspaceEdit)
res of
Maybe (Either UserFacingMessage WorkspaceEdit)
Nothing -> do
UserFacingMessage -> LspM Config (Either ResponseError Value)
forall cfg (m :: * -> *) a.
MonadLsp cfg m =>
UserFacingMessage -> m (Either ResponseError a)
showUserFacingMessage UserFacingMessage
TimedOut
Just (Left UserFacingMessage
ufm) -> do
UserFacingMessage -> LspM Config (Either ResponseError Value)
forall cfg (m :: * -> *) a.
MonadLsp cfg m =>
UserFacingMessage -> m (Either ResponseError a)
showUserFacingMessage UserFacingMessage
ufm
Just (Right WorkspaceEdit
edit) -> do
LspId 'WorkspaceApplyEdit
_ <- SServerMethod 'WorkspaceApplyEdit
-> MessageParams 'WorkspaceApplyEdit
-> (Either ResponseError (ResponseResult 'WorkspaceApplyEdit)
-> LspT Config IO ())
-> LspT Config IO (LspId 'WorkspaceApplyEdit)
forall (m :: Method 'FromServer 'Request) (f :: * -> *) config.
MonadLsp config f =>
SServerMethod m
-> MessageParams m
-> (Either ResponseError (ResponseResult m) -> f ())
-> f (LspId m)
sendRequest
SServerMethod 'WorkspaceApplyEdit
SWorkspaceApplyEdit
(Maybe Text -> WorkspaceEdit -> ApplyWorkspaceEditParams
ApplyWorkspaceEditParams Maybe Text
forall a. Maybe a
Nothing WorkspaceEdit
edit)
(LspT Config IO ()
-> Either ResponseError ApplyWorkspaceEditResponseBody
-> LspT Config IO ()
forall a b. a -> b -> a
const (LspT Config IO ()
-> Either ResponseError ApplyWorkspaceEditResponseBody
-> LspT Config IO ())
-> LspT Config IO ()
-> Either ResponseError ApplyWorkspaceEditResponseBody
-> LspT Config IO ()
forall a b. (a -> b) -> a -> b
$ () -> LspT Config IO ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
Either ResponseError Value
-> LspM Config (Either ResponseError Value)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError Value
-> LspM Config (Either ResponseError Value))
-> Either ResponseError Value
-> LspM Config (Either ResponseError Value)
forall a b. (a -> b) -> a -> b
$ Value -> Either ResponseError Value
forall a b. b -> Either a b
Right Value
Null
tacticCmd Text -> TacticsM ()
_ PluginId
_ IdeState
_ TacticParams
_ =
Either ResponseError Value
-> LspM Config (Either ResponseError Value)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError Value
-> LspM Config (Either ResponseError Value))
-> Either ResponseError Value
-> LspM Config (Either ResponseError Value)
forall a b. (a -> b) -> a -> b
$ ResponseError -> Either ResponseError Value
forall a b. a -> Either a b
Left (ResponseError -> Either ResponseError Value)
-> ResponseError -> Either ResponseError Value
forall a b. (a -> b) -> a -> b
$ ErrorCode -> Text -> ResponseError
mkErr ErrorCode
InvalidRequest Text
"Bad URI"
seconds :: Num a => a
seconds :: a
seconds = a
1e6
timingOut
:: Int
-> IO a
-> MaybeT IO a
timingOut :: Int -> IO a -> MaybeT IO a
timingOut Int
t IO a
m = IO (Maybe a) -> MaybeT IO a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe a) -> MaybeT IO a) -> IO (Maybe a) -> MaybeT IO a
forall a b. (a -> b) -> a -> b
$ Int -> IO a -> IO (Maybe a)
forall a. Int -> IO a -> IO (Maybe a)
timeout Int
t IO a
m
mkErr :: ErrorCode -> T.Text -> ResponseError
mkErr :: ErrorCode -> Text -> ResponseError
mkErr ErrorCode
code Text
err = ErrorCode -> Text -> Maybe Value -> ResponseError
ResponseError ErrorCode
code Text
err Maybe Value
forall a. Maybe a
Nothing
mkTacticResultEdits
:: Tracked age RealSrcSpan
-> DynFlags
-> ClientCapabilities
-> Uri
-> Tracked age (Annotated ParsedSource)
-> RunTacticResults
-> Either UserFacingMessage WorkspaceEdit
mkTacticResultEdits :: Tracked age RealSrcSpan
-> DynFlags
-> ClientCapabilities
-> Uri
-> Tracked age (Annotated ParsedSource)
-> RunTacticResults
-> Either UserFacingMessage WorkspaceEdit
mkTacticResultEdits (Tracked age RealSrcSpan -> RealSrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> RealSrcSpan
span) DynFlags
dflags ClientCapabilities
ccs Uri
uri (Tracked age (Annotated ParsedSource) -> Annotated ParsedSource
forall (age :: Age) a. Tracked age a -> a
unTrack -> Annotated ParsedSource
pm) RunTacticResults
rtr = do
[Synthesized (LHsExpr GhcPs)]
-> (Synthesized (LHsExpr GhcPs) -> Either UserFacingMessage ())
-> Either UserFacingMessage ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (RunTacticResults -> [Synthesized (LHsExpr GhcPs)]
rtr_other_solns RunTacticResults
rtr) ((Synthesized (LHsExpr GhcPs) -> Either UserFacingMessage ())
-> Either UserFacingMessage ())
-> (Synthesized (LHsExpr GhcPs) -> Either UserFacingMessage ())
-> Either UserFacingMessage ()
forall a b. (a -> b) -> a -> b
$ \Synthesized (LHsExpr GhcPs)
soln -> do
String -> LHsExpr GhcPs -> Either UserFacingMessage ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"other solution" (LHsExpr GhcPs -> Either UserFacingMessage ())
-> LHsExpr GhcPs -> Either UserFacingMessage ()
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. Synthesized a -> a
syn_val Synthesized (LHsExpr GhcPs)
soln
String
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
-> Either UserFacingMessage ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"with score" ((Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
-> Either UserFacingMessage ())
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
-> Either UserFacingMessage ()
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs)
-> Judgement
-> [Judgement]
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
scoreSolution Synthesized (LHsExpr GhcPs)
soln (RunTacticResults -> Judgement
rtr_jdg RunTacticResults
rtr) []
String -> LHsExpr GhcPs -> Either UserFacingMessage ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"solution" (LHsExpr GhcPs -> Either UserFacingMessage ())
-> LHsExpr GhcPs -> Either UserFacingMessage ()
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> LHsExpr GhcPs
rtr_extract RunTacticResults
rtr
DynFlags
-> ClientCapabilities
-> Uri
-> Annotated ParsedSource
-> Graft (Either String) ParsedSource
-> Either UserFacingMessage WorkspaceEdit
mkWorkspaceEdits DynFlags
dflags ClientCapabilities
ccs Uri
uri Annotated ParsedSource
pm (Graft (Either String) ParsedSource
-> Either UserFacingMessage WorkspaceEdit)
-> Graft (Either String) ParsedSource
-> Either UserFacingMessage WorkspaceEdit
forall a b. (a -> b) -> a -> b
$ SrcSpan -> RunTacticResults -> Graft (Either String) ParsedSource
graftHole (RealSrcSpan -> SrcSpan
RealSrcSpan RealSrcSpan
span) RunTacticResults
rtr
graftHole
:: SrcSpan
-> RunTacticResults
-> Graft (Either String) ParsedSource
graftHole :: SrcSpan -> RunTacticResults -> Graft (Either String) ParsedSource
graftHole SrcSpan
span RunTacticResults
rtr
| Judgement -> Bool
forall a. Judgement' a -> Bool
_jIsTopHole (RunTacticResults -> Judgement
rtr_jdg RunTacticResults
rtr)
= Proxy (Located [LMatch GhcPs (LHsExpr GhcPs)])
-> SrcSpan
-> (DynFlags
-> [LMatch GhcPs (LHsExpr GhcPs)]
-> GenericM (TransformT (Either String)))
-> Graft (Either String) ParsedSource
forall (m :: * -> *) a ast.
(Monad m, Data a, Typeable ast) =>
Proxy (Located ast)
-> SrcSpan
-> (DynFlags -> ast -> GenericM (TransformT m))
-> Graft m a
genericGraftWithSmallestM
(Proxy (Located [LMatch GhcPs (LHsExpr GhcPs)])
forall k (t :: k). Proxy t
Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) SrcSpan
span
((DynFlags
-> [LMatch GhcPs (LHsExpr GhcPs)]
-> GenericM (TransformT (Either String)))
-> Graft (Either String) ParsedSource)
-> (DynFlags
-> [LMatch GhcPs (LHsExpr GhcPs)]
-> GenericM (TransformT (Either String)))
-> Graft (Either String) ParsedSource
forall a b. (a -> b) -> a -> b
$ \DynFlags
dflags [LMatch GhcPs (LHsExpr GhcPs)]
matches ->
GenericM (TransformT (Either String))
-> GenericM (TransformT (Either String))
forall (m :: * -> *). Monad m => GenericM m -> GenericM m
everywhereM'
(GenericM (TransformT (Either String))
-> GenericM (TransformT (Either String)))
-> GenericM (TransformT (Either String))
-> GenericM (TransformT (Either String))
forall a b. (a -> b) -> a -> b
$ (Int
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)])
-> GenericM (TransformT (Either String))
forall b (m :: * -> *).
(Data b, Monad m) =>
(Int -> b -> m [b]) -> GenericM m
mkBindListT ((Int
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)])
-> GenericM (TransformT (Either String)))
-> (Int
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)])
-> GenericM (TransformT (Either String))
forall a b. (a -> b) -> a -> b
$ \Int
ix ->
DynFlags
-> SrcSpan
-> Int
-> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs)
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
graftDecl DynFlags
dflags SrcSpan
span Int
ix ((RdrName -> [Pat GhcPs] -> LHsDecl GhcPs)
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)])
-> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs)
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ \RdrName
name [Pat GhcPs]
pats ->
Maybe LexicalFixity -> OccName -> [AgdaMatch] -> LHsDecl GhcPs
splitToDecl
(case Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Judgement -> Bool
jNeedsToBindArgs (RunTacticResults -> Judgement
rtr_jdg RunTacticResults
rtr) of
Bool
True -> HsMatchContext RdrName -> Maybe LexicalFixity
forall p. HsMatchContext p -> Maybe LexicalFixity
matchContextFixity (HsMatchContext RdrName -> Maybe LexicalFixity)
-> (LMatch GhcPs (LHsExpr GhcPs) -> HsMatchContext RdrName)
-> LMatch GhcPs (LHsExpr GhcPs)
-> Maybe LexicalFixity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Match GhcPs (LHsExpr GhcPs) -> HsMatchContext RdrName
forall p body.
Match p body -> HsMatchContext (NameOrRdrName (IdP p))
m_ctxt (Match GhcPs (LHsExpr GhcPs) -> HsMatchContext RdrName)
-> (LMatch GhcPs (LHsExpr GhcPs) -> Match GhcPs (LHsExpr GhcPs))
-> LMatch GhcPs (LHsExpr GhcPs)
-> HsMatchContext RdrName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LMatch GhcPs (LHsExpr GhcPs) -> Match GhcPs (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
(LMatch GhcPs (LHsExpr GhcPs) -> Maybe LexicalFixity)
-> Maybe (LMatch GhcPs (LHsExpr GhcPs)) -> Maybe LexicalFixity
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [LMatch GhcPs (LHsExpr GhcPs)]
-> Maybe (LMatch GhcPs (LHsExpr GhcPs))
forall a. [a] -> Maybe a
listToMaybe [LMatch GhcPs (LHsExpr GhcPs)]
matches
Bool
False -> Maybe LexicalFixity
forall a. Maybe a
Nothing
)
(RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName RdrName
name)
([AgdaMatch] -> LHsDecl GhcPs) -> [AgdaMatch] -> LHsDecl GhcPs
forall a b. (a -> b) -> a -> b
$ AgdaMatch -> [AgdaMatch]
iterateSplit
(AgdaMatch -> [AgdaMatch]) -> AgdaMatch -> [AgdaMatch]
forall a b. (a -> b) -> a -> b
$ [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch
mkFirstAgda ((Pat GhcPs -> Pat GhcPs) -> [Pat GhcPs] -> [Pat GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pat GhcPs -> Pat GhcPs
unXPat [Pat GhcPs]
pats)
(HsExpr GhcPs -> AgdaMatch) -> HsExpr GhcPs -> AgdaMatch
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
(LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs))
-> LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> LHsExpr GhcPs
rtr_extract RunTacticResults
rtr
graftHole SrcSpan
span RunTacticResults
rtr
= SrcSpan -> LHsExpr GhcPs -> Graft (Either String) ParsedSource
forall ast a.
(ASTElement ast, Data a) =>
SrcSpan -> Located ast -> Graft (Either String) a
graft SrcSpan
span
(LHsExpr GhcPs -> Graft (Either String) ParsedSource)
-> LHsExpr GhcPs -> Graft (Either String) ParsedSource
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> LHsExpr GhcPs
rtr_extract RunTacticResults
rtr
matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity
matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity
matchContextFixity (FunRhs Located p
_ LexicalFixity
l SrcStrictness
_) = LexicalFixity -> Maybe LexicalFixity
forall a. a -> Maybe a
Just LexicalFixity
l
matchContextFixity HsMatchContext p
_ = Maybe LexicalFixity
forall a. Maybe a
Nothing
graftDecl
:: DynFlags
-> SrcSpan
-> Int
-> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs)
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
graftDecl :: DynFlags
-> SrcSpan
-> Int
-> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs)
-> LMatch GhcPs (LHsExpr GhcPs)
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
graftDecl DynFlags
dflags SrcSpan
dst Int
ix RdrName -> [Pat GhcPs] -> LHsDecl GhcPs
make_decl (L SrcSpan
src (AMatch (FunRhs (L SrcSpan
_ NameOrRdrName (IdP GhcPs)
name) LexicalFixity
_ SrcStrictness
_) [Pat GhcPs]
pats HsExpr GhcPs
_))
| SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src = do
L SrcSpan
_ HsDecl GhcPs
dec <- DynFlags
-> LHsDecl GhcPs -> TransformT (Either String) (LHsDecl GhcPs)
annotateDecl DynFlags
dflags (LHsDecl GhcPs -> TransformT (Either String) (LHsDecl GhcPs))
-> LHsDecl GhcPs -> TransformT (Either String) (LHsDecl GhcPs)
forall a b. (a -> b) -> a -> b
$ RdrName -> [Pat GhcPs] -> LHsDecl GhcPs
make_decl NameOrRdrName (IdP GhcPs)
RdrName
name [Pat GhcPs]
pats
case HsDecl GhcPs
dec of
ValD XValD GhcPs
_ (FunBind { fun_matches :: forall idL idR. HsBindLR idL idR -> MatchGroup idR (LHsExpr idR)
fun_matches = MG { mg_alts :: forall p body. MatchGroup p body -> Located [LMatch p body]
mg_alts = L SrcSpan
_ alts :: [LMatch GhcPs (LHsExpr GhcPs)]
alts@(LMatch GhcPs (LHsExpr GhcPs)
first_match : [LMatch GhcPs (LHsExpr GhcPs)]
_)}
}) -> do
Bool
-> TransformT (Either String) () -> TransformT (Either String) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
ix Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (TransformT (Either String) () -> TransformT (Either String) ())
-> TransformT (Either String) () -> TransformT (Either String) ()
forall a b. (a -> b) -> a -> b
$
LMatch GhcPs (LHsExpr GhcPs)
-> Int -> Int -> TransformT (Either String) ()
forall a (m :: * -> *).
(Data a, Monad m) =>
Located a -> Int -> Int -> TransformT m ()
setPrecedingLinesT LMatch GhcPs (LHsExpr GhcPs)
first_match Int
0 Int
0
[LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [LMatch GhcPs (LHsExpr GhcPs)]
alts
HsDecl GhcPs
_ -> Either String [LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Either String [LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)])
-> Either String [LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ String -> Either String [LMatch GhcPs (LHsExpr GhcPs)]
forall a b. a -> Either a b
Left String
"annotateDecl didn't produce a funbind"
graftDecl DynFlags
_ SrcSpan
_ Int
_ RdrName -> [Pat GhcPs] -> LHsDecl GhcPs
_ LMatch GhcPs (LHsExpr GhcPs)
x = [LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)])
-> [LMatch GhcPs (LHsExpr GhcPs)]
-> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ LMatch GhcPs (LHsExpr GhcPs) -> [LMatch GhcPs (LHsExpr GhcPs)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure LMatch GhcPs (LHsExpr GhcPs)
x