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


------------------------------------------------------------------------------
-- | A mapping from tactic commands to actual tactics for refinery.
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


------------------------------------------------------------------------------
-- | The LSP kind
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"


------------------------------------------------------------------------------
-- | Whether or not this code action is preferred -- ostensibly refers to
-- whether or not we can bind it to a key in vs code?
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


------------------------------------------------------------------------------
-- | Mapping from tactic commands to their contextual providers. See 'provide',
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
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


------------------------------------------------------------------------------
-- | Return an empty list if the given predicate doesn't hold over the length
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


------------------------------------------------------------------------------
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
-- UI.
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    -- ^ Uri of the file to fill the hole in
    , TacticParams -> Tracked 'Current Range
tp_range    :: Tracked 'Current Range  -- ^ The range of the hole
    , 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 []


------------------------------------------------------------------------------
-- | Restrict a 'TacticProvider', making sure it appears only when the given
-- predicate holds for the goal.
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 []


------------------------------------------------------------------------------
-- | Restrict a 'TacticProvider', making sure it appears only when the given
-- predicate holds for the goal.
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 []


------------------------------------------------------------------------------
-- | Restrict a 'TacticProvider', making sure it appears only when the given
-- predicate holds for the goal.
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


------------------------------------------------------------------------------
-- | Multiply a 'TacticProvider' for each binding, making sure it appears only
-- when the given predicate holds over the goal and binding types.
filterBindingType
    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
    -> (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 []


------------------------------------------------------------------------------
-- | Multiply a 'TacticProvider' by some feature projection out of the goal
-- type. Used e.g. to crete a code action for every data constructor.
filterTypeProjection
    :: (Type -> [a])  -- ^ Features of the goal to look into further
    -> (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


------------------------------------------------------------------------------
-- | Get access to the 'Config' when building a 'TacticProvider'.
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


------------------------------------------------------------------------------
-- | Terminal constructor for providing context-sensitive tactics. Tactics
-- given by 'provide' are always available.
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
        }


------------------------------------------------------------------------------
-- | Construct a 'CommandId'
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"


------------------------------------------------------------------------------
-- | We should show homos only when the goal type is the same as the binding
-- type, and that both are usual algebraic types.
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


------------------------------------------------------------------------------
-- | Lift a function of (codomain, domain) over a lambda case.
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



------------------------------------------------------------------------------
-- | We should show destruct for bindings only when those bindings have usual
-- algebraic types.
destructFilter :: Type -> Type -> Bool
destructFilter :: Type -> Type -> Bool
destructFilter Type
_ (Type -> Maybe TyCon
algebraicTyCon -> Just TyCon
_) = Bool
True
destructFilter Type
_ Type
_                          = Bool
False


------------------------------------------------------------------------------
-- | We should show destruct punning for bindings only when those bindings have
-- usual algebraic types, and when any of their data constructors are records.
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