diff --git a/plugins/hls-tactics-plugin/src/Wingman/Auto.hs b/plugins/hls-tactics-plugin/src/Wingman/Auto.hs index 31bba590ba..4e2ab202f4 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Auto.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs index ef133d12ad..4ca76efb34 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs +++ b/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) diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs index 0cd72bd62e..780b58c891 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index 10d008f7f7..784f5f475f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/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,7 +210,7 @@ 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) @@ -214,7 +218,7 @@ judgementForHole state nfp range features = do mkJudgementAndContext - :: FeatureSet + :: Config -> Type -> TrackedStale Bindings -> Tracked 'Current RealSrcSpan @@ -222,12 +226,12 @@ mkJudgementAndContext -> 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) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index f1753739e2..58cfd7b9ad 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index c9ace600f6..1494336562 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/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