{-# LANGUAGE CPP               #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TupleSections     #-}
{-# LANGUAGE TypeFamilies      #-}

{-# LANGUAGE NoMonoLocalBinds  #-}

module Wingman.LanguageServer where

import           ConLike
import           Control.Arrow ((***))
import           Control.Monad
import           Control.Monad.IO.Class
import           Control.Monad.RWS
import           Control.Monad.State (State, evalState)
import           Control.Monad.Trans.Maybe
import           Data.Bifunctor (first)
import           Data.Coerce
import           Data.Functor ((<&>))
import           Data.Functor.Identity (runIdentity)
import qualified Data.HashMap.Strict as Map
import           Data.IORef (readIORef)
import qualified Data.Map as M
import           Data.Maybe
import           Data.Set (Set)
import qualified Data.Set as S
import qualified Data.Text as T
import           Data.Traversable
import           Development.IDE (getFilesOfInterestUntracked, ShowDiagnostic (ShowDiag), srcSpanToRange)
import           Development.IDE (hscEnv)
import           Development.IDE.Core.RuleTypes
import           Development.IDE.Core.Rules (usePropertyAction)
import           Development.IDE.Core.Service (runAction)
import           Development.IDE.Core.Shake (IdeState (..), uses, define, use)
import qualified Development.IDE.Core.Shake as IDE
import           Development.IDE.Core.UseStale
import           Development.IDE.GHC.Compat hiding (parseExpr)
import           Development.IDE.GHC.Error (realSrcSpanToRange)
import           Development.IDE.GHC.ExactPrint
import           Development.IDE.Graph (Action, RuleResult, Rules, action)
import           Development.IDE.Graph.Classes (Binary, Hashable, NFData)
import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
import qualified FastString
import           GHC.Generics (Generic)
import           Generics.SYB hiding (Generic)
import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
import qualified Ide.Plugin.Config as Plugin
import           Ide.Plugin.Properties
import           Ide.PluginUtils (usePropertyLsp)
import           Ide.Types (PluginId)
import           Language.Haskell.GHC.ExactPrint (Transform)
import           Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
import           Language.LSP.Server (MonadLsp, sendNotification)
import           Language.LSP.Types              hiding
                                                 (SemanticTokenAbsolute (length, line),
                                                  SemanticTokenRelative (length),
                                                  SemanticTokensEdit (_start))
import           Language.LSP.Types.Capabilities
import           OccName
import           Prelude hiding (span)
import           Retrie (transformA)
import           SrcLoc (containsSpan)
import           TcRnTypes (tcg_binds, TcGblEnv)
import           Wingman.Context
import           Wingman.GHC
import           Wingman.Judgements
import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
import           Wingman.Judgements.Theta
import           Wingman.Range
import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
import           Wingman.Types


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"


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


runIde :: String -> String -> IdeState -> Action a -> IO a
runIde :: String -> String -> IdeState -> Action a -> IO a
runIde String
herald String
action IdeState
state = String -> IdeState -> Action a -> IO a
forall a. String -> IdeState -> Action a -> IO a
runAction (String
"Wingman." String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
herald String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"." String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
action) IdeState
state


runCurrentIde
    :: 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 (Tracked 'Current r)
runCurrentIde :: String
-> IdeState
-> NormalizedFilePath
-> a
-> MaybeT IO (Tracked 'Current r)
runCurrentIde String
herald IdeState
state NormalizedFilePath
nfp a
a =
  IO (Maybe (Tracked 'Current r)) -> MaybeT IO (Tracked 'Current r)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (Tracked 'Current r)) -> MaybeT IO (Tracked 'Current r))
-> IO (Maybe (Tracked 'Current r))
-> MaybeT IO (Tracked 'Current r)
forall a b. (a -> b) -> a -> b
$ (Maybe r -> Maybe (Tracked 'Current r))
-> IO (Maybe r) -> IO (Maybe (Tracked 'Current r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((r -> Tracked 'Current r) -> Maybe r -> Maybe (Tracked 'Current r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> Tracked 'Current r
forall age. age -> Tracked 'Current age
unsafeMkCurrent) (IO (Maybe r) -> IO (Maybe (Tracked 'Current r)))
-> IO (Maybe r) -> IO (Maybe (Tracked 'Current r))
forall a b. (a -> b) -> a -> b
$ String -> String -> IdeState -> Action (Maybe r) -> IO (Maybe r)
forall a. String -> String -> IdeState -> Action a -> IO a
runIde String
herald (a -> String
forall a. Show a => a -> String
show a
a) IdeState
state (Action (Maybe r) -> IO (Maybe r))
-> Action (Maybe r) -> IO (Maybe r)
forall a b. (a -> b) -> a -> b
$ a -> NormalizedFilePath -> Action (Maybe r)
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe v)
use a
a NormalizedFilePath
nfp


runStaleIde
    :: 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
-> IdeState
-> NormalizedFilePath
-> a
-> MaybeT IO (TrackedStale r)
runStaleIde String
herald IdeState
state NormalizedFilePath
nfp a
a =
  IO (Maybe (TrackedStale r)) -> MaybeT IO (TrackedStale r)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (TrackedStale r)) -> MaybeT IO (TrackedStale r))
-> IO (Maybe (TrackedStale r)) -> MaybeT IO (TrackedStale r)
forall a b. (a -> b) -> a -> b
$ String
-> String
-> IdeState
-> Action (Maybe (TrackedStale r))
-> IO (Maybe (TrackedStale r))
forall a. String -> String -> IdeState -> Action a -> IO a
runIde String
herald (a -> String
forall a. Show a => a -> String
show a
a) IdeState
state (Action (Maybe (TrackedStale r)) -> IO (Maybe (TrackedStale r)))
-> Action (Maybe (TrackedStale r)) -> IO (Maybe (TrackedStale r))
forall a b. (a -> b) -> a -> b
$ a -> NormalizedFilePath -> Action (Maybe (TrackedStale r))
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe (TrackedStale v))
useWithStale a
a NormalizedFilePath
nfp


unsafeRunStaleIde
    :: 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 r
unsafeRunStaleIde :: String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO r
unsafeRunStaleIde String
herald IdeState
state NormalizedFilePath
nfp a
a = do
  (r
r, PositionMapping
_) <- IO (Maybe (r, PositionMapping)) -> MaybeT IO (r, PositionMapping)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe (r, PositionMapping)) -> MaybeT IO (r, PositionMapping))
-> IO (Maybe (r, PositionMapping))
-> MaybeT IO (r, PositionMapping)
forall a b. (a -> b) -> a -> b
$ String
-> String
-> IdeState
-> Action (Maybe (r, PositionMapping))
-> IO (Maybe (r, PositionMapping))
forall a. String -> String -> IdeState -> Action a -> IO a
runIde String
herald (a -> String
forall a. Show a => a -> String
show a
a) IdeState
state (Action (Maybe (r, PositionMapping))
 -> IO (Maybe (r, PositionMapping)))
-> Action (Maybe (r, PositionMapping))
-> IO (Maybe (r, PositionMapping))
forall a b. (a -> b) -> a -> b
$ a -> NormalizedFilePath -> Action (Maybe (r, PositionMapping))
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe (v, PositionMapping))
IDE.useWithStale a
a NormalizedFilePath
nfp
  r -> MaybeT IO r
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r


------------------------------------------------------------------------------

properties :: Properties
  '[ 'PropertyKey "hole_severity" ('TEnum (Maybe DiagnosticSeverity))
   , 'PropertyKey "max_use_ctor_actions" 'TInteger
   , 'PropertyKey "timeout_duration" 'TInteger
   , 'PropertyKey "auto_gas" 'TInteger
   , 'PropertyKey "proofstate_styling" 'TBoolean
   ]
properties :: Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties = Properties '[]
emptyProperties
  Properties '[]
-> (Properties '[]
    -> Properties '[ 'PropertyKey "proofstate_styling" 'TBoolean])
-> Properties '[ 'PropertyKey "proofstate_styling" 'TBoolean]
forall a b. a -> (a -> b) -> b
& KeyNameProxy "proofstate_styling"
-> Text
-> Bool
-> Properties '[]
-> Properties '[ 'PropertyKey "proofstate_styling" 'TBoolean]
forall (s :: Symbol) (r :: [PropertyKey]).
(KnownSymbol s, NotElem s r) =>
KeyNameProxy s
-> Text
-> Bool
-> Properties r
-> Properties ('PropertyKey s 'TBoolean : r)
defineBooleanProperty IsLabel "proofstate_styling" (KeyNameProxy "proofstate_styling")
KeyNameProxy "proofstate_styling"
#proofstate_styling
    Text
"Should Wingman emit styling markup when showing metaprogram proof states?" Bool
True
  Properties '[ 'PropertyKey "proofstate_styling" 'TBoolean]
-> (Properties '[ 'PropertyKey "proofstate_styling" 'TBoolean]
    -> Properties
         '[ 'PropertyKey "auto_gas" 'TInteger,
            'PropertyKey "proofstate_styling" 'TBoolean])
-> Properties
     '[ 'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall a b. a -> (a -> b) -> b
& KeyNameProxy "auto_gas"
-> Text
-> Int
-> Properties '[ 'PropertyKey "proofstate_styling" 'TBoolean]
-> Properties
     '[ 'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall (s :: Symbol) (r :: [PropertyKey]).
(KnownSymbol s, NotElem s r) =>
KeyNameProxy s
-> Text
-> Int
-> Properties r
-> Properties ('PropertyKey s 'TInteger : r)
defineIntegerProperty IsLabel "auto_gas" (KeyNameProxy "auto_gas")
KeyNameProxy "auto_gas"
#auto_gas
    Text
"The depth of the search tree when performing \"Attempt to fill hole\". Bigger values will be able to derive more solutions, but will take exponentially more time." Int
4
  Properties
  '[ 'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
-> (Properties
      '[ 'PropertyKey "auto_gas" 'TInteger,
         'PropertyKey "proofstate_styling" 'TBoolean]
    -> Properties
         '[ 'PropertyKey "timeout_duration" 'TInteger,
            'PropertyKey "auto_gas" 'TInteger,
            'PropertyKey "proofstate_styling" 'TBoolean])
-> Properties
     '[ 'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall a b. a -> (a -> b) -> b
& KeyNameProxy "timeout_duration"
-> Text
-> Int
-> Properties
     '[ 'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> Properties
     '[ 'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall (s :: Symbol) (r :: [PropertyKey]).
(KnownSymbol s, NotElem s r) =>
KeyNameProxy s
-> Text
-> Int
-> Properties r
-> Properties ('PropertyKey s 'TInteger : r)
defineIntegerProperty IsLabel "timeout_duration" (KeyNameProxy "timeout_duration")
KeyNameProxy "timeout_duration"
#timeout_duration
    Text
"The timeout for Wingman actions, in seconds" Int
2
  Properties
  '[ 'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
-> (Properties
      '[ 'PropertyKey "timeout_duration" 'TInteger,
         'PropertyKey "auto_gas" 'TInteger,
         'PropertyKey "proofstate_styling" 'TBoolean]
    -> Properties
         '[ 'PropertyKey "max_use_ctor_actions" 'TInteger,
            'PropertyKey "timeout_duration" 'TInteger,
            'PropertyKey "auto_gas" 'TInteger,
            'PropertyKey "proofstate_styling" 'TBoolean])
-> Properties
     '[ 'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall a b. a -> (a -> b) -> b
& KeyNameProxy "max_use_ctor_actions"
-> Text
-> Int
-> Properties
     '[ 'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> Properties
     '[ 'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall (s :: Symbol) (r :: [PropertyKey]).
(KnownSymbol s, NotElem s r) =>
KeyNameProxy s
-> Text
-> Int
-> Properties r
-> Properties ('PropertyKey s 'TInteger : r)
defineIntegerProperty IsLabel
  "max_use_ctor_actions" (KeyNameProxy "max_use_ctor_actions")
KeyNameProxy "max_use_ctor_actions"
#max_use_ctor_actions
    Text
"Maximum number of `Use constructor <x>` code actions that can appear" Int
5
  Properties
  '[ 'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
-> (Properties
      '[ 'PropertyKey "max_use_ctor_actions" 'TInteger,
         'PropertyKey "timeout_duration" 'TInteger,
         'PropertyKey "auto_gas" 'TInteger,
         'PropertyKey "proofstate_styling" 'TBoolean]
    -> Properties
         '[ 'PropertyKey
              "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
            'PropertyKey "max_use_ctor_actions" 'TInteger,
            'PropertyKey "timeout_duration" 'TInteger,
            'PropertyKey "auto_gas" 'TInteger,
            'PropertyKey "proofstate_styling" 'TBoolean])
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall a b. a -> (a -> b) -> b
& KeyNameProxy "hole_severity"
-> Text
-> [(Maybe DiagnosticSeverity, Text)]
-> Maybe DiagnosticSeverity
-> Properties
     '[ 'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
forall (s :: Symbol) (r :: [PropertyKey]) a.
(KnownSymbol s, NotElem s r, ToJSON a, FromJSON a, Eq a, Show a) =>
KeyNameProxy s
-> Text
-> [(a, Text)]
-> a
-> Properties r
-> Properties ('PropertyKey s ('TEnum a) : r)
defineEnumProperty IsLabel "hole_severity" (KeyNameProxy "hole_severity")
KeyNameProxy "hole_severity"
#hole_severity
    Text
"The severity to use when showing hole diagnostics. These are noisy, but some editors don't allow jumping to all severities."
    [ (DiagnosticSeverity -> Maybe DiagnosticSeverity
forall a. a -> Maybe a
Just DiagnosticSeverity
DsError,   Text
"error")
    , (DiagnosticSeverity -> Maybe DiagnosticSeverity
forall a. a -> Maybe a
Just DiagnosticSeverity
DsWarning, Text
"warning")
    , (DiagnosticSeverity -> Maybe DiagnosticSeverity
forall a. a -> Maybe a
Just DiagnosticSeverity
DsInfo,    Text
"info")
    , (DiagnosticSeverity -> Maybe DiagnosticSeverity
forall a. a -> Maybe a
Just DiagnosticSeverity
DsHint,    Text
"hint")
    , (Maybe DiagnosticSeverity
forall a. Maybe a
Nothing,        Text
"none")
    ]
    Maybe DiagnosticSeverity
forall a. Maybe a
Nothing


-- | Get the the plugin config
getTacticConfig :: MonadLsp Plugin.Config m => PluginId -> m Config
getTacticConfig :: PluginId -> m Config
getTacticConfig PluginId
pId =
  Int -> Int -> Int -> Bool -> Config
Config
    (Int -> Int -> Int -> Bool -> Config)
-> m Int -> m (Int -> Int -> Bool -> Config)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> KeyNameProxy "max_use_ctor_actions"
-> PluginId
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> m (ToHsType 'TInteger)
forall (s :: Symbol) (k :: PropertyKey) (t :: PropertyType)
       (r :: [PropertyKey]) (m :: * -> *).
(HasProperty s k t r, MonadLsp Config m) =>
KeyNameProxy s -> PluginId -> Properties r -> m (ToHsType t)
usePropertyLsp IsLabel
  "max_use_ctor_actions" (KeyNameProxy "max_use_ctor_actions")
KeyNameProxy "max_use_ctor_actions"
#max_use_ctor_actions PluginId
pId Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties
    m (Int -> Int -> Bool -> Config)
-> m Int -> m (Int -> Bool -> Config)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KeyNameProxy "timeout_duration"
-> PluginId
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> m (ToHsType 'TInteger)
forall (s :: Symbol) (k :: PropertyKey) (t :: PropertyType)
       (r :: [PropertyKey]) (m :: * -> *).
(HasProperty s k t r, MonadLsp Config m) =>
KeyNameProxy s -> PluginId -> Properties r -> m (ToHsType t)
usePropertyLsp IsLabel "timeout_duration" (KeyNameProxy "timeout_duration")
KeyNameProxy "timeout_duration"
#timeout_duration PluginId
pId Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties
    m (Int -> Bool -> Config) -> m Int -> m (Bool -> Config)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KeyNameProxy "auto_gas"
-> PluginId
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> m (ToHsType 'TInteger)
forall (s :: Symbol) (k :: PropertyKey) (t :: PropertyType)
       (r :: [PropertyKey]) (m :: * -> *).
(HasProperty s k t r, MonadLsp Config m) =>
KeyNameProxy s -> PluginId -> Properties r -> m (ToHsType t)
usePropertyLsp IsLabel "auto_gas" (KeyNameProxy "auto_gas")
KeyNameProxy "auto_gas"
#auto_gas PluginId
pId Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties
    m (Bool -> Config) -> m Bool -> m Config
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> KeyNameProxy "proofstate_styling"
-> PluginId
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> m (ToHsType 'TBoolean)
forall (s :: Symbol) (k :: PropertyKey) (t :: PropertyType)
       (r :: [PropertyKey]) (m :: * -> *).
(HasProperty s k t r, MonadLsp Config m) =>
KeyNameProxy s -> PluginId -> Properties r -> m (ToHsType t)
usePropertyLsp IsLabel "proofstate_styling" (KeyNameProxy "proofstate_styling")
KeyNameProxy "proofstate_styling"
#proofstate_styling PluginId
pId Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties


getIdeDynflags
    :: IdeState
    -> NormalizedFilePath
    -> MaybeT IO DynFlags
getIdeDynflags :: IdeState -> NormalizedFilePath -> MaybeT IO DynFlags
getIdeDynflags IdeState
state NormalizedFilePath
nfp = do
  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
  -- which don't change very often.
  ModSummaryResult
msr <- String
-> IdeState
-> NormalizedFilePath
-> GetModSummaryWithoutTimestamps
-> MaybeT IO ModSummaryResult
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 r
unsafeRunStaleIde String
"getIdeDynflags" IdeState
state NormalizedFilePath
nfp GetModSummaryWithoutTimestamps
GetModSummaryWithoutTimestamps
  DynFlags -> MaybeT IO DynFlags
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DynFlags -> MaybeT IO DynFlags) -> DynFlags -> MaybeT IO DynFlags
forall a b. (a -> b) -> a -> b
$ ModSummary -> DynFlags
ms_hspp_opts (ModSummary -> DynFlags) -> ModSummary -> DynFlags
forall a b. (a -> b) -> a -> b
$ ModSummaryResult -> ModSummary
msrModSummary ModSummaryResult
msr

getAllMetaprograms :: Data a => a -> [String]
getAllMetaprograms :: a -> [String]
getAllMetaprograms = ([String] -> [String] -> [String])
-> GenericQ [String] -> GenericQ [String]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
(<>) (GenericQ [String] -> GenericQ [String])
-> GenericQ [String] -> GenericQ [String]
forall a b. (a -> b) -> a -> b
$ [String] -> (HsExpr GhcTc -> [String]) -> a -> [String]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [String]
forall a. Monoid a => a
mempty ((HsExpr GhcTc -> [String]) -> a -> [String])
-> (HsExpr GhcTc -> [String]) -> a -> [String]
forall a b. (a -> b) -> a -> b
$ \case
  WingmanMetaprogram FastString
fs -> [ FastString -> String
unpackFS FastString
fs ]
  (HsExpr GhcTc
_ :: HsExpr GhcTc)  -> [String]
forall a. Monoid a => a
mempty


------------------------------------------------------------------------------
-- | Find the last typechecked module, and find the most specific span, as well
-- as the judgement at the given range.
judgementForHole
    :: IdeState
    -> NormalizedFilePath
    -> Tracked 'Current Range
    -> Config
    -> MaybeT IO HoleJudgment
judgementForHole :: IdeState
-> NormalizedFilePath
-> Tracked 'Current Range
-> Config
-> MaybeT IO HoleJudgment
judgementForHole IdeState
state NormalizedFilePath
nfp Tracked 'Current Range
range Config
cfg = 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
"judgementForHole" IdeState
state NormalizedFilePath
nfp a
a

  TrackedStale Tracked ('Stale s) HieAstResult
asts PositionMap ('Stale s) 'Current
amapping  <- GetHieAst -> MaybeT IO (TrackedStale (RuleResult GetHieAst))
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 GetHieAst
GetHieAst
  case Tracked ('Stale s) HieAstResult -> HieAstResult
forall (age :: Age) a. Tracked age a -> a
unTrack Tracked ('Stale s) HieAstResult
asts of
    HAR _ _  _ _ (HieFromDisk _) -> String -> MaybeT IO HoleJudgment
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Need a fresh hie file"
    HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do
      Tracked ('Stale s) Range
range' <- Maybe (Tracked ('Stale s) Range)
-> MaybeT IO (Tracked ('Stale s) Range)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Tracked ('Stale s) Range)
 -> MaybeT IO (Tracked ('Stale s) Range))
-> Maybe (Tracked ('Stale s) Range)
-> MaybeT IO (Tracked ('Stale s) Range)
forall a b. (a -> b) -> a -> b
$ PositionMap ('Stale s) 'Current
-> Tracked 'Current Range -> Maybe (Tracked ('Stale s) Range)
forall a (from :: Age) (to :: Age).
MapAge a =>
PositionMap from to -> Tracked to a -> Maybe (Tracked from a)
mapAgeFrom PositionMap ('Stale s) 'Current
amapping Tracked 'Current Range
range
      TrackedStale Bindings
binds <- GetBindings -> MaybeT IO (TrackedStale (RuleResult GetBindings))
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 GetBindings
GetBindings
      tcg :: TrackedStale TcGblEnv
tcg@(TrackedStale Tracked ('Stale s) TcGblEnv
tcg_t PositionMap ('Stale s) 'Current
tcg_map)
          <- (TrackedStale TcModuleResult -> TrackedStale TcGblEnv)
-> MaybeT IO (TrackedStale TcModuleResult)
-> MaybeT IO (TrackedStale TcGblEnv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TcModuleResult -> TcGblEnv)
-> TrackedStale TcModuleResult -> TrackedStale TcGblEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcModuleResult -> TcGblEnv
tmrTypechecked)
           (MaybeT IO (TrackedStale TcModuleResult)
 -> MaybeT IO (TrackedStale TcGblEnv))
-> MaybeT IO (TrackedStale TcModuleResult)
-> MaybeT IO (TrackedStale TcGblEnv)
forall a b. (a -> b) -> a -> b
$ TypeCheck -> MaybeT IO (TrackedStale (RuleResult TypeCheck))
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 TypeCheck
TypeCheck

      TrackedStale HscEnvEq
hscenv <- GhcSessionDeps
-> MaybeT IO (TrackedStale (RuleResult GhcSessionDeps))
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 GhcSessionDeps
GhcSessionDeps

      (Tracked ('Stale s) RealSrcSpan
rss, a
g) <- Maybe (Tracked ('Stale s) RealSrcSpan, a)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan, a)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Tracked ('Stale s) RealSrcSpan, a)
 -> MaybeT IO (Tracked ('Stale s) RealSrcSpan, a))
-> Maybe (Tracked ('Stale s) RealSrcSpan, a)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan, a)
forall a b. (a -> b) -> a -> b
$ Tracked ('Stale s) Range
-> Tracked ('Stale s) (HieASTs a)
-> Maybe (Tracked ('Stale s) RealSrcSpan, a)
forall (age :: Age) b.
Tracked age Range
-> Tracked age (HieASTs b) -> Maybe (Tracked age RealSrcSpan, b)
getSpanAndTypeAtHole Tracked ('Stale s) Range
range' Tracked ('Stale s) (HieASTs a)
hf

      Tracked 'Current RealSrcSpan
new_rss <- Maybe (Tracked 'Current RealSrcSpan)
-> MaybeT IO (Tracked 'Current RealSrcSpan)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Tracked 'Current RealSrcSpan)
 -> MaybeT IO (Tracked 'Current RealSrcSpan))
-> Maybe (Tracked 'Current RealSrcSpan)
-> MaybeT IO (Tracked 'Current RealSrcSpan)
forall a b. (a -> b) -> a -> b
$ PositionMap ('Stale s) 'Current
-> Tracked ('Stale s) RealSrcSpan
-> Maybe (Tracked 'Current RealSrcSpan)
forall a (from :: Age) (to :: Age).
MapAge a =>
PositionMap from to -> Tracked from a -> Maybe (Tracked to a)
mapAgeTo PositionMap ('Stale s) 'Current
amapping Tracked ('Stale s) RealSrcSpan
rss
      Tracked ('Stale s) RealSrcSpan
tcg_rss <- Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Tracked ('Stale s) RealSrcSpan)
 -> MaybeT IO (Tracked ('Stale s) RealSrcSpan))
-> Maybe (Tracked ('Stale s) RealSrcSpan)
-> MaybeT IO (Tracked ('Stale s) RealSrcSpan)
forall a b. (a -> b) -> a -> b
$ PositionMap ('Stale s) 'Current
-> Tracked 'Current RealSrcSpan
-> Maybe (Tracked ('Stale s) RealSrcSpan)
forall a (from :: Age) (to :: Age).
MapAge a =>
PositionMap from to -> Tracked to a -> Maybe (Tracked from a)
mapAgeFrom PositionMap ('Stale s) 'Current
tcg_map Tracked 'Current RealSrcSpan
new_rss

      -- KnownThings is just the instances in scope. There are no ranges
      -- involved, so it's not crucial to track ages.
      let henv :: HscEnvEq
henv = TrackedStale HscEnvEq -> HscEnvEq
forall a. TrackedStale a -> a
untrackedStaleValue (TrackedStale HscEnvEq -> HscEnvEq)
-> TrackedStale HscEnvEq -> HscEnvEq
forall a b. (a -> b) -> a -> b
$ TrackedStale HscEnvEq
hscenv
      ExternalPackageState
eps <- IO ExternalPackageState -> MaybeT IO ExternalPackageState
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ExternalPackageState -> MaybeT IO ExternalPackageState)
-> IO ExternalPackageState -> MaybeT IO ExternalPackageState
forall a b. (a -> b) -> a -> b
$ IORef ExternalPackageState -> IO ExternalPackageState
forall a. IORef a -> IO a
readIORef (IORef ExternalPackageState -> IO ExternalPackageState)
-> IORef ExternalPackageState -> IO ExternalPackageState
forall a b. (a -> b) -> a -> b
$ HscEnv -> IORef ExternalPackageState
hsc_EPS (HscEnv -> IORef ExternalPackageState)
-> HscEnv -> IORef ExternalPackageState
forall a b. (a -> b) -> a -> b
$ HscEnvEq -> HscEnv
hscEnv HscEnvEq
henv

      (Judgement
jdg, Context
ctx) <- Maybe (Judgement, Context) -> MaybeT IO (Judgement, Context)
forall (m :: * -> *) a. Monad m => Maybe a -> MaybeT m a
liftMaybe (Maybe (Judgement, Context) -> MaybeT IO (Judgement, Context))
-> Maybe (Judgement, Context) -> MaybeT IO (Judgement, Context)
forall a b. (a -> b) -> a -> b
$ Config
-> Type
-> TrackedStale Bindings
-> Tracked 'Current RealSrcSpan
-> TrackedStale TcGblEnv
-> HscEnv
-> ExternalPackageState
-> Maybe (Judgement, Context)
mkJudgementAndContext Config
cfg a
Type
g TrackedStale Bindings
binds Tracked 'Current RealSrcSpan
new_rss TrackedStale TcGblEnv
tcg (HscEnvEq -> HscEnv
hscEnv HscEnvEq
henv) ExternalPackageState
eps
      let mp :: Maybe Text
mp = Tracked ('Stale s) SrcSpan
-> Tracked ('Stale s) TcGblEnv -> Maybe Text
forall (age :: Age).
Tracked age SrcSpan -> Tracked age TcGblEnv -> Maybe Text
getMetaprogramAtSpan ((RealSrcSpan -> SrcSpan)
-> Tracked ('Stale s) RealSrcSpan -> Tracked ('Stale s) SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RealSrcSpan -> SrcSpan
RealSrcSpan Tracked ('Stale s) RealSrcSpan
tcg_rss) Tracked ('Stale s) TcGblEnv
tcg_t

      DynFlags
dflags <- IdeState -> NormalizedFilePath -> MaybeT IO DynFlags
getIdeDynflags IdeState
state NormalizedFilePath
nfp
      HoleJudgment -> MaybeT IO HoleJudgment
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HoleJudgment -> MaybeT IO HoleJudgment)
-> HoleJudgment -> MaybeT IO HoleJudgment
forall a b. (a -> b) -> a -> b
$ HoleJudgment :: Tracked 'Current Range
-> Judgement -> Context -> DynFlags -> HoleSort -> HoleJudgment
HoleJudgment
        { hj_range :: Tracked 'Current Range
hj_range = (RealSrcSpan -> Range)
-> Tracked 'Current RealSrcSpan -> Tracked 'Current Range
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RealSrcSpan -> Range
realSrcSpanToRange Tracked 'Current RealSrcSpan
new_rss
        , hj_jdg :: Judgement
hj_jdg = Judgement
jdg
        , hj_ctx :: Context
hj_ctx = Context
ctx
        , hj_dflags :: DynFlags
hj_dflags = DynFlags
dflags
        , hj_hole_sort :: HoleSort
hj_hole_sort = Maybe Text -> HoleSort
holeSortFor Maybe Text
mp
        }


holeSortFor :: Maybe T.Text -> HoleSort
holeSortFor :: Maybe Text -> HoleSort
holeSortFor = HoleSort -> (Text -> HoleSort) -> Maybe Text -> HoleSort
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HoleSort
Hole Text -> HoleSort
Metaprogram


mkJudgementAndContext
    :: Config
    -> Type
    -> TrackedStale Bindings
    -> Tracked 'Current RealSrcSpan
    -> TrackedStale TcGblEnv
    -> HscEnv
    -> ExternalPackageState
    -> Maybe (Judgement, Context)
mkJudgementAndContext :: Config
-> Type
-> TrackedStale Bindings
-> Tracked 'Current RealSrcSpan
-> TrackedStale TcGblEnv
-> HscEnv
-> ExternalPackageState
-> Maybe (Judgement, Context)
mkJudgementAndContext Config
cfg Type
g (TrackedStale Tracked ('Stale s) Bindings
binds PositionMap ('Stale s) 'Current
bmap) Tracked 'Current RealSrcSpan
rss (TrackedStale Tracked ('Stale s) TcGblEnv
tcg PositionMap ('Stale s) 'Current
tcgmap) HscEnv
hscenv ExternalPackageState
eps = do
  Tracked ('Stale s) RealSrcSpan
binds_rss <- 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
bmap Tracked 'Current RealSrcSpan
rss
  Tracked ('Stale s) RealSrcSpan
tcg_rss <- 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
tcgmap Tracked 'Current RealSrcSpan
rss

  let tcs :: Tracked ('Stale s) (LHsBinds GhcTc)
tcs = (TcGblEnv -> LHsBinds GhcTc)
-> Tracked ('Stale s) TcGblEnv
-> Tracked ('Stale s) (LHsBinds GhcTc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcGblEnv -> LHsBinds GhcTc
tcg_binds Tracked ('Stale s) TcGblEnv
tcg
      ctx :: Context
ctx = Config
-> [(OccName, CType)]
-> TcGblEnv
-> HscEnv
-> ExternalPackageState
-> [Evidence]
-> Context
mkContext Config
cfg
              (((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
$ Tracked ('Stale s) [(Name, Maybe Type)] -> [(Name, Maybe Type)]
forall (age :: Age) a. Tracked age a -> a
unTrack
                (Tracked ('Stale s) [(Name, Maybe Type)] -> [(Name, Maybe Type)])
-> Tracked ('Stale s) [(Name, Maybe Type)] -> [(Name, Maybe Type)]
forall a b. (a -> b) -> a -> b
$ Bindings -> RealSrcSpan -> [(Name, Maybe Type)]
getDefiningBindings (Bindings -> RealSrcSpan -> [(Name, Maybe Type)])
-> Tracked ('Stale s) Bindings
-> Tracked ('Stale s) (RealSrcSpan -> [(Name, Maybe Type)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tracked ('Stale s) Bindings
binds Tracked ('Stale s) (RealSrcSpan -> [(Name, Maybe Type)])
-> Tracked ('Stale s) RealSrcSpan
-> Tracked ('Stale s) [(Name, Maybe Type)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tracked ('Stale s) RealSrcSpan
binds_rss)
              (Tracked ('Stale s) TcGblEnv -> TcGblEnv
forall (age :: Age) a. Tracked age a -> a
unTrack Tracked ('Stale s) TcGblEnv
tcg)
              HscEnv
hscenv
              ExternalPackageState
eps
              [Evidence]
evidence
      top_provs :: Hypothesis CType
top_provs = Tracked ('Stale s) RealSrcSpan
-> Tracked ('Stale s) (LHsBinds GhcTc) -> Hypothesis CType
forall (age :: Age).
Tracked age RealSrcSpan
-> Tracked age (LHsBinds GhcTc) -> Hypothesis CType
getRhsPosVals Tracked ('Stale s) RealSrcSpan
tcg_rss Tracked ('Stale s) (LHsBinds GhcTc)
tcs
      already_destructed :: Set OccName
already_destructed = Tracked ('Stale s) SrcSpan
-> Tracked ('Stale s) (LHsBinds GhcTc) -> Set OccName
forall (age :: Age).
Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> Set OccName
getAlreadyDestructed ((RealSrcSpan -> SrcSpan)
-> Tracked ('Stale s) RealSrcSpan -> Tracked ('Stale s) SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RealSrcSpan -> SrcSpan
RealSrcSpan Tracked ('Stale s) RealSrcSpan
tcg_rss) Tracked ('Stale s) (LHsBinds GhcTc)
tcs
      local_hy :: Hypothesis CType
local_hy = Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Hypothesis a -> Hypothesis a -> Hypothesis a
spliceProvenance Hypothesis CType
top_provs
               (Hypothesis CType -> Hypothesis CType)
-> Hypothesis CType -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ Tracked ('Stale s) RealSrcSpan
-> Tracked ('Stale s) Bindings -> Hypothesis CType
forall (age :: Age).
Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType
hypothesisFromBindings Tracked ('Stale s) RealSrcSpan
binds_rss Tracked ('Stale s) Bindings
binds
      evidence :: [Evidence]
evidence = Tracked ('Stale s) SrcSpan
-> Tracked ('Stale s) (LHsBinds GhcTc) -> [Evidence]
forall (age :: Age).
Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
getEvidenceAtHole ((RealSrcSpan -> SrcSpan)
-> Tracked ('Stale s) RealSrcSpan -> Tracked ('Stale s) SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RealSrcSpan -> SrcSpan
RealSrcSpan Tracked ('Stale s) RealSrcSpan
tcg_rss) Tracked ('Stale s) (LHsBinds GhcTc)
tcs
      cls_hy :: Hypothesis CType
cls_hy = (Evidence -> Hypothesis CType) -> [Evidence] -> Hypothesis CType
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Evidence -> Hypothesis CType
evidenceToHypothesis [Evidence]
evidence
      subst :: TCvSubst
subst = TacticState -> TCvSubst
ts_unifier (TacticState -> TCvSubst) -> TacticState -> TCvSubst
forall a b. (a -> b) -> a -> b
$ [Evidence] -> TacticState -> TacticState
evidenceToSubst [Evidence]
evidence TacticState
defaultTacticState
  (Judgement, Context) -> Maybe (Judgement, Context)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Judgement, Context) -> Maybe (Judgement, Context))
-> (Judgement, Context) -> Maybe (Judgement, Context)
forall a b. (a -> b) -> a -> b
$
    ( DisallowReason -> Set OccName -> Judgement -> Judgement
forall a.
DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
disallowing DisallowReason
AlreadyDestructed Set OccName
already_destructed
    (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ (CType -> CType) -> Judgement -> Judgement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> CType
CType (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCvSubst -> Type -> Type
substTyAddInScope TCvSubst
subst (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType) (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$
        Context -> Hypothesis CType -> Bool -> Type -> Judgement
mkFirstJudgement
          Context
ctx
          (Hypothesis CType
local_hy Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Semigroup a => a -> a -> a
<> Hypothesis CType
cls_hy)
          (Tracked ('Stale s) RealSrcSpan
-> Tracked ('Stale s) (LHsBinds GhcTc) -> Bool
forall (age :: Age).
Tracked age RealSrcSpan -> Tracked age (LHsBinds GhcTc) -> Bool
isRhsHole Tracked ('Stale s) RealSrcSpan
tcg_rss Tracked ('Stale s) (LHsBinds GhcTc)
tcs)
          Type
g
    , Context
ctx
    )


------------------------------------------------------------------------------
-- | Determine which bindings have already been destructed by the location of
-- the hole.
getAlreadyDestructed
    :: Tracked age SrcSpan
    -> Tracked age (LHsBinds GhcTc)
    -> Set OccName
getAlreadyDestructed :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> Set OccName
getAlreadyDestructed (Tracked age SrcSpan -> SrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> SrcSpan
span) (Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc
forall (age :: Age) a. Tracked age a -> a
unTrack -> LHsBinds GhcTc
binds) =
  SrcSpan -> GenericQ (Set OccName) -> LHsBinds GhcTc -> Set OccName
forall r. Monoid r => SrcSpan -> GenericQ r -> GenericQ r
everythingContaining SrcSpan
span
    (Set OccName -> (HsExpr GhcTc -> Set OccName) -> a -> Set OccName
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Set OccName
forall a. Monoid a => a
mempty ((HsExpr GhcTc -> Set OccName) -> a -> Set OccName)
-> (HsExpr GhcTc -> Set OccName) -> a -> Set OccName
forall a b. (a -> b) -> a -> b
$ \case
      Case (HsVar XVar GhcTc
_ (L SrcSpan
_ (IdP GhcTc -> OccName
forall name. HasOccName name => name -> OccName
occName -> OccName
var))) [(Pat GhcTc, LHsExpr GhcTc)]
_ ->
        OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
var
      (HsExpr GhcTc
_ :: HsExpr GhcTc) -> Set OccName
forall a. Monoid a => a
mempty
    ) LHsBinds GhcTc
binds


getSpanAndTypeAtHole
    :: Tracked age Range
    -> Tracked age (HieASTs b)
    -> Maybe (Tracked age RealSrcSpan, b)
getSpanAndTypeAtHole :: Tracked age Range
-> Tracked age (HieASTs b) -> Maybe (Tracked age RealSrcSpan, b)
getSpanAndTypeAtHole r :: Tracked age Range
r@(Tracked age Range -> Range
forall (age :: Age) a. Tracked age a -> a
unTrack -> Range
range) (Tracked age (HieASTs b) -> HieASTs b
forall (age :: Age) a. Tracked age a -> a
unTrack -> HieASTs b
hf) = do
  Maybe (Maybe (Tracked age RealSrcSpan, b))
-> Maybe (Tracked age RealSrcSpan, b)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (Tracked age RealSrcSpan, b))
 -> Maybe (Tracked age RealSrcSpan, b))
-> Maybe (Maybe (Tracked age RealSrcSpan, b))
-> Maybe (Tracked age RealSrcSpan, b)
forall a b. (a -> b) -> a -> b
$ [Maybe (Tracked age RealSrcSpan, b)]
-> Maybe (Maybe (Tracked age RealSrcSpan, b))
forall a. [a] -> Maybe a
listToMaybe ([Maybe (Tracked age RealSrcSpan, b)]
 -> Maybe (Maybe (Tracked age RealSrcSpan, b)))
-> [Maybe (Tracked age RealSrcSpan, b)]
-> Maybe (Maybe (Tracked age RealSrcSpan, b))
forall a b. (a -> b) -> a -> b
$ Map FastString (Maybe (Tracked age RealSrcSpan, b))
-> [Maybe (Tracked age RealSrcSpan, b)]
forall k a. Map k a -> [a]
M.elems (Map FastString (Maybe (Tracked age RealSrcSpan, b))
 -> [Maybe (Tracked age RealSrcSpan, b)])
-> Map FastString (Maybe (Tracked age RealSrcSpan, b))
-> [Maybe (Tracked age RealSrcSpan, b)]
forall a b. (a -> b) -> a -> b
$ ((FastString -> HieAST b -> Maybe (Tracked age RealSrcSpan, b))
 -> Map FastString (HieAST b)
 -> Map FastString (Maybe (Tracked age RealSrcSpan, b)))
-> Map FastString (HieAST b)
-> (FastString -> HieAST b -> Maybe (Tracked age RealSrcSpan, b))
-> Map FastString (Maybe (Tracked age RealSrcSpan, b))
forall a b c. (a -> b -> c) -> b -> a -> c
flip (FastString -> HieAST b -> Maybe (Tracked age RealSrcSpan, b))
-> Map FastString (HieAST b)
-> Map FastString (Maybe (Tracked age RealSrcSpan, b))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (HieASTs b -> Map FastString (HieAST b)
forall a. HieASTs a -> Map FastString (HieAST a)
getAsts HieASTs b
hf) ((FastString -> HieAST b -> Maybe (Tracked age RealSrcSpan, b))
 -> Map FastString (Maybe (Tracked age RealSrcSpan, b)))
-> (FastString -> HieAST b -> Maybe (Tracked age RealSrcSpan, b))
-> Map FastString (Maybe (Tracked age RealSrcSpan, b))
forall a b. (a -> b) -> a -> b
$ \FastString
fs HieAST b
ast ->
    case RealSrcSpan -> HieAST b -> Maybe (HieAST b)
forall a. RealSrcSpan -> HieAST a -> Maybe (HieAST a)
selectSmallestContaining (String -> Range -> RealSrcSpan
rangeToRealSrcSpan (FastString -> String
FastString.unpackFS FastString
fs) Range
range) HieAST b
ast of
      Maybe (HieAST b)
Nothing -> Maybe (Tracked age RealSrcSpan, b)
forall a. Maybe a
Nothing
      Just HieAST b
ast' -> do
        let info :: NodeInfo b
info = HieAST b -> NodeInfo b
forall a. HieAST a -> NodeInfo a
nodeInfo HieAST b
ast'
        b
ty <- [b] -> Maybe b
forall a. [a] -> Maybe a
listToMaybe ([b] -> Maybe b) -> [b] -> Maybe b
forall a b. (a -> b) -> a -> b
$ NodeInfo b -> [b]
forall a. NodeInfo a -> [a]
nodeType NodeInfo b
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 b -> Set (FastString, FastString)
forall a. NodeInfo a -> Set (FastString, FastString)
nodeAnnotations NodeInfo b
info
        -- Ensure we're actually looking at a hole here
        OccName
occ <- ((ModuleName -> Maybe OccName)
-> (Name -> Maybe OccName)
-> Either ModuleName Name
-> Maybe OccName
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe OccName -> ModuleName -> Maybe OccName
forall a b. a -> b -> a
const Maybe OccName
forall a. Maybe a
Nothing) (OccName -> Maybe OccName
forall a. a -> Maybe a
Just (OccName -> Maybe OccName)
-> (Name -> OccName) -> Name -> Maybe OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> OccName
forall name. HasOccName name => name -> OccName
occName) (Either ModuleName Name -> Maybe OccName)
-> Maybe (Either ModuleName Name) -> Maybe OccName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<)
             (Maybe (Either ModuleName Name) -> Maybe OccName)
-> (Map (Either ModuleName Name) (IdentifierDetails b)
    -> Maybe (Either ModuleName Name))
-> Map (Either ModuleName Name) (IdentifierDetails b)
-> Maybe OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either ModuleName Name] -> Maybe (Either ModuleName Name)
forall a. [a] -> Maybe a
listToMaybe
             ([Either ModuleName Name] -> Maybe (Either ModuleName Name))
-> (Map (Either ModuleName Name) (IdentifierDetails b)
    -> [Either ModuleName Name])
-> Map (Either ModuleName Name) (IdentifierDetails b)
-> Maybe (Either ModuleName Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Either ModuleName Name) -> [Either ModuleName Name]
forall a. Set a -> [a]
S.toList
             (Set (Either ModuleName Name) -> [Either ModuleName Name])
-> (Map (Either ModuleName Name) (IdentifierDetails b)
    -> Set (Either ModuleName Name))
-> Map (Either ModuleName Name) (IdentifierDetails b)
-> [Either ModuleName Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Either ModuleName Name) (IdentifierDetails b)
-> Set (Either ModuleName Name)
forall k a. Map k a -> Set k
M.keysSet
             (Map (Either ModuleName Name) (IdentifierDetails b)
 -> Maybe OccName)
-> Map (Either ModuleName Name) (IdentifierDetails b)
-> Maybe OccName
forall a b. (a -> b) -> a -> b
$ NodeInfo b -> Map (Either ModuleName Name) (IdentifierDetails b)
forall a. NodeInfo a -> NodeIdentifiers a
nodeIdentifiers NodeInfo b
info
        Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ OccName -> Bool
isHole OccName
occ
        (Tracked age RealSrcSpan, b) -> Maybe (Tracked age RealSrcSpan, b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tracked age Range -> RealSrcSpan -> Tracked age RealSrcSpan
forall (age :: Age) a b. Tracked age a -> b -> Tracked age b
unsafeCopyAge Tracked age Range
r (RealSrcSpan -> Tracked age RealSrcSpan)
-> RealSrcSpan -> Tracked age RealSrcSpan
forall a b. (a -> b) -> a -> b
$ HieAST b -> RealSrcSpan
forall a. HieAST a -> RealSrcSpan
nodeSpan HieAST b
ast', b
ty)



------------------------------------------------------------------------------
-- | Combine two (possibly-overlapping) hypotheses; using the provenance from
-- the first hypothesis if the bindings overlap.
spliceProvenance
    :: Hypothesis a  -- ^ Bindings to keep
    -> Hypothesis a  -- ^ Bindings to keep if they don't overlap with the first set
    -> Hypothesis a
spliceProvenance :: Hypothesis a -> Hypothesis a -> Hypothesis a
spliceProvenance Hypothesis a
top Hypothesis a
x =
  let bound :: Set OccName
bound = [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList ([OccName] -> Set OccName) -> [OccName] -> Set OccName
forall a b. (a -> b) -> a -> b
$ (HyInfo a -> OccName) -> [HyInfo a] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HyInfo a -> OccName
forall a. HyInfo a -> OccName
hi_name ([HyInfo a] -> [OccName]) -> [HyInfo a] -> [OccName]
forall a b. (a -> b) -> a -> b
$ Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis a
top
   in Hypothesis a -> Hypothesis a -> Hypothesis a
forall a. Monoid a => a -> a -> a
mappend Hypothesis a
top (Hypothesis a -> Hypothesis a) -> Hypothesis a -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ [HyInfo a] -> Hypothesis a
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo a] -> Hypothesis a)
-> ([HyInfo a] -> [HyInfo a]) -> [HyInfo a] -> Hypothesis a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo a -> Bool) -> [HyInfo a] -> [HyInfo a]
forall a. (a -> Bool) -> [a] -> [a]
filter ((OccName -> Set OccName -> Bool) -> Set OccName -> OccName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.notMember Set OccName
bound (OccName -> Bool) -> (HyInfo a -> OccName) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> OccName
forall a. HyInfo a -> OccName
hi_name) ([HyInfo a] -> Hypothesis a) -> [HyInfo a] -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis a
x


------------------------------------------------------------------------------
-- | Compute top-level position vals of a function
getRhsPosVals
    :: Tracked age RealSrcSpan
    -> Tracked age TypecheckedSource
    -> Hypothesis CType
getRhsPosVals :: Tracked age RealSrcSpan
-> Tracked age (LHsBinds GhcTc) -> Hypothesis CType
getRhsPosVals (Tracked age RealSrcSpan -> RealSrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> RealSrcSpan
rss) (Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc
forall (age :: Age) a. Tracked age a -> a
unTrack -> LHsBinds GhcTc
tcs)
  = (Hypothesis CType -> Hypothesis CType -> Hypothesis CType)
-> GenericQ (Hypothesis CType)
-> LHsBinds GhcTc
-> Hypothesis CType
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Semigroup a => a -> a -> a
(<>) (Hypothesis CType
-> (Match GhcTc (LHsExpr GhcTc) -> Hypothesis CType)
-> a
-> Hypothesis CType
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Hypothesis CType
forall a. Monoid a => a
mempty ((Match GhcTc (LHsExpr GhcTc) -> Hypothesis CType)
 -> a -> Hypothesis CType)
-> (Match GhcTc (LHsExpr GhcTc) -> Hypothesis CType)
-> a
-> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ \case
      TopLevelRHS OccName
name [PatCompat GhcTc]
ps
          (L (RealSrcSpan RealSrcSpan
span)  -- body with no guards and a single defn
            (HsVar XVar GhcTc
_ (L SrcSpan
_ IdP GhcTc
hole)))
        | RealSrcSpan -> RealSrcSpan -> Bool
containsSpan RealSrcSpan
rss RealSrcSpan
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
        -> (State Int (Hypothesis CType) -> Int -> Hypothesis CType)
-> Int -> State Int (Hypothesis CType) -> Hypothesis CType
forall a b c. (a -> b -> c) -> b -> a -> c
flip State Int (Hypothesis CType) -> Int -> Hypothesis CType
forall s a. State s a -> s -> a
evalState Int
0 (State Int (Hypothesis CType) -> Hypothesis CType)
-> State Int (Hypothesis CType) -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ OccName -> [PatCompat GhcTc] -> State Int (Hypothesis CType)
buildTopLevelHypothesis OccName
name [PatCompat GhcTc]
ps
      Match GhcTc (LHsExpr GhcTc)
_ -> Hypothesis CType
forall a. Monoid a => a
mempty
  ) LHsBinds GhcTc
tcs


------------------------------------------------------------------------------
-- | Construct a hypothesis given the patterns from the left side of a HsMatch.
-- These correspond to things that the user put in scope before running
-- tactics.
buildTopLevelHypothesis
    :: OccName  -- ^ Function name
    -> [PatCompat GhcTc]
    -> State Int (Hypothesis CType)
buildTopLevelHypothesis :: OccName -> [PatCompat GhcTc] -> State Int (Hypothesis CType)
buildTopLevelHypothesis OccName
name [PatCompat GhcTc]
ps = do
  ([Hypothesis CType] -> Hypothesis CType)
-> StateT Int Identity [Hypothesis CType]
-> State Int (Hypothesis CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Hypothesis CType] -> Hypothesis CType
forall a. Monoid a => [a] -> a
mconcat (StateT Int Identity [Hypothesis CType]
 -> State Int (Hypothesis CType))
-> StateT Int Identity [Hypothesis CType]
-> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$
    [(Int, Located (Pat GhcTc))]
-> ((Int, Located (Pat GhcTc)) -> State Int (Hypothesis CType))
-> StateT Int Identity [Hypothesis CType]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for ([Int] -> [Located (Pat GhcTc)] -> [(Int, Located (Pat GhcTc))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [PatCompat GhcTc]
[Located (Pat GhcTc)]
ps) (((Int, Located (Pat GhcTc)) -> State Int (Hypothesis CType))
 -> StateT Int Identity [Hypothesis CType])
-> ((Int, Located (Pat GhcTc)) -> State Int (Hypothesis CType))
-> StateT Int Identity [Hypothesis CType]
forall a b. (a -> b) -> a -> b
$ \(Int
ix, Located (Pat GhcTc)
p) ->
      Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy (OccName -> Int -> Int -> Provenance
TopLevelArgPrv OccName
name Int
ix (Int -> Provenance) -> Int -> Provenance
forall a b. (a -> b) -> a -> b
$ [Located (Pat GhcTc)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatCompat GhcTc]
[Located (Pat GhcTc)]
ps) PatCompat GhcTc
Located (Pat GhcTc)
p


------------------------------------------------------------------------------
-- | Construct a hypothesis for a single pattern, including building
-- sub-hypotheses for constructor pattern matches.
buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov (PatCompat GhcTc -> Pat GhcTc
forall p. PatCompattable p => PatCompat p -> Pat p
fromPatCompat -> Pat GhcTc
p0) =
  case Pat GhcTc
p0 of
    VarPat  XVarPat GhcTc
_ GenLocated SrcSpan (IdP GhcTc)
x   -> Hypothesis CType -> State Int (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Hypothesis CType -> State Int (Hypothesis CType))
-> Hypothesis CType -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ Id -> Provenance -> Hypothesis CType
mkIdHypothesis (Located Id -> SrcSpanLess (Located Id)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc GenLocated SrcSpan (IdP GhcTc)
Located Id
x) Provenance
prov
    LazyPat XLazyPat GhcTc
_ PatCompat GhcTc
p   -> Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov PatCompat GhcTc
p
    AsPat   XAsPat GhcTc
_ GenLocated SrcSpan (IdP GhcTc)
x PatCompat GhcTc
p -> do
      Hypothesis CType
hy' <- Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov PatCompat GhcTc
p
      Hypothesis CType -> State Int (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Hypothesis CType -> State Int (Hypothesis CType))
-> Hypothesis CType -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ Id -> Provenance -> Hypothesis CType
mkIdHypothesis (Located Id -> SrcSpanLess (Located Id)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc GenLocated SrcSpan (IdP GhcTc)
Located Id
x) Provenance
prov Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Semigroup a => a -> a -> a
<> Hypothesis CType
hy'
    ParPat  XParPat GhcTc
_ PatCompat GhcTc
p   -> Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov PatCompat GhcTc
p
    BangPat XBangPat GhcTc
_ PatCompat GhcTc
p   -> Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov PatCompat GhcTc
p
    ViewPat XViewPat GhcTc
_ LHsExpr GhcTc
_ PatCompat GhcTc
p -> Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov PatCompat GhcTc
p
    -- Desugar lists into cons
    ListPat XListPat GhcTc
_ [] -> Hypothesis CType -> State Int (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Hypothesis CType
forall a. Monoid a => a
mempty
    ListPat x :: XListPat GhcTc
x@(ListPatTc ty _) (PatCompat GhcTc
p : [PatCompat GhcTc]
ps) ->
      Provenance
-> ConLike
-> [Type]
-> [(Int, PatCompat GhcTc)]
-> State Int (Hypothesis CType)
mkDerivedConHypothesis Provenance
prov (DataCon -> ConLike
RealDataCon DataCon
consDataCon) [Type
ty]
        [ (Int
0, PatCompat GhcTc
p)
        , (Int
1, Pat GhcTc -> PatCompat GhcTc
forall p. PatCompattable p => Pat p -> PatCompat p
toPatCompat (Pat GhcTc -> PatCompat GhcTc) -> Pat GhcTc -> PatCompat GhcTc
forall a b. (a -> b) -> a -> b
$ XListPat GhcTc -> [PatCompat GhcTc] -> Pat GhcTc
forall p. XListPat p -> [LPat p] -> Pat p
ListPat XListPat GhcTc
x [PatCompat GhcTc]
ps)
        ]
    -- Desugar tuples into an explicit constructor
    TuplePat XTuplePat GhcTc
tys [PatCompat GhcTc]
pats Boxity
boxity ->
      Provenance
-> ConLike
-> [Type]
-> [(Int, PatCompat GhcTc)]
-> State Int (Hypothesis CType)
mkDerivedConHypothesis
        Provenance
prov
        (DataCon -> ConLike
RealDataCon (DataCon -> ConLike) -> DataCon -> ConLike
forall a b. (a -> b) -> a -> b
$ Boxity -> Int -> DataCon
tupleDataCon Boxity
boxity (Int -> DataCon) -> Int -> DataCon
forall a b. (a -> b) -> a -> b
$ [Located (Pat GhcTc)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PatCompat GhcTc]
[Located (Pat GhcTc)]
pats)
        [Type]
XTuplePat GhcTc
tys
          ([(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType))
-> [(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ [Int] -> [Located (Pat GhcTc)] -> [(Int, Located (Pat GhcTc))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0.. ] [PatCompat GhcTc]
[Located (Pat GhcTc)]
pats
    ConPatOut (L SrcSpan
_ ConLike
con) [Type]
args [Id]
_ [Id]
_ TcEvBinds
_ HsConPatDetails GhcTc
f HsWrapper
_ ->
      case HsConPatDetails GhcTc
f of
        PrefixCon [PatCompat GhcTc]
l_pgt ->
          Provenance
-> ConLike
-> [Type]
-> [(Int, PatCompat GhcTc)]
-> State Int (Hypothesis CType)
mkDerivedConHypothesis Provenance
prov ConLike
con [Type]
args ([(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType))
-> [(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ [Int] -> [Located (Pat GhcTc)] -> [(Int, Located (Pat GhcTc))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [PatCompat GhcTc]
[Located (Pat GhcTc)]
l_pgt
        InfixCon PatCompat GhcTc
pgt PatCompat GhcTc
pgt5 ->
          Provenance
-> ConLike
-> [Type]
-> [(Int, PatCompat GhcTc)]
-> State Int (Hypothesis CType)
mkDerivedConHypothesis Provenance
prov ConLike
con [Type]
args ([(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType))
-> [(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ [Int] -> [Located (Pat GhcTc)] -> [(Int, Located (Pat GhcTc))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [PatCompat GhcTc
Located (Pat GhcTc)
pgt, PatCompat GhcTc
Located (Pat GhcTc)
pgt5]
        RecCon HsRecFields GhcTc (PatCompat GhcTc)
r ->
          Provenance
-> ConLike
-> [Type]
-> HsRecFields GhcTc (PatCompat GhcTc)
-> State Int (Hypothesis CType)
mkDerivedRecordHypothesis Provenance
prov ConLike
con [Type]
args HsRecFields GhcTc (PatCompat GhcTc)
r
#if __GLASGOW_HASKELL__ >= 808
    SigPat  XSigPat GhcTc
_ PatCompat GhcTc
p LHsSigWcType (NoGhcTc GhcTc)
_ -> Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov PatCompat GhcTc
p
#endif
#if __GLASGOW_HASKELL__ == 808
    XPat   p      -> buildPatHy prov $ unLoc p
#endif
    Pat GhcTc
_             -> Hypothesis CType -> State Int (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Hypothesis CType
forall a. Monoid a => a
mempty


------------------------------------------------------------------------------
-- | Like 'mkDerivedConHypothesis', but for record patterns.
mkDerivedRecordHypothesis
    :: Provenance
    -> ConLike  -- ^ Destructing constructor
    -> [Type]   -- ^ Applied type variables
    -> HsRecFields GhcTc (PatCompat GhcTc)
    -> State Int (Hypothesis CType)
mkDerivedRecordHypothesis :: Provenance
-> ConLike
-> [Type]
-> HsRecFields GhcTc (PatCompat GhcTc)
-> State Int (Hypothesis CType)
mkDerivedRecordHypothesis Provenance
prov ConLike
dc [Type]
args (HsRecFields ((LHsRecField GhcTc (Located (Pat GhcTc))
 -> HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc)))
-> [LHsRecField GhcTc (Located (Pat GhcTc))]
-> [HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsRecField GhcTc (Located (Pat GhcTc))
-> HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc))
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc -> [HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc))]
fs) Maybe (Located Int)
_)
  | Just [(OccName, CType)]
rec_fields <- ConLike -> Maybe [(OccName, CType)]
getRecordFields ConLike
dc
  = do
    let field_lookup :: Map FastString Int
field_lookup = [(FastString, Int)] -> Map FastString Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(FastString, Int)] -> Map FastString Int)
-> [(FastString, Int)] -> Map FastString Int
forall a b. (a -> b) -> a -> b
$ [FastString] -> [Int] -> [(FastString, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((OccName, CType) -> FastString)
-> [(OccName, CType)] -> [FastString]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName -> FastString
occNameFS (OccName -> FastString)
-> ((OccName, CType) -> OccName) -> (OccName, CType) -> FastString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst) [(OccName, CType)]
rec_fields) [Int
0..]
    Provenance
-> ConLike
-> [Type]
-> [(Int, PatCompat GhcTc)]
-> State Int (Hypothesis CType)
mkDerivedConHypothesis Provenance
prov ConLike
dc [Type]
args ([(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType))
-> [(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ [HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc))]
fs [HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc))]
-> (HsRecField' (FieldOcc GhcTc) (Located (Pat GhcTc))
    -> (Int, Located (Pat GhcTc)))
-> [(Int, Located (Pat GhcTc))]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(HsRecField (L SrcSpan
_ FieldOcc GhcTc
rec_occ) Located (Pat GhcTc)
p Bool
_) ->
      ( Map FastString Int
field_lookup Map FastString Int -> FastString -> Int
forall k a. Ord k => Map k a -> k -> a
M.! (OccName -> FastString
occNameFS (OccName -> FastString) -> OccName -> FastString
forall a b. (a -> b) -> a -> b
$ RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName (RdrName -> OccName) -> RdrName -> OccName
forall a b. (a -> b) -> a -> b
$ Located RdrName -> SrcSpanLess (Located RdrName)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc (Located RdrName -> SrcSpanLess (Located RdrName))
-> Located RdrName -> SrcSpanLess (Located RdrName)
forall a b. (a -> b) -> a -> b
$ FieldOcc GhcTc -> Located RdrName
forall pass. FieldOcc pass -> Located RdrName
rdrNameFieldOcc FieldOcc GhcTc
rec_occ)
      , Located (Pat GhcTc)
p
      )
mkDerivedRecordHypothesis Provenance
_ ConLike
_ [Type]
_ HsRecFields GhcTc (PatCompat GhcTc)
_ =
  String -> State Int (Hypothesis CType)
forall a. HasCallStack => String -> a
error String
"impossible! using record pattern on something that isn't a record"


------------------------------------------------------------------------------
-- | Construct a fake variable name. Used to track the provenance of top-level
-- pattern matches which otherwise wouldn't have anything to attach their
-- 'TopLevelArgPrv' to.
mkFakeVar :: State Int OccName
mkFakeVar :: State Int OccName
mkFakeVar = do
  Int
i <- StateT Int Identity Int
forall s (m :: * -> *). MonadState s m => m s
get
  Int -> StateT Int Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> StateT Int Identity ()) -> Int -> StateT Int Identity ()
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  OccName -> State Int OccName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OccName -> State Int OccName) -> OccName -> State Int OccName
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc (String -> OccName) -> String -> OccName
forall a b. (a -> b) -> a -> b
$ String
"_" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i


------------------------------------------------------------------------------
-- | Construct a fake varible to attach the current 'Provenance' to, and then
-- build a sub-hypothesis for the pattern match.
mkDerivedConHypothesis
    :: Provenance
    -> ConLike                   -- ^ Destructing constructor
    -> [Type]                    -- ^ Applied type variables
    -> [(Int, PatCompat GhcTc)]  -- ^ Patterns, and their order in the data con
    -> State Int (Hypothesis CType)
mkDerivedConHypothesis :: Provenance
-> ConLike
-> [Type]
-> [(Int, PatCompat GhcTc)]
-> State Int (Hypothesis CType)
mkDerivedConHypothesis Provenance
prov ConLike
dc [Type]
args [(Int, PatCompat GhcTc)]
ps = do
  OccName
var <- State Int OccName
mkFakeVar
  Hypothesis CType
hy' <- ([Hypothesis CType] -> Hypothesis CType)
-> StateT Int Identity [Hypothesis CType]
-> State Int (Hypothesis CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Hypothesis CType] -> Hypothesis CType
forall a. Monoid a => [a] -> a
mconcat (StateT Int Identity [Hypothesis CType]
 -> State Int (Hypothesis CType))
-> StateT Int Identity [Hypothesis CType]
-> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$
    [(Int, Located (Pat GhcTc))]
-> ((Int, Located (Pat GhcTc)) -> State Int (Hypothesis CType))
-> StateT Int Identity [Hypothesis CType]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Int, PatCompat GhcTc)]
[(Int, Located (Pat GhcTc))]
ps (((Int, Located (Pat GhcTc)) -> State Int (Hypothesis CType))
 -> StateT Int Identity [Hypothesis CType])
-> ((Int, Located (Pat GhcTc)) -> State Int (Hypothesis CType))
-> StateT Int Identity [Hypothesis CType]
forall a b. (a -> b) -> a -> b
$ \(Int
ix, Located (Pat GhcTc)
p) -> do
      let prov' :: Provenance
prov' = PatVal -> Provenance
PatternMatchPrv
               (PatVal -> Provenance) -> PatVal -> Provenance
forall a b. (a -> b) -> a -> b
$ Maybe OccName -> Set OccName -> Uniquely ConLike -> Int -> PatVal
PatVal (OccName -> Maybe OccName
forall a. a -> Maybe a
Just OccName
var)
                        (OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
var Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Provenance -> Set OccName
provAncestryOf Provenance
prov)
                        (ConLike -> Uniquely ConLike
forall a. a -> Uniquely a
Uniquely ConLike
dc)
                        Int
ix
      Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
buildPatHy Provenance
prov' PatCompat GhcTc
Located (Pat GhcTc)
p
  Hypothesis CType -> State Int (Hypothesis CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    (Hypothesis CType -> State Int (Hypothesis CType))
-> Hypothesis CType -> State Int (Hypothesis CType)
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Monoid a => a -> a -> a
mappend Hypothesis CType
hy'
    (Hypothesis CType -> Hypothesis CType)
-> Hypothesis CType -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis
    ([HyInfo CType] -> Hypothesis CType)
-> [HyInfo CType] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> [HyInfo CType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    (HyInfo CType -> [HyInfo CType]) -> HyInfo CType -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
var (DisallowReason -> Provenance -> Provenance
DisallowedPrv DisallowReason
AlreadyDestructed Provenance
prov)
    (CType -> HyInfo CType) -> CType -> HyInfo CType
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType
    -- TODO(sandy): This is the completely wrong type, but we don't have a good
    -- way to get the real one. It's probably OK though, since we're generating
    -- this term with a disallowed provenance, and it doesn't actually exist
    -- anyway.
    (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ ConLike -> [Type] -> Type
conLikeResTy ConLike
dc [Type]
args


------------------------------------------------------------------------------
-- | Build a 'Hypothesis' given an 'Id'.
mkIdHypothesis :: Id -> Provenance -> Hypothesis CType
mkIdHypothesis :: Id -> Provenance -> Hypothesis CType
mkIdHypothesis (Id -> (OccName, CType)
splitId -> (OccName
name, CType
ty)) Provenance
prov =
  [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo CType] -> Hypothesis CType)
-> [HyInfo CType] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> [HyInfo CType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HyInfo CType -> [HyInfo CType]) -> HyInfo CType -> [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
name Provenance
prov CType
ty


------------------------------------------------------------------------------
-- | Is this hole immediately to the right of an equals sign?
isRhsHole :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Bool
isRhsHole :: Tracked age RealSrcSpan -> Tracked age (LHsBinds GhcTc) -> Bool
isRhsHole (Tracked age RealSrcSpan -> RealSrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> RealSrcSpan
rss) (Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc
forall (age :: Age) a. Tracked age a -> a
unTrack -> 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 RealSrcSpan
span) HsExpr GhcTc
_) -> RealSrcSpan -> RealSrcSpan -> Bool
containsSpan RealSrcSpan
rss RealSrcSpan
span
      Match GhcTc (LHsExpr GhcTc)
_                                        -> Bool
False
    ) LHsBinds GhcTc
tcs


ufmSeverity :: UserFacingMessage -> MessageType
ufmSeverity :: UserFacingMessage -> MessageType
ufmSeverity UserFacingMessage
NotEnoughGas            = MessageType
MtInfo
ufmSeverity UserFacingMessage
TacticErrors            = MessageType
MtError
ufmSeverity UserFacingMessage
TimedOut                = MessageType
MtInfo
ufmSeverity UserFacingMessage
NothingToDo             = MessageType
MtInfo
ufmSeverity (InfrastructureError Text
_) = MessageType
MtError


mkShowMessageParams :: UserFacingMessage -> ShowMessageParams
mkShowMessageParams :: UserFacingMessage -> ShowMessageParams
mkShowMessageParams UserFacingMessage
ufm = MessageType -> Text -> ShowMessageParams
ShowMessageParams (UserFacingMessage -> MessageType
ufmSeverity UserFacingMessage
ufm) (Text -> ShowMessageParams) -> Text -> ShowMessageParams
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ UserFacingMessage -> String
forall a. Show a => a -> String
show UserFacingMessage
ufm


showLspMessage :: MonadLsp cfg m => ShowMessageParams -> m ()
showLspMessage :: ShowMessageParams -> m ()
showLspMessage = SServerMethod 'WindowShowMessage
-> MessageParams 'WindowShowMessage -> m ()
forall (m :: Method 'FromServer 'Notification) (f :: * -> *)
       config.
MonadLsp config f =>
SServerMethod m -> MessageParams m -> f ()
sendNotification SServerMethod 'WindowShowMessage
SWindowShowMessage


-- This rule only exists for generating file diagnostics
-- so the RuleResult is empty
data WriteDiagnostics = WriteDiagnostics
    deriving (WriteDiagnostics -> WriteDiagnostics -> Bool
(WriteDiagnostics -> WriteDiagnostics -> Bool)
-> (WriteDiagnostics -> WriteDiagnostics -> Bool)
-> Eq WriteDiagnostics
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WriteDiagnostics -> WriteDiagnostics -> Bool
$c/= :: WriteDiagnostics -> WriteDiagnostics -> Bool
== :: WriteDiagnostics -> WriteDiagnostics -> Bool
$c== :: WriteDiagnostics -> WriteDiagnostics -> Bool
Eq, Int -> WriteDiagnostics -> String -> String
[WriteDiagnostics] -> String -> String
WriteDiagnostics -> String
(Int -> WriteDiagnostics -> String -> String)
-> (WriteDiagnostics -> String)
-> ([WriteDiagnostics] -> String -> String)
-> Show WriteDiagnostics
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [WriteDiagnostics] -> String -> String
$cshowList :: [WriteDiagnostics] -> String -> String
show :: WriteDiagnostics -> String
$cshow :: WriteDiagnostics -> String
showsPrec :: Int -> WriteDiagnostics -> String -> String
$cshowsPrec :: Int -> WriteDiagnostics -> String -> String
Show, Typeable, (forall x. WriteDiagnostics -> Rep WriteDiagnostics x)
-> (forall x. Rep WriteDiagnostics x -> WriteDiagnostics)
-> Generic WriteDiagnostics
forall x. Rep WriteDiagnostics x -> WriteDiagnostics
forall x. WriteDiagnostics -> Rep WriteDiagnostics x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep WriteDiagnostics x -> WriteDiagnostics
$cfrom :: forall x. WriteDiagnostics -> Rep WriteDiagnostics x
Generic)

instance Hashable WriteDiagnostics
instance NFData   WriteDiagnostics
instance Binary   WriteDiagnostics

type instance RuleResult WriteDiagnostics = ()

wingmanRules :: PluginId -> Rules ()
wingmanRules :: PluginId -> Rules ()
wingmanRules PluginId
plId = do
  (WriteDiagnostics -> NormalizedFilePath -> Action (IdeResult ()))
-> Rules ()
forall k v.
IdeRule k v =>
(k -> NormalizedFilePath -> Action (IdeResult v)) -> Rules ()
define ((WriteDiagnostics -> NormalizedFilePath -> Action (IdeResult ()))
 -> Rules ())
-> (WriteDiagnostics
    -> NormalizedFilePath -> Action (IdeResult ()))
-> Rules ()
forall a b. (a -> b) -> a -> b
$ \WriteDiagnostics
WriteDiagnostics NormalizedFilePath
nfp ->
    KeyNameProxy "hole_severity"
-> PluginId
-> Properties
     '[ 'PropertyKey
          "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
        'PropertyKey "max_use_ctor_actions" 'TInteger,
        'PropertyKey "timeout_duration" 'TInteger,
        'PropertyKey "auto_gas" 'TInteger,
        'PropertyKey "proofstate_styling" 'TBoolean]
-> Action (ToHsType ('TEnum (Maybe DiagnosticSeverity)))
forall (s :: Symbol) (k :: PropertyKey) (t :: PropertyType)
       (r :: [PropertyKey]).
HasProperty s k t r =>
KeyNameProxy s -> PluginId -> Properties r -> Action (ToHsType t)
usePropertyAction IsLabel "hole_severity" (KeyNameProxy "hole_severity")
KeyNameProxy "hole_severity"
#hole_severity PluginId
plId Properties
  '[ 'PropertyKey
       "hole_severity" ('TEnum (Maybe DiagnosticSeverity)),
     'PropertyKey "max_use_ctor_actions" 'TInteger,
     'PropertyKey "timeout_duration" 'TInteger,
     'PropertyKey "auto_gas" 'TInteger,
     'PropertyKey "proofstate_styling" 'TBoolean]
properties Action (Maybe DiagnosticSeverity)
-> (Maybe DiagnosticSeverity -> Action (IdeResult ()))
-> Action (IdeResult ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe DiagnosticSeverity
Nothing -> IdeResult () -> Action (IdeResult ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(NormalizedFilePath, ShowDiagnostic, Diagnostic)]
forall a. Monoid a => a
mempty, () -> Maybe ()
forall a. a -> Maybe a
Just ())
      Just DiagnosticSeverity
severity ->
        GetParsedModule
-> NormalizedFilePath -> Action (Maybe ParsedModule)
forall k v.
IdeRule k v =>
k -> NormalizedFilePath -> Action (Maybe v)
use GetParsedModule
GetParsedModule NormalizedFilePath
nfp Action (Maybe ParsedModule)
-> (Maybe ParsedModule -> Action (IdeResult ()))
-> Action (IdeResult ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Maybe ParsedModule
Nothing ->
            IdeResult () -> Action (IdeResult ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Maybe ()
forall a. Maybe a
Nothing)
          Just ParsedModule
pm -> do
            let holes :: [Range]
                holes :: [Range]
holes =
                  ([Range] -> [Range] -> [Range])
-> GenericQ [Range] -> GenericQ [Range]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [Range] -> [Range] -> [Range]
forall a. Semigroup a => a -> a -> a
(<>)
                    ([Range]
-> (GenLocated SrcSpan (HsExpr GhcPs) -> [Range]) -> a -> [Range]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [Range]
forall a. Monoid a => a
mempty ((GenLocated SrcSpan (HsExpr GhcPs) -> [Range]) -> a -> [Range])
-> (GenLocated SrcSpan (HsExpr GhcPs) -> [Range]) -> a -> [Range]
forall a b. (a -> b) -> a -> b
$ \case
                      L SrcSpan
span (HsVar XVar GhcPs
_ (L SrcSpan
_ IdP GhcPs
name))
                        | OccName -> Bool
isHole (RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName IdP GhcPs
RdrName
name) ->
                            Maybe Range -> [Range]
forall a. Maybe a -> [a]
maybeToList (Maybe Range -> [Range]) -> Maybe Range -> [Range]
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Maybe Range
srcSpanToRange SrcSpan
span
                      L SrcSpan
span (HsUnboundVar XUnboundVar GhcPs
_ (TrueExprHole OccName
occ))
                        | OccName -> Bool
isHole OccName
occ ->
                            Maybe Range -> [Range]
forall a. Maybe a -> [a]
maybeToList (Maybe Range -> [Range]) -> Maybe Range -> [Range]
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Maybe Range
srcSpanToRange SrcSpan
span
#if __GLASGOW_HASKELL__ <= 808
                      L span (EWildPat _) ->
                        maybeToList $ srcSpanToRange span
#endif
                      (GenLocated SrcSpan (HsExpr GhcPs)
_ :: LHsExpr GhcPs) -> [Range]
forall a. Monoid a => a
mempty
                    ) (ParsedSource -> [Range]) -> ParsedSource -> [Range]
forall a b. (a -> b) -> a -> b
$ ParsedModule -> ParsedSource
pm_parsed_source ParsedModule
pm
            IdeResult () -> Action (IdeResult ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              ( (Range -> (NormalizedFilePath, ShowDiagnostic, Diagnostic))
-> [Range] -> [(NormalizedFilePath, ShowDiagnostic, Diagnostic)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Range
r -> (NormalizedFilePath
nfp, ShowDiagnostic
ShowDiag, DiagnosticSeverity -> Range -> Diagnostic
mkDiagnostic DiagnosticSeverity
severity Range
r)) [Range]
holes
              , () -> Maybe ()
forall a. a -> Maybe a
Just ()
              )

  Action () -> Rules ()
forall a. Action a -> Rules ()
action (Action () -> Rules ()) -> Action () -> Rules ()
forall a b. (a -> b) -> a -> b
$ do
    HashMap NormalizedFilePath FileOfInterestStatus
files <- Action (HashMap NormalizedFilePath FileOfInterestStatus)
getFilesOfInterestUntracked
    Action [Maybe ()] -> Action ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Action [Maybe ()] -> Action ()) -> Action [Maybe ()] -> Action ()
forall a b. (a -> b) -> a -> b
$ WriteDiagnostics -> [NormalizedFilePath] -> Action [Maybe ()]
forall k v.
IdeRule k v =>
k -> [NormalizedFilePath] -> Action [Maybe v]
uses WriteDiagnostics
WriteDiagnostics ([NormalizedFilePath] -> Action [Maybe ()])
-> [NormalizedFilePath] -> Action [Maybe ()]
forall a b. (a -> b) -> a -> b
$ HashMap NormalizedFilePath FileOfInterestStatus
-> [NormalizedFilePath]
forall k v. HashMap k v -> [k]
Map.keys HashMap NormalizedFilePath FileOfInterestStatus
files


mkDiagnostic :: DiagnosticSeverity -> Range -> Diagnostic
mkDiagnostic :: DiagnosticSeverity -> Range -> Diagnostic
mkDiagnostic DiagnosticSeverity
severity Range
r =
  Range
-> Maybe DiagnosticSeverity
-> Maybe (Int |? Text)
-> Maybe Text
-> Text
-> Maybe (List DiagnosticTag)
-> Maybe (List DiagnosticRelatedInformation)
-> Diagnostic
Diagnostic Range
r
    (DiagnosticSeverity -> Maybe DiagnosticSeverity
forall a. a -> Maybe a
Just DiagnosticSeverity
severity)
    ((Int |? Text) -> Maybe (Int |? Text)
forall a. a -> Maybe a
Just ((Int |? Text) -> Maybe (Int |? Text))
-> (Int |? Text) -> Maybe (Int |? Text)
forall a b. (a -> b) -> a -> b
$ Text -> Int |? Text
forall a b. b -> a |? b
InR Text
"hole")
    (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"wingman")
    Text
"Hole"
    (List DiagnosticTag -> Maybe (List DiagnosticTag)
forall a. a -> Maybe a
Just (List DiagnosticTag -> Maybe (List DiagnosticTag))
-> List DiagnosticTag -> Maybe (List DiagnosticTag)
forall a b. (a -> b) -> a -> b
$ [DiagnosticTag] -> List DiagnosticTag
forall a. [a] -> List a
List [DiagnosticTag
DtUnnecessary])
    Maybe (List DiagnosticRelatedInformation)
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Transform a 'Graft' over the AST into a 'WorkspaceEdit'.
mkWorkspaceEdits
    :: DynFlags
    -> ClientCapabilities
    -> Uri
    -> Annotated ParsedSource
    -> Graft (Either String) ParsedSource
    -> Either UserFacingMessage WorkspaceEdit
mkWorkspaceEdits :: DynFlags
-> ClientCapabilities
-> Uri
-> Annotated ParsedSource
-> Graft (Either String) ParsedSource
-> Either UserFacingMessage WorkspaceEdit
mkWorkspaceEdits DynFlags
dflags ClientCapabilities
ccs Uri
uri Annotated ParsedSource
pm Graft (Either String) ParsedSource
g = do
  let pm' :: Annotated ParsedSource
pm' = Identity (Annotated ParsedSource) -> Annotated ParsedSource
forall a. Identity a -> a
runIdentity (Identity (Annotated ParsedSource) -> Annotated ParsedSource)
-> Identity (Annotated ParsedSource) -> Annotated ParsedSource
forall a b. (a -> b) -> a -> b
$ Annotated ParsedSource
-> (ParsedSource -> TransformT Identity ParsedSource)
-> Identity (Annotated ParsedSource)
forall (m :: * -> *) ast1 ast2.
Monad m =>
Annotated ast1 -> (ast1 -> TransformT m ast2) -> m (Annotated ast2)
transformA Annotated ParsedSource
pm ParsedSource -> TransformT Identity ParsedSource
forall a. Data a => a -> Transform a
annotateMetaprograms
  let response :: Either String WorkspaceEdit
response = DynFlags
-> ClientCapabilities
-> Uri
-> Graft (Either String) ParsedSource
-> Annotated ParsedSource
-> Either String WorkspaceEdit
transform DynFlags
dflags ClientCapabilities
ccs Uri
uri Graft (Either String) ParsedSource
g Annotated ParsedSource
pm'
   in (String -> UserFacingMessage)
-> Either String WorkspaceEdit
-> Either UserFacingMessage WorkspaceEdit
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Text -> UserFacingMessage
InfrastructureError (Text -> UserFacingMessage)
-> (String -> Text) -> String -> UserFacingMessage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack) Either String WorkspaceEdit
response


------------------------------------------------------------------------------
-- | Add ExactPrint annotations to every metaprogram in the source tree.
-- Usually the ExactPrint module can do this for us, but we've enabled
-- QuasiQuotes, so the round-trip print/parse journey will crash.
annotateMetaprograms :: Data a => a -> Transform a
annotateMetaprograms :: a -> Transform a
annotateMetaprograms = (forall a. Data a => a -> Transform a)
-> forall a. Data a => a -> Transform a
forall (m :: * -> *). Monad m => GenericM m -> GenericM m
everywhereM ((forall a. Data a => a -> Transform a)
 -> forall a. Data a => a -> Transform a)
-> (forall a. Data a => a -> Transform a)
-> forall a. Data a => a -> Transform a
forall a b. (a -> b) -> a -> b
$ (GenLocated SrcSpan (HsExpr GhcPs)
 -> TransformT Identity (GenLocated SrcSpan (HsExpr GhcPs)))
-> a -> TransformT Identity a
forall (m :: * -> *) a b.
(Monad m, Typeable a, Typeable b) =>
(b -> m b) -> a -> m a
mkM ((GenLocated SrcSpan (HsExpr GhcPs)
  -> TransformT Identity (GenLocated SrcSpan (HsExpr GhcPs)))
 -> a -> TransformT Identity a)
-> (GenLocated SrcSpan (HsExpr GhcPs)
    -> TransformT Identity (GenLocated SrcSpan (HsExpr GhcPs)))
-> a
-> TransformT Identity a
forall a b. (a -> b) -> a -> b
$ \case
  L SrcSpan
ss (WingmanMetaprogram FastString
mp) -> do
    let x :: GenLocated SrcSpan (HsExpr GhcPs)
x = SrcSpan -> HsExpr GhcPs -> GenLocated SrcSpan (HsExpr GhcPs)
forall l e. l -> e -> GenLocated l e
L SrcSpan
ss (HsExpr GhcPs -> GenLocated SrcSpan (HsExpr GhcPs))
-> HsExpr GhcPs -> GenLocated SrcSpan (HsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ FastString -> HsExpr GhcPs
MetaprogramSyntax FastString
mp
    let anns :: Anns
anns = [Comment] -> GenLocated SrcSpan (HsExpr GhcPs) -> Anns -> Anns
forall a. Annotate a => [Comment] -> Located a -> Anns -> Anns
addAnnotationsForPretty [] GenLocated SrcSpan (HsExpr GhcPs)
x Anns
forall a. Monoid a => a
mempty
    (Anns -> Anns) -> TransformT Identity ()
forall (m :: * -> *). Monad m => (Anns -> Anns) -> TransformT m ()
modifyAnnsT ((Anns -> Anns) -> TransformT Identity ())
-> (Anns -> Anns) -> TransformT Identity ()
forall a b. (a -> b) -> a -> b
$ Anns -> Anns -> Anns
forall a. Monoid a => a -> a -> a
mappend Anns
anns
    GenLocated SrcSpan (HsExpr GhcPs)
-> TransformT Identity (GenLocated SrcSpan (HsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenLocated SrcSpan (HsExpr GhcPs)
x
  (GenLocated SrcSpan (HsExpr GhcPs)
x :: LHsExpr GhcPs) -> GenLocated SrcSpan (HsExpr GhcPs)
-> TransformT Identity (GenLocated SrcSpan (HsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenLocated SrcSpan (HsExpr GhcPs)
x


------------------------------------------------------------------------------
-- | Find the source of a tactic metaprogram at the given span.
getMetaprogramAtSpan
    :: Tracked age SrcSpan
    -> Tracked age TcGblEnv
    -> Maybe T.Text
getMetaprogramAtSpan :: Tracked age SrcSpan -> Tracked age TcGblEnv -> Maybe Text
getMetaprogramAtSpan (Tracked age SrcSpan -> SrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> SrcSpan
ss)
  = ((SrcSpan, Text) -> Text) -> Maybe (SrcSpan, Text) -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcSpan, Text) -> Text
forall a b. (a, b) -> b
snd
  (Maybe (SrcSpan, Text) -> Maybe Text)
-> (Tracked age TcGblEnv -> Maybe (SrcSpan, Text))
-> Tracked age TcGblEnv
-> Maybe Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SrcSpan, Text)] -> Maybe (SrcSpan, Text)
forall a. [a] -> Maybe a
listToMaybe
  ([(SrcSpan, Text)] -> Maybe (SrcSpan, Text))
-> (Tracked age TcGblEnv -> [(SrcSpan, Text)])
-> Tracked age TcGblEnv
-> Maybe (SrcSpan, Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> GenericQ [(SrcSpan, Text)]
metaprogramQ SrcSpan
ss
  (LHsBinds GhcTc -> [(SrcSpan, Text)])
-> (Tracked age TcGblEnv -> LHsBinds GhcTc)
-> Tracked age TcGblEnv
-> [(SrcSpan, Text)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcGblEnv -> LHsBinds GhcTc
tcg_binds
  (TcGblEnv -> LHsBinds GhcTc)
-> (Tracked age TcGblEnv -> TcGblEnv)
-> Tracked age TcGblEnv
-> LHsBinds GhcTc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tracked age TcGblEnv -> TcGblEnv
forall (age :: Age) a. Tracked age a -> a
unTrack