diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs index 9686306257..d0237acff2 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs @@ -5,7 +5,7 @@ module Ide.Plugin.Tactic.KnownStrategies where import Control.Monad.Error.Class import Ide.Plugin.Tactic.Context (getCurrentDefinitions) import Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary) -import Ide.Plugin.Tactic.Machinery (tracing) +import Ide.Plugin.Tactic.Machinery (tracing, try') import Ide.Plugin.Tactic.Tactics import Ide.Plugin.Tactic.Types import OccName (mkVarOcc) @@ -29,7 +29,7 @@ known name t = do deriveFmap :: TacticsM () deriveFmap = do - try intros + try' intros overAlgebraicTerms homo choice [ overFunctions apply >> auto' 2 diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs index a4569af5b9..26c21dad62 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs @@ -272,3 +272,16 @@ requireConcreteHole m = do 0 -> m _ -> throwError TooPolymorphic + +------------------------------------------------------------------------------ +-- | The 'try' that comes in refinery 0.3 causes unnecessary backtracking and +-- balloons the search space. This thing just tries it, but doesn't backtrack +-- if it fails. +-- +-- TODO(sandy): Remove this when we upgrade to 0.4 +try' + :: Functor m + => TacticT jdg ext err s m () + -> TacticT jdg ext err s m () +try' t = commit t $ pure () + diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index f75fb07054..89cbea9b0d 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -309,21 +309,17 @@ localTactic t f = do 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 +refine = do + try' intros + try' splitSingle + try' intros auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress auto' n = do let loop = auto' (n - 1) - try intros + try' intros choice [ overFunctions $ \fname -> do apply fname diff --git a/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected index e6e43592a4..9428bf12d9 100644 --- a/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected +++ b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected @@ -1,3 +1,3 @@ test :: ((), (b, c), d) -test = ((), (_, _), _) +test = (_, _, _)