Implement "use constructor" code action

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs

@@ -13,30 +13,28 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
-import           Bag                                              (bagToList,
-                                                                   listToBag)
-import           Control.Exception                                (evaluate)
+import           Bag (bagToList, listToBag)
+import           Control.Exception (evaluate)
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
-import           Data.Bifunctor                                   (Bifunctor (bimap))
-import           Data.Bool                                        (bool)
-import           Data.Data                                        (Data)
+import           Data.Bifunctor (Bifunctor (bimap))
+import           Data.Bool (bool)
+import           Data.Data (Data)
 import           Data.Foldable (for_)
-import           Data.Generics.Aliases                            (mkQ)
-import           Data.Generics.Schemes                            (everything)
+import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Schemes (everything)
 import           Data.Maybe
 import           Data.Monoid
-import qualified Data.Text                                        as T
+import qualified Data.Text as T
 import           Data.Traversable
-import           Development.IDE.Core.Shake                       (IdeState (..))
+import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
 import           Development.Shake.Classes
 import           Ide.Plugin.Tactic.CaseSplit
-import           Ide.Plugin.Tactic.FeatureSet                     (Feature (..),
-                                                                   hasFeature)
+import           Ide.Plugin.Tactic.FeatureSet (Feature (..), hasFeature)
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.LanguageServer
 import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
@@ -49,7 +47,7 @@ import           Language.LSP.Server
 import           Language.LSP.Types
 import           Language.LSP.Types.Capabilities
 import           OccName
-import           Prelude                                          hiding (span)
+import           Prelude hiding (span)
 import           System.Timeout
 
 
@@ -71,14 +69,14 @@ descriptor plId = (defaultPluginDescriptor plId)
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      features <- getFeatureSet (shakeExtras state)
+      cfg <- getTacticConfig $ shakeExtras state
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range features
+        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound]
             dflags
-            features
+            cfg
             plId
             uri
             range

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs

@@ -21,7 +21,7 @@ import qualified Data.Text  as T
 ------------------------------------------------------------------------------
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
-data Feature = CantHaveAnEmptyDataType
+data Feature = FeatureUseDataCon
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs

@@ -9,26 +9,25 @@
 
 module Ide.Plugin.Tactic.GHC where
 
+import           Control.Arrow
 import           Control.Monad.State
-import           Data.Function              (on)
-import           Data.List                  (isPrefixOf)
-import qualified Data.Map                   as M
-import           Data.Maybe                 (isJust)
-import           Data.Set                   (Set)
-import qualified Data.Set                   as S
+import           Data.Function (on)
+import           Data.List (isPrefixOf)
+import qualified Data.Map as M
+import           Data.Maybe (isJust)
+import           Data.Set (Set)
+import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
 import           Development.IDE.GHC.Compat
-import           GHC.SourceGen              (case', lambda, match)
-import           Generics.SYB               (Data, everything, everywhere,
-                                             listify, mkQ, mkT)
+import           GHC.SourceGen (case', lambda, match)
+import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
 import           Ide.Plugin.Tactic.Types
 import           OccName
 import           TcType
 import           TyCoRep
 import           Type
-import           TysWiredIn                 (charTyCon, doubleTyCon, floatTyCon,
-                                             intTyCon)
+import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
 import           Unique
 import           Var
 
@@ -81,6 +80,12 @@ tacticsThetaTy :: Type -> ThetaType
 tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 
 
+------------------------------------------------------------------------------
+-- | Get the data cons of a type, if it has any.
+tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
+tacticsGetDataCons =
+  fmap (first tyConDataCons) . splitTyConApp_maybe
+
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
 -- skolems.
@@ -126,12 +131,18 @@ algebraicTyCon _ = Nothing
 
 
 ------------------------------------------------------------------------------
--- | We can't compare 'RdrName' for equality directly. Instead, compare them by
--- their 'OccName's.
+-- | We can't compare 'RdrName' for equality directly. Instead, sloppily
+-- compare them by their 'OccName's.
 eqRdrName :: RdrName -> RdrName -> Bool
 eqRdrName = (==) `on` occNameString . occName
 
 
+------------------------------------------------------------------------------
+-- | Compare two 'OccName's for unqualified equality.
+sloppyEqOccName :: OccName -> OccName -> Bool
+sloppyEqOccName = (==) `on` occNameString
+
+
 ------------------------------------------------------------------------------
 -- | Does this thing contain any references to 'HsVar's with the given
 -- 'RdrName'?

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

@@ -44,7 +44,7 @@ import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.TestTypes          (TacticCommand,
-                                                       cfg_feature_set)
+                                                       cfg_feature_set, emptyConfig, Config)
 import           Ide.Plugin.Tactic.Types
 import           Language.LSP.Server                  (MonadLsp)
 import           Language.LSP.Types
@@ -82,13 +82,19 @@ runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp
 
 
 ------------------------------------------------------------------------------
--- | Get the current feature set from the plugin config.
-getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet
-getFeatureSet extras = do
+-- | Get the the plugin config
+getTacticConfig :: MonadLsp Plugin.Config m => ShakeExtras -> m Config
+getTacticConfig extras = do
   pcfg <- getPluginConfig extras "tactics"
   pure $ case fromJSON $ Object $ plcConfig pcfg of
-    Success cfg -> cfg_feature_set cfg
-    Error _     -> defaultFeatures
+    Success cfg -> cfg
+    Error _     -> emptyConfig
+
+
+------------------------------------------------------------------------------
+-- | Get the current feature set from the plugin config.
+getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet
+getFeatureSet  = fmap cfg_feature_set . getTacticConfig
 
 
 getIdeDynflags

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE OverloadedStrings  #-}
 {-# LANGUAGE ViewPatterns       #-}
+{-# OPTIONS_GHC -Wall           #-}
 
 module Ide.Plugin.Tactic.LanguageServer.TacticProviders
   ( commandProvider
@@ -14,12 +15,14 @@ module Ide.Plugin.Tactic.LanguageServer.TacticProviders
 import           Control.Monad
 import           Control.Monad.Error.Class    (MonadError (throwError))
 import           Data.Aeson
+import           Data.Bool (bool)
 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           DataCon (dataConName)
 import           Development.IDE.GHC.Compat
 import           GHC.Generics
 import           GHC.LanguageExtensions.Type  (Extension (LambdaCase))
@@ -47,6 +50,7 @@ commandTactic Destruct               = useNameFromHypothesis destruct
 commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
+commandTactic UseDataCon             = userSplit
 
 
 ------------------------------------------------------------------------------
@@ -71,14 +75,34 @@ commandProvider HomomorphismLambdaCase =
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
+commandProvider UseDataCon =
+  withConfig $ \cfg ->
+    requireFeature FeatureUseDataCon $
+      filterTypeProjection
+          ( guardLength (<= cfg_max_use_ctor_actions cfg)
+          . fromMaybe []
+          . fmap fst
+          . tacticsGetDataCons
+          ) $ \dcon ->
+        provide UseDataCon
+          . T.pack
+          . occNameString
+          . occName
+          $ dataConName dcon
+
+
+------------------------------------------------------------------------------
+-- | Return an empty list if the given predicate doesn't hold over the length
+guardLength :: (Int -> Bool) -> [a] -> [a]
+guardLength f as = bool [] as $ f $ length as
 
 
 ------------------------------------------------------------------------------
 -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
 -- UI.
 type TacticProvider
      = DynFlags
-    -> FeatureSet
+    -> Config
     -> PluginId
     -> Uri
     -> Range
@@ -99,28 +123,28 @@ data TacticParams = TacticParams
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- 'Feature' is in the feature set.
 requireFeature :: Feature -> TacticProvider -> TacticProvider
-requireFeature f tp dflags fs plId uri range jdg = do
-  guard $ hasFeature f fs
-  tp dflags fs plId uri range jdg
+requireFeature f tp dflags cfg plId uri range jdg = do
+  guard $ hasFeature f $ cfg_feature_set cfg
+  tp dflags cfg plId uri range jdg
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 requireExtension :: Extension -> TacticProvider -> TacticProvider
-requireExtension ext tp dflags fs plId uri range jdg =
+requireExtension ext tp dflags cfg plId uri range jdg =
   case xopt ext dflags of
-    True  -> tp dflags fs plId uri range jdg
+    True  -> tp dflags cfg plId uri range jdg
     False -> pure []
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp dflags fs plId uri range jdg =
+filterGoalType p tp dflags cfg plId uri range jdg =
   case p $ unCType $ jGoal jdg of
-    True  -> tp dflags fs plId uri range jdg
+    True  -> tp dflags cfg plId uri range jdg
     False -> pure []
 
 
@@ -131,16 +155,34 @@ filterBindingType
     :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
-filterBindingType p tp dflags fs plId uri range jdg =
+filterBindingType p tp dflags cfg plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
    in fmap join $ for (unHypothesis hy) $ \hi ->
         let ty = unCType $ hi_type hi
          in case p (unCType g) ty of
-              True  -> tp (hi_name hi) ty dflags fs plId uri range jdg
+              True  -> tp (hi_name hi) ty dflags cfg plId uri range jdg
               False -> 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 p tp dflags cfg plId uri range jdg =
+  fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
+      tp a dflags cfg plId uri range jdg
+
+
+------------------------------------------------------------------------------
+-- | Get access to the 'Config' when building a 'TacticProvider'.
+withConfig :: (Config -> TacticProvider) -> TacticProvider
+withConfig tp dflags cfg plId uri range jdg = tp cfg dflags cfg plId uri range jdg
+
+
 
 ------------------------------------------------------------------------------
 -- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
@@ -174,7 +216,6 @@ tcCommandId :: TacticCommand -> CommandId
 tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
 
 
-
 ------------------------------------------------------------------------------
 -- | We should show homos only when the goal type is the same as the binding
 -- type, and that both are usual algebraic types.

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs

@@ -31,7 +31,7 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
-import           Name (occNameString)
+import           Name (occNameString, occName)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
@@ -197,10 +197,9 @@ splitAuto :: TacticsM ()
 splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
   jdg <- goal
   let g = jGoal jdg
-  case splitTyConApp_maybe $ unCType g of
+  case tacticsGetDataCons $ unCType g of
     Nothing -> throwError $ GoalMismatch "split" g
-    Just (tc, _) -> do
-      let dcs = tyConDataCons tc
+    Just (dcs, _) -> do
       case isSplitWhitelisted jdg of
         True -> choice $ fmap splitDataCon dcs
         False -> do
@@ -222,18 +221,36 @@ requireNewHoles m = do
 
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
+--
+-- INVARIANT: Assumes the give datacon is appropriate to construct the type
+-- with.
 splitDataCon :: DataCon -> TacticsM ()
 splitDataCon dc =
   requireConcreteHole $ tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
     let g = jGoal jdg
     case splitTyConApp_maybe $ unCType g of
       Just (tc, apps) -> do
-        case elem dc $ tyConDataCons tc of
-          True  -> buildDataCon (unwhitelistingSplit jdg) dc apps
-          False -> throwError $ IncorrectDataCon dc
+        buildDataCon (unwhitelistingSplit jdg) dc apps
       Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
 
+------------------------------------------------------------------------------
+-- | User-facing tactic to implement "Use constructor <x>"
+userSplit :: OccName -> TacticsM ()
+userSplit occ = do
+  jdg <- goal
+  let g = jGoal jdg
+  -- TODO(sandy): It's smelly that we need to find the datacon to generate the
+  -- code action, send it as a string, and then look it up again. Can we push
+  -- this over LSP somehow instead?
+  case splitTyConApp_maybe $ unCType g of
+    Just (tc, apps) -> do
+      case find (sloppyEqOccName occ . occName . dataConName)
+             $ tyConDataCons tc of
+        Just dc -> splitDataCon dc
+        Nothing -> throwError $ NotInScope occ
+
+
 ------------------------------------------------------------------------------
 -- | @matching f@ takes a function from a judgement to a @Tactic@, and
 -- then applies the resulting @Tactic@.