Merge branch 'master' into declarative-custom-config

Author: berberman

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/Judgements.hs

@@ -16,6 +16,7 @@ import           Development.IDE.Spans.LocalBindings
 import           OccName
 import           SrcLoc
 import           Type
+import           Wingman.GHC (algebraicTyCon)
 import           Wingman.Types
 
 
@@ -61,7 +62,10 @@ withNewGoal t = field @"_jGoal" .~ t
 
 
 introduce :: Hypothesis a -> Judgement' a -> Judgement' a
-introduce hy = field @"_jHypothesis" <>~ hy
+-- NOTE(sandy): It's important that we put the new hypothesis terms first,
+-- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs
+-- after a previously-destructed term.
+introduce hy = field @"_jHypothesis" %~ mappend hy
 
 
 ------------------------------------------------------------------------------
@@ -149,7 +153,10 @@ findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
 findPositionVal jdg defn pos = listToMaybe $ do
   -- It's important to inspect the entire hypothesis here, as we need to trace
   -- ancstry through potentially disallowed terms in the hypothesis.
-  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg
+  (name, hi) <- M.toList
+              $ M.map (overProvenance expandDisallowed)
+              $ hyByName
+              $ jEntireHypothesis jdg
   case hi_provenance hi of
     TopLevelArgPrv defn' pos' _
       | defn == defn'
@@ -238,12 +245,13 @@ patternHypothesis scrutinee dc jdg
   = introduceHypothesis $ \_ pos ->
       PatternMatchPrv $
         PatVal
-            scrutinee
-            (maybe mempty
-                  (\scrut -> S.singleton scrut <> getAncestry jdg scrut)
-                  scrutinee)
-            (Uniquely dc)
-            pos
+          scrutinee
+          (maybe
+              mempty
+              (\scrut -> S.singleton scrut <> getAncestry jdg scrut)
+              scrutinee)
+          (Uniquely dc)
+          pos
 
 
 ------------------------------------------------------------------------------
@@ -285,6 +293,21 @@ jLocalHypothesis
   . jHypothesis
 
 
+------------------------------------------------------------------------------
+-- | Given a judgment, return the hypotheses that are acceptable to destruct.
+--
+-- We use the ordering of the hypothesis for this purpose. Since new bindings
+-- are always inserted at the beginning, we can impose a canonical ordering on
+-- which order to try destructs by what order they are introduced --- stopping
+-- at the first one we've already destructed.
+jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType]
+jAcceptableDestructTargets
+  = filter (isJust . algebraicTyCon . unCType . hi_type)
+  . takeWhile (not . isAlreadyDestructed . hi_provenance)
+  . unHypothesis
+  . jEntireHypothesis
+
+
 ------------------------------------------------------------------------------
 -- | If we're in a top hole, the name of the defining function.
 isTopHole :: Context -> Judgement' a -> Maybe OccName
@@ -391,6 +414,12 @@ isDisallowed :: Provenance -> Bool
 isDisallowed DisallowedPrv{} = True
 isDisallowed _               = False
 
+------------------------------------------------------------------------------
+-- | Has this term already been disallowed?
+isAlreadyDestructed :: Provenance -> Bool
+isAlreadyDestructed (DisallowedPrv AlreadyDestructed _) = True
+isAlreadyDestructed _ = False
+
 
 ------------------------------------------------------------------------------
 -- | Eliminates 'DisallowedPrv' provenances.

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
 
 ------------------------------------------------------------------------------
@@ -339,9 +358,7 @@ overFunctions =
 
 overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overAlgebraicTerms =
-  attemptOn $ filter (isJust . algebraicTyCon . unCType . hi_type)
-            . unHypothesis
-            . jHypothesis
+  attemptOn jAcceptableDestructTargets
 
 
 allNames :: Judgement -> Set OccName

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

@@ -240,6 +240,10 @@ instance Uniquable a => Ord (Uniquely a) where
   compare = nonDetCmpUnique `on` getUnique . getViaUnique
 
 
+-- NOTE(sandy): The usage of list here is mostly for convenience, but if it's
+-- ever changed, make sure to correspondingly update
+-- 'jAcceptableDestructTargets' so that it correctly identifies newly
+-- introduced terms.
 newtype Hypothesis a = Hypothesis
   { unHypothesis :: [HyInfo a]
   }

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
+