Correctly split non-varpats in tactics

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

@@ -9,7 +9,6 @@ module Ide.Plugin.Tactic.CaseSplit
   , splitToDecl
   ) where
 
-import           Control.Lens
 import           Data.Bool (bool)
 import           Data.Data
 import           Data.Generics
@@ -37,13 +36,9 @@ mkFirstAgda pats body = AgdaMatch pats body
 -- splitting it into multiple matches: one for each alternative of the case.
 agdaSplit :: AgdaMatch -> [AgdaMatch]
 agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do
-  (i, pat) <- zip [id @Int 0 ..] pats
-  case pat of
-    VarPat _ (L _ patname) | eqRdrName patname var -> do
-      (case_pat, body) <- matches
-      -- TODO(sandy): use an at pattern if necessary
-      pure $ AgdaMatch (pats & ix i .~ case_pat) body
-    _ -> []
+  (pat, body) <- matches
+  -- TODO(sandy): use an at pattern if necessary
+  pure $ AgdaMatch (rewriteVarPat var pat pats) body
 agdaSplit x = [x]
 
 
@@ -63,6 +58,14 @@ wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case
   (x :: Pat GhcPs) -> x
 
 
+------------------------------------------------------------------------------
+-- | Replace a 'VarPat' with the given @'Pat' GhcPs@.
+rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a
+rewriteVarPat name rep = everywhere $ mkT $ \case
+  VarPat _ (L _ var) | eqRdrName name var -> rep
+  (x :: Pat GhcPs) -> x
+
+
 ------------------------------------------------------------------------------
 -- | Construct an 'HsDecl' from a set of 'AgdaMatch'es.
 splitToDecl

test/functional/Tactic.hs

@@ -128,6 +128,7 @@ tests = testGroup
   , goldenTest "FmapJoin.hs"                2 14 Auto ""
   , goldenTest "Fgmap.hs"                   2 9  Auto ""
   , goldenTest "FmapJoinInLet.hs"           4 19 Auto ""
+  , goldenTest "SplitPattern.hs"            7 25 Destruct "a"
   ]
 
 

test/testdata/tactic/SplitPattern.hs

@@ -0,0 +1,8 @@
+data ADT = One | Two Int | Three | Four Bool ADT | Five
+
+case_split :: ADT -> Int
+case_split One = _
+case_split (Two i) = _
+case_split Three = _
+case_split (Four b a) = _
+case_split Five = _

test/testdata/tactic/SplitPattern.hs.expected

@@ -0,0 +1,12 @@
+data ADT = One | Two Int | Three | Four Bool ADT | Five
+
+case_split :: ADT -> Int
+case_split One = _
+case_split (Two i) = _
+case_split Three = _
+case_split (Four b One) = _
+case_split (Four b (Two i)) = _
+case_split (Four b Three) = _
+case_split (Four b (Four b2 a3)) = _
+case_split (Four b Five) = _
+case_split Five = _