Wingman.LanguageServer.TacticProviders

Documentation

commandProvider :: TacticCommand -> TacticProvider

Mapping from tactic commands to their contextual providers. See provide, filterGoalType and filterBindingType for the nitty gritty.

commandTactic :: TacticCommand -> Text -> TacticsM ()

A mapping from tactic commands to actual tactics for refinery.

tcCommandId :: TacticCommand -> CommandId

Construct a CommandId

data TacticParams

Constructors

TacticParams

Fields

• tp_file :: Uri

  Uri of the file to fill the hole in

• tp_range :: Tracked 'Current Range

  The range of the hole

• tp_var_name :: Text

Instances

Eq TacticParams

Defined in Wingman.LanguageServer.TacticProviders

Methods

(==) :: TacticParams -> TacticParams -> Bool

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

Show TacticParams

Defined in Wingman.LanguageServer.TacticProviders

Methods

showsPrec :: Int -> TacticParams -> ShowS

show :: TacticParams -> String

showList :: [TacticParams] -> ShowS

Generic TacticParams

Defined in Wingman.LanguageServer.TacticProviders

Associated Types

type Rep TacticParams :: Type -> Type

Methods

from :: TacticParams -> Rep TacticParams x

to :: Rep TacticParams x -> TacticParams

ToJSON TacticParams

Defined in Wingman.LanguageServer.TacticProviders

Methods

toJSON :: TacticParams -> Value

toEncoding :: TacticParams -> Encoding

toJSONList :: [TacticParams] -> Value

toEncodingList :: [TacticParams] -> Encoding

FromJSON TacticParams

Defined in Wingman.LanguageServer.TacticProviders

Methods

parseJSON :: Value -> Parser TacticParams

parseJSONList :: Value -> Parser [TacticParams]

type Rep TacticParams

Defined in Wingman.LanguageServer.TacticProviders

type Rep TacticParams = D1 ('MetaData "TacticParams" "Wingman.LanguageServer.TacticProviders" "hls-tactics-plugin-1.3.0.0-E5QWF1lCxNYDpSB9okEqox" 'False) (C1 ('MetaCons "TacticParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "tp_file") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Uri) :*: (S1 ('MetaSel ('Just "tp_range") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Tracked 'Current Range)) :*: S1 ('MetaSel ('Just "tp_var_name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))))

data TacticProviderData

Constructors

TacticProviderData

Fields

• tpd_dflags :: DynFlags
• tpd_config :: Config
• tpd_plid :: PluginId
• tpd_uri :: Uri
• tpd_range :: Tracked 'Current Range
• tpd_jdg :: Judgement
• tpd_hole_sort :: HoleSort

useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a

Lift a function over HyInfos to one that takes an OccName and tries to look it up in the hypothesis.