{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE NumDecimals         #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ViewPatterns        #-}

-- | A plugin that uses tactics to synthesize code
module Ide.Plugin.Tactic
  ( descriptor
  , tacticTitle
  , TacticCommand (..)
  ) where

import           Control.Arrow
import           Control.Monad
import           Control.Monad.Trans
import           Control.Monad.Trans.Maybe
import           Data.Aeson
import           Data.Coerce
import           Data.Functor ((<&>))
import           Data.Generics.Aliases (mkQ)
import           Data.Generics.Schemes (everything)
import           Data.List
import           Data.Map (Map)
import qualified Data.Map as M
import           Data.Maybe
import           Data.Monoid
import qualified Data.Set as S
import qualified Data.Text as T
import           Data.Traversable
import           Development.IDE.Core.PositionMapping
import           Development.IDE.Core.RuleTypes
import           Development.IDE.Core.Service (runAction)
import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
import           Development.IDE.GHC.Compat
import           Development.IDE.GHC.Error (realSrcSpanToRange)
import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
import           Development.Shake (Action)
import           DynFlags (xopt)
import qualified FastString
import           GHC.Generics (Generic)
import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
import           Ide.Plugin.Tactic.Auto
import           Ide.Plugin.Tactic.Context
import           Ide.Plugin.Tactic.GHC
import           Ide.Plugin.Tactic.Judgements
import           Ide.Plugin.Tactic.Range
import           Ide.Plugin.Tactic.Tactics
import           Ide.Plugin.Tactic.TestTypes
import           Ide.Plugin.Tactic.Types
import           Ide.PluginUtils
import           Ide.TreeTransform (transform, graft, useAnnotatedSource)
import           Ide.Types
import           Language.Haskell.LSP.Core (clientCapabilities)
import           Language.Haskell.LSP.Types
import           OccName
import           SrcLoc (containsSpan)
import           System.Timeout
import           TcRnTypes (tcg_binds)


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
        = (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)
              ((OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
tacticCmd ((OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams)
-> (OccName -> TacticsM ())
-> CommandFunction IdeState TacticParams
forall a b. (a -> b) -> a -> b
$ TacticCommand -> OccName -> TacticsM ()
commandTactic TacticCommand
tc))
              [TacticCommand
forall a. Bounded a => a
minBound .. TacticCommand
forall a. Bounded a => a
maxBound]
    , pluginCodeActionProvider :: Maybe (CodeActionProvider IdeState)
pluginCodeActionProvider = CodeActionProvider IdeState -> Maybe (CodeActionProvider IdeState)
forall a. a -> Maybe a
Just CodeActionProvider IdeState
codeActionProvider
    }

tacticDesc :: T.Text -> T.Text
tacticDesc :: Text -> Text
tacticDesc Text
name = Text
"fill the hole using the " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" tactic"

------------------------------------------------------------------------------
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
-- UI.
type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult]


------------------------------------------------------------------------------
-- | Construct a 'CommandId'
tcCommandId :: TacticCommand -> CommandId
tcCommandId :: TacticCommand -> CommandId
tcCommandId TacticCommand
c = Text -> CommandId
coerce (Text -> CommandId) -> Text -> CommandId
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"tactics" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> TacticCommand -> String
forall a. Show a => a -> String
show TacticCommand
c String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"Command"


------------------------------------------------------------------------------
-- | The name of the command for the LS.
tcCommandName :: TacticCommand -> T.Text
tcCommandName :: TacticCommand -> Text
tcCommandName = String -> Text
T.pack (String -> Text)
-> (TacticCommand -> String) -> TacticCommand -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticCommand -> String
forall a. Show a => a -> String
show

