implement isovector#21 : splitting on datatype

One code action per datatype constructor is produced.

Author: WorldSEnder

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,9 @@ commandProvider Auto  = provide Auto ""
 commandProvider Intros =
   filterGoalType isFunction $
     provide Intros ""
+commandProvider Split =
+  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 +114,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 +190,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 +272,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 +281,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
+  jdg <- goal
+  let g = jGoal jdg
+  case splitTyConApp_maybe $ unCType g of
+    Nothing -> throwError $ GoalMismatch ("splitDataCon'" ++ unsafeRender dcn) g
+    Just (tc, _) -> do
+      let dcs = tyConDataCons tc
+          mdc = find ((== dcn) . getOccName) dcs
+      case mdc of
+        Nothing -> throwError $ GoalMismatch ("splitDataCon'" ++ unsafeRender dcn) 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

@@ -80,6 +80,11 @@ tests = testGroup
       "T3.hs" 7 13
       [ (id, DestructLambdaCase, "")
       ]
+  , mkTest
+      "Produces datatype split actions"
+      "T2.hs" 16 14
+      [ (id, Split, "T")
+      ]
   , mkTest
       "Doesn't suggest lambdacase without -XLambdaCase"
       "T2.hs" 11 25

test/testdata/tactic/T2.hs

@@ -10,3 +10,7 @@ foo  = _
 dontSuggestLambdaCase :: Either a b -> Int
 dontSuggestLambdaCase = _
 
+data T = T !(Int, Int)
+
+suggestCon :: T
+suggestCon = _