Add "Refine hole" code action (#1463)

* Implement "use constructor" code action

* Haddock

* Make use ctor actions configurable

* Undo more stupid formatting

* Use loose parsing for config

* Only show unifiable ctors

* Don't use guard in IO

Missing features were accidentally blocking all code actions

* Push data con matching into tacticsGetDataCons

* Implement a refine tactic for Reed

* Implement a refine tactic for Reed

Author: isovector

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

@@ -144,6 +144,7 @@ mkWorkspaceEdits
     -> Either ResponseError (Maybe WorkspaceEdit)
 mkWorkspaceEdits span dflags ccs uri pm rtr = do
   for_ (rtr_other_solns rtr) $ traceMX "other solution"
+  traceMX "solution" $ rtr_extract rtr
   let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags ccs uri g pm
    in case response of

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

@@ -21,7 +21,9 @@ import qualified Data.Text  as T
 ------------------------------------------------------------------------------
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
-data Feature = FeatureUseDataCon
+data Feature
+  = FeatureUseDataCon
+  | FeatureRefineHole
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 

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

@@ -84,11 +84,12 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
 tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons ty =
+tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =
   splitTyConApp_maybe ty <&> \(tc, apps) ->
     ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
     , apps
     )
+tacticsGetDataCons _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh

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

@@ -51,6 +51,7 @@ commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 commandTactic UseDataCon             = userSplit
+commandTactic Refine                 = const refine
 
 
 ------------------------------------------------------------------------------
@@ -89,6 +90,9 @@ commandProvider UseDataCon =
           . occNameString
           . occName
           $ dataConName dcon
+commandProvider Refine =
+  requireFeature FeatureRefineHole $
+    provide Refine ""
 
 
 ------------------------------------------------------------------------------

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

@@ -207,6 +207,19 @@ splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
             splitDataCon dc
 
 
+------------------------------------------------------------------------------
+-- | Like 'split', but only works if there is a single matching data
+-- constructor for the goal.
+splitSingle :: TacticsM ()
+splitSingle = tracing "splitSingle" $ do
+  jdg <- goal
+  let g = jGoal jdg
+  case tacticsGetDataCons $ unCType g of
+    Just ([dc], _) -> do
+      splitDataCon dc
+    _ -> throwError $ GoalMismatch "splitSingle" g
+
+
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
 -- have a different goal than current goal.
@@ -268,6 +281,17 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
+refine :: TacticsM ()
+refine = go 3
+  where
+    go 0 = pure ()
+    go n = do
+      let try_that_doesnt_suck t = commit t $ pure ()
+      try_that_doesnt_suck intros
+      try_that_doesnt_suck splitSingle
+      go $ n - 1
+
+
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do

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

@@ -20,6 +20,7 @@ data TacticCommand
   | DestructLambdaCase
   | HomomorphismLambdaCase
   | UseDataCon
+  | Refine
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -31,6 +32,7 @@ tacticTitle Homomorphism var         = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _     = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
 tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
+tacticTitle Refine _                 = "Refine hole"
 
 
 ------------------------------------------------------------------------------

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

@@ -105,6 +105,17 @@ spec = do
       useTest "Left"  "UseConLeft.hs"  2 8
       useTest "Right" "UseConRight.hs" 2 8
 
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/refine/"'
+  describe "refine" $ do
+    let refineTest = mkGoldenTest allFeatures Refine ""
+    describe "golden" $ do
+      refineTest "RefineIntro.hs"  2 8
+      refineTest "RefineCon.hs"    2 8
+      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/RefineCon.hs

@@ -0,0 +1,3 @@
+test :: ((), (b, c), d)
+test = _
+

plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected

@@ -0,0 +1,3 @@
+test :: ((), (b, c), d)
+test = ((), (_, _), _)
+

plugins/hls-tactics-plugin/test/golden/RefineGADT.hs

@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  One :: (b -> Int) -> GADT Int
+  Two :: GADT Bool
+
+test :: z -> GADT Int
+test = _
+