Wingman: "Intro and destruct" code action (#2077)

* Make intros' more configurable

* Add a new "introduce and destruct" code action

* Add tests

* Add provider tests

Author: isovector

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

@@ -129,6 +129,7 @@ test-suite tests
     CodeAction.DestructPunSpec
     CodeAction.DestructSpec
     CodeAction.IntrosSpec
+    CodeAction.IntroDestructSpec
     CodeAction.RefineSpec
     CodeAction.RunMetaprogramSpec
     CodeAction.UseDataConSpec

plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs

@@ -47,6 +47,7 @@ import           Wingman.Types
 commandTactic :: TacticCommand -> T.Text -> TacticsM ()
 commandTactic Auto                   = const auto
 commandTactic Intros                 = const intros
+commandTactic IntroAndDestruct       = const introAndDestruct
 commandTactic Destruct               = useNameFromHypothesis destruct . mkVarOcc . T.unpack
 commandTactic DestructPun            = useNameFromHypothesis destructPun . mkVarOcc . T.unpack
 commandTactic Homomorphism           = useNameFromHypothesis homo . mkVarOcc . T.unpack
@@ -64,6 +65,7 @@ commandTactic RunMetaprogram         = parseMetaprogram
 tacticKind :: TacticCommand -> T.Text
 tacticKind Auto                   = "fillHole"
 tacticKind Intros                 = "introduceLambda"
+tacticKind IntroAndDestruct       = "introduceAndDestruct"
 tacticKind Destruct               = "caseSplit"
 tacticKind DestructPun            = "caseSplitPun"
 tacticKind Homomorphism           = "homomorphicCaseSplit"
@@ -82,9 +84,10 @@ tacticKind RunMetaprogram         = "runMetaprogram"
 tacticPreferred :: TacticCommand -> Bool
 tacticPreferred Auto                   = True
 tacticPreferred Intros                 = True
+tacticPreferred IntroAndDestruct       = True
 tacticPreferred Destruct               = True
 tacticPreferred DestructPun            = False
-tacticPreferred Homomorphism           = False
+tacticPreferred Homomorphism           = True
 tacticPreferred DestructLambdaCase     = False
 tacticPreferred HomomorphismLambdaCase = False
 tacticPreferred DestructAll            = True
@@ -110,6 +113,10 @@ commandProvider Intros =
   requireHoleSort (== Hole) $
   filterGoalType isFunction $
     provide Intros ""
+commandProvider IntroAndDestruct =
+  requireHoleSort (== Hole) $
+  filterGoalType (liftLambdaCase False (\_ -> isJust . algebraicTyCon)) $
+    provide IntroAndDestruct ""
 commandProvider Destruct =
   requireHoleSort (== Hole) $
   filterBindingType destructFilter $ \occ _ ->

plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs

@@ -76,7 +76,7 @@ commands =
           ])
       (pure . \case
         []    -> intros
-        names -> intros' $ Just names
+        names -> intros' $ IntroduceOnlyNamed names
       )
       [ Example
           Nothing
@@ -100,7 +100,7 @@ commands =
 
   , command "intro" Deterministic (Bind One)
       "Construct a lambda expression, binding an argument with the given name."
-      (pure . intros' . Just . pure)
+      (pure . intros' . IntroduceOnlyNamed . pure)
       [ Example
           Nothing
           ["aye"]

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

@@ -117,21 +117,32 @@ restrictPositionForApplication f app = do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = intros' Nothing
+intros = intros' IntroduceAllUnnamed
+
+
+data IntroParams
+  = IntroduceAllUnnamed
+  | IntroduceOnlyNamed [OccName]
+  | IntroduceOnlyUnnamed Int
+  deriving stock (Eq, Ord, Show)
+
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros'
-    :: Maybe [OccName]  -- ^ When 'Nothing', generate a new name for every
-                        -- variable. Otherwise, only bind the variables named.
+    :: IntroParams
     -> TacticsM ()
-intros' names = rule $ \jdg -> do
+intros' params = rule $ \jdg -> do
   let g  = jGoal jdg
   case tacticsSplitFunTy $ unCType g of
     (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g
     (_, _, args, res) -> do
       ctx <- ask
-      let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names
+      let gen_names = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args
+          occs = case params of
+            IntroduceAllUnnamed -> gen_names
+            IntroduceOnlyNamed names -> names
+            IntroduceOnlyUnnamed n -> take n gen_names
           num_occs = length occs
           top_hole = isTopHole ctx jdg
           bindings = zip occs $ coerce args
@@ -148,6 +159,24 @@ intros' names = rule $ \jdg -> do
           & #syn_val   %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc
 
 
+------------------------------------------------------------------------------
+-- | Introduce a single lambda argument, and immediately destruct it.
+introAndDestruct :: TacticsM ()
+introAndDestruct = do
+  hy <- fmap unHypothesis $ hyDiff $ intros' $ IntroduceOnlyUnnamed 1
+  -- This case should never happen, but I'm validating instead of parsing.
+  -- Adding a log to be reminded if the invariant ever goes false.
+  --
+  -- But note that this isn't a game-ending bug. In the worst case, we'll
+  -- accidentally bind too many variables, and incorrectly unify between them.
+  -- Which means some GADT cases that should be eliminated won't be --- not the
+  -- end of the world.
+  unless (length hy == 1) $
+    traceMX "BUG: Introduced too many variables for introAndDestruct! Please report me if you see this! " hy
+
+  for_ hy destruct
+
+
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destructAuto :: HyInfo CType -> TacticsM ()

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

@@ -59,6 +59,7 @@ import Data.IORef
 data TacticCommand
   = Auto
   | Intros
+  | IntroAndDestruct
   | Destruct
   | DestructPun
   | Homomorphism
@@ -77,6 +78,7 @@ tacticTitle = (mappend "Wingman: " .) . go
   where
     go Auto _                   = "Attempt to fill hole"
     go Intros _                 = "Introduce lambda"
+    go IntroAndDestruct _       = "Introduce and destruct term"
     go Destruct var             = "Case split on " <> var
     go DestructPun var          = "Split on " <> var <> " with NamedFieldPuns"
     go Homomorphism var         = "Homomorphic case split on " <> var

plugins/hls-tactics-plugin/test/CodeAction/IntroDestructSpec.hs

@@ -0,0 +1,36 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module CodeAction.IntroDestructSpec where
+
+import Wingman.Types
+import Test.Hspec
+import Utils
+
+
+spec :: Spec
+spec = do
+  let test l c = goldenTest IntroAndDestruct "" l c
+               . mappend "IntroDestruct"
+
+  describe "golden" $ do
+    test 4  5 "One"
+    test 2  5 "Many"
+    test 4 11 "LetBinding"
+
+  describe "provider" $ do
+    mkTest
+      "Can intro and destruct an algebraic ty"
+      "IntroDestructProvider" 2 12
+      [ (id, IntroAndDestruct, "")
+      ]
+    mkTest
+      "Won't intro and destruct a non-algebraic ty"
+      "IntroDestructProvider" 5 12
+      [ (not, IntroAndDestruct, "")
+      ]
+    mkTest
+      "Can't intro, so no option"
+      "IntroDestructProvider" 8 17
+      [ (not, IntroAndDestruct, "")
+      ]
+

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

@@ -0,0 +1,6 @@
+test :: IO ()
+test = do
+  let x :: Bool -> Int
+      x False = _w0
+      x True = _w1
+  pure ()

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

@@ -0,0 +1,5 @@
+test :: IO ()
+test = do
+  let x :: Bool -> Int
+      x = _
+  pure ()

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

@@ -0,0 +1,4 @@
+x :: Bool -> Maybe Int -> String -> Int
+x False = _w0
+x True = _w1
+

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

@@ -0,0 +1,3 @@
+x :: Bool -> Maybe Int -> String -> Int
+x = _
+