module Wingman.Auto where

import           Control.Monad.Reader.Class (asks)
import           Control.Monad.State (gets)
import qualified Data.Set as S
import           Refinery.Tactic
import           Wingman.Judgements
import           Wingman.KnownStrategies
import           Wingman.Machinery (tracing, getCurrentDefinitions)
import           Wingman.Tactics
import           Wingman.Types


------------------------------------------------------------------------------
-- | Automatically solve a goal.
auto :: TacticsM ()
auto :: TacticsM ()
auto = do
  Judgement
jdg <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  Set TyVar
skolems <- (TacticState -> Set TyVar)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Set TyVar)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> Set TyVar
ts_skolems
  Int
gas <- (Context -> Int)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Int
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Context -> Int)
 -> TacticT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      Int)
-> (Context -> Int)
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     Int
forall a b. (a -> b) -> a -> b
$ Config -> Int
cfg_auto_gas (Config -> Int) -> (Context -> Config) -> Context -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Config
ctxConfig
  [(OccName, CType)]
current <- TacticsM [(OccName, CType)]
getCurrentDefinitions
  String -> Judgement -> TacticsM ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"goal" Judgement
jdg
  String -> [(OccName, CType)] -> TacticsM ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"ctx" [(OccName, CType)]
current
  String -> Set TyVar -> TacticsM ()
forall (m :: * -> *) a. (Monad m, Show a) => String -> a -> m ()
traceMX String
"skolems" Set TyVar
skolems
  TacticsM () -> TacticsM () -> TacticsM ()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
commit TacticsM ()
knownStrategies
    (TacticsM () -> TacticsM ())
-> ([OccName] -> TacticsM ()) -> [OccName] -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s a.
Functor m =>
String
-> TacticT jdg (Synthesized ext) err s m a
-> TacticT jdg (Synthesized ext) err s m a
tracing String
"auto"
    (TacticsM () -> TacticsM ())
-> ([OccName] -> TacticsM ()) -> [OccName] -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> (Judgement -> Judgement) -> TacticsM ()
forall a. TacticsM a -> (Judgement -> Judgement) -> TacticsM a
localTactic (Int -> TacticsM ()
auto' Int
gas)
    ((Judgement -> Judgement) -> TacticsM ())
-> ([OccName] -> Judgement -> Judgement)
-> [OccName]
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisallowReason -> Set OccName -> Judgement -> Judgement
forall a.
DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
disallowing DisallowReason
RecursiveCall
    (Set OccName -> Judgement -> Judgement)
-> ([OccName] -> Set OccName)
-> [OccName]
-> Judgement
-> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList
    ([OccName] -> TacticsM ()) -> [OccName] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ ((OccName, CType) -> OccName) -> [(OccName, CType)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst [(OccName, CType)]
current