{-# 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           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


------------------------------------------------------------------------------
-- | An 'Interaction' for a 'TacticCommand'.
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
$ \env :: LspEnv
env@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
..} 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 :: FileContext
le_config :: Config
le_dflags :: DynFlags
le_pluginId :: PluginId
le_ideState :: IdeState
le_fileContext :: LspEnv -> FileContext
le_config :: LspEnv -> Config
le_dflags :: LspEnv -> DynFlags
le_pluginId :: LspEnv -> PluginId
le_ideState :: LspEnv -> IdeState
..} HoleJudgment{..} FileContext{Maybe (Tracked 'Current Range)
NormalizedFilePath
Uri
fc_range :: FileContext -> Maybe (Tracked 'Current Range)
fc_nfp :: FileContext -> NormalizedFilePath
fc_uri :: FileContext -> Uri
fc_range :: Maybe (Tracked 'Current Range)
fc_nfp :: NormalizedFilePath
fc_uri :: Uri
..} Text
var_name -> do
        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, 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
le_ideState NormalizedFilePath
fc_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
fc_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.
(Eq a, Hashable a, Binary 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
        let t :: TacticsM ()
t = TacticCommand -> Text -> TacticsM ()
commandTactic TacticCommand
cmd Text
var_name

        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 (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) 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 -> SrcSpan
RealSrcSpan (RealSrcSpan -> SrcSpan) -> RealSrcSpan -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Tracked ('Stale s) RealSrcSpan -> RealSrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack Tracked ('Stale s) RealSrcSpan
pm_span) 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
  ]


------------------------------------------------------------------------------
-- | The number of microseconds in a second
seconds :: Num a => a
seconds :: a
seconds = a
1e6


------------------------------------------------------------------------------
-- | Transform some tactic errors into a 'UserFacingMessage'.
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


------------------------------------------------------------------------------
-- | 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 :: 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
                   -- If the user has explicitly bound arguments, use the
                   -- fixity they wrote.
                   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
                   -- Otherwise, choose based on the name of the function.
                   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


------------------------------------------------------------------------------
-- | Keep a fixity if one was present in the 'HsMatchContext'.
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


------------------------------------------------------------------------------
-- | 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 :: 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
          -- 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.
          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