Known fmap strategy

haskell-language-server.cabal

@@ -93,11 +93,13 @@ executable haskell-language-server
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
     Ide.Plugin.Tactic
+    Ide.Plugin.Tactic.Auto
     Ide.Plugin.Tactic.CodeGen
     Ide.Plugin.Tactic.Context
     Ide.Plugin.Tactic.Debug
     Ide.Plugin.Tactic.GHC
     Ide.Plugin.Tactic.Judgements
+    Ide.Plugin.Tactic.KnownStrategies
     Ide.Plugin.Tactic.Machinery
     Ide.Plugin.Tactic.Naming
     Ide.Plugin.Tactic.Range

plugins/tactics/src/Ide/Plugin/Tactic.hs

@@ -39,6 +39,7 @@ import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin (mkLspCommand)
+import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements

plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs

@@ -0,0 +1,18 @@
+module Ide.Plugin.Tactic.Auto where
+
+import Control.Applicative
+import Ide.Plugin.Tactic.Context
+import Ide.Plugin.Tactic.Judgements
+import Ide.Plugin.Tactic.KnownStrategies
+import Ide.Plugin.Tactic.Tactics
+import Ide.Plugin.Tactic.Types
+
+
+------------------------------------------------------------------------------
+-- | Automatically solve a goal.
+auto :: TacticsM ()
+auto = do
+  current <- getCurrentDefinitions
+  knownStrategies
+    <|> (localTactic (auto' 4) $ disallowing $ fmap fst current)
+

plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs

@@ -0,0 +1,37 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Ide.Plugin.Tactic.KnownStrategies where
+
+import Control.Monad.Error.Class
+import Ide.Plugin.Tactic.Context (getCurrentDefinitions)
+import Ide.Plugin.Tactic.Tactics
+import Ide.Plugin.Tactic.Types
+import OccName (mkVarOcc)
+import Refinery.Tactic
+
+
+knownStrategies :: TacticsM ()
+knownStrategies = choice
+  [ deriveFmap
+  ]
+
+
+known :: String -> TacticsM () -> TacticsM ()
+known name t = do
+  getCurrentDefinitions >>= \case
+    [(def, _)] | def == mkVarOcc name -> do
+      traceMX "running known strategy" name
+      t
+    _ -> throwError NoApplicableTactic
+
+
+deriveFmap :: TacticsM ()
+deriveFmap = known "fmap" $ do
+  try intros
+  overAlgebraicTerms homo
+  choice
+    [ overFunctions apply >> auto' 2
+    , assumption
+    , recursion
+    ]
+

plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs

@@ -21,6 +21,7 @@ import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
 import qualified Data.Set as S
+import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
 import           GHC.SourceGen.Expr
@@ -32,12 +33,11 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
+import           Name (nameOccName)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Name (nameOccName)
-import DataCon
 
 
 ------------------------------------------------------------------------------
@@ -242,43 +242,31 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
-------------------------------------------------------------------------------
--- | Automatically solve a goal.
-auto :: TacticsM ()
-auto = do
-  current <- getCurrentDefinitions
-  jdg <- goal
-  traceM $ mappend "!!!auto current:" $ show current
-  traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 5) $ disallowing $ fmap fst current
-
-
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
   let loop = auto' (n - 1)
   try intros
   choice
-    [ attemptOn functionNames $ \fname -> do
+    [ overFunctions $ \fname -> do
         apply fname
         loop
-    , attemptOn algebraicNames $ \aname -> do
+    , overAlgebraicTerms $ \aname -> do
         destructAuto aname
         loop
     , splitAuto >> loop
     , assumption >> loop
     , recursion
     ]
 
+overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
+overFunctions =
+  attemptOn $ M.keys . M.filter (isFunction . unCType) . jHypothesis
 
-functionNames :: Judgement -> [OccName]
-functionNames  =
-  M.keys . M.filter (isFunction . unCType) . jHypothesis
-
-
-algebraicNames :: Judgement -> [OccName]
-algebraicNames =
-  M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
+overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
+overAlgebraicTerms =
+  attemptOn $
+    M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
 
 
 allNames :: Judgement -> [OccName]