{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Wingman.LanguageServer.TacticProviders
( commandProvider
, commandTactic
, tcCommandId
, TacticParams (..)
, TacticProviderData (..)
, useNameFromHypothesis
) where
import Control.Monad
import Data.Aeson
import Data.Bool (bool)
import Data.Coerce
import Data.Maybe
import Data.Monoid
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Traversable
import DataCon (dataConName)
import Development.IDE.Core.UseStale (Tracked, Age(..))
import Development.IDE.GHC.Compat
import GHC.Generics
import GHC.LanguageExtensions.Type (Extension (LambdaCase))
import Ide.PluginUtils
import Ide.Types
import Language.LSP.Types hiding
(SemanticTokenAbsolute (length, line),
SemanticTokenRelative (length),
SemanticTokensEdit (_start))
import OccName
import Prelude hiding (span)
import Wingman.Auto
import Wingman.GHC
import Wingman.Judgements
import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons)
import Wingman.Metaprogramming.Parser (parseMetaprogram)
import Wingman.Tactics
import Wingman.Types
commandTactic :: TacticCommand -> T.Text -> TacticsM ()
commandTactic :: TacticCommand -> Text -> TacticsM ()
commandTactic TacticCommand
Auto = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
auto
commandTactic TacticCommand
Intros = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
intros
commandTactic TacticCommand
Destruct = (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
destruct (OccName -> TacticsM ())
-> (Text -> OccName) -> Text -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccName
mkVarOcc (String -> OccName) -> (Text -> String) -> Text -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack
commandTactic TacticCommand
DestructPun = (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
destructPun (OccName -> TacticsM ())
-> (Text -> OccName) -> Text -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccName
mkVarOcc (String -> OccName) -> (Text -> String) -> Text -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack
commandTactic TacticCommand
Homomorphism = (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
homo (OccName -> TacticsM ())
-> (Text -> OccName) -> Text -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccName
mkVarOcc (String -> OccName) -> (Text -> String) -> Text -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack
commandTactic TacticCommand
DestructLambdaCase = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
destructLambdaCase
commandTactic TacticCommand
HomomorphismLambdaCase = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
homoLambdaCase
commandTactic TacticCommand
DestructAll = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
destructAll
commandTactic TacticCommand
UseDataCon = OccName -> TacticsM ()
userSplit (OccName -> TacticsM ())
-> (Text -> OccName) -> Text -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccName
mkVarOcc (String -> OccName) -> (Text -> String) -> Text -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack
commandTactic TacticCommand
Refine = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
refine
commandTactic TacticCommand
BeginMetaprogram = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
metaprogram
commandTactic TacticCommand
RunMetaprogram = Text -> TacticsM ()
parseMetaprogram
tacticKind :: TacticCommand -> T.Text
tacticKind :: TacticCommand -> Text
tacticKind TacticCommand
Auto = Text
"fillHole"
tacticKind TacticCommand
Intros = Text
"introduceLambda"
tacticKind TacticCommand
Destruct = Text
"caseSplit"
tacticKind TacticCommand
DestructPun = Text
"caseSplitPun"
tacticKind TacticCommand
Homomorphism = Text
"homomorphicCaseSplit"
tacticKind TacticCommand
DestructLambdaCase = Text
"lambdaCase"
tacticKind TacticCommand
HomomorphismLambdaCase = Text
"homomorphicLambdaCase"
tacticKind TacticCommand
DestructAll = Text
"splitFuncArgs"
tacticKind TacticCommand
UseDataCon = Text
"useConstructor"
tacticKind TacticCommand
Refine = Text
"refine"
tacticKind TacticCommand
BeginMetaprogram = Text
"beginMetaprogram"
tacticKind TacticCommand
RunMetaprogram = Text
"runMetaprogram"
tacticPreferred :: TacticCommand -> Bool
tacticPreferred :: TacticCommand -> Bool
tacticPreferred TacticCommand
Auto = Bool
True
tacticPreferred TacticCommand
Intros = Bool
True
tacticPreferred TacticCommand
Destruct = Bool
True
tacticPreferred TacticCommand
DestructPun = Bool
False
tacticPreferred TacticCommand
Homomorphism = Bool
False
tacticPreferred TacticCommand
DestructLambdaCase = Bool
False
tacticPreferred TacticCommand
HomomorphismLambdaCase = Bool
False
tacticPreferred TacticCommand
DestructAll = Bool
True
tacticPreferred TacticCommand
UseDataCon = Bool
True
tacticPreferred TacticCommand
Refine = Bool
True
tacticPreferred TacticCommand
BeginMetaprogram = Bool
False
tacticPreferred TacticCommand
RunMetaprogram = Bool
True
mkTacticKind :: TacticCommand -> CodeActionKind
mkTacticKind :: TacticCommand -> CodeActionKind
mkTacticKind =
Text -> CodeActionKind
CodeActionUnknown (Text -> CodeActionKind)
-> (TacticCommand -> Text) -> TacticCommand -> CodeActionKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
"refactor.wingman." (Text -> Text) -> (TacticCommand -> Text) -> TacticCommand -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticCommand -> Text
tacticKind
commandProvider :: TacticCommand -> TacticProvider
commandProvider :: TacticCommand -> TacticProvider
commandProvider TacticCommand
Auto =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticCommand -> Text -> TacticProvider
provide TacticCommand
Auto Text
""
commandProvider TacticCommand
Intros =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType Type -> Bool
isFunction (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticCommand -> Text -> TacticProvider
provide TacticCommand
Intros Text
""
commandProvider TacticCommand
Destruct =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
destructFilter ((OccName -> Type -> TacticProvider) -> TacticProvider)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \OccName
occ Type
_ ->
TacticCommand -> Text -> TacticProvider
provide TacticCommand
Destruct (Text -> TacticProvider) -> Text -> TacticProvider
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString OccName
occ
commandProvider TacticCommand
DestructPun =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
destructPunFilter ((OccName -> Type -> TacticProvider) -> TacticProvider)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \OccName
occ Type
_ ->
TacticCommand -> Text -> TacticProvider
provide TacticCommand
DestructPun (Text -> TacticProvider) -> Text -> TacticProvider
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString OccName
occ
commandProvider TacticCommand
Homomorphism =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
homoFilter ((OccName -> Type -> TacticProvider) -> TacticProvider)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \OccName
occ Type
_ ->
TacticCommand -> Text -> TacticProvider
provide TacticCommand
Homomorphism (Text -> TacticProvider) -> Text -> TacticProvider
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString OccName
occ
commandProvider TacticCommand
DestructLambdaCase =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
Extension -> TacticProvider -> TacticProvider
requireExtension Extension
LambdaCase (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType (Maybe Bool -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Bool -> Bool) -> (Type -> Maybe Bool) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Bool
lambdaCaseable) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticCommand -> Text -> TacticProvider
provide TacticCommand
DestructLambdaCase Text
""
commandProvider TacticCommand
HomomorphismLambdaCase =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
Extension -> TacticProvider -> TacticProvider
requireExtension Extension
LambdaCase (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType (Bool -> (Type -> Type -> Bool) -> Type -> Bool
forall r. r -> (Type -> Type -> r) -> Type -> r
liftLambdaCase Bool
False Type -> Type -> Bool
homoFilter) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticCommand -> Text -> TacticProvider
provide TacticCommand
HomomorphismLambdaCase Text
""
commandProvider TacticCommand
DestructAll =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Judgement -> TacticProvider) -> TacticProvider
withJudgement ((Judgement -> TacticProvider) -> TacticProvider)
-> (Judgement -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \Judgement
jdg ->
case Judgement -> Bool
forall a. Judgement' a -> Bool
_jIsTopHole Judgement
jdg Bool -> Bool -> Bool
&& Judgement -> Bool
forall a. Judgement' a -> Bool
jHasBoundArgs Judgement
jdg of
Bool
True -> TacticCommand -> Text -> TacticProvider
provide TacticCommand
DestructAll Text
""
Bool
False -> TacticProvider
forall a. Monoid a => a
mempty
commandProvider TacticCommand
UseDataCon =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Config -> TacticProvider) -> TacticProvider
withConfig ((Config -> TacticProvider) -> TacticProvider)
-> (Config -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \Config
cfg ->
(Type -> [DataCon])
-> (DataCon -> TacticProvider) -> TacticProvider
forall a. (Type -> [a]) -> (a -> TacticProvider) -> TacticProvider
filterTypeProjection
( (Int -> Bool) -> [DataCon] -> [DataCon]
forall a. (Int -> Bool) -> [a] -> [a]
guardLength (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Config -> Int
cfg_max_use_ctor_actions Config
cfg)
([DataCon] -> [DataCon])
-> (Type -> [DataCon]) -> Type -> [DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataCon] -> Maybe [DataCon] -> [DataCon]
forall a. a -> Maybe a -> a
fromMaybe []
(Maybe [DataCon] -> [DataCon])
-> (Type -> Maybe [DataCon]) -> Type -> [DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([DataCon], [Type]) -> [DataCon])
-> Maybe ([DataCon], [Type]) -> Maybe [DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DataCon], [Type]) -> [DataCon]
forall a b. (a, b) -> a
fst
(Maybe ([DataCon], [Type]) -> Maybe [DataCon])
-> (Type -> Maybe ([DataCon], [Type])) -> Type -> Maybe [DataCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons
) ((DataCon -> TacticProvider) -> TacticProvider)
-> (DataCon -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \DataCon
dcon ->
TacticCommand -> Text -> TacticProvider
provide TacticCommand
UseDataCon
(Text -> TacticProvider)
-> (Name -> Text) -> Name -> TacticProvider
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack
(String -> Text) -> (Name -> String) -> Name -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString
(OccName -> String) -> (Name -> OccName) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> OccName
forall name. HasOccName name => name -> OccName
occName
(Name -> TacticProvider) -> Name -> TacticProvider
forall a b. (a -> b) -> a -> b
$ DataCon -> Name
dataConName DataCon
dcon
commandProvider TacticCommand
Refine =
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticCommand -> Text -> TacticProvider
provide TacticCommand
Refine Text
""
commandProvider TacticCommand
BeginMetaprogram =
TacticProvider -> TacticProvider
requireGHC88OrHigher (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort (HoleSort -> HoleSort -> Bool
forall a. Eq a => a -> a -> Bool
== HoleSort
Hole) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
TacticCommand -> Text -> TacticProvider
provide TacticCommand
BeginMetaprogram Text
""
commandProvider TacticCommand
RunMetaprogram =
TacticProvider -> TacticProvider
requireGHC88OrHigher (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
(Text -> TacticProvider) -> TacticProvider
withMetaprogram ((Text -> TacticProvider) -> TacticProvider)
-> (Text -> TacticProvider) -> TacticProvider
forall a b. (a -> b) -> a -> b
$ \Text
mp ->
TacticCommand -> Text -> TacticProvider
provide TacticCommand
RunMetaprogram Text
mp
requireGHC88OrHigher :: TacticProvider -> TacticProvider
requireGHC88OrHigher :: TacticProvider -> TacticProvider
requireGHC88OrHigher TacticProvider
tp TacticProviderData
tpd =
#if __GLASGOW_HASKELL__ >= 808
TacticProvider
tp TacticProviderData
tpd
#else
mempty
#endif
guardLength :: (Int -> Bool) -> [a] -> [a]
guardLength :: (Int -> Bool) -> [a] -> [a]
guardLength Int -> Bool
f [a]
as = [a] -> [a] -> Bool -> [a]
forall a. a -> a -> Bool -> a
bool [] [a]
as (Bool -> [a]) -> Bool -> [a]
forall a b. (a -> b) -> a -> b
$ Int -> Bool
f (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as
type TacticProvider
= TacticProviderData
-> IO [Command |? CodeAction]
data TacticProviderData = TacticProviderData
{ TacticProviderData -> DynFlags
tpd_dflags :: DynFlags
, TacticProviderData -> Config
tpd_config :: Config
, TacticProviderData -> PluginId
tpd_plid :: PluginId
, TacticProviderData -> Uri
tpd_uri :: Uri
, TacticProviderData -> Tracked 'Current Range
tpd_range :: Tracked 'Current Range
, TacticProviderData -> Judgement
tpd_jdg :: Judgement
, TacticProviderData -> HoleSort
tpd_hole_sort :: HoleSort
}
data TacticParams = TacticParams
{ TacticParams -> Uri
tp_file :: Uri
, TacticParams -> Tracked 'Current Range
tp_range :: Tracked 'Current Range
, TacticParams -> Text
tp_var_name :: T.Text
}
deriving stock (Int -> TacticParams -> ShowS
[TacticParams] -> ShowS
TacticParams -> String
(Int -> TacticParams -> ShowS)
-> (TacticParams -> String)
-> ([TacticParams] -> ShowS)
-> Show TacticParams
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TacticParams] -> ShowS
$cshowList :: [TacticParams] -> ShowS
show :: TacticParams -> String
$cshow :: TacticParams -> String
showsPrec :: Int -> TacticParams -> ShowS
$cshowsPrec :: Int -> TacticParams -> ShowS
Show, TacticParams -> TacticParams -> Bool
(TacticParams -> TacticParams -> Bool)
-> (TacticParams -> TacticParams -> Bool) -> Eq TacticParams
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TacticParams -> TacticParams -> Bool
$c/= :: TacticParams -> TacticParams -> Bool
== :: TacticParams -> TacticParams -> Bool
$c== :: TacticParams -> TacticParams -> Bool
Eq, (forall x. TacticParams -> Rep TacticParams x)
-> (forall x. Rep TacticParams x -> TacticParams)
-> Generic TacticParams
forall x. Rep TacticParams x -> TacticParams
forall x. TacticParams -> Rep TacticParams x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TacticParams x -> TacticParams
$cfrom :: forall x. TacticParams -> Rep TacticParams x
Generic)
deriving anyclass ([TacticParams] -> Encoding
[TacticParams] -> Value
TacticParams -> Encoding
TacticParams -> Value
(TacticParams -> Value)
-> (TacticParams -> Encoding)
-> ([TacticParams] -> Value)
-> ([TacticParams] -> Encoding)
-> ToJSON TacticParams
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [TacticParams] -> Encoding
$ctoEncodingList :: [TacticParams] -> Encoding
toJSONList :: [TacticParams] -> Value
$ctoJSONList :: [TacticParams] -> Value
toEncoding :: TacticParams -> Encoding
$ctoEncoding :: TacticParams -> Encoding
toJSON :: TacticParams -> Value
$ctoJSON :: TacticParams -> Value
ToJSON, Value -> Parser [TacticParams]
Value -> Parser TacticParams
(Value -> Parser TacticParams)
-> (Value -> Parser [TacticParams]) -> FromJSON TacticParams
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [TacticParams]
$cparseJSONList :: Value -> Parser [TacticParams]
parseJSON :: Value -> Parser TacticParams
$cparseJSON :: Value -> Parser TacticParams
FromJSON)
requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider
requireHoleSort HoleSort -> Bool
p TacticProvider
tp TacticProviderData
tpd =
case HoleSort -> Bool
p (HoleSort -> Bool) -> HoleSort -> Bool
forall a b. (a -> b) -> a -> b
$ TacticProviderData -> HoleSort
tpd_hole_sort TacticProviderData
tpd of
Bool
True -> TacticProvider
tp TacticProviderData
tpd
Bool
False -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
withMetaprogram :: (T.Text -> TacticProvider) -> TacticProvider
withMetaprogram :: (Text -> TacticProvider) -> TacticProvider
withMetaprogram Text -> TacticProvider
tp TacticProviderData
tpd =
case TacticProviderData -> HoleSort
tpd_hole_sort TacticProviderData
tpd of
Metaprogram Text
mp -> Text -> TacticProvider
tp Text
mp TacticProviderData
tpd
HoleSort
_ -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
requireExtension :: Extension -> TacticProvider -> TacticProvider
requireExtension :: Extension -> TacticProvider -> TacticProvider
requireExtension Extension
ext TacticProvider
tp TacticProviderData
tpd =
case Extension -> DynFlags -> Bool
xopt Extension
ext (DynFlags -> Bool) -> DynFlags -> Bool
forall a b. (a -> b) -> a -> b
$ TacticProviderData -> DynFlags
tpd_dflags TacticProviderData
tpd of
Bool
True -> TacticProvider
tp TacticProviderData
tpd
Bool
False -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
filterGoalType Type -> Bool
p TacticProvider
tp TacticProviderData
tpd =
case Type -> Bool
p (Type -> Bool) -> Type -> Bool
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal (Judgement -> CType) -> Judgement -> CType
forall a b. (a -> b) -> a -> b
$ TacticProviderData -> Judgement
tpd_jdg TacticProviderData
tpd of
Bool
True -> TacticProvider
tp TacticProviderData
tpd
Bool
False -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
withJudgement :: (Judgement -> TacticProvider) -> TacticProvider
withJudgement :: (Judgement -> TacticProvider) -> TacticProvider
withJudgement Judgement -> TacticProvider
tp TacticProviderData
tpd = Judgement -> TacticProvider
tp (TacticProviderData -> Judgement
tpd_jdg TacticProviderData
tpd) TacticProviderData
tpd
filterBindingType
:: (Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider)
-> TacticProvider
filterBindingType :: (Type -> Type -> Bool)
-> (OccName -> Type -> TacticProvider) -> TacticProvider
filterBindingType Type -> Type -> Bool
p OccName -> Type -> TacticProvider
tp TacticProviderData
tpd =
let jdg :: Judgement
jdg = TacticProviderData -> Judgement
tpd_jdg TacticProviderData
tpd
hy :: Hypothesis CType
hy = Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jLocalHypothesis Judgement
jdg
g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
in ([[Command |? CodeAction]] -> [Command |? CodeAction])
-> IO [[Command |? CodeAction]] -> IO [Command |? CodeAction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Command |? CodeAction]] -> [Command |? CodeAction]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO [[Command |? CodeAction]] -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]] -> IO [Command |? CodeAction]
forall a b. (a -> b) -> a -> b
$ [HyInfo CType]
-> (HyInfo CType -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis CType
hy) ((HyInfo CType -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]])
-> (HyInfo CType -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]]
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
hi ->
let ty :: Type
ty = CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi
in case Type -> Type -> Bool
p (CType -> Type
unCType CType
g) Type
ty of
Bool
True -> OccName -> Type -> TacticProvider
tp (HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi) Type
ty TacticProviderData
tpd
Bool
False -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
filterTypeProjection
:: (Type -> [a])
-> (a -> TacticProvider)
-> TacticProvider
filterTypeProjection :: (Type -> [a]) -> (a -> TacticProvider) -> TacticProvider
filterTypeProjection Type -> [a]
p a -> TacticProvider
tp TacticProviderData
tpd =
([[Command |? CodeAction]] -> [Command |? CodeAction])
-> IO [[Command |? CodeAction]] -> IO [Command |? CodeAction]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Command |? CodeAction]] -> [Command |? CodeAction]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO [[Command |? CodeAction]] -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]] -> IO [Command |? CodeAction]
forall a b. (a -> b) -> a -> b
$ [a]
-> (a -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (Type -> [a]
p (Type -> [a]) -> Type -> [a]
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType (CType -> Type) -> CType -> Type
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal (Judgement -> CType) -> Judgement -> CType
forall a b. (a -> b) -> a -> b
$ TacticProviderData -> Judgement
tpd_jdg TacticProviderData
tpd) ((a -> IO [Command |? CodeAction]) -> IO [[Command |? CodeAction]])
-> (a -> IO [Command |? CodeAction])
-> IO [[Command |? CodeAction]]
forall a b. (a -> b) -> a -> b
$ \a
a ->
a -> TacticProvider
tp a
a TacticProviderData
tpd
withConfig :: (Config -> TacticProvider) -> TacticProvider
withConfig :: (Config -> TacticProvider) -> TacticProvider
withConfig Config -> TacticProvider
tp TacticProviderData
tpd = Config -> TacticProvider
tp (TacticProviderData -> Config
tpd_config TacticProviderData
tpd) TacticProviderData
tpd
provide :: TacticCommand -> T.Text -> TacticProvider
provide :: TacticCommand -> Text -> TacticProvider
provide TacticCommand
tc Text
name TacticProviderData{DynFlags
Tracked 'Current Range
Uri
PluginId
HoleSort
Judgement
Config
tpd_hole_sort :: HoleSort
tpd_jdg :: Judgement
tpd_range :: Tracked 'Current Range
tpd_uri :: Uri
tpd_plid :: PluginId
tpd_config :: Config
tpd_dflags :: DynFlags
tpd_hole_sort :: TacticProviderData -> HoleSort
tpd_jdg :: TacticProviderData -> Judgement
tpd_range :: TacticProviderData -> Tracked 'Current Range
tpd_uri :: TacticProviderData -> Uri
tpd_plid :: TacticProviderData -> PluginId
tpd_config :: TacticProviderData -> Config
tpd_dflags :: TacticProviderData -> DynFlags
..} = do
let title :: Text
title = TacticCommand -> Text -> Text
tacticTitle TacticCommand
tc Text
name
params :: TacticParams
params = TacticParams :: Uri -> Tracked 'Current Range -> Text -> TacticParams
TacticParams { tp_file :: Uri
tp_file = Uri
tpd_uri , tp_range :: Tracked 'Current Range
tp_range = Tracked 'Current Range
tpd_range , tp_var_name :: Text
tp_var_name = Text
name }
cmd :: Command
cmd = PluginId -> CommandId -> Text -> Maybe [Value] -> Command
mkLspCommand PluginId
tpd_plid (TacticCommand -> CommandId
tcCommandId TacticCommand
tc) Text
title ([Value] -> Maybe [Value]
forall a. a -> Maybe a
Just [TacticParams -> Value
forall a. ToJSON a => a -> Value
toJSON TacticParams
params])
[Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
([Command |? CodeAction] -> IO [Command |? CodeAction])
-> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall a b. (a -> b) -> a -> b
$ (Command |? CodeAction) -> [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
((Command |? CodeAction) -> [Command |? CodeAction])
-> (Command |? CodeAction) -> [Command |? CodeAction]
forall a b. (a -> b) -> a -> b
$ CodeAction -> Command |? CodeAction
forall a b. b -> a |? b
InR
(CodeAction -> Command |? CodeAction)
-> CodeAction -> Command |? CodeAction
forall a b. (a -> b) -> a -> b
$ CodeAction :: Text
-> Maybe CodeActionKind
-> Maybe (List Diagnostic)
-> Maybe Bool
-> Maybe Reason
-> Maybe WorkspaceEdit
-> Maybe Command
-> Maybe Value
-> CodeAction
CodeAction
{ $sel:_title:CodeAction :: Text
_title = Text
title
, $sel:_kind:CodeAction :: Maybe CodeActionKind
_kind = CodeActionKind -> Maybe CodeActionKind
forall a. a -> Maybe a
Just (CodeActionKind -> Maybe CodeActionKind)
-> CodeActionKind -> Maybe CodeActionKind
forall a b. (a -> b) -> a -> b
$ TacticCommand -> CodeActionKind
mkTacticKind TacticCommand
tc
, $sel:_diagnostics:CodeAction :: Maybe (List Diagnostic)
_diagnostics = Maybe (List Diagnostic)
forall a. Maybe a
Nothing
, $sel:_isPreferred:CodeAction :: Maybe Bool
_isPreferred = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ TacticCommand -> Bool
tacticPreferred TacticCommand
tc
, $sel:_disabled:CodeAction :: Maybe Reason
_disabled = Maybe Reason
forall a. Maybe a
Nothing
, $sel:_edit:CodeAction :: Maybe WorkspaceEdit
_edit = Maybe WorkspaceEdit
forall a. Maybe a
Nothing
, $sel:_command:CodeAction :: Maybe Command
_command = Command -> Maybe Command
forall a. a -> Maybe a
Just Command
cmd
, $sel:_xdata:CodeAction :: Maybe Value
_xdata = Maybe Value
forall a. Maybe a
Nothing
}
tcCommandId :: TacticCommand -> CommandId
tcCommandId :: TacticCommand -> CommandId
tcCommandId TacticCommand
c = Text -> CommandId
coerce (Text -> CommandId) -> Text -> CommandId
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
"tactics" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TacticCommand -> String
forall a. Show a => a -> String
show TacticCommand
c String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"Command"
homoFilter :: Type -> Type -> Bool
homoFilter :: Type -> Type -> Bool
homoFilter Type
codomain Type
domain =
case Type -> Type -> Maybe (Set (Uniquely DataCon))
uncoveredDataCons Type
domain Type
codomain of
Just Set (Uniquely DataCon)
s -> Set (Uniquely DataCon) -> Bool
forall a. Set a -> Bool
S.null Set (Uniquely DataCon)
s
Maybe (Set (Uniquely DataCon))
_ -> Bool
False
liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
liftLambdaCase r
nil Type -> Type -> r
f Type
t =
case Type -> ([TyVar], [Type], [Type], Type)
tacticsSplitFunTy Type
t of
([TyVar]
_, [Type]
_, Type
arg : [Type]
_, Type
res) -> Type -> Type -> r
f Type
res Type
arg
([TyVar], [Type], [Type], Type)
_ -> r
nil
destructFilter :: Type -> Type -> Bool
destructFilter :: Type -> Type -> Bool
destructFilter Type
_ (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
_) = Bool
True
destructFilter Type
_ Type
_ = Bool
False
destructPunFilter :: Type -> Type -> Bool
destructPunFilter :: Type -> Type -> Bool
destructPunFilter Type
_ (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
tc) =
(DataCon -> Bool) -> [DataCon] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (DataCon -> Bool) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FieldLabel] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([FieldLabel] -> Bool)
-> (DataCon -> [FieldLabel]) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> [FieldLabel]
dataConFieldLabels) ([DataCon] -> Bool) -> [DataCon] -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc
destructPunFilter Type
_ Type
_ = Bool
False