{-# LANGUAGE CPP               #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Wingman.LanguageServer.TacticProviders
  ( commandProvider
  , commandTactic
  , TacticProviderData (..)
  ) where

import           Control.Monad
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           Development.IDE.GHC.Compat
import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
import           Ide.Types
import           Language.LSP.Types hiding (SemanticTokenAbsolute (..), SemanticTokenRelative (..))
import           Prelude hiding (span)
import           Wingman.AbstractLSP.Types
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
IntroAndDestruct       = TacticsM () -> Text -> TacticsM ()
forall a b. a -> b -> a
const TacticsM ()
introAndDestruct
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
IntroAndDestruct       = Text
"introduceAndDestruct"
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
IntroAndDestruct       = Bool
True
tacticPreferred TacticCommand
Destruct               = Bool
True
tacticPreferred TacticCommand
DestructPun            = Bool
False
tacticPreferred TacticCommand
Homomorphism           = Bool
True
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
IntroAndDestruct =
  (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 (Bool -> (Type -> Type -> Bool) -> Type -> Bool
forall r. r -> (Type -> Type -> r) -> Type -> r
liftLambdaCase Bool
False (\Type
_ -> Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TyCon -> Bool) -> (Type -> Maybe TyCon) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
algebraicTyCon)) (TacticProvider -> TacticProvider)
-> TacticProvider -> TacticProvider
forall a b. (a -> b) -> a -> b
$
    TacticCommand -> Text -> TacticProvider
provide TacticCommand
IntroAndDestruct 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]
-> (([DataCon], [Type]) -> [DataCon])
-> Maybe ([DataCon], [Type])
-> [DataCon]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ([DataCon], [Type]) -> [DataCon]
forall a b. (a, b) -> a
fst
        (Maybe ([DataCon], [Type]) -> [DataCon])
-> (Type -> Maybe ([DataCon], [Type])) -> Type -> [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
#if __GLASGOW_HASKELL__ >= 808
requireGHC88OrHigher :: TacticProvider -> TacticProvider
requireGHC88OrHigher TacticProvider
tp TacticProviderData
tpd =
  TacticProvider
tp TacticProviderData
tpd
#else
requireGHC88OrHigher _ _=
  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
    -> [(Metadata, T.Text)]


data TacticProviderData = TacticProviderData
  { TacticProviderData -> LspEnv
tpd_lspEnv :: LspEnv
  , TacticProviderData -> Judgement
tpd_jdg    :: Judgement
  , TacticProviderData -> HoleSort
tpd_hole_sort :: HoleSort
  }


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 -> []

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
_ -> []


------------------------------------------------------------------------------
-- | 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
$ LspEnv -> DynFlags
le_dflags (LspEnv -> DynFlags) -> LspEnv -> DynFlags
forall a b. (a -> b) -> a -> b
$ TacticProviderData -> LspEnv
tpd_lspEnv TacticProviderData
tpd of
    Bool
True  -> TacticProvider
tp TacticProviderData
tpd
    Bool
False -> []


------------------------------------------------------------------------------
-- | 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 -> []


------------------------------------------------------------------------------
-- | 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 Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis CType
hy [HyInfo CType]
-> (HyInfo CType -> [(Metadata, Text)]) -> [(Metadata, Text)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m 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 -> []


------------------------------------------------------------------------------
-- | 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 =
  (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] -> (a -> [(Metadata, Text)]) -> [(Metadata, Text)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m 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 (LspEnv -> Config
le_config (LspEnv -> Config) -> LspEnv -> Config
forall a b. (a -> b) -> a -> b
$ TacticProviderData -> LspEnv
tpd_lspEnv 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
_ =
  (Metadata, Text) -> [(Metadata, Text)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> CodeActionKind -> Bool -> Metadata
Metadata (TacticCommand -> Text -> Text
tacticTitle TacticCommand
tc Text
name) (TacticCommand -> CodeActionKind
mkTacticKind TacticCommand
tc) (TacticCommand -> Bool
tacticPreferred TacticCommand
tc), Text
name)


------------------------------------------------------------------------------
-- | 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 -> String -> String
forall a. Semigroup a => a -> a -> a
<> TacticCommand -> String
forall a. Show a => a -> String
show TacticCommand
c String -> String -> String
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 -> r) -> Type -> r
forall a b. (a -> b) -> a -> b
$ Type -> Type
forall a. Scaled a -> Scaled a
scaledThing 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) =
  Bool -> Bool
not (Bool -> Bool) -> ([DataCon] -> Bool) -> [DataCon] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> Bool) -> [DataCon] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([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


instance IsContinuationSort TacticCommand where
  toCommandId :: TacticCommand -> CommandId
toCommandId = TacticCommand -> CommandId
tcCommandId