Safe Haskell	None
Language	Haskell2010

Wingman.LanguageServer.TacticProviders

Synopsis

commandProvider :: TacticCommand -> TacticProvider
commandTactic :: ParserContext -> TacticCommand -> Text -> IO (TacticsM ())
tcCommandId :: TacticCommand -> CommandId
data TacticParams = TacticParams {
- tp_file :: Uri
- tp_range :: Tracked 'Current Range
- tp_var_name :: Text
}
data TacticProviderData = TacticProviderData {
- 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

Documentation

commandProvider :: TacticCommand -> TacticProvider Source #

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

commandTactic :: ParserContext -> TacticCommand -> Text -> IO (TacticsM ()) Source #

A mapping from tactic commands to actual tactics for refinery.

tcCommandId :: TacticCommand -> CommandId Source #

Construct a CommandId

data TacticParams Source #

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

Instances details

Eq TacticParams Source #
Instance details Defined in Wingman.LanguageServer.TacticProviders Methods (==) :: TacticParams -> TacticParams -> Bool # (/=) :: TacticParams -> TacticParams -> Bool #
Show TacticParams Source #
Instance details Defined in Wingman.LanguageServer.TacticProviders Methods showsPrec :: Int -> TacticParams -> ShowS # show :: TacticParams -> String # showList :: [TacticParams] -> ShowS #
Generic TacticParams Source #
Instance details 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 Source #
Instance details Defined in Wingman.LanguageServer.TacticProviders Methods toJSON :: TacticParams -> Value # toEncoding :: TacticParams -> Encoding # toJSONList :: [TacticParams] -> Value # toEncodingList :: [TacticParams] -> Encoding #
FromJSON TacticParams Source #
Instance details Defined in Wingman.LanguageServer.TacticProviders Methods parseJSON :: Value -> Parser TacticParams # parseJSONList :: Value -> Parser [TacticParams] #
type Rep TacticParams Source #
Instance details Defined in Wingman.LanguageServer.TacticProviders type Rep TacticParams = D1 ('MetaData "TacticParams" "Wingman.LanguageServer.TacticProviders" "hls-tactics-plugin-1.2.0.0-ISyG8qIj9D072QqyrjxihH" '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 Source #

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

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