Split tactic for datatypes

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

@@ -20,6 +20,7 @@ import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Coerce
+import qualified Data.Foldable as F
 import qualified Data.Map as M
 import           Data.Maybe
 import qualified Data.Set as S
@@ -92,6 +93,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
@@ -110,11 +115,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
 
@@ -185,6 +191,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.
@@ -259,7 +273,7 @@ judgementForHole state nfp range = do
 
 
 
-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
@@ -268,7 +282,6 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
         case runTactic ctx jdg
               $ tac
-              $ mkVarOcc
               $ T.unpack var_name of
           Left err ->
             pure $ (, Nothing)

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

@@ -3,6 +3,7 @@
 module Ide.Plugin.Tactic.GHC where
 
 import Data.Maybe (isJust)
+import DataCon
 import TcType
 import TyCoRep
 import TyCon
@@ -67,3 +68,11 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = 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

@@ -155,10 +155,9 @@ split :: TacticsM ()
 split = do
   jdg <- goal
   let g = jGoal jdg
-  case splitTyConApp_maybe $ unCType g of
+  case tyDataCons $ unCType g of
     Nothing -> throwError $ GoalMismatch "getGoalTyCon" g
-    Just (tc, _) -> do
-      let dcs = tyConDataCons tc
+    Just dcs -> do
       choice $ fmap splitDataCon dcs
 
 
@@ -175,6 +174,22 @@ splitDataCon dc = rule $ \jdg -> do
     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"

test/functional/Tactic.hs

@@ -21,6 +21,7 @@ import           Language.Haskell.LSP.Types (ApplyWorkspaceEditRequest, Position
 import           Test.Hls.Util
 import           Test.Tasty
 import           Test.Tasty.HUnit
+import Test.Tasty.ExpectedFailure (ignoreTestBecause)
 import           System.FilePath
 import System.Directory (doesFileExist)
 import Control.Monad (unless)
@@ -80,6 +81,27 @@ tests = testGroup
       "T3.hs" 7 13
       [ (id, DestructLambdaCase, "")
       ]
+  , ignoreTestBecause "Not implemented, see #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
@@ -95,6 +117,7 @@ tests = testGroup
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
   , goldenTest "GoldenGADTDestruct.hs"      7 17 Destruct "gadt"
   , goldenTest "GoldenGADTAuto.hs"          7 13 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 = _