Safe Haskell	None
Language	Haskell2010

Wingman.LanguageServer

Synopsis

newtype Log = LogShake Log
tacticDesc :: Text -> Text
tcCommandName :: TacticCommand -> Text
runIde :: String -> String -> IdeState -> Action a -> IO a
runIdeAction :: String -> String -> IdeState -> IdeAction a -> IO a
runCurrentIde :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO (Tracked 'Current r)
runStaleIde :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO (TrackedStale r)
unsafeRunStaleIde :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO r
unsafeRunStaleIdeFast :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO 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]
getTacticConfig :: MonadLsp Config m => PluginId -> m Config
getIdeDynflags :: IdeState -> NormalizedFilePath -> MaybeT IO DynFlags
getAllMetaprograms :: Data a => a -> [String]
judgementForHole :: IdeState -> NormalizedFilePath -> Tracked 'Current Range -> Config -> MaybeT IO HoleJudgment
holeSortFor :: Maybe Text -> HoleSort
mkJudgementAndContext :: Config -> Type -> TrackedStale Bindings -> Tracked 'Current RealSrcSpan -> TrackedStale TcGblEnv -> HscEnv -> ExternalPackageState -> Maybe (Judgement, Context)
getAlreadyDestructed :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> Set OccName
getSpanAndTypeAtHole :: Tracked age Range -> Tracked age (HieASTs Type) -> Maybe (Tracked age RealSrcSpan, Type)
spliceProvenance :: Hypothesis a -> Hypothesis a -> Hypothesis a
getRhsPosVals :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Hypothesis CType
buildTopLevelHypothesis :: OccName -> [PatCompat GhcTc] -> State Int (Hypothesis CType)
buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
mkDerivedRecordHypothesis :: Provenance -> ConLike -> [Type] -> HsRecFields GhcTc (PatCompat GhcTc) -> State Int (Hypothesis CType)
mkFakeVar :: State Int OccName
mkDerivedConHypothesis :: Provenance -> ConLike -> [Type] -> [(Int, PatCompat GhcTc)] -> State Int (Hypothesis CType)
mkIdHypothesis :: Id -> Provenance -> Hypothesis CType
isRhsHoleWithoutWhere :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Bool
ufmSeverity :: UserFacingMessage -> MessageType
mkShowMessageParams :: UserFacingMessage -> ShowMessageParams
showLspMessage :: MonadLsp cfg m => ShowMessageParams -> m ()
data WriteDiagnostics = WriteDiagnostics
data GetMetaprograms = GetMetaprograms
wingmanRules :: Recorder (WithPriority Log) -> PluginId -> Rules ()
mkDiagnostic :: DiagnosticSeverity -> Range -> Diagnostic
mkWorkspaceEdits :: DynFlags -> ClientCapabilities -> Uri -> Annotated ParsedSource -> Graft (Either String) ParsedSource -> Either UserFacingMessage WorkspaceEdit
annotateMetaprograms :: Data a => a -> Transform a
getMetaprogramAtSpan :: Tracked age SrcSpan -> Tracked age TcGblEnv -> Maybe Text

Documentation

newtype Log Source #

Constructors

LogShake Log

Instances

Instances details

Show Log Source #
Instance details Defined in Wingman.LanguageServer Methods showsPrec :: Int -> Log -> ShowS # show :: Log -> String # showList :: [Log] -> ShowS #
Pretty Log Source #
Instance details Defined in Wingman.LanguageServer Methods pretty :: Log -> Doc ann # prettyList :: [Log] -> Doc ann #

tacticDesc :: Text -> Text Source #

tcCommandName :: TacticCommand -> Text Source #

The name of the command for the LS.

runIde :: String -> String -> IdeState -> Action a -> IO a Source #

runIdeAction :: String -> String -> IdeState -> IdeAction a -> IO a Source #

runCurrentIde :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO (Tracked 'Current r) Source #

runStaleIde :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO (TrackedStale r) Source #

unsafeRunStaleIde :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO r Source #

unsafeRunStaleIdeFast :: forall a r. (r ~ RuleResult a, Eq a, Hashable a, Show a, Typeable a, NFData a, Show r, Typeable r, NFData r) => String -> IdeState -> NormalizedFilePath -> a -> MaybeT IO r Source #

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] Source #

getTacticConfig :: MonadLsp Config m => PluginId -> m Config Source #

Get the the plugin config

getIdeDynflags :: IdeState -> NormalizedFilePath -> MaybeT IO DynFlags Source #

getAllMetaprograms :: Data a => a -> [String] Source #

judgementForHole :: IdeState -> NormalizedFilePath -> Tracked 'Current Range -> Config -> MaybeT IO HoleJudgment Source #

Find the last typechecked module, and find the most specific span, as well as the judgement at the given range.

holeSortFor :: Maybe Text -> HoleSort Source #

mkJudgementAndContext :: Config -> Type -> TrackedStale Bindings -> Tracked 'Current RealSrcSpan -> TrackedStale TcGblEnv -> HscEnv -> ExternalPackageState -> Maybe (Judgement, Context) Source #

getAlreadyDestructed :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> Set OccName Source #

Determine which bindings have already been destructed by the location of the hole.

getSpanAndTypeAtHole :: Tracked age Range -> Tracked age (HieASTs Type) -> Maybe (Tracked age RealSrcSpan, Type) Source #

spliceProvenance Source #

Arguments

