Separate tactics into its own package

cabal.project

@@ -2,6 +2,7 @@ packages:
          ./
          ghcide
          hls-plugin-api
+         ./plugins/tactics
 
 source-repository-package
   type: git
@@ -20,6 +21,6 @@ package ghcide
 
 write-ghc-environment-files: never
 
-index-state: 2020-10-08T12:51:21Z
+index-state: 2020-10-16T04:00:00Z
 
 allow-newer: data-tree-print:base

haskell-language-server.cabal

@@ -80,7 +80,7 @@ library
 executable haskell-language-server
   import:           agpl, common-deps
   main-is:          Main.hs
-  hs-source-dirs:   exe plugins/default/src plugins/tactics/src
+  hs-source-dirs:   exe plugins/default/src
   other-modules:
     Ide.Plugin.Eval
     Ide.Plugin.Example
@@ -93,19 +93,6 @@ executable haskell-language-server
     Ide.Plugin.Pragmas
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
-    Ide.Plugin.Tactic
-    Ide.Plugin.Tactic.CodeGen
-    Ide.Plugin.Tactic.Context
-    Ide.Plugin.Tactic.Debug
-    Ide.Plugin.Tactic.GHC
-    Ide.Plugin.Tactic.Judgements
-    Ide.Plugin.Tactic.Machinery
-    Ide.Plugin.Tactic.Naming
-    Ide.Plugin.Tactic.Range
-    Ide.Plugin.Tactic.Tactics
-    Ide.Plugin.Tactic.Types
-    Ide.Plugin.Tactic.TestTypes
-    Ide.TreeTransform
 
   ghc-options:
     -threaded -Wall -Wno-name-shadowing -Wredundant-constraints
@@ -133,6 +120,7 @@ executable haskell-language-server
     , haskell-language-server
     , haskell-lsp              ^>=0.22
     , hls-plugin-api
+    , hls-tactics-plugin
     , lens
     , ormolu                   ^>=0.1.2
     , regex-tdfa
@@ -151,14 +139,9 @@ executable haskell-language-server
     , stylish-haskell          ^>=0.12
     , temporary
     , text
-    , syb
     , time
     , transformers
     , unordered-containers
-    , ghc-source-gen
-    , refinery                 ^>=0.2
-    , ghc-exactprint
-    , fingertree
 
   if flag(agpl)
     build-depends: brittany

hie.yaml.cbl

@@ -26,7 +26,7 @@ cradle:
               component: "haskell-language-server:exe:haskell-language-server"
 
             - path: "./plugins/tactics/src"
-              component: "haskell-language-server:exe:haskell-language-server"
+              component: "lib:hls-tactics-plugin"
 
             - path: "./exe/Wrapper.hs"
               component: "haskell-language-server:exe:haskell-language-server-wrapper"

hie.yaml.stack

@@ -22,7 +22,7 @@ cradle:
             - path: "./plugins/default/src"
               component: "haskell-language-server:exe:haskell-language-server"
             - path: "./plugins/tactics/src"
-              component: "haskell-language-server:exe:haskell-language-server"
+              component: "hls-tactics-plugin:lib:hls-tactics-plugin"
 
             - path: "./exe/Arguments.hs"
               component: "haskell-language-server:exe:haskell-language-server"

plugins/default/src/Ide/Plugin/ModuleName.hs

@@ -94,7 +94,6 @@ import           Development.IDE.Core.Shake
 import           Data.Text                      ( pack )
 import           System.Directory               ( canonicalizePath )
 import           Data.List
-import           Ide.Plugin.Tactic.Debug        ( unsafeRender )
 -- |Plugin descriptor
 descriptor :: PluginId -> PluginDescriptor
 descriptor plId = (defaultPluginDescriptor plId)

plugins/tactics/hls-tactics-plugin.cabal

