It works as a code lens!

Author: isovector

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

@@ -1,7 +1,8 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE OverloadedLabels #-}
-{-# LANGUAGE TupleSections    #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE OverloadedLabels  #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections     #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module Wingman.CodeGen
   ( module Wingman.CodeGen
@@ -65,7 +66,7 @@ destructMatches f scrut t jdg = do
               args = conLikeInstOrigArgTys' con apps
           modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
           subst <- gets ts_unifier
-          names <- mkManyGoodNames (hyNamesInScope hy) args
+          let names = mkManyGoodNames (hyNamesInScope hy) args
           let hy' = patternHypothesis scrut con jdg
                   $ zip names
                   $ coerce args
@@ -81,6 +82,20 @@ destructMatches f scrut t jdg = do
             & #syn_val     %~ match [mkDestructPat con names] . unLoc
 
 
+destructionFor :: Hypothesis a -> Type -> Maybe [RawMatch]
+destructionFor hy t = do
+  case tacticsGetDataCons t of
+    Nothing -> Nothing
+    Just ([], _) -> Nothing
+    Just (dcs, apps) -> do
+      for dcs $ \dc -> do
+        let con = RealDataCon dc
+            args = conLikeInstOrigArgTys' con apps
+            names = mkManyGoodNames (hyNamesInScope hy) args
+        pure $ match [mkDestructPat con names] $ var "_"
+
+
+
 ------------------------------------------------------------------------------
 -- | Produces a pattern for a data con and the names of its fields.
 mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs

plugins/hls-tactics-plugin/src/Wingman/Naming.hs

@@ -77,12 +77,12 @@ mkGoodName in_scope t =
 ------------------------------------------------------------------------------
 -- | Like 'mkGoodName' but creates several apart names.
 mkManyGoodNames
-  :: (Traversable t, Monad m)
+  :: (Traversable t)
   => Set OccName
   -> t Type
-  -> m (t OccName)
+  -> t OccName
 mkManyGoodNames in_scope args =
-  flip evalStateT in_scope $ for args $ \at -> do
+  flip evalState in_scope $ for args $ \at -> do
     in_scope <- get
     let n = mkGoodName in_scope at
     modify $ S.insert n

plugins/hls-tactics-plugin/src/Wingman/Plugin.hs

@@ -15,8 +15,11 @@ import           Data.Aeson
 import           Data.Bifunctor (first)
 import           Data.Data
 import           Data.Foldable (for_)
+import           Data.Functor ((<&>))
+import qualified Data.HashMap.Strict as HM
 import           Data.Maybe
 import qualified Data.Text as T
+import           Development.IDE (realSrcSpanToRange)
 import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent)
 import           Development.IDE.GHC.Compat
@@ -36,9 +39,8 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
-import Data.Functor ((<&>))
-import Development.IDE (srcSpanToRange, realSrcSpanToRange)
-import qualified Data.HashMap.Strict as HM
+import Wingman.CodeGen (destructionFor)
+import GHC.SourceGen (case', var)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -76,15 +78,16 @@ completionProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
         holes <- completionForHole  state nfp $ cfg_feature_set cfg
         traceMX "found holes" holes
         pure $ Right $ List $ holes <&> \(ss, ty) ->
-          let range = realSrcSpanToRange $ unTrack ss
+          let range@(Range _ ep) = realSrcSpanToRange $ unTrack ss
+              rep_range = Range ep ep
            in CodeLens
                 range
                 (Just $ mkLspCommand plId
                   (CommandId "emptycase.complete")
-                  "Complete case constructors" $
+                  ("Complete case constructors (" <> T.pack (unsafeRender ty) <> ")") $
                     Just $ pure $ toJSON $
                       WorkspaceEdit
-                        (Just $ HM.singleton uri $ List $ pure $ TextEdit range $ T.pack $ unsafeRender ty)
+                        (Just $ HM.singleton uri $ List $ pure $ TextEdit rep_range $ T.pack $ mappend "\n" $ unlines $ drop 1 $ lines $ unsafeRender $ case' (var "_")  $ fromJust $ destructionFor mempty ty)
                         Nothing
                         Nothing
                 )

plugins/hls-tactics-plugin/src/Wingman/Tactics.hs

@@ -99,7 +99,7 @@ intros = rule $ \jdg -> do
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
-      vs <- mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
+      let vs = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
       let top_hole = isTopHole ctx jdg
           hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
           jdg' = introduce hy'