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