{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module Ide.Plugin.Tactic.LanguageServer.TacticProviders
( commandProvider
, commandTactic
, tcCommandId
, TacticParams (..)
) where
import Control.Monad
import Control.Monad.Error.Class (MonadError(throwError))
import Data.Aeson
import Data.Coerce
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid
import qualified Data.Text as T
import Data.Traversable
import Development.IDE.GHC.Compat
import GHC.Generics
import GHC.LanguageExtensions.Type (Extension (LambdaCase))
import Ide.Plugin.Tactic.Auto
import Ide.Plugin.Tactic.FeatureSet
import Ide.Plugin.Tactic.GHC
import Ide.Plugin.Tactic.Judgements
import Ide.Plugin.Tactic.Tactics
import Ide.Plugin.Tactic.TestTypes
import Ide.Plugin.Tactic.Types
import Ide.PluginUtils
import Ide.Types
import Language.LSP.Types
import OccName
import Prelude hiding (span)
import Refinery.Tactic (goal)
commandTactic :: TacticCommand -> OccName -> TacticsM ()
commandTactic :: TacticCommand -> OccName -> TacticsM ()
commandTactic TacticCommand
Auto = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
auto
commandTactic TacticCommand
Intros = TacticsM () -> OccName -> 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
commandTactic TacticCommand
Homomorphism = (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
homo
commandTactic TacticCommand
DestructLambdaCase = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
destructLambdaCase
commandTactic TacticCommand
HomomorphismLambdaCase = TacticsM () -> OccName -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
homoLambdaCase
commandProvider :: TacticCommand -> TacticProvider
commandProvider :: TacticCommand -> TacticProvider
commandProvider TacticCommand
Auto = TacticCommand -> Text -> TacticProvider
provide TacticCommand
Auto Text
""
commandProvider TacticCommand
Intros =
(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 =
(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
Homomorphism =
(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 =
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 =
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
""
type TacticProvider
= DynFlags
-> FeatureSet
-> PluginId
-> Uri
-> Range
-> Judgement
-> IO [Command |? CodeAction]
data TacticParams = TacticParams
{ TacticParams -> Uri
tp_file :: Uri
, TacticParams -> Range
tp_range :: 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)
requireFeature :: Feature -> TacticProvider -> TacticProvider
requireFeature :: Feature -> TacticProvider -> TacticProvider
requireFeature Feature
f TacticProvider
tp DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg = do
Bool -> IO ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> IO ()) -> Bool -> IO ()
forall a b. (a -> b) -> a -> b
$ Feature -> FeatureSet -> Bool
hasFeature Feature
f FeatureSet
fs
TacticProvider
tp DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg
requireExtension :: Extension -> TacticProvider -> TacticProvider
requireExtension :: Extension -> TacticProvider -> TacticProvider
requireExtension Extension
ext TacticProvider
tp DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg =
case Extension -> DynFlags -> Bool
xopt Extension
ext DynFlags
dflags of
Bool
True -> TacticProvider
tp DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg
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 DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg =
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
jdg of
Bool
True -> TacticProvider
tp DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg
Bool
False -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
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 DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg =
let hy :: Hypothesis CType
hy = Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis 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 DynFlags
dflags FeatureSet
fs PluginId
plId Uri
uri Range
range Judgement
jdg
Bool
False -> [Command |? CodeAction] -> IO [Command |? CodeAction]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM a
f OccName
name = do
Hypothesis CType
hy <- Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis (Judgement -> Hypothesis CType)
-> TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
-> TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
(Hypothesis CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TacticT
Judgement
(Trace, LHsExpr GhcPs)
TacticError
TacticState
ExtractM
Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName Hypothesis CType
hy of
Just HyInfo CType
hi -> HyInfo CType -> TacticsM a
f HyInfo CType
hi
Maybe (HyInfo CType)
Nothing -> TacticError -> TacticsM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> TacticsM a) -> TacticError -> TacticsM a
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
NotInScope OccName
name
provide :: TacticCommand -> T.Text -> TacticProvider
provide :: TacticCommand -> Text -> TacticProvider
provide TacticCommand
tc Text
name DynFlags
_ FeatureSet
_ PluginId
plId Uri
uri Range
range Judgement
_ = do
let title :: Text
title = TacticCommand -> Text -> Text
tacticTitle TacticCommand
tc Text
name
params :: TacticParams
params = TacticParams :: Uri -> Range -> Text -> TacticParams
TacticParams { tp_file :: Uri
tp_file = Uri
uri , tp_range :: Range
tp_range = Range
range , tp_var_name :: Text
tp_var_name = Text
name }
cmd :: Command
cmd = PluginId -> CommandId -> Text -> Maybe [Value] -> Command
mkLspCommand PluginId
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
$ Text
-> Maybe CodeActionKind
-> Maybe (List Diagnostic)
-> Maybe Bool
-> Maybe Reason
-> Maybe WorkspaceEdit
-> Maybe Command
-> CodeAction
CodeAction Text
title (CodeActionKind -> Maybe CodeActionKind
forall a. a -> Maybe a
Just CodeActionKind
CodeActionQuickFix) Maybe (List Diagnostic)
forall a. Maybe a
Nothing Maybe Bool
forall a. Maybe a
Nothing Maybe Reason
forall a. Maybe a
Nothing Maybe WorkspaceEdit
forall a. Maybe a
Nothing
(Maybe Command -> CodeAction) -> Maybe Command -> CodeAction
forall a b. (a -> b) -> a -> b
$ Command -> Maybe Command
forall a. a -> Maybe a
Just Command
cmd
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