diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs index 91a000ff05..632f6e12e7 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs +++ b/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..] diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 6dd9d18ff6..1fa209c4ce 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/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. diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index d4c2d7a2bd..9c861d827c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 858b24aa59..9fc607b730 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/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 ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index 84cd06a507..2b12243f6c 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/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" diff --git a/plugins/hls-tactics-plugin/test/golden/AutoZip.hs b/plugins/hls-tactics-plugin/test/golden/AutoZip.hs new file mode 100644 index 0000000000..98d6335988 --- /dev/null +++ b/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 = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/AutoZip.hs.expected b/plugins/hls-tactics-plugin/test/golden/AutoZip.hs.expected new file mode 100644 index 0000000000..4b1ede7122 --- /dev/null +++ b/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 +