From 0b3e3193332ef6b97a82e8ccf0a938f7b4db74c9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 22 Feb 2021 17:34:26 -0800
Subject: [PATCH] Successfully split non-varpats

---
 .../src/Ide/Plugin/Tactic/CaseSplit.hs        | 19 +++++++++++--------
 test/functional/Tactic.hs                     |  1 +
 test/testdata/tactic/SplitPattern.hs          |  8 ++++++++
 test/testdata/tactic/SplitPattern.hs.expected | 12 ++++++++++++
 4 files changed, 32 insertions(+), 8 deletions(-)
 create mode 100644 test/testdata/tactic/SplitPattern.hs
 create mode 100644 test/testdata/tactic/SplitPattern.hs.expected

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
index 04d0f9bb12..33bdefe811 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CaseSplit.hs
+++ b/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
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index 59835755c8..7282772042 100644
--- a/test/functional/Tactic.hs
+++ b/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"
   ]
 
 
diff --git a/test/testdata/tactic/SplitPattern.hs b/test/testdata/tactic/SplitPattern.hs
new file mode 100644
index 0000000000..952b8e3476
--- /dev/null
+++ b/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 = _
diff --git a/test/testdata/tactic/SplitPattern.hs.expected b/test/testdata/tactic/SplitPattern.hs.expected
new file mode 100644
index 0000000000..720b6fe3c4
--- /dev/null
+++ b/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 = _