module Ide.Plugin.Tactic.Auto where

import Control.Monad.State (gets)
import Ide.Plugin.Tactic.Context
import Ide.Plugin.Tactic.Judgements
import Ide.Plugin.Tactic.KnownStrategies
import Ide.Plugin.Tactic.Machinery (tracing)
import Ide.Plugin.Tactic.Tactics
import Ide.Plugin.Tactic.Types
import Refinery.Tactic


------------------------------------------------------------------------------
-- | Automatically solve a goal.
auto :: TacticsM ()
auto :: TacticsM ()
auto = do
  Judgement
jdg <- TacticT
  Judgement
  (Trace, 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
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Set TyVar)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> Set TyVar
ts_skolems
  [(OccName, CType)]
current <- TacticT
  Judgement
  (Trace, LHsExpr GhcPs)
  TacticError
  TacticState
  ExtractM
  [(OccName, CType)]
forall (m :: * -> *). MonadReader Context m => m [(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 (Trace, ext) err s m a
-> TacticT jdg (Trace, 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
4)
    ((Judgement -> Judgement) -> TacticsM ())
-> ([OccName] -> Judgement -> Judgement)
-> [OccName]
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisallowReason -> [OccName] -> Judgement -> Judgement
forall a.
DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
disallowing DisallowReason
RecursiveCall
    ([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