hls-tactics-plugin-1.6.2.0: Wingman plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Wingman.LanguageServer

Synopsis

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 #

tcCommandName :: TacticCommand -> Text Source #

The name of the command for the LS.

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 #

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

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.

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

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

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.

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.

data WriteDiagnostics Source #

Constructors

WriteDiagnostics 

Instances

Instances details
Eq WriteDiagnostics Source # 
Instance details

Defined in Wingman.LanguageServer

Show WriteDiagnostics Source # 
Instance details

Defined in Wingman.LanguageServer

Generic WriteDiagnostics Source # 
Instance details

Defined in Wingman.LanguageServer

Associated Types

type Rep WriteDiagnostics :: Type -> Type #

Hashable WriteDiagnostics Source # 
Instance details

Defined in Wingman.LanguageServer

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

data GetMetaprograms Source #

Constructors

GetMetaprograms 

Instances

Instances details
Eq GetMetaprograms Source # 
Instance details

Defined in Wingman.LanguageServer

Show GetMetaprograms Source # 
Instance details

Defined in Wingman.LanguageServer

Generic GetMetaprograms Source # 
Instance details

Defined in Wingman.LanguageServer

Associated Types

type Rep GetMetaprograms :: Type -> Type #

Hashable GetMetaprograms Source # 
Instance details

Defined in Wingman.LanguageServer

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

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.