-------------------------------------------------------------------------
-- |
-- Module      : Control.Monad.Logic
-- Copyright   : (c) Dan Doel
-- License     : BSD3
--
-- Maintainer  : dan.doel@gmail.com
-- Stability   : experimental
-- Portability : non-portable (multi-parameter type classes)
--
-- A backtracking, logic programming monad.
--
--    Adapted from the paper
--    /Backtracking, Interleaving, and Terminating
--        Monad Transformers/, by
--    Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry
--    (<http://okmij.org/ftp/papers/LogicT.pdf>).
-------------------------------------------------------------------------

{-# 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,
    -- * The Logic monad
    Logic,
    logic,
    runLogic,
    observe,
    observeMany,
    observeAll,
    -- * The LogicT monad transformer
    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

-------------------------------------------------------------------------
-- | A monad transformer for performing backtracking computations
-- layered over another monad @m@.
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 }

-------------------------------------------------------------------------
-- | Extracts the first result from a LogicT computation,
-- failing otherwise.
#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 lt :: 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 "No answer.")

-------------------------------------------------------------------------
-- | Extracts all results from a LogicT computation.
observeAllT :: Monad m => LogicT m a -> m [a]
observeAllT :: LogicT m a -> m [a]
observeAllT m :: 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 [])

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a LogicT computation.
observeManyT :: Monad m => Int -> LogicT m a -> m [a]
observeManyT :: Int -> LogicT m a -> m [a]
observeManyT n :: Int
n m :: LogicT m a
m
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 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
== 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
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 Nothing _ = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
 sk (Just (a :: a
a, m' :: LogicT m a
m')) _ = (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
-1) LogicT m a
m'

-------------------------------------------------------------------------
-- | Runs a LogicT computation with the specified initial success and
-- failure continuations.
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

-------------------------------------------------------------------------
-- | The basic Logic monad, for performing backtracking computations
-- returning values of type @a@.
type Logic = LogicT Identity

-------------------------------------------------------------------------
-- | A smart constructor for Logic computations.
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic f :: 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
$ \k :: 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
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

-------------------------------------------------------------------------
-- | Extracts the first result from a Logic computation.
observe :: Logic a -> a
observe :: Logic a -> a
observe lt :: 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 "No answer.")

-------------------------------------------------------------------------
-- | Extracts all results from a Logic computation.
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

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a Logic computation.
observeMany :: Int -> Logic a -> [a]
observeMany :: Int -> Logic a -> [a]
observeMany i :: 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
-- Implementing 'observeMany' using 'observeManyT' is quite costly,
-- because it calls 'msplit' multiple times.

-------------------------------------------------------------------------
-- | Runs a Logic computation with the specified initial success and
-- failure continuations.
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic l :: Logic a
l s :: a -> r -> r
s f :: 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 f :: a -> b
f lt :: 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
$ \sk :: b -> f r -> f r
sk fk :: 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
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
$ \sk :: a -> f r -> f r
sk fk :: f r
fk -> a -> f r -> f r
sk a
a f r
fk
    f :: LogicT f (a -> b)
f <*> :: LogicT f (a -> b) -> LogicT f a -> LogicT f b
<*> a :: 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
$ \sk :: b -> f r -> f r
sk fk :: 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 (\g :: a -> b
g fk' :: 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
$ \_ fk :: f r
fk -> f r
fk
    f1 :: LogicT f a
f1 <|> :: LogicT f a -> LogicT f a -> LogicT f a
<|> f2 :: 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
$ \sk :: a -> f r -> f r
sk fk :: 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
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
$ \sk :: a -> m r -> m r
sk fk :: m r
fk -> a -> m r -> m r
sk a
a m r
fk
    m :: LogicT m a
m >>= :: LogicT m a -> (a -> LogicT m b) -> LogicT m b
>>= f :: 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
$ \sk :: b -> m r -> m r
sk fk :: 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
a fk' :: 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 _ = (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
$ \_ fk :: 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
$ \_ fk :: m r
fk -> m r
fk
    m1 :: LogicT m a
m1 mplus :: LogicT m a -> LogicT m a -> LogicT m a
`mplus` m2 :: 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
$ \sk :: a -> m r -> m r
sk fk :: 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 :: 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
$ \sk :: a -> m r -> m r
sk fk :: 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 -> 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' is quite costly even if the base 'Monad' is 'Identity'.
    -- Try to avoid it.
    msplit :: LogicT m a -> LogicT m (Maybe (a, LogicT m a))
msplit m :: 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
a fk :: 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 m :: 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
$ \sk :: a -> m r -> m r
sk fk :: 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
a _ -> a -> m r -> m r
sk a
a m r
fk) m r
fk
    lnot :: LogicT m a -> LogicT m ()
lnot m :: 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
$ \sk :: () -> m r -> m r
sk fk :: 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 (\_ _ -> 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 f :: a -> m
f m :: 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 f :: a -> b -> b
f z :: b
z m :: 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 g :: a -> f b
g l :: 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
a ft :: 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
a l' :: 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'

-- Needs undecidable instances
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 f :: r -> r
f (LogicT m :: 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
$ \sk :: a -> m r -> m r
sk fk :: 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)

-- Needs undecidable instances
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

-- Needs undecidable instances
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 m :: LogicT m a
m h :: 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
$ \sk :: a -> m r -> m r
sk fk :: m r
fk -> let
      handle :: m r -> m r
handle r :: 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
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 -> 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