1
2module Wingman.Auto where
3
4import           Control.Monad.Reader.Class (asks)
5import           Control.Monad.State (gets)
6import qualified Data.Set as S
7import           Refinery.Tactic
8import           Wingman.Judgements
9import           Wingman.KnownStrategies
10import           Wingman.Machinery (tracing, getCurrentDefinitions)
11import           Wingman.Tactics
12import           Wingman.Types
13
14
15------------------------------------------------------------------------------
16-- | Automatically solve a goal.
17auto :: TacticsM ()
18auto = do
19  jdg <- goal
20  skolems <- gets ts_skolems
21  gas <- asks $ cfg_auto_gas . ctxConfig
22  current <- getCurrentDefinitions
23  traceMX "goal" jdg
24  traceMX "ctx" current
25  traceMX "skolems" skolems
26  commit knownStrategies
27    . tracing "auto"
28    . localTactic (auto' gas)
29    . disallowing RecursiveCall
30    . S.fromList
31    $ fmap fst current
32
33