Agda-style case splitting for tactics

ghcide/src/Development/IDE/GHC/ExactPrint.hs

@@ -1,9 +1,10 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP                #-}
 {-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE RankNTypes         #-}
+{-# LANGUAGE TupleSections      #-}
+{-# LANGUAGE TypeFamilies       #-}
 
 module Development.IDE.GHC.ExactPrint
     ( Graft(..),
@@ -15,6 +16,8 @@ module Development.IDE.GHC.ExactPrint
       hoistGraft,
       graftWithM,
       graftWithSmallestM,
+      graftSmallestDecls,
+      graftSmallestDeclsWithM,
       transform,
       transformM,
       useAnnotatedSource,
@@ -60,9 +63,16 @@ import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities)
 import Outputable (Outputable, ppr, showSDoc)
 import Retrie.ExactPrint hiding (parseDecl, parseExpr, parsePattern, parseType)
 import Parser (parseIdentifier)
+import Data.List (isPrefixOf)
+import Data.Traversable (for)
 #if __GLASGOW_HASKELL__ == 808
 import Control.Arrow
 #endif
+#if __GLASGOW_HASKELL__ > 808
+import Bag (listToBag)
+import ErrUtils (mkErrMsg)
+import Outputable (text, neverQualify)
+#endif
 
 
 ------------------------------------------------------------------------------
@@ -202,6 +212,71 @@ graftWithoutParentheses dst val = Graft $ \dflags a -> do
             )
             a
 
+
+------------------------------------------------------------------------------
+-- | 'parseDecl' fails to parse decls that span multiple lines at the top
+-- layout --- eg. things like:
+--
+-- @
+-- not True = False
+-- not False = True
+-- @
+--
+-- This function splits up each top-layout declaration, parses them
+-- individually, and then merges them back into a single decl.
+parseDecls :: DynFlags -> FilePath -> String -> ParseResult (LHsDecl GhcPs)
+parseDecls dflags fp str = do
+  let mono_decls = fmap unlines $ groupByFirstLine $ lines str
+  decls <-
+    for (zip [id @Int 0..] mono_decls) $ \(ix, line) ->
+      parseDecl dflags (fp <> show ix) line
+  mergeDecls decls
+
+
+------------------------------------------------------------------------------
+-- | Combine decls together. See 'parseDecl' for more information.
+mergeDecls :: [(Anns, LHsDecl GhcPs)] -> ParseResult (LHsDecl GhcPs)
+mergeDecls [x] = pure x
+mergeDecls ((anns,  L _ (ValD ext fb@FunBind{fun_matches = mg@MG {mg_alts = L _ alts}}))
+          -- Since 'groupByFirstLine' separates matches, we are guaranteed to
+          -- only have a single alternative here. We want to add it to 'alts'
+          -- above.
+          : (anns', L _ (ValD _ FunBind{fun_matches = MG {mg_alts = L _ [alt]}}))
+          : decls) =
+  mergeDecls $
+    ( anns <> setPrecedingLines alt 1 0 anns'
+    , noLoc $ ValD ext $ fb
+        { fun_matches = mg { mg_alts = noLoc $ alts <> [alt] }
+        }
+    ) : decls
+mergeDecls _ = throwParseError "mergeDecls: attempted to merge something that wasn't a ValD FunBind"
+
+
+throwParseError :: String -> ParseResult a
+#if __GLASGOW_HASKELL__ > 808
+throwParseError
+  = Left . listToBag . pure . mkErrMsg unsafeGlobalDynFlags noSrcSpan neverQualify . text
+#else
+throwParseError = Left . (noSrcSpan, )
+#endif
+
+
+------------------------------------------------------------------------------
+-- | Groups strings by the Haskell top-layout rules, assuming each element of
+-- the list corresponds to a line. For example, the list
+--
+-- @["a", " a1", " a2", "b", " b1"]@
+--
+-- will be grouped to
+--
+-- @[["a", " a1", " a2"], ["b", " b1"]]@
+groupByFirstLine :: [String] -> [[String]]
+groupByFirstLine [] = []
+groupByFirstLine (str : strs) =
+  let (same, diff) = span (isPrefixOf " ") strs
+   in (str : same) : groupByFirstLine diff
+
+
 ------------------------------------------------------------------------------
 
 graftWithM ::
@@ -271,6 +346,44 @@ graftDecls dst decs0 = Graft $ \dflags a -> do
             | otherwise = DL.singleton (L src e) <> go rest
     modifyDeclsT (pure . DL.toList . go) a
 
+graftSmallestDecls ::
+    forall a.
+    (HasDecls a) =>
+    SrcSpan ->
+    [LHsDecl GhcPs] ->
+    Graft (Either String) a
+graftSmallestDecls dst decs0 = Graft $ \dflags a -> do
+    decs <- forM decs0 $ \decl -> do
+        (anns, decl') <- annotateDecl dflags decl
+        modifyAnnsT $ mappend anns
+        pure decl'
+    let go [] = DL.empty
+        go (L src e : rest)
+            | dst `isSubspanOf` src = DL.fromList decs <> DL.fromList rest
+            | otherwise = DL.singleton (L src e) <> go rest
+    modifyDeclsT (pure . DL.toList . go) a
+
+graftSmallestDeclsWithM ::
+    forall a.
+    (HasDecls a) =>
+    SrcSpan ->
+    (LHsDecl GhcPs -> TransformT (Either String) (Maybe [LHsDecl GhcPs])) ->
+    Graft (Either String) a
+graftSmallestDeclsWithM dst toDecls = Graft $ \dflags a -> do
+    let go [] = pure DL.empty
+        go (e@(L src _) : rest)
+            | dst `isSubspanOf` src = toDecls e >>= \case
+                Just decs0 -> do
+                    decs <- forM decs0 $ \decl -> do
+                        (anns, decl') <-
+                            annotateDecl dflags decl
+                        modifyAnnsT $ mappend anns
+                        pure decl'
+                    pure $ DL.fromList decs <> DL.fromList rest
+                Nothing -> (DL.singleton e <>) <$> go rest
+            | otherwise = (DL.singleton e <>) <$> go rest
+    modifyDeclsT (fmap DL.toList . go) a
+
 graftDeclsWithM ::
     forall a m.
     (HasDecls a, Fail.MonadFail m) =>
@@ -358,7 +471,7 @@ annotateDecl :: DynFlags -> LHsDecl GhcPs -> TransformT (Either String) (Anns, L
 annotateDecl dflags ast = do
     uniq <- show <$> uniqueSrcSpanT
     let rendered = render dflags ast
-    (anns, expr') <- lift $ mapLeft show $ parseDecl dflags uniq rendered
+    (anns, expr') <- lift $ mapLeft show $ parseDecls dflags uniq rendered
     let anns' = setPrecedingLines expr' 1 0 anns
     pure (anns', expr')
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

@@ -24,6 +24,7 @@ library
   exposed-modules:
     Ide.Plugin.Tactic
     Ide.Plugin.Tactic.Auto
+    Ide.Plugin.Tactic.CaseSplit
     Ide.Plugin.Tactic.CodeGen
     Ide.Plugin.Tactic.CodeGen.Utils
     Ide.Plugin.Tactic.Context