Wingman: configurable auto search depth (#1771)

* Pass around the entire Config object instaed of just featureset

* Make auto gas configurable

Author: isovector

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

@@ -1,5 +1,7 @@
+
 module Wingman.Auto where
 
+import           Control.Monad.Reader.Class (asks)
 import           Control.Monad.State (gets)
 import qualified Data.Set as S
 import           Refinery.Tactic
@@ -17,13 +19,14 @@ auto :: TacticsM ()
 auto = do
   jdg <- goal
   skolems <- gets ts_skolems
+  gas <- asks $ cfg_auto_gas . ctxConfig
   current <- getCurrentDefinitions
   traceMX "goal" jdg
   traceMX "ctx" current
   traceMX "skolems" skolems
   commit knownStrategies
     . tracing "auto"
-    . localTactic (auto' 4)
+    . localTactic (auto' gas)
     . disallowing RecursiveCall
     . S.fromList
     $ fmap fst current

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

@@ -13,27 +13,26 @@ import           OccName
 import           TcRnTypes
 import           TcType (tcSplitTyConApp, tcSplitPhiTy)
 import           TysPrim (alphaTys)
-import           Wingman.FeatureSet (FeatureSet)
 import           Wingman.Judgements.Theta
 import           Wingman.Types
 
 
 mkContext
-    :: FeatureSet
+    :: Config
     -> [(OccName, CType)]
     -> TcGblEnv
     -> ExternalPackageState
     -> KnownThings
     -> [Evidence]
     -> Context
-mkContext features locals tcg eps kt ev = Context
+mkContext cfg locals tcg eps kt ev = Context
   { ctxDefiningFuncs = locals
   , ctxModuleFuncs = fmap splitId
                    . (getFunBindId =<<)
                    . fmap unLoc
                    . bagToList
                    $ tcg_binds tcg
-  , ctxFeatureSet = features
+  , ctxConfig = cfg
   , ctxInstEnvs =
       InstEnvs
         (eps_inst_env eps)

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

@@ -29,7 +29,7 @@ knownStrategies = choice
 -- | Guard a tactic behind a feature.
 featureGuard :: Feature -> TacticsM a -> TacticsM a
 featureGuard feat t = do
-  fs <- asks ctxFeatureSet
+  fs <- asks $ cfg_feature_set . ctxConfig
   case hasFeature feat fs of
     True -> t
     False -> empty

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

@@ -131,8 +131,11 @@ properties :: Properties
    , 'PropertyKey "max_use_ctor_actions" 'TInteger
    , 'PropertyKey "features" 'TString
    , 'PropertyKey "timeout_duration" 'TInteger
+   , 'PropertyKey "auto_gas" 'TInteger
    ]
 properties = emptyProperties
+  & defineIntegerProperty #auto_gas
+    "The depth of the search tree when performing \"Attempt to fill hole\". Bigger values will be able to derive more solutions, but will take exponentially more time." 4
   & defineIntegerProperty #timeout_duration
     "The timeout for Wingman actions, in seconds" 2
   & defineStringProperty #features
@@ -157,6 +160,7 @@ getTacticConfig pId =
     <$> (parseFeatureSet <$> usePropertyLsp #features pId properties)
     <*> usePropertyLsp #max_use_ctor_actions pId properties
     <*> usePropertyLsp #timeout_duration pId properties
+    <*> usePropertyLsp #auto_gas pId properties
 
 ------------------------------------------------------------------------------
 -- | Get the current feature set from the plugin config.
@@ -182,9 +186,9 @@ judgementForHole
     :: IdeState
     -> NormalizedFilePath
     -> Tracked 'Current Range
-    -> FeatureSet
+    -> Config
     -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
-judgementForHole state nfp range features = do
+judgementForHole state nfp range cfg = do
   let stale a = runStaleIde "judgementForHole" state nfp a
 
   TrackedStale asts amapping  <- stale GetHieAst
@@ -206,28 +210,28 @@ judgementForHole state nfp range features = do
       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
       kt <- knownThings (untrackedStaleValue tcg) henv
 
-      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt
+      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
 
       dflags <- getIdeDynflags state nfp
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
 
 
 mkJudgementAndContext
-    :: FeatureSet
+    :: Config
     -> Type
     -> TrackedStale Bindings
     -> Tracked 'Current RealSrcSpan
     -> TrackedStale TcGblEnv
     -> ExternalPackageState
     -> KnownThings
     -> Maybe (Judgement, Context)
-mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
+mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
   binds_rss <- mapAgeFrom bmap rss
   tcg_rss <- mapAgeFrom tcgmap rss
 
   let tcs = fmap tcg_binds tcg
-      ctx = mkContext features
+      ctx = mkContext cfg
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ unTrack
                 $ getDefiningBindings <$> binds <*> binds_rss)

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

@@ -70,7 +70,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
+        (_, jdg, _, dflags) <- judgementForHole state nfp range cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData
@@ -99,11 +99,10 @@ tacticCmd tac pId state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       let stale a = runStaleIde "tacticCmd" state nfp a
 
-      features <- getFeatureSet pId
       ccs <- getClientCapabilities
       cfg <- getTacticConfig pId
       res <- liftIO $ runMaybeT $ do
-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range features
+        (range', jdg, ctx, dflags) <- judgementForHole state nfp range cfg
         let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) range'
         TrackedStale pm pmmap <- stale GetAnnotatedParsedSource
         pm_span <- liftMaybe $ mapAgeFrom pmmap span

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

@@ -80,6 +80,16 @@ data Config = Config
   { cfg_feature_set          :: FeatureSet
   , cfg_max_use_ctor_actions :: Int
   , cfg_timeout_seconds      :: Int
+  , cfg_auto_gas             :: Int
+  }
+  deriving (Eq, Ord, Show)
+
+emptyConfig :: Config
+emptyConfig = Config
+  { cfg_feature_set = mempty
+  , cfg_max_use_ctor_actions = 5
+  , cfg_timeout_seconds = 2
+  , cfg_auto_gas = 4
   }
 
 ------------------------------------------------------------------------------
@@ -398,7 +408,7 @@ data Context = Context
     -- ^ The functions currently being defined
   , ctxModuleFuncs   :: [(OccName, CType)]
     -- ^ Everything defined in the current module
-  , ctxFeatureSet    :: FeatureSet
+  , ctxConfig        :: Config
   , ctxKnownThings   :: KnownThings
   , ctxInstEnvs      :: InstEnvs
   , ctxTheta         :: Set CType
@@ -409,7 +419,7 @@ instance Show Context where
     [ "Context "
     , showsPrec 10 ctxDefiningFuncs ""
     , showsPrec 10 ctxModuleFuncs ""
-    , showsPrec 10 ctxFeatureSet ""
+    , showsPrec 10 ctxConfig ""
     , showsPrec 10 ctxTheta ""
     ]
 
@@ -429,7 +439,7 @@ emptyContext
   = Context
       { ctxDefiningFuncs = mempty
       , ctxModuleFuncs = mempty
-      , ctxFeatureSet = mempty
+      , ctxConfig = emptyConfig
       , ctxKnownThings = error "empty known things from emptyContext"
       , ctxInstEnvs = InstEnvs mempty mempty mempty
       , ctxTheta = mempty