{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE NoMonoLocalBinds #-}
module Wingman.AbstractLSP.TacticActions where
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 Development.IDE.GHC.Compat
import Development.IDE.GHC.ExactPrint
import Generics.SYB.GHC (mkBindListT, everywhereM')
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.Core.Service (getIdeOptionsIO)
import Development.IDE.Types.Options (IdeTesting(IdeTesting), IdeOptions (IdeOptions, optTesting))
makeTacticInteraction
:: TacticCommand
-> Interaction
makeTacticInteraction :: TacticCommand -> Interaction
makeTacticInteraction TacticCommand
cmd =
Continuation TacticCommand HoleTarget Text -> Interaction
forall target sort b.
(IsTarget target, IsContinuationSort sort, ToJSON b, FromJSON b) =>
Continuation sort target b -> Interaction
Interaction (Continuation TacticCommand HoleTarget Text -> Interaction)
-> Continuation TacticCommand HoleTarget Text -> Interaction
forall a b. (a -> b) -> a -> b
$ TacticCommand
-> SynthesizeCommand HoleTarget Text
-> (LspEnv
-> TargetArgs HoleTarget
-> FileContext
-> Text
-> MaybeT (LspM Config) [ContinuationResult])
-> Continuation TacticCommand HoleTarget Text
forall sort target payload.
sort
-> SynthesizeCommand target payload
-> (LspEnv
-> TargetArgs target
-> FileContext
-> payload
-> MaybeT (LspM Config) [ContinuationResult])
-> Continuation sort target payload
Continuation @_ @HoleTarget TacticCommand
cmd
((LspEnv
-> TargetArgs HoleTarget
-> MaybeT (LspM Config) [(Metadata, Text)])
-> SynthesizeCommand HoleTarget Text
forall a b.
(LspEnv -> TargetArgs a -> MaybeT (LspM Config) [(Metadata, b)])
-> SynthesizeCommand a b
SynthesizeCodeAction ((LspEnv
-> TargetArgs HoleTarget
-> MaybeT (LspM Config) [(Metadata, Text)])
-> SynthesizeCommand HoleTarget Text)
-> (LspEnv
-> TargetArgs HoleTarget
-> MaybeT (LspM Config) [(Metadata, Text)])
-> SynthesizeCommand HoleTarget Text
forall a b. (a -> b) -> a -> b
$ \LspEnv
env TargetArgs HoleTarget
hj -> do
[(Metadata, Text)] -> MaybeT (LspM Config) [(Metadata, Text)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Metadata, Text)] -> MaybeT (LspM Config) [(Metadata, Text)])
-> [(Metadata, Text)] -> MaybeT (LspM Config) [(Metadata, Text)]
forall a b. (a -> b) -> a -> b
$ TacticCommand -> TacticProvider
commandProvider TacticCommand
cmd TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticProviderData :: LspEnv -> Judgement -> HoleSort -> TacticProviderData
TacticProviderData
{ tpd_lspEnv :: LspEnv
tpd_lspEnv = LspEnv
env
, tpd_jdg :: Judgement
tpd_jdg = HoleJudgment -> Judgement
hj_jdg HoleJudgment
TargetArgs HoleTarget
hj
, tpd_hole_sort :: HoleSort
tpd_hole_sort = HoleJudgment -> HoleSort
hj_hole_sort HoleJudgment
TargetArgs HoleTarget
hj
}
)
((LspEnv
-> TargetArgs HoleTarget
-> FileContext
-> Text
-> MaybeT (LspM Config) [ContinuationResult])
-> Continuation TacticCommand HoleTarget Text)
-> (LspEnv
-> TargetArgs HoleTarget
-> FileContext
-> Text
-> MaybeT (LspM Config) [ContinuationResult])
-> Continuation TacticCommand HoleTarget Text
forall a b. (a -> b) -> a -> b
$ \LspEnv{DynFlags
IdeState
PluginId
Config
FileContext
le_fileContext :: LspEnv -> FileContext
le_config :: LspEnv -> Config
le_dflags :: LspEnv -> DynFlags
le_pluginId :: LspEnv -> PluginId
le_ideState :: LspEnv -> IdeState
le_fileContext :: FileContext
le_config :: Config
le_dflags :: DynFlags
le_pluginId :: PluginId
le_ideState :: IdeState
..} HoleJudgment{..} FileContext{Maybe (Tracked 'Current Range)
Uri
fc_range :: FileContext -> Maybe (Tracked 'Current Range)
fc_uri :: FileContext -> Uri
fc_range :: Maybe (Tracked 'Current Range)
fc_uri :: Uri
..} Text
var_name -> do
NormalizedFilePath
nfp <- Uri -> MaybeT (LspM Config) NormalizedFilePath
forall (m :: * -> *).
Applicative m =>
Uri -> MaybeT m NormalizedFilePath
getNfp Uri
fc_uri
let stale :: a -> MaybeT IO (TrackedStale (RuleResult a))
stale a
a = String
-> IdeState
-> NormalizedFilePath
-> a
-> MaybeT IO (TrackedStale (RuleResult a))
forall a r.
(r ~ RuleResult a, Eq a, Hashable 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
le_ideState NormalizedFilePath
nfp a
a
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)
_ PositionMap ('Stale s) 'Current
pmmap <- (IO (Maybe (TrackedStale (Annotated ParsedSource)))
-> LspM Config (Maybe (TrackedStale (Annotated ParsedSource))))
-> MaybeT IO (TrackedStale (Annotated ParsedSource))
-> MaybeT (LspM Config) (TrackedStale (Annotated ParsedSource))
forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe a) -> n (Maybe b)) -> MaybeT m a -> MaybeT n b
mapMaybeT IO (Maybe (TrackedStale (Annotated ParsedSource)))
-> LspM Config (Maybe (TrackedStale (Annotated ParsedSource)))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (MaybeT IO (TrackedStale (Annotated ParsedSource))
-> MaybeT (LspM Config) (TrackedStale (Annotated ParsedSource)))
-> MaybeT IO (TrackedStale (Annotated ParsedSource))
-> MaybeT (LspM Config) (TrackedStale (Annotated ParsedSource))
forall a b. (a -> b) -> a -> b
$ GetAnnotatedParsedSource
-> MaybeT IO (TrackedStale (RuleResult GetAnnotatedParsedSource))
forall a.
(Hashable a, Show a, Show (RuleResult a), Typeable a,
Typeable (RuleResult a), NFData a, NFData (RuleResult a)) =>
a -> MaybeT IO (TrackedStale (RuleResult a))
stale GetAnnotatedParsedSource
GetAnnotatedParsedSource
Tracked ('Stale s) RealSrcSpan
pm_span <- Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT (LspM Config) (Tracked ('Stale s) RealSrcSpan)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT (LspM Config) (Tracked ('Stale s) RealSrcSpan))
-> Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT (LspM Config) (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
IdeOptions{optTesting :: IdeOptions -> IdeTesting
optTesting = IdeTesting Bool
isTesting} <-
IO IdeOptions -> MaybeT (LspM Config) IdeOptions
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO IdeOptions -> MaybeT (LspM Config) IdeOptions)
-> IO IdeOptions -> MaybeT (LspM Config) IdeOptions
forall a b. (a -> b) -> a -> b
$ ShakeExtras -> IO IdeOptions
getIdeOptionsIO (IdeState -> ShakeExtras
shakeExtras IdeState
le_ideState)
let t :: TacticsM ()
t = TacticCommand -> Text -> TacticsM ()
commandTactic TacticCommand
cmd Text
var_name
timeout :: Int
timeout = if Bool
isTesting then Int
forall a. Bounded a => a
maxBound else Config -> Int
cfg_timeout_seconds Config
le_config Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
forall a. Num a => a
seconds
IO [ContinuationResult]
-> MaybeT (LspM Config) [ContinuationResult]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [ContinuationResult]
-> MaybeT (LspM Config) [ContinuationResult])
-> IO [ContinuationResult]
-> MaybeT (LspM Config) [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ Int
-> Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic Int
timeout Context
hj_ctx Judgement
hj_jdg TacticsM ()
t IO (Either [TacticError] RunTacticResults)
-> (Either [TacticError] RunTacticResults
-> IO [ContinuationResult])
-> IO [ContinuationResult]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left [TacticError]
err ->
[ContinuationResult] -> IO [ContinuationResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
([ContinuationResult] -> IO [ContinuationResult])
-> [ContinuationResult] -> IO [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ ContinuationResult -> [ContinuationResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(ContinuationResult -> [ContinuationResult])
-> ContinuationResult -> [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ [UserFacingMessage] -> ContinuationResult
ErrorMessages
([UserFacingMessage] -> ContinuationResult)
-> [UserFacingMessage] -> ContinuationResult
forall a b. (a -> b) -> a -> b
$ UserFacingMessage -> [UserFacingMessage]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(UserFacingMessage -> [UserFacingMessage])
-> UserFacingMessage -> [UserFacingMessage]
forall a b. (a -> b) -> a -> b
$ [TacticError] -> UserFacingMessage
mkUserFacingMessage [TacticError]
err
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) ->
[ContinuationResult] -> IO [ContinuationResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
([ContinuationResult] -> IO [ContinuationResult])
-> [ContinuationResult] -> IO [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> [ContinuationResult] -> [ContinuationResult]
addTimeoutMessage RunTacticResults
rtr
([ContinuationResult] -> [ContinuationResult])
-> [ContinuationResult] -> [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ ContinuationResult -> [ContinuationResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(ContinuationResult -> [ContinuationResult])
-> ContinuationResult -> [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ [UserFacingMessage] -> ContinuationResult
ErrorMessages
([UserFacingMessage] -> ContinuationResult)
-> [UserFacingMessage] -> ContinuationResult
forall a b. (a -> b) -> a -> b
$ UserFacingMessage -> [UserFacingMessage]
forall (f :: * -> *) a. Applicative f => a -> f a
pure UserFacingMessage
NothingToDo
LHsExpr GhcPs
_ -> do
[Synthesized (LHsExpr GhcPs)]
-> (Synthesized (LHsExpr GhcPs) -> IO ()) -> IO ()
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) -> IO ()) -> IO ())
-> (Synthesized (LHsExpr GhcPs) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Synthesized (LHsExpr GhcPs)
soln -> do
String -> LHsExpr GhcPs -> IO ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"other solution" (LHsExpr GhcPs -> IO ()) -> LHsExpr GhcPs -> IO ()
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)
-> IO ()
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)
-> IO ())
-> (Penalize Int, Reward Bool, Penalize Int, Penalize Int,
Reward Int, Penalize Int, Penalize Int)
-> IO ()
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 -> IO ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"solution" (LHsExpr GhcPs -> IO ()) -> LHsExpr GhcPs -> IO ()
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> LHsExpr GhcPs
rtr_extract RunTacticResults
rtr
[ContinuationResult] -> IO [ContinuationResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
([ContinuationResult] -> IO [ContinuationResult])
-> [ContinuationResult] -> IO [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> [ContinuationResult] -> [ContinuationResult]
addTimeoutMessage RunTacticResults
rtr
([ContinuationResult] -> [ContinuationResult])
-> [ContinuationResult] -> [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ ContinuationResult -> [ContinuationResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(ContinuationResult -> [ContinuationResult])
-> ContinuationResult -> [ContinuationResult]
forall a b. (a -> b) -> a -> b
$ Graft (Either String) ParsedSource -> ContinuationResult
GraftEdit
(Graft (Either String) ParsedSource -> ContinuationResult)
-> Graft (Either String) ParsedSource -> ContinuationResult
forall a b. (a -> b) -> a -> b
$ SrcSpan -> RunTacticResults -> Graft (Either String) ParsedSource
graftHole (RealSrcSpan -> Maybe () -> SrcSpan
RealSrcSpan (Tracked ('Stale s) RealSrcSpan -> RealSrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack Tracked ('Stale s) RealSrcSpan
pm_span) Maybe ()
forall a. Maybe a
Nothing) RunTacticResults
rtr
addTimeoutMessage :: RunTacticResults -> [ContinuationResult] -> [ContinuationResult]
addTimeoutMessage :: RunTacticResults -> [ContinuationResult] -> [ContinuationResult]
addTimeoutMessage RunTacticResults
rtr = [ContinuationResult]
-> [ContinuationResult] -> [ContinuationResult]
forall a. Monoid a => a -> a -> a
mappend
[ [UserFacingMessage] -> ContinuationResult
ErrorMessages ([UserFacingMessage] -> ContinuationResult)
-> [UserFacingMessage] -> ContinuationResult
forall a b. (a -> b) -> a -> b
$ UserFacingMessage -> [UserFacingMessage]
forall (f :: * -> *) a. Applicative f => a -> f a
pure UserFacingMessage
TimedOut
| RunTacticResults -> Bool
rtr_timed_out RunTacticResults
rtr
]
seconds :: Num a => a
seconds :: a
seconds = a
1e6
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 [] = UserFacingMessage
NothingToDo
mkUserFacingMessage [TacticError]
_ = UserFacingMessage
TacticErrors
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 l ast a.
(ASTElement l ast, Data a) =>
SrcSpan -> LocatedAn l 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