Add "Split all function arguments" code action

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

@@ -22,7 +22,8 @@ import qualified Data.Text  as T
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
 data Feature
-  = FeatureUseDataCon
+  = FeatureDestructAll
+  | FeatureUseDataCon
   | FeatureRefineHole
   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

@@ -50,6 +50,7 @@ commandTactic Destruct               = useNameFromHypothesis destruct
 commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
+commandTactic DestructAll            = const destructAll
 commandTactic UseDataCon             = userSplit
 commandTactic Refine                 = const refine
 
@@ -76,6 +77,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
 commandProvider UseDataCon =
   withConfig $ \cfg ->
     requireFeature FeatureUseDataCon $
@@ -153,6 +160,14 @@ filterGoalType p tp dflags cfg 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

@@ -256,6 +256,24 @@ splitDataCon dc =
 
 
 ------------------------------------------------------------------------------
+-- | 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
+
+--------------------------------------------------------------------------------
 -- | User-facing tactic to implement "Use constructor <x>"
 userSplit :: OccName -> TacticsM ()
 userSplit occ = do

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

@@ -19,6 +19,7 @@ data TacticCommand
   | Homomorphism
   | DestructLambdaCase
   | HomomorphismLambdaCase
+  | DestructAll
   | UseDataCon
   | Refine
   deriving (Eq, Ord, Show, Enum, Bounded)
@@ -31,6 +32,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"
 tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
 tacticTitle Refine _                 = "Refine hole"
 

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

@@ -73,6 +73,34 @@ spec = do
 
   let goldenTest = mkGoldenTest allFeatures
 
+  -- 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
+
+
   -- test via:
   -- stack test hls-tactics-plugin --test-arguments '--match "Golden/use constructor/"'
   describe "use constructor" $ do
@@ -115,7 +143,6 @@ spec = do
       refineTest "RefineReader.hs" 4 8
       refineTest "RefineGADT.hs"   8 8
 
-
   describe "golden tests" $ do
     let autoTest = mkGoldenTest allFeatures Auto ""
 

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 = _