:: Hypothesis a	Bindings to keep
-> Hypothesis a	Bindings to keep if they don't overlap with the first set
-> Hypothesis a

Combine two (possibly-overlapping) hypotheses; using the provenance from the first hypothesis if the bindings overlap.

getRhsPosVals :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Hypothesis CType Source #

Compute top-level position vals of a function

buildTopLevelHypothesis Source #

Arguments

:: OccName	Function name
-> [PatCompat GhcTc]
-> State Int (Hypothesis CType)

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.

buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType) Source #

Construct a hypothesis for a single pattern, including building sub-hypotheses for constructor pattern matches.

mkDerivedRecordHypothesis Source #

Arguments

:: Provenance
-> ConLike	Destructing constructor
-> [Type]	Applied type variables
-> HsRecFields GhcTc (PatCompat GhcTc)
-> State Int (Hypothesis CType)

Like mkDerivedConHypothesis, but for record patterns.

mkFakeVar :: State Int OccName Source #

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.

mkDerivedConHypothesis Source #

Arguments

:: Provenance
-> ConLike	Destructing constructor
-> [Type]	Applied type variables
-> [(Int, PatCompat GhcTc)]	Patterns, and their order in the data con
-> State Int (Hypothesis CType)

Construct a fake varible to attach the current Provenance to, and then build a sub-hypothesis for the pattern match.

mkIdHypothesis :: Id -> Provenance -> Hypothesis CType Source #

Build a Hypothesis given an Id.

isRhsHoleWithoutWhere :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Bool Source #

Is this hole immediately to the right of an equals sign --- and is there no where clause attached to it?

It's important that there is no where clause because otherwise it gets clobbered. See #2183 for an example.

This isn't a perfect check, and produces some ugly code. But it's much much better than the alternative, which is to destructively modify the user's AST.

ufmSeverity :: UserFacingMessage -> MessageType Source #

mkShowMessageParams :: UserFacingMessage -> ShowMessageParams Source #

showLspMessage :: MonadLsp cfg m => ShowMessageParams -> m () Source #

data WriteDiagnostics Source #

Constructors

WriteDiagnostics

Instances

Instances details

Eq WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer Methods (==) :: WriteDiagnostics -> WriteDiagnostics -> Bool # (/=) :: WriteDiagnostics -> WriteDiagnostics -> Bool #
Show WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer Methods showsPrec :: Int -> WriteDiagnostics -> ShowS # show :: WriteDiagnostics -> String # showList :: [WriteDiagnostics] -> ShowS #
Generic WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer Associated Types type Rep WriteDiagnostics :: Type -> Type # Methods from :: WriteDiagnostics -> Rep WriteDiagnostics x # to :: Rep WriteDiagnostics x -> WriteDiagnostics #
Hashable WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer Methods hashWithSalt :: Int -> WriteDiagnostics -> Int # hash :: WriteDiagnostics -> Int #
NFData WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer Methods rnf :: WriteDiagnostics -> () #
type Rep WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer type Rep WriteDiagnostics = D1 ('MetaData "WriteDiagnostics" "Wingman.LanguageServer" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) (C1 ('MetaCons "WriteDiagnostics" 'PrefixI 'False) (U1 :: Type -> Type))
type RuleResult WriteDiagnostics Source #
Instance details Defined in Wingman.LanguageServer type RuleResult WriteDiagnostics = ()

data GetMetaprograms Source #

Constructors

GetMetaprograms

Instances

Instances details

Eq GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer Methods (==) :: GetMetaprograms -> GetMetaprograms -> Bool # (/=) :: GetMetaprograms -> GetMetaprograms -> Bool #
Show GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer Methods showsPrec :: Int -> GetMetaprograms -> ShowS # show :: GetMetaprograms -> String # showList :: [GetMetaprograms] -> ShowS #
Generic GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer Associated Types type Rep GetMetaprograms :: Type -> Type # Methods from :: GetMetaprograms -> Rep GetMetaprograms x # to :: Rep GetMetaprograms x -> GetMetaprograms #
Hashable GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer Methods hashWithSalt :: Int -> GetMetaprograms -> Int # hash :: GetMetaprograms -> Int #
NFData GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer Methods rnf :: GetMetaprograms -> () #
type Rep GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer type Rep GetMetaprograms = D1 ('MetaData "GetMetaprograms" "Wingman.LanguageServer" "hls-tactics-plugin-1.6.2.0-F0S9kfzWGRh6ZnCEvC7DkD" 'False) (C1 ('MetaCons "GetMetaprograms" 'PrefixI 'False) (U1 :: Type -> Type))
type RuleResult GetMetaprograms Source #
Instance details Defined in Wingman.LanguageServer type RuleResult GetMetaprograms = [(Tracked 'Current RealSrcSpan, Text)]

wingmanRules :: Recorder (WithPriority Log) -> PluginId -> Rules () Source #

mkDiagnostic :: DiagnosticSeverity -> Range -> Diagnostic Source #

mkWorkspaceEdits :: DynFlags -> ClientCapabilities -> Uri -> Annotated ParsedSource -> Graft (Either String) ParsedSource -> Either UserFacingMessage WorkspaceEdit Source #

Transform a Graft over the AST into a WorkspaceEdit.

annotateMetaprograms :: Data a => a -> Transform a Source #

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.

getMetaprogramAtSpan :: Tracked age SrcSpan -> Tracked age TcGblEnv -> Maybe Text Source #

Find the source of a tactic metaprogram at the given span.