{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
module Wingman.LanguageServer.TacticProviders
( commandProvider
, commandTactic
, tcCommandId
, TacticParams (..)
, TacticProviderData (..)
, useNameFromHypothesis
) where
import Control.Monad
import Control.Monad.Reader (runReaderT)
import Data.Aeson
import Data.Bool (bool)
import Data.Coerce
import Data.Maybe
import Data.Monoid
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
import OccName
import Prelude hiding (span)
import Wingman.Auto
import Wingman.GHC
import Wingman.Judgements
import Wingman.Machinery (useNameFromHypothesis)
import Wingman.Metaprogramming.Lexer (ParserContext)
import Wingman.Metaprogramming.Parser (parseMetaprogram)
import Wingman.Tactics
import Wingman.Types
commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ())
commandTactic :: ParserContext -> TacticCommand -> Text -> IO (TacticsM ())
commandTactic ParserContext
_ TacticCommand
Auto = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
auto
commandTactic ParserContext
_ TacticCommand
Intros = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
intros
commandTactic ParserContext
_ TacticCommand
Destruct = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 ParserContext
_ TacticCommand
DestructPun = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 ParserContext
_ TacticCommand
Homomorphism = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 ParserContext
_ TacticCommand
DestructLambdaCase = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
destructLambdaCase
commandTactic ParserContext
_ TacticCommand
HomomorphismLambdaCase = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
homoLambdaCase
commandTactic ParserContext
_ TacticCommand
DestructAll = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
destructAll
commandTactic ParserContext
_ TacticCommand
UseDataCon = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 ParserContext
_ TacticCommand
Refine = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
refine
commandTactic ParserContext
_ TacticCommand
BeginMetaprogram = TacticsM () -> IO (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> IO (TacticsM ()))
-> (Text -> TacticsM ()) -> Text -> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
metaprogram
commandTactic ParserContext
c TacticCommand
RunMetaprogram = (ReaderT ParserContext IO (TacticsM ())
-> ParserContext -> IO (TacticsM ()))
-> ParserContext
-> ReaderT ParserContext IO (TacticsM ())
-> IO (TacticsM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT ParserContext IO (TacticsM ())
-> ParserContext -> IO (TacticsM ())
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ParserContext
c (ReaderT ParserContext IO (TacticsM ()) -> IO (TacticsM ()))
-> (Text -> ReaderT ParserContext IO (TacticsM ()))
-> Text
-> IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> ReaderT ParserContext IO (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 ((Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True) (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
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 -> Maybe TyCon
algebraicTyCon -> Just TyCon
t1) (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
t2) = TyCon
t1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
t2
homoFilter Type
_ Type
_ = Bool
False
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