Implement "split" tactic

hie.yaml.stack

@@ -23,7 +23,7 @@ cradle:
               component: "haskell-language-server:exe:haskell-language-server"
 
             - path: "./plugins/tactics/src"
-              component: "hls-tactics-plugin:lib:hls-tactics-plugin"
+              component: "hls-tactics-plugin:lib"
 
             - path: "./plugins/tactics/test"
               component: "hls-tactics-plugin:test:tests"

plugins/tactics/src/Ide/Plugin/Tactic.hs

@@ -26,6 +26,7 @@ import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
 import           Data.List
+import qualified Data.Foldable as F
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
@@ -103,6 +104,10 @@ commandProvider Auto  = provide Auto ""
 commandProvider Intros =
   filterGoalType isFunction $
     provide Intros ""
+commandProvider Split =
+  filterGoalType (isJust . algebraicTyCon) $
+    foldMapGoalType (F.fold . tyDataCons) $ \dc ->
+      provide Split $ T.pack $ occNameString $ getOccName dc
 commandProvider Destruct =
   filterBindingType destructFilter $ \occ _ ->
     provide Destruct $ T.pack $ occNameString occ
@@ -121,11 +126,12 @@ commandProvider HomomorphismLambdaCase =
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
-commandTactic :: TacticCommand -> OccName -> TacticsM ()
+commandTactic :: TacticCommand -> String -> TacticsM ()
 commandTactic Auto         = const auto
 commandTactic Intros       = const intros
-commandTactic Destruct     = destruct
-commandTactic Homomorphism = homo
+commandTactic Split        = splitDataCon' . mkDataOcc
+commandTactic Destruct     = destruct . mkVarOcc
+commandTactic Homomorphism = homo . mkVarOcc
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 
@@ -196,6 +202,14 @@ requireExtension ext tp dflags plId uri range jdg =
     False -> pure []
 
 
+------------------------------------------------------------------------------
+-- | Create a 'TacticProvider' for each occurance of an 'a' in the foldable container
+-- extracted from the goal type. Useful instantiations for 't' include 'Maybe' or '[]'.
+foldMapGoalType :: Foldable t => (Type -> t a) -> (a -> TacticProvider) -> TacticProvider
+foldMapGoalType f tpa dflags plId uri range jdg =
+  foldMap tpa (f $ unCType $ jGoal jdg) dflags plId uri range jdg
+
+
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
@@ -289,7 +303,7 @@ spliceProvenance provs =
     overProvenance (maybe id const $ M.lookup name provs) hi
 
 
-tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
+tacticCmd :: (String -> TacticsM ()) -> CommandFunction TacticParams
 tacticCmd tac lf state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right Null, Nothing) $ do
@@ -298,20 +312,19 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
         x <- lift $ timeout 2e8 $
           case runTactic ctx jdg
-                $ tac
-                $ mkVarOcc
-                $ T.unpack var_name of
-            Left err ->
-              pure $ (, Nothing)
-                $ Left
-                $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right rtr -> do
-              traceMX "solns" $ rtr_other_solns rtr
-              let g = graft (RealSrcSpan span) $ rtr_extract rtr
-                  response = transform dflags (clientCapabilities lf) uri g pm
-              pure $ case response of
-                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
-                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+                  $ tac
+                  $ T.unpack var_name of
+              Left err ->
+                pure $ (, Nothing)
+                  $ Left
+                  $ ResponseError InvalidRequest (T.pack $ show err) Nothing
+              Right rtr -> do
+                traceMX "solns" $ rtr_other_solns rtr
+                let g = graft (RealSrcSpan span) $ rtr_extract rtr
+                    response = transform dflags (clientCapabilities lf) uri g pm
+                pure $ case response of
+                  Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
+                  Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
         pure $ case x of
           Just y -> y
           Nothing -> (, Nothing)

plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs

@@ -6,6 +6,7 @@
 module Ide.Plugin.Tactic.GHC where
 
 import           Control.Monad.State
+import           DataCon
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
 import           Data.Traversable
@@ -148,3 +149,10 @@ getPatName (fromPatCompat -> p0) =
 #endif
     _             -> Nothing
 
+------------------------------------------------------------------------------
+-- | What data-constructor, if any, does the type have?
+tyDataCons :: Type -> Maybe [DataCon]
+tyDataCons g = do
+  (tc, _) <- splitTyConApp_maybe g
+  pure $ tyConDataCons tc
+

plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs

@@ -186,10 +186,9 @@ split :: TacticsM ()
 split = tracing "split(user)" $ do
   jdg <- goal
   let g = jGoal jdg
