Wingman.LanguageServer

Documentation

tacticDesc :: Text -> Text

tcCommandName :: TacticCommand -> Text

The name of the command for the LS.

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

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)

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)

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

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

Get the the plugin config

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

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

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

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

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

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

getSpanAndTypeAtHole :: Tracked age Range -> Tracked age (HieASTs b) -> Maybe (Tracked age RealSrcSpan, b)

spliceProvenance

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

Compute top-level position vals of a function

buildTopLevelHypothesis

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)

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

mkDerivedRecordHypothesis

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

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

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

Build a Hypothesis given an Id.

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

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

mkShowMessageParams :: UserFacingMessage -> ShowMessageParams

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

data WriteDiagnostics

Constructors

WriteDiagnostics

Instances

Eq WriteDiagnostics

Defined in Wingman.LanguageServer

Methods

(==) :: WriteDiagnostics -> WriteDiagnostics -> Bool

(/=) :: WriteDiagnostics -> WriteDiagnostics -> Bool

Show WriteDiagnostics

Defined in Wingman.LanguageServer

Methods

showsPrec :: Int -> WriteDiagnostics -> ShowS

show :: WriteDiagnostics -> String

showList :: [WriteDiagnostics] -> ShowS

Generic WriteDiagnostics

Defined in Wingman.LanguageServer

Associated Types

type Rep WriteDiagnostics :: Type -> Type

Methods

from :: WriteDiagnostics -> Rep WriteDiagnostics x

to :: Rep WriteDiagnostics x -> WriteDiagnostics

Hashable WriteDiagnostics

Defined in Wingman.LanguageServer

Methods

hashWithSalt :: Int -> WriteDiagnostics -> Int

hash :: WriteDiagnostics -> Int

Binary WriteDiagnostics

Defined in Wingman.LanguageServer

Methods

put :: WriteDiagnostics -> Put

get :: Get WriteDiagnostics

putList :: [WriteDiagnostics] -> Put

NFData WriteDiagnostics

Defined in Wingman.LanguageServer

Methods

rnf :: WriteDiagnostics -> ()

type Rep WriteDiagnostics

Defined in Wingman.LanguageServer

type Rep WriteDiagnostics = D1 ('MetaData "WriteDiagnostics" "Wingman.LanguageServer" "hls-tactics-plugin-1.4.0.0-CDY1FtnQAdCF6qnNiOOrMd" 'False) (C1 ('MetaCons "WriteDiagnostics" 'PrefixI 'False) (U1 :: Type -> Type))

type RuleResult WriteDiagnostics

Defined in Wingman.LanguageServer

type RuleResult WriteDiagnostics = ()

wingmanRules :: PluginId -> Rules ()

mkDiagnostic :: DiagnosticSeverity -> Range -> Diagnostic

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

Transform a Graft over the AST into a WorkspaceEdit.

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

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

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