From b80813bdb1bae1e19281358eee1ba4f9a630000a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 12:37:28 -0800 Subject: [PATCH 1/2] Use try' everywhere --- .../src/Ide/Plugin/Tactic/KnownStrategies.hs | 4 ++-- .../src/Ide/Plugin/Tactic/Machinery.hs | 13 +++++++++++++ .../src/Ide/Plugin/Tactic/Tactics.hs | 2 +- 3 files changed, 16 insertions(+), 3 deletions(-) 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 da8f9f86e2..be6276dbe5 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -322,7 +322,7 @@ 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 From 360d62d198e9249f18e41b6a3fa30d8ba7fa2188 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 12:37:43 -0800 Subject: [PATCH 2/2] Make refine much less aggressive --- .../src/Ide/Plugin/Tactic/Tactics.hs | 12 ++++-------- .../test/golden/RefineCon.hs.expected | 2 +- 2 files changed, 5 insertions(+), 9 deletions(-) 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 be6276dbe5..ec8d93e840 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -308,14 +308,10 @@ 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 () 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 = (_, _, _)