-  case splitTyConApp_maybe $ unCType g of
-    Nothing -> throwError $ GoalMismatch "split" g
-    Just (tc, _) -> do
-      let dcs = tyConDataCons tc
+  case tyDataCons $ unCType g of
+    Nothing -> throwError $ GoalMismatch "split(user)" g
+    Just dcs -> do
       choice $ fmap splitDataCon dcs
 
 
@@ -238,6 +237,22 @@ splitDataCon dc =
       Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
 
+------------------------------------------------------------------------------
+-- | Attempt to instantiate the named data constructor to solve the goal.
+splitDataCon' :: OccName -> TacticsM ()
+splitDataCon' dcn = do
+  let tacname = "splitDataCon'(" ++ unsafeRender dcn ++ ")"
+  jdg <- goal
+  let g = jGoal jdg
+  case tyDataCons $ unCType g of
+    Nothing -> throwError $ GoalMismatch tacname g
+    Just dcs -> do
+      let mdc = find ((== dcn) . getOccName) dcs
+      case mdc of
+        Nothing -> throwError $ GoalMismatch tacname g
+        Just dc -> splitDataCon dc
+
+
 ------------------------------------------------------------------------------
 -- | @matching f@ takes a function from a judgement to a @Tactic@, and
 -- then applies the resulting @Tactic@.

plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs

@@ -11,6 +11,7 @@ import qualified Data.Text as T
 data TacticCommand
   = Auto
   | Intros
+  | Split
   | Destruct
   | Homomorphism
   | DestructLambdaCase
@@ -21,6 +22,7 @@ data TacticCommand
 tacticTitle :: TacticCommand -> T.Text -> T.Text
 tacticTitle Auto _ = "Attempt to fill hole"
 tacticTitle Intros _ = "Introduce lambda"
+tacticTitle Split cname = "Introduce constructor " <> cname
 tacticTitle Destruct var = "Case split on " <> var
 tacticTitle Homomorphism var = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _ = "Lambda case split"

stack.yaml

@@ -0,0 +1 @@
+stack-8.6.5.yaml

test/functional/Tactic.hs

@@ -85,6 +85,27 @@ tests = testGroup
       "T3.hs" 7 13
       [ (id, DestructLambdaCase, "")
       ]
+  , ignoreTestBecause "Not implemented, see isovector/haskell-language-server#31" $ mkTest
+      "Splits Int with I# when -XMagicHash is enabled"
+      "T3.hs" 10 14
+      [ (id, Split, "I#")
+      ]
+  , mkTest
+      "Produces datatype split action for single-constructor types"
+      "T2.hs" 16 14
+      [ (id, Split, "T")
+      ]
+  , mkTest
+      "Produces datatype split action for multiple constructors"
+      "T2.hs" 21 15
+      [ (id, Split, "T21")
+      , (id, Split, "T22")
+      ]
+  , mkTest
+      "Doesn't suggest MagicHash constructors without -XMagicHash"
+      "T2.hs" 24 14
+      [ (not, Split, "I#")
+      ]
   , mkTest
       "Doesn't suggest lambdacase without -XLambdaCase"
       "T2.hs" 11 25
@@ -115,6 +136,7 @@ tests = testGroup
       $ goldenTest "GoldenApplicativeThen.hs"   2 11 Auto ""
   , goldenTest "GoldenSafeHead.hs"          2 12 Auto ""
   , expectFail "GoldenFish.hs"              5 18 Auto ""
+  , goldenTest "GoldenSplitPair.hs"         2 11 Split "(,)"
   ]
 
 

test/testdata/tactic/GoldenSplitPair.hs

@@ -0,0 +1,2 @@
+thePair :: (Int, Int)
+thePair = _

test/testdata/tactic/GoldenSplitPair.hs.expected

@@ -0,0 +1,2 @@
+thePair :: (Int, Int)
+thePair = (_, _)

test/testdata/tactic/T2.hs

@@ -10,3 +10,15 @@ foo  = _
 dontSuggestLambdaCase :: Either a b -> Int
 dontSuggestLambdaCase = _
 
+data T = T !(Int, Int)
+
+suggestCon :: T
+suggestCon = _
+
+data T2 = T21 Int | T22 Int Int
+
+suggestCons :: T2
+suggestCons = _
+
+suggestInt :: Int
+suggestInt = _

test/testdata/tactic/T3.hs

@@ -1,8 +1,10 @@
-{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LambdaCase, MagicHash #-}
 
 suggestHomomorphicLC :: Either a b -> Either a b
 suggestHomomorphicLC = _
 
 suggestLC :: Either a b -> Int
 suggestLC = _
 
+suggestInt :: Int
+suggestInt = _