{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Safe #-}
#endif
module Control.Monad.Logic (
module Control.Monad.Logic.Class,
Logic,
logic,
runLogic,
observe,
observeMany,
observeAll,
LogicT(..),
runLogicT,
observeT,
observeManyT,
observeAllT,
module Control.Monad,
module Control.Monad.Trans
) where
import Control.Applicative
import Control.Monad
import qualified Control.Monad.Fail as Fail
import Control.Monad.Identity
import Control.Monad.Trans
import Control.Monad.Reader.Class
import Control.Monad.State.Class
import Control.Monad.Error.Class
#if !MIN_VERSION_base(4,8,0)
import Data.Monoid (Monoid(mappend, mempty))
#endif
import qualified Data.Foldable as F
import qualified Data.Traversable as T
import Control.Monad.Logic.Class
newtype LogicT m a =
LogicT { LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }
#if !MIN_VERSION_base(4,13,0)
observeT :: Monad m => LogicT m a -> m a
#else
observeT :: MonadFail m => LogicT m a -> m a
#endif
observeT :: LogicT m a -> m a
observeT LogicT m a
lt = LogicT m a -> (a -> m a -> m a) -> m a -> m a
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
lt (m a -> m a -> m a
forall a b. a -> b -> a
const (m a -> m a -> m a) -> (a -> m a) -> a -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return) (String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No answer.")
observeAllT :: Monad m => LogicT m a -> m [a]
observeAllT :: LogicT m a -> m [a]
observeAllT LogicT m a
m = LogicT m a -> (a -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (([a] -> [a]) -> m [a] -> m [a]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (([a] -> [a]) -> m [a] -> m [a])
-> (a -> [a] -> [a]) -> a -> m [a] -> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:)) ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
observeManyT :: Monad m => Int -> LogicT m a -> m [a]
observeManyT :: Int -> LogicT m a -> m [a]
observeManyT Int
n LogicT m a
m
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = LogicT m a -> (a -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m [a]
_ -> [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a]) ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
| Bool
otherwise = LogicT m (Maybe (a, LogicT m a))
-> (Maybe (a, LogicT m a) -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (LogicT m a -> LogicT m (Maybe (a, LogicT m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit LogicT m a
m) Maybe (a, LogicT m a) -> m [a] -> m [a]
forall (m :: * -> *) a p.
Monad m =>
Maybe (a, LogicT m a) -> p -> m [a]
sk ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
where
sk :: Maybe (a, LogicT m a) -> p -> m [a]
sk Maybe (a, LogicT m a)
Nothing p
_ = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
sk (Just (a
a, LogicT m a
m')) p
_ = (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> m [a] -> m [a]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` Int -> LogicT m a -> m [a]
forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
observeManyT (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) LogicT m a
m'
runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT = LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT
type Logic = LogicT Identity
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic forall r. (a -> r -> r) -> r -> r
f = (forall r.
(a -> Identity r -> Identity r) -> Identity r -> Identity r)
-> Logic a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r.
(a -> Identity r -> Identity r) -> Identity r -> Identity r)
-> Logic a)
-> (forall r.
(a -> Identity r -> Identity r) -> Identity r -> Identity r)
-> Logic a
forall a b. (a -> b) -> a -> b
$ \a -> Identity r -> Identity r
k -> r -> Identity r
forall a. a -> Identity a
Identity (r -> Identity r) -> (Identity r -> r) -> Identity r -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(a -> r -> r) -> r -> r
forall r. (a -> r -> r) -> r -> r
f (\a
a -> Identity r -> r
forall a. Identity a -> a
runIdentity (Identity r -> r) -> (r -> Identity r) -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity r -> Identity r
k a
a (Identity r -> Identity r) -> (r -> Identity r) -> r -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> Identity r
forall a. a -> Identity a
Identity) (r -> r) -> (Identity r -> r) -> Identity r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Identity r -> r
forall a. Identity a -> a
runIdentity
observe :: Logic a -> a
observe :: Logic a -> a
observe Logic a
lt = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ Logic a
-> (a -> Identity a -> Identity a) -> Identity a -> Identity a
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT Logic a
lt (Identity a -> Identity a -> Identity a
forall a b. a -> b -> a
const (Identity a -> Identity a -> Identity a)
-> (a -> Identity a) -> a -> Identity a -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return) (String -> Identity a
forall a. HasCallStack => String -> a
error String
"No answer.")
observeAll :: Logic a -> [a]
observeAll :: Logic a -> [a]
observeAll = Identity [a] -> [a]
forall a. Identity a -> a
runIdentity (Identity [a] -> [a])
-> (Logic a -> Identity [a]) -> Logic a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Logic a -> Identity [a]
forall (m :: * -> *) a. Monad m => LogicT m a -> m [a]
observeAllT
observeMany :: Int -> Logic a -> [a]
observeMany :: Int -> Logic a -> [a]
observeMany Int
i = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
i ([a] -> [a]) -> (Logic a -> [a]) -> Logic a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Logic a -> [a]
forall a. Logic a -> [a]
observeAll
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic Logic a
l a -> r -> r
s r
f = Identity r -> r
forall a. Identity a -> a
runIdentity (Identity r -> r) -> Identity r -> r
forall a b. (a -> b) -> a -> b
$ Logic a
-> (a -> Identity r -> Identity r) -> Identity r -> Identity r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT Logic a
l a -> Identity r -> Identity r
si Identity r
fi
where
si :: a -> Identity r -> Identity r
si = (r -> r) -> Identity r -> Identity r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((r -> r) -> Identity r -> Identity r)
-> (a -> r -> r) -> a -> Identity r -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> r -> r
s
fi :: Identity r
fi = r -> Identity r
forall a. a -> Identity a
Identity r
f
instance Functor (LogicT f) where
fmap :: (a -> b) -> LogicT f a -> LogicT f b
fmap a -> b
f LogicT f a
lt = (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b)
-> (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall a b. (a -> b) -> a -> b
$ \b -> f r -> f r
sk f r
fk -> LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
lt (b -> f r -> f r
sk (b -> f r -> f r) -> (a -> b) -> a -> f r -> f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f r
fk
instance Applicative (LogicT f) where
pure :: a -> LogicT f a
pure a
a = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
-> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall a b. (a -> b) -> a -> b
$ \a -> f r -> f r
sk f r
fk -> a -> f r -> f r
sk a
a f r
fk
LogicT f (a -> b)
f <*> :: LogicT f (a -> b) -> LogicT f a -> LogicT f b
<*> LogicT f a
a = (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b)
-> (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall a b. (a -> b) -> a -> b
$ \b -> f r -> f r
sk f r
fk -> LogicT f (a -> b) -> ((a -> b) -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f (a -> b)
f (\a -> b
g f r
fk' -> LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
a (b -> f r -> f r
sk (b -> f r -> f r) -> (a -> b) -> a -> f r -> f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g) f r
fk') f r
fk
instance Alternative (LogicT f) where
empty :: LogicT f a
empty = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
-> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall a b. (a -> b) -> a -> b
$ \a -> f r -> f r
_ f r
fk -> f r
fk
LogicT f a
f1 <|> :: LogicT f a -> LogicT f a -> LogicT f a
<|> LogicT f a
f2 = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
-> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall a b. (a -> b) -> a -> b
$ \a -> f r -> f r
sk f r
fk -> LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
f1 a -> f r -> f r
sk (LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
f2 a -> f r -> f r
sk f r
fk)
instance Monad (LogicT m) where
return :: a -> LogicT m a
return a
a = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> a -> m r -> m r
sk a
a m r
fk
LogicT m a
m >>= :: LogicT m a -> (a -> LogicT m b) -> LogicT m b
>>= a -> LogicT m b
f = (forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b)
-> (forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b
forall a b. (a -> b) -> a -> b
$ \b -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m r
fk' -> LogicT m b -> (b -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (a -> LogicT m b
f a
a) b -> m r -> m r
sk m r
fk') m r
fk
#if !MIN_VERSION_base(4,13,0)
fail = Fail.fail
#endif
instance Fail.MonadFail (LogicT m) where
fail :: String -> LogicT m a
fail String
_ = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
_ m r
fk -> m r
fk
instance MonadPlus (LogicT m) where
mzero :: LogicT m a
mzero = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
_ m r
fk -> m r
fk
LogicT m a
m1 mplus :: LogicT m a -> LogicT m a -> LogicT m a
`mplus` LogicT m a
m2 = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m1 a -> m r -> m r
sk (LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m2 a -> m r -> m r
sk m r
fk)
instance MonadTrans LogicT where
lift :: m a -> LogicT m a
lift m a
m = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> m a
m m a -> (a -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> a -> m r -> m r
sk a
a m r
fk
instance (MonadIO m) => MonadIO (LogicT m) where
liftIO :: IO a -> LogicT m a
liftIO = m a -> LogicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> LogicT m a) -> (IO a -> m a) -> IO a -> LogicT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
instance (Monad m) => MonadLogic (LogicT m) where
msplit :: LogicT m a -> LogicT m (Maybe (a, LogicT m a))
msplit LogicT m a
m = m (Maybe (a, LogicT m a)) -> LogicT m (Maybe (a, LogicT m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Maybe (a, LogicT m a)) -> LogicT m (Maybe (a, LogicT m a)))
-> m (Maybe (a, LogicT m a)) -> LogicT m (Maybe (a, LogicT m a))
forall a b. (a -> b) -> a -> b
$ LogicT m a
-> (a -> m (Maybe (a, LogicT m a)) -> m (Maybe (a, LogicT m a)))
-> m (Maybe (a, LogicT m a))
-> m (Maybe (a, LogicT m a))
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m a -> m (Maybe (a, LogicT m a)) -> m (Maybe (a, LogicT m a))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) (m :: * -> *) a b.
(MonadTrans t, Monad m, Monad m, MonadLogic (t m)) =>
a -> m (Maybe (b, t m b)) -> m (Maybe (a, t m b))
ssk (Maybe (a, LogicT m a) -> m (Maybe (a, LogicT m a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, LogicT m a)
forall a. Maybe a
Nothing)
where
ssk :: a -> m (Maybe (b, t m b)) -> m (Maybe (a, t m b))
ssk a
a m (Maybe (b, t m b))
fk = Maybe (a, t m b) -> m (Maybe (a, t m b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, t m b) -> m (Maybe (a, t m b)))
-> Maybe (a, t m b) -> m (Maybe (a, t m b))
forall a b. (a -> b) -> a -> b
$ (a, t m b) -> Maybe (a, t m b)
forall a. a -> Maybe a
Just (a
a, (m (Maybe (b, t m b)) -> t m (Maybe (b, t m b))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Maybe (b, t m b))
fk t m (Maybe (b, t m b)) -> (Maybe (b, t m b) -> t m b) -> t m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe (b, t m b) -> t m b
forall (m :: * -> *) a. MonadLogic m => Maybe (a, m a) -> m a
reflect))
once :: LogicT m a -> LogicT m a
once LogicT m a
m = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m r
_ -> a -> m r -> m r
sk a
a m r
fk) m r
fk
lnot :: LogicT m a -> LogicT m ()
lnot LogicT m a
m = (forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ()
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ())
-> (forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ()
forall a b. (a -> b) -> a -> b
$ \() -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
_ m r
_ -> m r
fk) (() -> m r -> m r
sk () m r
fk)
#if MIN_VERSION_base(4,8,0)
instance {-# OVERLAPPABLE #-} (Monad m, F.Foldable m) => F.Foldable (LogicT m) where
foldMap :: (a -> m) -> LogicT m a -> m
foldMap a -> m
f LogicT m a
m = m m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
F.fold (m m -> m) -> m m -> m
forall a b. (a -> b) -> a -> b
$ LogicT m a -> (a -> m m -> m m) -> m m -> m m
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m ((m -> m) -> m m -> m m
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((m -> m) -> m m -> m m) -> (a -> m -> m) -> a -> m m -> m m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> m -> m
forall a. Monoid a => a -> a -> a
mappend (m -> m -> m) -> (a -> m) -> a -> m -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m
f) (m -> m m
forall (m :: * -> *) a. Monad m => a -> m a
return m
forall a. Monoid a => a
mempty)
instance {-# OVERLAPPING #-} F.Foldable (LogicT Identity) where
foldr :: (a -> b -> b) -> b -> LogicT Identity a -> b
foldr a -> b -> b
f b
z LogicT Identity a
m = LogicT Identity a -> (a -> b -> b) -> b -> b
forall a r. Logic a -> (a -> r -> r) -> r -> r
runLogic LogicT Identity a
m a -> b -> b
f b
z
#else
instance (Monad m, F.Foldable m) => F.Foldable (LogicT m) where
foldMap f m = F.fold $ unLogicT m (liftM . mappend . f) (return mempty)
#endif
instance T.Traversable (LogicT Identity) where
traverse :: (a -> f b) -> LogicT Identity a -> f (LogicT Identity b)
traverse a -> f b
g LogicT Identity a
l = LogicT Identity a
-> (a -> f (LogicT Identity b) -> f (LogicT Identity b))
-> f (LogicT Identity b)
-> f (LogicT Identity b)
forall a r. Logic a -> (a -> r -> r) -> r -> r
runLogic LogicT Identity a
l (\a
a f (LogicT Identity b)
ft -> b -> LogicT Identity b -> LogicT Identity b
forall (m :: * -> *) a. MonadPlus m => a -> m a -> m a
cons (b -> LogicT Identity b -> LogicT Identity b)
-> f b -> f (LogicT Identity b -> LogicT Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
g a
a f (LogicT Identity b -> LogicT Identity b)
-> f (LogicT Identity b) -> f (LogicT Identity b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (LogicT Identity b)
ft) (LogicT Identity b -> f (LogicT Identity b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure LogicT Identity b
forall (m :: * -> *) a. MonadPlus m => m a
mzero)
where cons :: a -> m a -> m a
cons a
a m a
l' = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` m a
l'
instance MonadReader r m => MonadReader r (LogicT m) where
ask :: LogicT m r
ask = m r -> LogicT m r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: * -> *). MonadReader r m => m r
ask
local :: (r -> r) -> LogicT m a -> LogicT m a
local r -> r
f (LogicT forall r. (a -> m r -> m r) -> m r -> m r
m) = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> do
r
env <- m r
forall r (m :: * -> *). MonadReader r m => m r
ask
(r -> r) -> m r -> m r
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ (a -> m r -> m r) -> m r -> m r
forall r. (a -> m r -> m r) -> m r -> m r
m (((r -> r) -> m r -> m r
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (r -> r -> r
forall a b. a -> b -> a
const r
env) (m r -> m r) -> (m r -> m r) -> m r -> m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((m r -> m r) -> m r -> m r)
-> (a -> m r -> m r) -> a -> m r -> m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m r -> m r
sk) ((r -> r) -> m r -> m r
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (r -> r -> r
forall a b. a -> b -> a
const r
env) m r
fk)
instance MonadState s m => MonadState s (LogicT m) where
get :: LogicT m s
get = m s -> LogicT m s
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m s
forall s (m :: * -> *). MonadState s m => m s
get
put :: s -> LogicT m ()
put = m () -> LogicT m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> LogicT m ()) -> (s -> m ()) -> s -> LogicT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put
instance MonadError e m => MonadError e (LogicT m) where
throwError :: e -> LogicT m a
throwError = m a -> LogicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> LogicT m a) -> (e -> m a) -> e -> LogicT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
catchError :: LogicT m a -> (e -> LogicT m a) -> LogicT m a
catchError LogicT m a
m e -> LogicT m a
h = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> let
handle :: m r -> m r
handle m r
r = m r
r m r -> (e -> m r) -> m r
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e
e -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (e -> LogicT m a
h e
e) a -> m r -> m r
sk m r
fk
in m r -> m r
handle (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a -> a -> m r -> m r
sk a
a (m r -> m r) -> (m r -> m r) -> m r -> m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m r -> m r
handle) m r
fk