module Theory.Tools.LoopBreakers (
useAutoLoopBreakersAC
) where
import Control.Applicative
import Control.Monad.Fresh
import Control.Monad.Reader
import Data.DAG.Simple
import Theory.Model
premSolvingRelAC :: (a -> [(PremIdx, LNFact)])
-> (a -> [(ConcIdx, LNFact)])
-> (a -> [LNSubstVFresh])
-> [a]
-> WithMaude (Relation (a, PremIdx))
premSolvingRelAC ePrems eConcs eVariants rules = reader $ \hnd -> do
(toRu, from) <- dataflowRelAC hnd
(toPrem, _) <- ePrems toRu
return (from, (toRu, toPrem))
where
dataflowRelAC hnd = do
ruFrom <- rules
ruTo <- rules
(premIdx, premFa0) <- ePrems ruTo
guard $ or $ do
premFa <- instances ruTo premFa0
concFa <- instances ruFrom =<< (snd <$> eConcs ruFrom)
let concFaFresh = rename concFa `evalFresh` avoid premFa
return $ (`runReader` hnd) (unifiableLNFacts concFaFresh premFa)
return (ruFrom, (ruTo, premIdx))
instances ru fa = do
subst <- eVariants ru
return (apply (subst `freshToFreeAvoiding` fa) fa)
useAutoLoopBreakersAC
:: Ord a
=> (a -> [(PremIdx, LNFact)])
-> (a -> [(ConcIdx, LNFact)])
-> (a -> [LNSubstVFresh])
-> ([PremIdx] -> a -> a)
-> [a]
-> WithMaude ([a], Relation (a, PremIdx), [(a, PremIdx)])
useAutoLoopBreakersAC ePrems eConcs eVariants addAnn rules =
reader $ \hnd ->
let solveRel = (`runReader` hnd) $
premSolvingRelAC ePrems eConcs eVariants rules
breakers = dfsLoopBreakers $ solveRel
in ( do ru <- rules
return (addAnn [ u | (ru', u) <- breakers, ru == ru' ] ru)
, solveRel
, breakers
)