Add "Split all function arguments" code action

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

@@ -90,7 +90,7 @@ codeActionProvider _ _ _ = pure $ Right $ List []
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
 tacticCmd tac state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      features <- getFeatureSet (shakeExtras state)
+      features <- getFeatureSet $ shakeExtras state
       ccs <- getClientCapabilities
       res <- liftIO $ fromMaybeT (Right Nothing) $ do
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range features

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

@@ -21,7 +21,8 @@ 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
+  = FeatureDestructAll
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 

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

@@ -295,6 +295,17 @@ hyNamesInScope :: Hypothesis a -> Set OccName
 hyNamesInScope = M.keysSet . hyByName
 
 
+------------------------------------------------------------------------------
+-- | Are there any top-level function argument bindings in this judgement?
+jHasBoundArgs :: Judgement' a -> Bool
+jHasBoundArgs
+  = not
+  . null
+  . filter (isTopLevel . hi_provenance)
+  . unHypothesis
+  . jLocalHypothesis
+
+
 ------------------------------------------------------------------------------
 -- | Fold a hypothesis into a single mapping from name to info. This
 -- unavoidably will cause duplicate names (things like methods) to shadow one

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
@@ -47,6 +48,7 @@ commandTactic Destruct               = useNameFromHypothesis destruct
 commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
+commandTactic DestructAll            = const destructAll
 
 
 ------------------------------------------------------------------------------
@@ -71,6 +73,12 @@ commandProvider HomomorphismLambdaCase =
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
+commandProvider DestructAll =
+  requireFeature FeatureDestructAll $
+    withJudgement $ \jdg ->
+      case _jIsTopHole jdg && jHasBoundArgs jdg of
+        True  -> provide DestructAll ""
+        False -> mempty
 
 
 ------------------------------------------------------------------------------
@@ -100,8 +108,9 @@ data TacticParams = TacticParams
 -- '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
+  case hasFeature f fs of
+    True  -> tp dflags fs plId uri range jdg
+    False -> pure []
 
 
 ------------------------------------------------------------------------------
@@ -124,6 +133,14 @@ filterGoalType p tp dflags fs plId uri range jdg =
     False -> pure []
 
 
+------------------------------------------------------------------------------
+-- | Restrict a 'TacticProvider', making sure it appears only when the given
+-- predicate holds for the goal.
+withJudgement :: (Judgement -> TacticProvider) -> TacticProvider
+withJudgement tp dflags fs plId uri range jdg =
+  tp jdg dflags fs plId uri range jdg
+
+
 ------------------------------------------------------------------------------
 -- | Multiply a 'TacticProvider' for each binding, making sure it appears only
 -- when the given predicate holds over the goal and binding types.

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

@@ -234,6 +234,25 @@ splitDataCon dc =
       Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
 
+------------------------------------------------------------------------------
+-- | Perform a case split on each top-level argument. Used to implement the
+-- "Destruct all function arguments" action.
+destructAll :: TacticsM ()
+destructAll = do
+  jdg <- goal
+  let args = fmap fst
+           $ sortOn (Down . snd)
+           $ mapMaybe (\(hi, prov) ->
+              case prov of
+                TopLevelArgPrv _ idx _ -> pure (hi, idx)
+                _ -> Nothing
+                )
+           $ fmap (\hi -> (hi, hi_provenance hi))
+           $ unHypothesis
+           $ jHypothesis jdg
+  for_ args destruct
+
+
 ------------------------------------------------------------------------------
 -- | @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
+  | DestructAll
   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 DestructAll _            = "Split all function arguments"
 
 
 ------------------------------------------------------------------------------

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

@@ -73,6 +73,34 @@ spec = do
       [ (not, DestructLambdaCase, "")
       ]
 
+
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/destruct all/"'
+  describe "destruct all" $ do
+    let destructAllTest = mkGoldenTest allFeatures DestructAll ""
+    describe "provider" $ do
+      mkTest
+        "Requires args on lhs of ="
+        "DestructAllProvider.hs" 3 21
+        [ (not, DestructAll, "")
+        ]
+      mkTest
+        "Can't be a non-top-hole"
+        "DestructAllProvider.hs" 8 19
+        [ (not, DestructAll, "")
+        , (id, Destruct, "a")
+        , (id, Destruct, "b")
+        ]
+      mkTest
+        "Provides a destruct all otherwise"
+        "DestructAllProvider.hs" 12 22
+        [ (id, DestructAll, "")
+        ]
+
+    describe "golden" $ do
+      destructAllTest "DestructAllAnd.hs"  2 11
+      destructAllTest "DestructAllMany.hs" 4 23
+
   describe "golden tests" $ do
     let goldenTest = mkGoldenTest allFeatures
         autoTest = mkGoldenTest allFeatures Auto ""
@@ -150,6 +178,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/DestructAllAnd.hs

@@ -0,0 +1,2 @@
+and :: Bool -> Bool -> Bool
+and x y = _

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

@@ -0,0 +1,5 @@
+and :: Bool -> Bool -> Bool
+and False False = _
+and True False = _
+and False True = _
+and True True = _

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

@@ -0,0 +1,4 @@
+data ABC = A | B | C
+
+many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()
+many u e b mabc abc = _

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

@@ -0,0 +1,27 @@
+data ABC = A | B | C
+
+many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()
+many () (Left a) False Nothing A = _
+many () (Right b5) False Nothing A = _
+many () (Left a) True Nothing A = _
+many () (Right b5) True Nothing A = _
+many () (Left a6) False (Just a) A = _
+many () (Right b6) False (Just a) A = _
+many () (Left a6) True (Just a) A = _
+many () (Right b6) True (Just a) A = _
+many () (Left a) False Nothing B = _
+many () (Right b5) False Nothing B = _
+many () (Left a) True Nothing B = _
+many () (Right b5) True Nothing B = _
+many () (Left a6) False (Just a) B = _
+many () (Right b6) False (Just a) B = _
+many () (Left a6) True (Just a) B = _
+many () (Right b6) True (Just a) B = _
+many () (Left a) False Nothing C = _
+many () (Right b5) False Nothing C = _
+many () (Left a) True Nothing C = _
+many () (Right b5) True Nothing C = _
+many () (Left a6) False (Just a) C = _
+many () (Right b6) False (Just a) C = _
+many () (Left a6) True (Just a) C = _
+many () (Right b6) True (Just a) C = _

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

@@ -0,0 +1,12 @@
+-- we need to name the args ourselves first
+nothingToDestruct :: [a] -> [a] -> [a]
+nothingToDestruct = _
+
+
+-- can't destruct all for non-top-level holes
+notTop :: Bool -> Bool -> Bool
+notTop a b = a && _
+
+-- destruct all is ok
+canDestructAll :: Bool -> Bool -> Bool
+canDestructAll a b = _