------------------------------------------------------------------------------
-- | Mapping from tactic commands to their contextual providers. See 'provide',
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
commandProvider :: TacticCommand -> TacticProvider
commandProvider :: TacticCommand -> TacticProvider
commandProvider TacticCommand
Auto  = TacticCommand -> Text -> TacticProvider
provide TacticCommand
Auto Text
""
commandProvider TacticCommand
Intros =
  (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType Type -> Bool
isFunction (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
    TacticCommand -> Text -> TacticProvider
provide TacticCommand
Intros Text
""
commandProvider TacticCommand
Destruct =
  (Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
destructFilter ((OccName -> Type -> TacticProvider) -> TacticProvider)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \OccName
occ Type
_ ->
    TacticCommand -> Text -> TacticProvider
provide TacticCommand
Destruct (Text -> TacticProvider) -> Text -> TacticProvider
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString OccName
occ
commandProvider TacticCommand
Homomorphism =
  (Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
homoFilter ((OccName -> Type -> TacticProvider) -> TacticProvider)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \OccName
occ Type
_ ->
    TacticCommand -> Text -> TacticProvider
provide TacticCommand
Homomorphism (Text -> TacticProvider) -> Text -> TacticProvider
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString OccName
occ
commandProvider TacticCommand
DestructLambdaCase =
  Extension -> TacticProvider -> TacticProvider
requireExtension Extension
LambdaCase (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
    (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType (Maybe Bool -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Bool -> Bool) -> (Type -> Maybe Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Bool
lambdaCaseable) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
      TacticCommand -> Text -> TacticProvider
provide TacticCommand
DestructLambdaCase Text
""
commandProvider TacticCommand
HomomorphismLambdaCase =
  Extension -> TacticProvider -> TacticProvider
requireExtension Extension
LambdaCase (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
    (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType ((Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) (Maybe Bool -> Bool) -> (Type -> Maybe Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Bool
lambdaCaseable) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
      TacticCommand -> Text -> TacticProvider
provide TacticCommand
HomomorphismLambdaCase Text
""


------------------------------------------------------------------------------
-- | A mapping from tactic commands to actual tactics for refinery.
commandTactic :: TacticCommand -> OccName -> TacticsM ()
commandTactic :: TacticCommand -> OccName -> TacticsM ()
commandTactic TacticCommand
Auto         = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
auto
commandTactic TacticCommand
Intros       = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
intros
commandTactic TacticCommand
Destruct     = OccName -> TacticsM ()
destruct
commandTactic TacticCommand
Homomorphism = OccName -> TacticsM ()
homo
commandTactic TacticCommand
DestructLambdaCase     = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
destructLambdaCase
commandTactic TacticCommand
HomomorphismLambdaCase = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
homoLambdaCase


------------------------------------------------------------------------------
-- | We should show homos only when the goal type is the same as the binding
-- type, and that both are usual algebraic types.
homoFilter :: Type -> Type -> Bool
homoFilter :: Type -> Type -> Bool
homoFilter (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
t1) (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
t2) = TyCon
t1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
t2
homoFilter Type
_ Type
_ = Bool
False


------------------------------------------------------------------------------
-- | We should show destruct for bindings only when those bindings have usual
-- algebraic types.
destructFilter :: Type -> Type -> Bool
destructFilter :: Type -> Type -> Bool
destructFilter Type
_ (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
_) = Bool
True
destructFilter Type
_ Type
_ = Bool
False


runIde :: IdeState -> Action a -> IO a
runIde :: IdeState -> Action a -> IO a
runIde IdeState
state = String -> IdeState -> Action a -> IO a
forall a. String -> IdeState -> Action a -> IO a
runAction String
"tactic" IdeState
state


codeActionProvider :: CodeActionProvider IdeState
codeActionProvider :: CodeActionProvider IdeState
codeActionProvider LspFuncs Config
_conf IdeState
state PluginId
plId (TextDocumentIdentifier Uri
uri) Range
range CodeActionContext
_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 =
      Either ResponseError (List CAResult)
-> MaybeT IO (Either ResponseError (List CAResult))
-> IO (Either ResponseError (List CAResult))
forall (m :: * -> *) a. Functor m => a -> MaybeT m a -> m a
fromMaybeT (List CAResult -> Either ResponseError (List CAResult)
forall a b. b -> Either a b
Right (List CAResult -> Either ResponseError (List CAResult))
-> List CAResult -> Either ResponseError (List CAResult)
forall a b. (a -> b) -> a -> b
$ [CAResult] -> List CAResult
forall a. [a] -> List a
List []) (MaybeT IO (Either ResponseError (List CAResult))
 -> IO (Either ResponseError (List CAResult)))
-> MaybeT IO (Either ResponseError (List CAResult))
-> IO (Either ResponseError (List CAResult))
forall a b. (a -> b) -> a -> b
$ do
        (Range
_, Judgement
jdg, Context
_, DynFlags
dflags) <- IdeState
-> NormalizedFilePath
-> Range
-> MaybeT IO (Range, Judgement, Context, DynFlags)
judgementForHole IdeState
state NormalizedFilePath
nfp Range
range
        [CAResult]
actions <- IO [CAResult] -> MaybeT IO [CAResult]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [CAResult] -> MaybeT IO [CAResult])
-> IO [CAResult] -> MaybeT IO [CAResult]
forall a b. (a -> b) -> a -> b
$
          -- This foldMap is over the function monoid.
          (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]
            DynFlags
dflags
            PluginId
plId
            Uri
uri
            Range
range
            Judgement
jdg
        Either ResponseError (List CAResult)
-> MaybeT IO (Either ResponseError (List CAResult))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError (List CAResult)
 -> MaybeT IO (Either ResponseError (List CAResult)))
-> Either ResponseError (List CAResult)
-> MaybeT IO (Either ResponseError (List CAResult))
forall a b. (a -> b) -> a -> b
$ List CAResult -> Either ResponseError (List CAResult)
forall a b. b -> Either a b
Right (List CAResult -> Either ResponseError (List CAResult))
-> List CAResult -> Either ResponseError (List CAResult)
forall a b. (a -> b) -> a -> b
$ [CAResult] -> List CAResult
forall a. [a] -> List a
List [CAResult]
actions
codeActionProvider LspFuncs Config
_ IdeState
_ PluginId
_ TextDocumentIdentifier
_ Range
_ CodeActionContext
_ = Either ResponseError (List CAResult)
-> IO (Either ResponseError (List CAResult))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either ResponseError (List CAResult)
 -> IO (Either ResponseError (List CAResult)))
-> Either ResponseError (List CAResult)
-> IO (Either ResponseError (List CAResult))
forall a b. (a -> b) -> a -> b
$ List CAResult -> Either ResponseError (List CAResult)
forall a b. b -> Either a b
Right (List CAResult -> Either ResponseError (List CAResult))
-> List CAResult -> Either ResponseError (List CAResult)
forall a b. (a -> b) -> a -> b
$ [CodeAction] -> List CAResult
codeActions []


codeActions :: [CodeAction] -> List CAResult
codeActions :: [CodeAction] -> List CAResult
codeActions = [CAResult] -> List CAResult
forall a. [a] -> List a
List ([CAResult] -> List CAResult)
-> ([CodeAction] -> [CAResult]) -> [CodeAction] -> List CAResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CodeAction -> CAResult) -> [CodeAction] -> [CAResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CodeAction -> CAResult
CACodeAction


------------------------------------------------------------------------------
-- | Terminal constructor for providing context-sensitive tactics. Tactics
-- given by 'provide' are always available.
provide :: TacticCommand -> T.Text -> TacticProvider
provide :: TacticCommand -> Text -> TacticProvider
provide TacticCommand
tc Text
name DynFlags
_ PluginId
plId Uri
uri Range
range Judgement
_ = do
  let title :: Text
title = TacticCommand -> Text -> Text
tacticTitle TacticCommand
tc Text
name
      params :: TacticParams
params = TacticParams :: Uri -> Range -> Text -> TacticParams
TacticParams { file :: Uri
file = Uri
uri , range :: Range
range = Range
range , var_name :: Text
var_name = Text
name }
  Command
cmd <- PluginId -> CommandId -> Text -> Maybe [Value] -> IO Command
mkLspCommand PluginId
plId (TacticCommand -> CommandId
tcCommandId TacticCommand
tc) Text
title ([Value] -> Maybe [Value]
forall a. a -> Maybe a
Just [TacticParams -> Value
forall a. ToJSON a => a -> Value
toJSON TacticParams
params])
  [CAResult] -> IO [CAResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ([CAResult] -> IO [CAResult]) -> [CAResult] -> IO [CAResult]
forall a b. (a -> b) -> a -> b
$ CAResult -> [CAResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    (CAResult -> [CAResult]) -> CAResult -> [CAResult]
forall a b. (a -> b) -> a -> b
$ CodeAction -> CAResult
CACodeAction
    (CodeAction -> CAResult) -> CodeAction -> CAResult
forall a b. (a -> b) -> a -> b
$ Text
-> Maybe CodeActionKind
-> Maybe (List Diagnostic)
-> Maybe WorkspaceEdit
-> Maybe Command
-> CodeAction
CodeAction Text
title (CodeActionKind -> Maybe CodeActionKind
forall a. a -> Maybe a
Just CodeActionKind
CodeActionQuickFix) Maybe (List Diagnostic)
forall a. Maybe a
Nothing Maybe WorkspaceEdit
forall a. Maybe a
Nothing
    (Maybe Command -> CodeAction) -> Maybe Command -> CodeAction
forall a b. (a -> b) -> a -> b
$ Command -> Maybe Command
forall a. a -> Maybe a
Just Command
cmd


------------------------------------------------------------------------------
-- | Restrict a 'TacticProvider', making sure it appears only when the given
-- predicate holds for the goal.
requireExtension :: Extension -> TacticProvider -> TacticProvider
requireExtension :: Extension -> TacticProvider -> TacticProvider
requireExtension Extension
ext TacticProvider
tp DynFlags
dflags PluginId
plId Uri
uri Range
range Judgement
jdg =
  case Extension -> DynFlags -> Bool
xopt Extension
ext DynFlags
dflags of
    Bool
True  -> TacticProvider
tp DynFlags
dflags PluginId
plId Uri
uri Range
range Judgement
jdg
    Bool
False -> [CAResult] -> IO [CAResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []


------------------------------------------------------------------------------
-- | Restrict a 'TacticProvider', making sure it appears only when the given
-- predicate holds for the goal.
filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType Type -> Bool
p TacticProvider
tp DynFlags
dflags PluginId
plId Uri
uri Range
range Judgement
jdg =
  case Type -> Bool
p (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg of
    Bool
True  -> TacticProvider
tp DynFlags
dflags PluginId
plId Uri
uri Range
range Judgement
jdg
    Bool
False -> [CAResult] -> IO [CAResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []


------------------------------------------------------------------------------
-- | Multiply a 'TacticProvider' for each binding, making sure it appears only
-- when the given predicate holds over the goal and binding types.
filterBindingType
    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
    -> (OccName -> Type -> TacticProvider)
    -> TacticProvider
filterBindingType :: (Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
p OccName -> Type -> TacticProvider
tp DynFlags
dflags PluginId
plId Uri
uri Range
range Judgement
jdg =
  let hy :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg
      g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
   in ([[CAResult]] -> [CAResult]) -> IO [[CAResult]] -> IO [CAResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[CAResult]] -> [CAResult]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO [[CAResult]] -> IO [CAResult])
-> IO [[CAResult]] -> IO [CAResult]
forall a b. (a -> b) -> a -> b
$ [(OccName, HyInfo CType)]
-> ((OccName, HyInfo CType) -> IO [CAResult]) -> IO [[CAResult]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (Map OccName (HyInfo CType) -> [(OccName, HyInfo CType)]
forall k a. Map k a -> [(k, a)]
M.toList Map OccName (HyInfo CType)
hy) (((OccName, HyInfo CType) -> IO [CAResult]) -> IO [[CAResult]])
-> ((OccName, HyInfo CType) -> IO [CAResult]) -> IO [[CAResult]]
forall a b. (a -> b) -> a -> b
$ \(OccName
occ, HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType Type
ty) ->
        case Type -> Type -> Bool
p (CType -> Type
unCType CType
g) Type
ty of
          Bool
True  -> OccName -> Type -> TacticProvider
tp OccName
occ Type
ty DynFlags
dflags PluginId
plId Uri
uri Range
range Judgement
jdg
          Bool
False -> [CAResult] -> IO [CAResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []


data TacticParams = TacticParams
    { TacticParams -> Uri
file :: Uri -- ^ Uri of the file to fill the hole in
    , TacticParams -> Range
range :: Range -- ^ The range of the hole
    , TacticParams -> Text
var_name :: T.Text
    }
  deriving (Int -> TacticParams -> String -> String
[TacticParams] -> String -> String
TacticParams -> String
(Int -> TacticParams -> String -> String)
-> (TacticParams -> String)
-> ([TacticParams] -> String -> String)
-> Show TacticParams
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [TacticParams] -> String -> String
$cshowList :: [TacticParams] -> String -> String
show :: TacticParams -> String
$cshow :: TacticParams -> String
showsPrec :: Int -> TacticParams -> String -> String
$cshowsPrec :: Int -> TacticParams -> String -> String
Show, TacticParams -> TacticParams -> Bool
(TacticParams -> TacticParams -> Bool)
-> (TacticParams -> TacticParams -> Bool) -> Eq TacticParams
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TacticParams -> TacticParams -> Bool
$c/= :: TacticParams -> TacticParams -> Bool
== :: TacticParams -> TacticParams -> Bool
$c== :: TacticParams -> TacticParams -> Bool
Eq, (forall x. TacticParams -> Rep TacticParams x)
-> (forall x. Rep TacticParams x -> TacticParams)
-> Generic TacticParams
forall x. Rep TacticParams x -> TacticParams
forall x. TacticParams -> Rep TacticParams x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TacticParams x -> TacticParams
$cfrom :: forall x. TacticParams -> Rep TacticParams x
Generic, [TacticParams] -> Encoding
[TacticParams] -> Value
TacticParams -> Encoding
TacticParams -> Value
(TacticParams -> Value)
-> (TacticParams -> Encoding)
-> ([TacticParams] -> Value)
-> ([TacticParams] -> Encoding)
-> ToJSON TacticParams
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [TacticParams] -> Encoding
$ctoEncodingList :: [TacticParams] -> Encoding
toJSONList :: [TacticParams] -> Value
$ctoJSONList :: [TacticParams] -> Value
toEncoding :: TacticParams -> Encoding
$ctoEncoding :: TacticParams -> Encoding
toJSON :: TacticParams -> Value
$ctoJSON :: TacticParams -> Value
ToJSON, Value -> Parser [TacticParams]
Value -> Parser TacticParams
(Value -> Parser TacticParams)
-> (Value -> Parser [TacticParams]) -> FromJSON TacticParams
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [TacticParams]
$cparseJSONList :: Value -> Parser [TacticParams]
parseJSON :: Value -> Parser TacticParams
$cparseJSON :: Value -> Parser TacticParams
FromJSON)


------------------------------------------------------------------------------
-- | Find the last typechecked module, and find the most specific span, as well
-- as the judgement at the given range.
judgementForHole
    :: IdeState
    -> NormalizedFilePath
    -> Range
    -> MaybeT IO (Range, Judgement, Context, DynFlags)
judgementForHole :: IdeState
-> NormalizedFilePath
-> Range
-> MaybeT IO (Range, Judgement, Context, DynFlags)
judgementForHole IdeState
state NormalizedFilePath
nfp Range
range = do
  (HieAstResult
asts, PositionMapping
amapping) <- IO (Maybe (HieAstResult, PositionMapping))
-> MaybeT IO (HieAstResult, PositionMapping)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (HieAstResult, PositionMapping))
 -> MaybeT IO (HieAstResult, PositionMapping))
-> IO (Maybe (HieAstResult, PositionMapping))
-> MaybeT IO (HieAstResult, PositionMapping)
forall a b. (a -> b) -> a -> b
$ IdeState
-> Action (Maybe (HieAstResult, PositionMapping))
-> IO (Maybe (HieAstResult, PositionMapping))
forall a. IdeState -> Action a -> IO a
runIde IdeState
state (Action (Maybe (HieAstResult, PositionMapping))
 -> IO (Maybe (HieAstResult, PositionMapping)))
-> Action (Maybe (HieAstResult, PositionMapping))
-> IO (Maybe (HieAstResult, PositionMapping))
forall a b. (a -> b) -> a -> b
$ GetHieAst
-> NormalizedFilePath
-> Action (Maybe (HieAstResult, PositionMapping))
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe (v, PositionMapping))
useWithStale GetHieAst
GetHieAst NormalizedFilePath
nfp
  Range
range' <- Maybe Range -> MaybeT IO Range
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe Range -> MaybeT IO Range) -> Maybe Range -> MaybeT IO Range
forall a b. (a -> b) -> a -> b
$ PositionMapping -> Range -> Maybe Range
fromCurrentRange PositionMapping
amapping Range
range

  (Bindings
binds, PositionMapping
_) <- IO (Maybe (Bindings, PositionMapping))
-> MaybeT IO (Bindings, PositionMapping)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (Bindings, PositionMapping))
 -> MaybeT IO (Bindings, PositionMapping))
-> IO (Maybe (Bindings, PositionMapping))
-> MaybeT IO (Bindings, PositionMapping)
forall a b. (a -> b) -> a -> b
$ IdeState
-> Action (Maybe (Bindings, PositionMapping))
-> IO (Maybe (Bindings, PositionMapping))
forall a. IdeState -> Action a -> IO a
runIde IdeState
state (Action (Maybe (Bindings, PositionMapping))
 -> IO (Maybe (Bindings, PositionMapping)))
-> Action (Maybe (Bindings, PositionMapping))
-> IO (Maybe (Bindings, PositionMapping))
forall a b. (a -> b) -> a -> b
$ GetBindings
-> NormalizedFilePath -> Action (Maybe (Bindings, PositionMapping))
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe (v, PositionMapping))
useWithStale GetBindings
GetBindings NormalizedFilePath
nfp

  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
  -- which don't change very often.
  ((ModSummary
modsum,[LImportDecl GhcPs]
_), PositionMapping
_) <- IO (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
-> MaybeT IO ((ModSummary, [LImportDecl GhcPs]), PositionMapping)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
 -> MaybeT IO ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
-> IO (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
-> MaybeT IO ((ModSummary, [LImportDecl GhcPs]), PositionMapping)
forall a b. (a -> b) -> a -> b
$ IdeState
-> Action
     (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
-> IO (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
forall a. IdeState -> Action a -> IO a
runIde IdeState
state (Action
   (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
 -> IO (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping)))
-> Action
     (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
-> IO (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
forall a b. (a -> b) -> a -> b
$ GetModSummaryWithoutTimestamps
-> NormalizedFilePath
-> Action
     (Maybe ((ModSummary, [LImportDecl GhcPs]), PositionMapping))
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe (v, PositionMapping))
useWithStale GetModSummaryWithoutTimestamps
GetModSummaryWithoutTimestamps NormalizedFilePath
nfp
  let dflags :: DynFlags
dflags = ModSummary -> DynFlags
ms_hspp_opts ModSummary
modsum

  (Span
rss, Type
goal) <- Maybe (Span, Type) -> MaybeT IO (Span, Type)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Span, Type) -> MaybeT IO (Span, Type))
-> Maybe (Span, Type) -> MaybeT IO (Span, Type)
forall a b. (a -> b) -> a -> b
$ Maybe (Maybe (Span, Type)) -> Maybe (Span, Type)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (Span, Type)) -> Maybe (Span, Type))
-> Maybe (Maybe (Span, Type)) -> Maybe (Span, Type)
forall a b. (a -> b) -> a -> b
$ [Maybe (Span, Type)] -> Maybe (Maybe (Span, Type))
forall a. [a] -> Maybe a
listToMaybe ([Maybe (Span, Type)] -> Maybe (Maybe (Span, Type)))
-> [Maybe (Span, Type)] -> Maybe (Maybe (Span, Type))
forall a b. (a -> b) -> a -> b
$ Map FastString (Maybe (Span, Type)) -> [Maybe (Span, Type)]
forall k a. Map k a -> [a]
M.elems (Map FastString (Maybe (Span, Type)) -> [Maybe (Span, Type)])
-> Map FastString (Maybe (Span, Type)) -> [Maybe (Span, Type)]
forall a b. (a -> b) -> a -> b
$ ((FastString -> HieAST Type -> Maybe (Span, Type))
 -> Map FastString (HieAST Type)
 -> Map FastString (Maybe (Span, Type)))
-> Map FastString (HieAST Type)
-> (FastString -> HieAST Type -> Maybe (Span, Type))
-> Map FastString (Maybe (Span, Type))
forall a b c. (a -> b -> c) -> b -> a -> c
flip (FastString -> HieAST Type -> Maybe (Span, Type))
-> Map FastString (HieAST Type)
-> Map FastString (Maybe (Span, Type))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (HieASTs Type -> Map FastString (HieAST Type)
forall a. HieASTs a -> Map FastString (HieAST a)
getAsts (HieASTs Type -> Map FastString (HieAST Type))
-> HieASTs Type -> Map FastString (HieAST Type)
forall a b. (a -> b) -> a -> b
$ HieAstResult -> HieASTs Type
hieAst HieAstResult
asts) ((FastString -> HieAST Type -> Maybe (Span, Type))
 -> Map FastString (Maybe (Span, Type)))
-> (FastString -> HieAST Type -> Maybe (Span, Type))
-> Map FastString (Maybe (Span, Type))
forall a b. (a -> b) -> a -> b
$ \FastString
fs HieAST Type
ast ->
      case Span -> HieAST Type -> Maybe (HieAST Type)
forall a. Span -> HieAST a -> Maybe (HieAST a)
selectSmallestContaining (String -> Range -> Span
rangeToRealSrcSpan (FastString -> String
FastString.unpackFS FastString
fs) Range
range') HieAST Type
ast of
        Maybe (HieAST Type)
Nothing -> Maybe (Span, Type)
forall a. Maybe a
Nothing
        Just HieAST Type
ast' -> do
          let info :: NodeInfo Type
info = HieAST Type -> NodeInfo Type
forall a. HieAST a -> NodeInfo a
nodeInfo HieAST Type
ast'
          Type
ty <- [Type] -> Maybe Type
forall a. [a] -> Maybe a
listToMaybe ([Type] -> Maybe Type) -> [Type] -> Maybe Type
forall a b. (a -> b) -> a -> b
$ NodeInfo Type -> [Type]
forall a. NodeInfo a -> [a]
nodeType NodeInfo Type
info
          Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (FastString
"HsUnboundVar",FastString
"HsExpr") (FastString, FastString) -> Set (FastString, FastString) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` NodeInfo Type -> Set (FastString, FastString)
forall a. NodeInfo a -> Set (FastString, FastString)
nodeAnnotations NodeInfo Type
info
          (Span, Type) -> Maybe (Span, Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HieAST Type -> Span
forall a. HieAST a -> Span
nodeSpan HieAST Type
ast', Type
ty)

  Range
resulting_range <- Maybe Range -> MaybeT IO Range
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe Range -> MaybeT IO Range) -> Maybe Range -> MaybeT IO Range
forall a b. (a -> b) -> a -> b
$ PositionMapping -> Range -> Maybe Range
toCurrentRange PositionMapping
amapping (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Span -> Range
realSrcSpanToRange Span
rss
  (TcModuleResult
tcmod, PositionMapping
_) <- IO (Maybe (TcModuleResult, PositionMapping))
-> MaybeT IO (TcModuleResult, PositionMapping)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (TcModuleResult, PositionMapping))
 -> MaybeT IO (TcModuleResult, PositionMapping))
-> IO (Maybe (TcModuleResult, PositionMapping))
-> MaybeT IO (TcModuleResult, PositionMapping)
forall a b. (a -> b) -> a -> b
$ IdeState
-> Action (Maybe (TcModuleResult, PositionMapping))
-> IO (Maybe (TcModuleResult, PositionMapping))
forall a. IdeState -> Action a -> IO a
runIde IdeState
state (Action (Maybe (TcModuleResult, PositionMapping))
 -> IO (Maybe (TcModuleResult, PositionMapping)))
-> Action (Maybe (TcModuleResult, PositionMapping))
-> IO (Maybe (TcModuleResult, PositionMapping))
forall a b. (a -> b) -> a -> b
$ TypeCheck
-> NormalizedFilePath
-> Action (Maybe (TcModuleResult, PositionMapping))
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe (v, PositionMapping))
useWithStale TypeCheck
TypeCheck NormalizedFilePath
nfp
  let tcg :: TcGblEnv
tcg  = TcModuleResult -> TcGblEnv
tmrTypechecked TcModuleResult
tcmod
      tcs :: LHsBinds GhcTc
tcs = TcGblEnv -> LHsBinds GhcTc
tcg_binds TcGblEnv
tcg
      ctx :: Context
ctx = [(OccName, CType)] -> TcGblEnv -> Context
mkContext
              (((Name, Maybe Type) -> Maybe (OccName, CType))
-> [(Name, Maybe Type)] -> [(OccName, CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((OccName, Maybe CType) -> Maybe (OccName, CType)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA ((OccName, Maybe CType) -> Maybe (OccName, CType))
-> ((Name, Maybe Type) -> (OccName, Maybe CType))
-> (Name, Maybe Type)
-> Maybe (OccName, CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> OccName
forall name. HasOccName name => name -> OccName
occName (Name -> OccName)
-> (Maybe Type -> Maybe CType)
-> (Name, Maybe Type)
-> (OccName, Maybe CType)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Maybe Type -> Maybe CType
coerce))
                ([(Name, Maybe Type)] -> [(OccName, CType)])
-> [(Name, Maybe Type)] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ Bindings -> Span -> [(Name, Maybe Type)]
getDefiningBindings Bindings
binds Span
rss)
              TcGblEnv
tcg
      top_provs :: Map OccName Provenance
top_provs = Span -> LHsBinds GhcTc -> Map OccName Provenance
getRhsPosVals Span
rss LHsBinds GhcTc
tcs
      local_hy :: Map OccName (HyInfo CType)
local_hy = Map OccName Provenance
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a.
Map OccName Provenance
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
spliceProvenance Map OccName Provenance
top_provs
               (Map OccName (HyInfo CType) -> Map OccName (HyInfo CType))
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Span -> Bindings -> Map OccName (HyInfo CType)
hypothesisFromBindings Span
rss Bindings
binds
      cls_hy :: Map OccName (HyInfo CType)
cls_hy = Context -> Map OccName (HyInfo CType)
contextMethodHypothesis Context
ctx
  (Range, Judgement, Context, DynFlags)
-> MaybeT IO (Range, Judgement, Context, DynFlags)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( Range
resulting_range
       , Map OccName (HyInfo CType) -> Bool -> Type -> Judgement
mkFirstJudgement
           (Map OccName (HyInfo CType)
local_hy Map OccName (HyInfo CType)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a. Semigroup a => a -> a -> a
<> Map OccName (HyInfo CType)
cls_hy)
           (Span -> LHsBinds GhcTc -> Bool
isRhsHole Span
rss LHsBinds GhcTc
tcs)
           Type
goal
       , Context
ctx
       , DynFlags
dflags
       )


spliceProvenance
    :: Map OccName Provenance
    -> Map OccName (HyInfo a)
    -> Map OccName (HyInfo a)
spliceProvenance :: Map OccName Provenance
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
spliceProvenance Map OccName Provenance
provs =
  (OccName -> HyInfo a -> HyInfo a)
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey ((OccName -> HyInfo a -> HyInfo a)
 -> Map OccName (HyInfo a) -> Map OccName (HyInfo a))
-> (OccName -> HyInfo a -> HyInfo a)
-> Map OccName (HyInfo a)
-> Map OccName (HyInfo a)
forall a b. (a -> b) -> a -> b
$ \OccName
name HyInfo a
hi ->
    (Provenance -> Provenance) -> HyInfo a -> HyInfo a
forall a. (Provenance -> Provenance) -> HyInfo a -> HyInfo a
overProvenance ((Provenance -> Provenance)
-> (Provenance -> Provenance -> Provenance)
-> Maybe Provenance
-> Provenance
-> Provenance
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Provenance -> Provenance
forall a. a -> a
id Provenance -> Provenance -> Provenance
forall a b. a -> b -> a
const (Maybe Provenance -> Provenance -> Provenance)
-> Maybe Provenance -> Provenance -> Provenance
forall a b. (a -> b) -> a -> b
$ OccName -> Map OccName Provenance -> Maybe Provenance
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name Map OccName Provenance
provs) HyInfo a
hi


tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
tacticCmd OccName -> TacticsM ()
tac LspFuncs Config
lf IdeState
state (TacticParams Uri
uri 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 =
      (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> MaybeT
     IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall (m :: * -> *) a. Functor m => a -> MaybeT m a -> m a
fromMaybeT (Value -> Either ResponseError Value
forall a b. b -> Either a b
Right Value
Null, Maybe (ServerMethod, ApplyWorkspaceEditParams)
forall a. Maybe a
Nothing) (MaybeT
   IO
   (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
 -> IO
      (Either ResponseError Value,
       Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> MaybeT
     IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall a b. (a -> b) -> a -> b
$ do
        (Range
range', Judgement
jdg, Context
ctx, DynFlags
dflags) <- IdeState
-> NormalizedFilePath
-> Range
-> MaybeT IO (Range, Judgement, Context, DynFlags)
judgementForHole IdeState
state NormalizedFilePath
nfp Range
range
        let span :: Span
span = String -> Range -> Span
rangeToRealSrcSpan (NormalizedFilePath -> String
fromNormalizedFilePath NormalizedFilePath
nfp) Range
range'
        Annotated ParsedSource
pm <- IO (Maybe (Annotated ParsedSource))
-> MaybeT IO (Annotated ParsedSource)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (Annotated ParsedSource))
 -> MaybeT IO (Annotated ParsedSource))
-> IO (Maybe (Annotated ParsedSource))
-> MaybeT IO (Annotated ParsedSource)
forall a b. (a -> b) -> a -> b
$ String
-> IdeState
-> NormalizedFilePath
-> IO (Maybe (Annotated ParsedSource))
useAnnotatedSource String
"tacticsCmd" IdeState
state NormalizedFilePath
nfp
        Maybe
  (Either ResponseError Value,
   Maybe (ServerMethod, ApplyWorkspaceEditParams))
x <- IO
  (Maybe
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> MaybeT
     IO
     (Maybe
        (Either ResponseError Value,
         Maybe (ServerMethod, ApplyWorkspaceEditParams)))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO
   (Maybe
      (Either ResponseError Value,
       Maybe (ServerMethod, ApplyWorkspaceEditParams)))
 -> MaybeT
      IO
      (Maybe
         (Either ResponseError Value,
          Maybe (ServerMethod, ApplyWorkspaceEditParams))))
-> IO
     (Maybe
        (Either ResponseError Value,
         Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> MaybeT
     IO
     (Maybe
        (Either ResponseError Value,
         Maybe (ServerMethod, ApplyWorkspaceEditParams)))
forall a b. (a -> b) -> a -> b
$ Int
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Maybe
        (Either ResponseError Value,
         Maybe (ServerMethod, ApplyWorkspaceEditParams)))
forall a. Int -> IO a -> IO (Maybe a)
timeout Int
2e8 (IO
   (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
 -> IO
      (Maybe
         (Either ResponseError Value,
          Maybe (ServerMethod, ApplyWorkspaceEditParams))))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Maybe
        (Either ResponseError Value,
         Maybe (ServerMethod, ApplyWorkspaceEditParams)))
forall a b. (a -> b) -> a -> b
$
          case Context
-> Judgement
-> TacticsM ()
-> Either [TacticError] RunTacticResults
runTactic Context
ctx Judgement
jdg
                (TacticsM () -> Either [TacticError] RunTacticResults)
-> TacticsM () -> Either [TacticError] RunTacticResults
forall a b. (a -> b) -> a -> b
$ OccName -> TacticsM ()
tac
                (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc
                (String -> OccName) -> String -> OccName
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
var_name of
            Left [TacticError]
err ->
              (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Either ResponseError Value,
  Maybe (ServerMethod, ApplyWorkspaceEditParams))
 -> IO
      (Either ResponseError Value,
       Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall a b. (a -> b) -> a -> b
$ (, Maybe (ServerMethod, ApplyWorkspaceEditParams)
forall a. Maybe a
Nothing)
                (Either ResponseError Value
 -> (Either ResponseError Value,
     Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> Either ResponseError Value
-> (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
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 -> Maybe Value -> ResponseError
ResponseError ErrorCode
InvalidRequest (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ [TacticError] -> String
forall a. Show a => a -> String
show [TacticError]
err) Maybe Value
forall a. Maybe a
Nothing
            Right RunTacticResults
rtr -> do
              String -> [(Trace, LHsExpr GhcPs)] -> IO ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"solns" ([(Trace, LHsExpr GhcPs)] -> IO ())
-> [(Trace, LHsExpr GhcPs)] -> IO ()
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> [(Trace, LHsExpr GhcPs)]
rtr_other_solns RunTacticResults
rtr
              let g :: Graft ParsedSource
g = SrcSpan -> LHsExpr GhcPs -> Graft ParsedSource
forall a. Data a => SrcSpan -> LHsExpr GhcPs -> Graft a
graft (Span -> SrcSpan
RealSrcSpan Span
span) (LHsExpr GhcPs -> Graft ParsedSource)
-> LHsExpr GhcPs -> Graft ParsedSource
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> LHsExpr GhcPs
rtr_extract RunTacticResults
rtr
                  response :: Either String WorkspaceEdit
response = DynFlags
-> ClientCapabilities
-> Uri
-> Graft ParsedSource
-> Annotated ParsedSource
-> Either String WorkspaceEdit
transform DynFlags
dflags (LspFuncs Config -> ClientCapabilities
forall c. LspFuncs c -> ClientCapabilities
clientCapabilities LspFuncs Config
lf) Uri
uri Graft ParsedSource
g Annotated ParsedSource
pm
              (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Either ResponseError Value,
  Maybe (ServerMethod, ApplyWorkspaceEditParams))
 -> IO
      (Either ResponseError Value,
       Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall a b. (a -> b) -> a -> b
$ case Either String WorkspaceEdit
response of
                Right WorkspaceEdit
res -> (Value -> Either ResponseError Value
forall a b. b -> Either a b
Right Value
Null , (ServerMethod, ApplyWorkspaceEditParams)
-> Maybe (ServerMethod, ApplyWorkspaceEditParams)
forall a. a -> Maybe a
Just (ServerMethod
WorkspaceApplyEdit, WorkspaceEdit -> ApplyWorkspaceEditParams
ApplyWorkspaceEditParams WorkspaceEdit
res))
                Left String
err -> (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 -> Maybe Value -> ResponseError
ResponseError ErrorCode
InternalError (String -> Text
T.pack String
err) Maybe Value
forall a. Maybe a
Nothing, Maybe (ServerMethod, ApplyWorkspaceEditParams)
forall a. Maybe a
Nothing)
        (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> MaybeT
     IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Either ResponseError Value,
  Maybe (ServerMethod, ApplyWorkspaceEditParams))
 -> MaybeT
      IO
      (Either ResponseError Value,
       Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> MaybeT
     IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall a b. (a -> b) -> a -> b
$ case Maybe
  (Either ResponseError Value,
   Maybe (ServerMethod, ApplyWorkspaceEditParams))
x of
          Just (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
y -> (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
y
          Maybe
  (Either ResponseError Value,
   Maybe (ServerMethod, ApplyWorkspaceEditParams))
Nothing -> (, Maybe (ServerMethod, ApplyWorkspaceEditParams)
forall a. Maybe a
Nothing)
                   (Either ResponseError Value
 -> (Either ResponseError Value,
     Maybe (ServerMethod, ApplyWorkspaceEditParams)))
-> Either ResponseError Value
-> (Either ResponseError Value,
    Maybe (ServerMethod, ApplyWorkspaceEditParams))
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 -> Maybe Value -> ResponseError
ResponseError ErrorCode
InvalidRequest Text
"timed out" Maybe Value
forall a. Maybe a
Nothing
tacticCmd OccName -> TacticsM ()
_ LspFuncs Config
_ IdeState
_ TacticParams
_ =
  (Either ResponseError Value,
 Maybe (ServerMethod, ApplyWorkspaceEditParams))
-> IO
     (Either ResponseError Value,
      Maybe (ServerMethod, ApplyWorkspaceEditParams))
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( 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 -> Maybe Value -> ResponseError
ResponseError ErrorCode
InvalidRequest (String -> Text
T.pack String
"Bad URI") Maybe Value
forall a. Maybe a
Nothing
       , Maybe (ServerMethod, ApplyWorkspaceEditParams)
forall a. Maybe a
Nothing
       )


fromMaybeT :: Functor m => a -> MaybeT m a -> m a
fromMaybeT :: a -> MaybeT m a -> m a
fromMaybeT a
def = (Maybe a -> a) -> m (Maybe a) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
def) (m (Maybe a) -> m a)
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT m a -> m (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT

liftMaybe :: Monad m => Maybe a -> MaybeT m a
liftMaybe :: Maybe a -> MaybeT m a
liftMaybe Maybe a
a = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (Maybe a) -> MaybeT m a
forall a b. (a -> b) -> a -> b
$ Maybe a -> m (Maybe a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
a


------------------------------------------------------------------------------
-- | Is this hole immediately to the right of an equals sign?
isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool
isRhsHole :: Span -> LHsBinds GhcTc -> Bool
isRhsHole Span
rss LHsBinds GhcTc
tcs = (Bool -> Bool -> Bool) -> GenericQ Bool -> LHsBinds GhcTc -> Bool
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Bool -> Bool -> Bool
(||) (Bool -> (Match GhcTc (LHsExpr GhcTc) -> Bool) -> a -> Bool
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Bool
False ((Match GhcTc (LHsExpr GhcTc) -> Bool) -> a -> Bool)
-> (Match GhcTc (LHsExpr GhcTc) -> Bool) -> a -> Bool
forall a b. (a -> b) -> a -> b
$ \case
  TopLevelRHS OccName
_ [PatCompat GhcTc]
_ (L (RealSrcSpan Span
span) HsExpr GhcTc
_) -> Span -> Span -> Bool
containsSpan Span
rss Span
span
  Match GhcTc (LHsExpr GhcTc)
_ -> Bool
False
  ) LHsBinds GhcTc
tcs


------------------------------------------------------------------------------
-- | Compute top-level position vals of a function
getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance
getRhsPosVals :: Span -> LHsBinds GhcTc -> Map OccName Provenance
getRhsPosVals Span
rss LHsBinds GhcTc
tcs
  = [(OccName, Provenance)] -> Map OccName Provenance
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  ([(OccName, Provenance)] -> Map OccName Provenance)
-> [(OccName, Provenance)] -> Map OccName Provenance
forall a b. (a -> b) -> a -> b
$ [[(OccName, Provenance)]] -> [(OccName, Provenance)]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join
  ([[(OccName, Provenance)]] -> [(OccName, Provenance)])
-> [[(OccName, Provenance)]] -> [(OccName, Provenance)]
forall a b. (a -> b) -> a -> b
$ Maybe [(OccName, Provenance)] -> [[(OccName, Provenance)]]
forall a. Maybe a -> [a]
maybeToList
  (Maybe [(OccName, Provenance)] -> [[(OccName, Provenance)]])
-> Maybe [(OccName, Provenance)] -> [[(OccName, Provenance)]]
forall a b. (a -> b) -> a -> b
$ First [(OccName, Provenance)] -> Maybe [(OccName, Provenance)]
forall a. First a -> Maybe a
getFirst
  (First [(OccName, Provenance)] -> Maybe [(OccName, Provenance)])
-> First [(OccName, Provenance)] -> Maybe [(OccName, Provenance)]
forall a b. (a -> b) -> a -> b
$ (First [(OccName, Provenance)]
 -> First [(OccName, Provenance)] -> First [(OccName, Provenance)])
-> GenericQ (First [(OccName, Provenance)])
-> LHsBinds GhcTc
-> First [(OccName, Provenance)]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything First [(OccName, Provenance)]
-> First [(OccName, Provenance)] -> First [(OccName, Provenance)]
forall a. Semigroup a => a -> a -> a
(<>) (First [(OccName, Provenance)]
-> (Match GhcTc (LHsExpr GhcTc) -> First [(OccName, Provenance)])
-> a
-> First [(OccName, Provenance)]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ First [(OccName, Provenance)]
forall a. Monoid a => a
mempty ((Match GhcTc (LHsExpr GhcTc) -> First [(OccName, Provenance)])
 -> a -> First [(OccName, Provenance)])
-> (Match GhcTc (LHsExpr GhcTc) -> First [(OccName, Provenance)])
-> a
-> First [(OccName, Provenance)]
forall a b. (a -> b) -> a -> b
$ \case
      TopLevelRHS OccName
name [PatCompat GhcTc]
ps
          (L (RealSrcSpan Span
span)  -- body with no guards and a single defn
            (HsVar XVar GhcTc
_ (L SrcSpan
_ IdP GhcTc
hole)))
        | Span -> Span -> Bool
containsSpan Span
rss Span
span  -- which contains our span
        , OccName -> Bool
isHole (OccName -> Bool) -> OccName -> Bool
forall a b. (a -> b) -> a -> b
$ Id -> OccName
forall name. HasOccName name => name -> OccName
occName IdP GhcTc
Id
hole  -- and the span is a hole
        -> Maybe [(OccName, Provenance)] -> First [(OccName, Provenance)]
forall a. Maybe a -> First a
First (Maybe [(OccName, Provenance)] -> First [(OccName, Provenance)])
-> Maybe [(OccName, Provenance)] -> First [(OccName, Provenance)]
forall a b. (a -> b) -> a -> b
$ do
            [OccName]
patnames <- (Located (Pat GhcTc) -> Maybe OccName)
-> [Located (Pat GhcTc)] -> Maybe [OccName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PatCompat GhcTc -> Maybe OccName
Located (Pat GhcTc) -> Maybe OccName
getPatName [PatCompat GhcTc]
[Located (Pat GhcTc)]
ps
            [(OccName, Provenance)] -> Maybe [(OccName, Provenance)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(OccName, Provenance)] -> Maybe [(OccName, Provenance)])
-> [(OccName, Provenance)] -> Maybe [(OccName, Provenance)]
forall a b. (a -> b) -> a -> b
$ [OccName] -> [Provenance] -> [(OccName, Provenance)]
forall a b. [a] -> [b] -> [(a, b)]
zip [OccName]
patnames ([Provenance] -> [(OccName, Provenance)])
-> [Provenance] -> [(OccName, Provenance)]
forall a b. (a -> b) -> a -> b
$ [Int
0..] [Int] -> (Int -> Provenance) -> [Provenance]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> OccName -> Int -> Provenance
TopLevelArgPrv OccName
name
      Match GhcTc (LHsExpr GhcTc)
_ -> First [(OccName, Provenance)]
forall a. Monoid a => a
mempty
  ) LHsBinds GhcTc
tcs



-- TODO(sandy): Make this more robust
isHole :: OccName -> Bool
isHole :: OccName -> Bool
isHole = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"_" (String -> Bool) -> (OccName -> String) -> OccName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString