Implement "use constructor" code action

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/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,6 +75,25 @@ commandProvider HomomorphismLambdaCase =
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
+commandProvider UseDataCon =
+  requireFeature FeatureUseDataCon $
+    filterTypeProjection
+        ( guardLength (<= 5)
+        . 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
 
 
 ------------------------------------------------------------------------------
@@ -141,6 +164,17 @@ filterBindingType p tp dflags fs 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 fs plId uri range jdg =
+  fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
+      tp a dflags fs plId uri range jdg
+
 
 ------------------------------------------------------------------------------
 -- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
@@ -174,7 +208,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@.

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

@@ -17,6 +17,7 @@ data TacticCommand
   | Homomorphism
   | DestructLambdaCase
   | HomomorphismLambdaCase
+  | UseDataCon
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -27,6 +28,7 @@ tacticTitle Destruct var             = "Case split on " <> var
 tacticTitle Homomorphism var         = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _     = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
+tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/test/GoldenSpec.hs

@@ -8,26 +8,24 @@
 module GoldenSpec where
 
 import           Control.Applicative.Combinators (skipManyTill)
-import           Control.Lens                    hiding (failing, (<.>))
-import           Control.Monad                   (unless)
+import           Control.Lens hiding (failing, (<.>))
+import           Control.Monad (unless)
 import           Control.Monad.IO.Class
 import           Data.Aeson
-import           Data.Default                    (Default (def))
+import           Data.Default (Default (def))
 import           Data.Foldable
-import qualified Data.Map                        as M
+import qualified Data.Map as M
 import           Data.Maybe
-import           Data.Text                       (Text)
-import qualified Data.Text.IO                    as T
-import qualified Ide.Plugin.Config               as Plugin
-import           Ide.Plugin.Tactic.FeatureSet    (FeatureSet, allFeatures)
+import           Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+import qualified Ide.Plugin.Config as Plugin
+import           Ide.Plugin.Tactic.FeatureSet (FeatureSet, allFeatures)
 import           Ide.Plugin.Tactic.TestTypes
 import           Language.LSP.Test
 import           Language.LSP.Types
-import           Language.LSP.Types.Lens         hiding (actions, applyEdit,
-                                                  capabilities, executeCommand,
-                                                  id, line, message, name,
-                                                  rename, title)
-import           System.Directory                (doesFileExist)
+import           Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title)
+import           System.Directory (doesFileExist)
 import           System.FilePath
 import           Test.Hspec
 
@@ -73,9 +71,35 @@ spec = do
       [ (not, DestructLambdaCase, "")
       ]
 
+  let goldenTest = mkGoldenTest allFeatures
+
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/use constructor/"'
+  describe "use constructor" $ do
+    let useTest = mkGoldenTest allFeatures UseDataCon
+    describe "provider" $ do
+      mkTest
+        "Suggests all data cons for Either"
+        "ConProviders.hs" 3 6
+        [ (id, UseDataCon, "Left")
+        , (id, UseDataCon, "Right")
+        , (not, UseDataCon, ":")
+        , (not, UseDataCon, "[]")
+        , (not, UseDataCon, "C1")
+        ]
+      mkTest
+        "Suggests no data cons for big types"
+        "ConProviders.hs" 9 17 $ do
+          c <- [1 :: Int .. 10]
+          pure $ (not, UseDataCon, T.pack $ show c)
+
+    describe "golden" $ do
+      useTest "(,)"   "UseConPair.hs"  2 8
+      useTest "Left"  "UseConLeft.hs"  2 8
+      useTest "Right" "UseConRight.hs" 2 8
+
   describe "golden tests" $ do
-    let goldenTest = mkGoldenTest allFeatures
-        autoTest = mkGoldenTest allFeatures Auto ""
+    let autoTest = mkGoldenTest allFeatures Auto ""
 
     goldenTest Intros "" "GoldenIntros.hs" 2 8
     autoTest "GoldenEitherAuto.hs"        2 11
@@ -150,6 +174,7 @@ mkTest
     -> SpecWith (Arg Bool)
 mkTest name fp line col ts = it name $ do
   runSession testCommand fullCaps tacticPath $ do
+    setFeatureSet allFeatures
     doc <- openDoc fp "haskell"
     _ <- waitForDiagnostics
     actions <- getCodeActions doc $ pointRange line col

plugins/hls-tactics-plugin/test/golden/ConProviders.hs

@@ -0,0 +1,10 @@
+-- Should suggest Left and Right, but not []
+t1 :: Either a b
+t1 = _
+
+
+data ManyConstructors = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10
+
+noCtorsIfMany :: ManyConstructors
+noCtorsIfMany = _
+

plugins/hls-tactics-plugin/test/golden/UseConLeft.hs

@@ -0,0 +1,3 @@
+test :: Either a b
+test = _
+

plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected

@@ -0,0 +1,3 @@
+test :: Either a b
+test = Left _
+

plugins/hls-tactics-plugin/test/golden/UseConPair.hs

@@ -0,0 +1,2 @@
+test :: (a, b)
+test = _

plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected

@@ -0,0 +1,2 @@
+test :: (a, b)
+test = (_, _)

plugins/hls-tactics-plugin/test/golden/UseConRight.hs

@@ -0,0 +1,3 @@
+test :: Either a b
+test = _
+

plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected

@@ -0,0 +1,3 @@
+test :: Either a b
+test = Right _
+