Try a homomorphic destruct before a standard destruct (#1582)

* Try a homomorphic destruct before a standard destruct

* Add zip test

* Remove a debug trace

* Split out the attemptWhen combinator

Author: isovector

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

@@ -13,6 +13,7 @@ import           ConLike
 import           Control.Lens ((%~), (<>~), (&))
 import           Control.Monad.Except
 import           Control.Monad.State
+import           Data.Bool (bool)
 import           Data.Generics.Labels ()
 import           Data.List
 import           Data.Maybe (mapMaybe)
@@ -183,18 +184,19 @@ destructLambdaCase' f jdg = do
 ------------------------------------------------------------------------------
 -- | Construct a data con with subgoals for each field.
 buildDataCon
-    :: Judgement
+    :: Bool       -- Should we blacklist destruct?
+    -> Judgement
     -> ConLike            -- ^ The data con to build
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (Synthesized (LHsExpr GhcPs))
-buildDataCon jdg dc tyapps = do
+buildDataCon should_blacklist jdg dc tyapps = do
   let args = conLikeInstOrigArgTys' dc tyapps
   ext
       <- fmap unzipTrace
        $ traverse ( \(arg, n) ->
                     newSubgoal
                   . filterSameTypeFromOtherPositions dc n
-                  . blacklistingDestruct
+                  . bool id blacklistingDestruct should_blacklist
                   . flip withNewGoal jdg
                   $ CType arg
                   ) $ zip args [0..]

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

@@ -87,7 +87,7 @@ runTactic ctx jdg t =
               RunTacticResults
                 { rtr_trace = syn_trace syn
                 , rtr_extract = simplify $ syn_val syn
-                , rtr_other_solns = reverse . fmap fst $ take 5 sorted
+                , rtr_other_solns = reverse . fmap fst $ sorted
                 , rtr_jdg = jdg
                 , rtr_ctx = ctx
                 }
@@ -223,6 +223,16 @@ unify goal inst = do
     Nothing -> throwError (UnificationError inst goal)
 
 
+------------------------------------------------------------------------------
+-- | Prefer the first tactic to the second, if the bool is true. Otherwise, just run the second tactic.
+--
+-- This is useful when you have a clever pruning solution that isn't always
+-- applicable.
+attemptWhen :: TacticsM a -> TacticsM a -> Bool -> TacticsM a
+attemptWhen _  t2 False = t2
+attemptWhen t1 t2 True  = commit t1 t2
+
+
 ------------------------------------------------------------------------------
 -- | Get the class methods of a 'PredType', correctly dealing with
 -- instantiation of quantified class types.

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

@@ -139,7 +139,7 @@ mkWorkspaceEdits
     -> Either UserFacingMessage WorkspaceEdit
 mkWorkspaceEdits span dflags ccs uri pm rtr = do
   for_ (rtr_other_solns rtr) $ \soln -> do
-    traceMX "other solution" soln
+    traceMX "other solution" $ syn_val soln
     traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) []
   traceMX "solution" $ rtr_extract rtr
   let g = graftHole (RealSrcSpan span) rtr

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

@@ -108,7 +108,7 @@ intros = rule $ \jdg -> do
 destructAuto :: HyInfo CType -> TacticsM ()
 destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do
   jdg <- goal
-  let subtactic = rule $ destruct' (const subgoal) hi
+  let subtactic = destructOrHomoAuto hi
   case isPatternMatch $ hi_provenance hi of
     True ->
       pruning subtactic $ \jdgs ->
@@ -121,6 +121,25 @@ destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do
     False -> subtactic
 
 
+------------------------------------------------------------------------------
+-- | When running auto, in order to prune the auto search tree, we try
+-- a homomorphic destruct whenever possible. If that produces any results, we
+-- can probably just prune the other side.
+destructOrHomoAuto :: HyInfo CType -> TacticsM ()
+destructOrHomoAuto hi = tracing "destructOrHomoAuto" $ do
+  jdg <- goal
+  let g  = unCType $ jGoal jdg
+      ty = unCType $ hi_type hi
+
+  attemptWhen
+      (rule $ destruct' (\dc jdg ->
+        buildDataCon False jdg dc $ snd $ splitAppTys g) hi)
+      (rule $ destruct' (const subgoal) hi)
+    $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of
+        (Just (gtc, _), Just (tytc, _)) -> gtc == tytc
+        _ -> False
+
+
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destruct :: HyInfo CType -> TacticsM ()
@@ -132,7 +151,7 @@ destruct hi = requireConcreteHole $ tracing "destruct(user)" $
 -- | Case split, using the same data constructor in the matches.
 homo :: HyInfo CType -> TacticsM ()
 homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg ->
-  buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+  buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
 ------------------------------------------------------------------------------
@@ -147,7 +166,7 @@ homoLambdaCase :: TacticsM ()
 homoLambdaCase =
   tracing "homoLambdaCase" $
     rule $ destructLambdaCase' $ \dc jdg ->
-      buildDataCon jdg dc
+      buildDataCon False jdg dc
         . snd
         . splitAppTys
         . unCType
@@ -242,7 +261,7 @@ splitConLike dc =
     let g = jGoal jdg
     case splitTyConApp_maybe $ unCType g of
       Just (_, apps) -> do
-        buildDataCon (unwhitelistingSplit jdg) dc apps
+        buildDataCon True (unwhitelistingSplit jdg) dc apps
       Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
 ------------------------------------------------------------------------------

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

@@ -49,6 +49,7 @@ spec = do
     autoTest  9 12 "AutoEndo.hs"
     autoTest  2 16 "AutoEmptyString.hs"
     autoTest  7 35 "AutoPatSynUse.hs"
+    autoTest  2 28 "AutoZip.hs"
 
     failing "flaky in CI" $
       autoTest 2 11 "GoldenApplicativeThen.hs"

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

@@ -0,0 +1,3 @@
+zip_it_up_and_zip_it_out :: [a] -> [b] -> [(a, b)]
+zip_it_up_and_zip_it_out = _
+

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

@@ -0,0 +1,6 @@
+zip_it_up_and_zip_it_out :: [a] -> [b] -> [(a, b)]
+zip_it_up_and_zip_it_out _ [] = []
+zip_it_up_and_zip_it_out [] (_ : _) = []
+zip_it_up_and_zip_it_out (a : l_a5) (b : l_b3)
+  = (a, b) : zip_it_up_and_zip_it_out l_a5 l_b3
+