We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 828c0fc commit 0156bacCopy full SHA for 0156bac
plugins/hls-tactics-plugin/src/Wingman/Auto.hs
@@ -1,5 +1,7 @@
1
+
2
module Wingman.Auto where
3
4
+import Control.Monad.Reader.Class (asks)
5
import Control.Monad.State (gets)
6
import qualified Data.Set as S
7
import Refinery.Tactic
@@ -17,13 +19,14 @@ auto :: TacticsM ()
17
19
auto = do
18
20
jdg <- goal
21
skolems <- gets ts_skolems
22
+ gas <- asks $ cfg_auto_gas . ctxConfig
23
current <- getCurrentDefinitions
24
traceMX "goal" jdg
25
traceMX "ctx" current
26
traceMX "skolems" skolems
27
commit knownStrategies
28
. tracing "auto"
- . localTactic (auto' 4)
29
+ . localTactic (auto' gas)
30
. disallowing RecursiveCall
31
. S.fromList
32
$ fmap fst current
0 commit comments