@@ -0,0 +1,80 @@
+cabal-version:      2.2
+category:           Development
+name:               hls-tactics-plugin
+version:            0.5.1.0
+synopsis:           LSP server for GHC
+description:
+  Please see the README on GitHub at <https://github.com/isovector/hls-tactics-plugin#readme>
+
+homepage:           https://github.com/isovector/hls-tactics-plugin#readme
+bug-reports:        https://github.com/isovector/hls-tactics-plugin/issues
+author:             Sandy Maguire, Reed Mullanix
+maintainer:         [email protected]
+copyright:          Sandy Maguire, Reed Mullanix
+-- license:            Apache-2.0
+-- license-file:       LICENSE
+build-type:         Simple
+-- extra-source-files:
+--   README.md
+--   ChangeLog.md
+
+flag pedantic
+  description: Enable -Werror
+  default:     False
+  manual:      True
+
+source-repository head
+  type:     git
+  location: https://github.com/isovector/hls-tactics-plugin
+
+library
+  hs-source-dirs:   src
+  exposed-modules:
+    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
+    Ide.Plugin.Tactic.Tactics
+    Ide.Plugin.Tactic.Types
+    Ide.Plugin.Tactic.TestTypes
+    Ide.TreeTransform
+
+  ghc-options:
+    -Wno-name-shadowing -Wredundant-constraints
+  if flag(pedantic)
+    ghc-options: -Werror
+
+  build-depends:
+    , aeson
+    , base           >=4.12 && <5
+    , containers
+    , directory
+    , extra
+    , filepath
+    , fingertree
+    , generic-lens
+    , ghc
+    , ghc-boot-th
+    , ghc-exactprint
+    , ghc-source-gen
+    , ghcide         >=0.1
+    , haskell-lsp    ^>=0.22
+    , hls-plugin-api
+    , lens
+    , mtl
+    , refinery       ^>=0.3
+    , retrie         >=0.1.1.0
+    , shake          >=0.17.5
+    , syb
+    , text
+    , transformers
+
+  default-language: Haskell2010
+

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

@@ -1,7 +1,9 @@
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE PatternSynonyms     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE TypeApplications    #-}
@@ -20,8 +22,12 @@ import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Coerce
+import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Schemes (everything)
+import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
+import           Data.Monoid
 import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
@@ -38,6 +44,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
@@ -50,6 +57,8 @@ import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           SrcLoc (containsSpan)
+import           System.Timeout
 
 
 descriptor :: PluginId -> PluginDescriptor
@@ -250,12 +259,24 @@ judgementForHole state nfp range = do
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
+      tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
               tcg
       hyps = hypothesisFromBindings rss binds
-  pure (resulting_range, mkFirstJudgement hyps goal, ctx, dflags)
+  pure ( resulting_range
+       , mkFirstJudgement
+           hyps
+           (isRhsHole rss tcs)
+           (maybe
+              mempty
+              (uncurry M.singleton . fmap pure)
+                $ getRhsPosVals rss tcs)
+           goal
+       , ctx
+       , dflags
+       )
 
 
 
@@ -266,20 +287,26 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        case runTactic ctx jdg
-              $ tac
-              $ mkVarOcc
-              $ T.unpack var_name of
-          Left err ->
-            pure $ (, Nothing)
-              $ Left
-              $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-          Right res -> do
-            let g = graft (RealSrcSpan span) res
-                response = transform dflags (clientCapabilities lf) uri g pm
-            pure $ case response of
-               Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
-               Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+        x <- lift $ timeout 2e8 $
+          case runTactic ctx jdg
+                $ tac
+                $ mkVarOcc
+                $ T.unpack var_name of
+            Left err ->
+              pure $ (, Nothing)
+                $ Left
+                $ ResponseError InvalidRequest (T.pack $ show err) Nothing
+            Right (_, ext) -> do
+              let g = graft (RealSrcSpan span) ext
+                  response = transform dflags (clientCapabilities lf) uri g pm
+              pure $ case response of
+                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
+                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+        pure $ case x of
+          Just y -> y
+          Nothing -> (, Nothing)
+                   $ Left
+                   $ ResponseError InvalidRequest "timed out" Nothing
 tacticCmd _ _ _ _ =
   pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing
        , Nothing
@@ -292,3 +319,34 @@ fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
+
+------------------------------------------------------------------------------
+-- | Is this hole immediately to the right of an equals sign?
+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool
+isRhsHole rss tcs = everything (||) (mkQ False $ \case
+  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span
+  _ -> False
+  ) tcs
+
+
+------------------------------------------------------------------------------
+-- | Compute top-level position vals of a function
+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
+getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
+  TopLevelRHS name ps
+      (L (RealSrcSpan span)  -- body with no guards and a single defn
+         (HsVar _ (L _ hole)))
+    | containsSpan rss span  -- which contains our span
+    , isHole $ occName hole  -- and the span is a hole
+    -> First $ do
+        patnames <- traverse getPatName ps
+        pure (occName name, patnames)
+  _ -> mempty
+  ) tcs
+
+
+
+-- TODO(sandy): Make this more robust
+isHole :: OccName -> Bool
+isHole = isPrefixOf "_" . occNameString
+

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

@@ -0,0 +1,25 @@
+module Ide.Plugin.Tactic.Auto where
+
+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
+import Refinery.Tactic
+import Ide.Plugin.Tactic.Machinery (tracing)
+
+
+------------------------------------------------------------------------------
+-- | Automatically solve a goal.
+auto :: TacticsM ()
+auto = do
+  jdg <- goal
+  current <- getCurrentDefinitions
+  traceMX "goal" jdg
+  traceMX "ctx" current
+  commit knownStrategies
+    . tracing "auto"
+    . localTactic (auto' 4)
+    . disallowing
+    $ fmap fst current
+