-------------------------------------------------------------------------
-- |
-- Module      : Control.Monad.Logic
-- Copyright   : (c) 2007-2014 Dan Doel,
--               (c) 2011-2013 Edward Kmett,
--               (c) 2014      Roman Cheplyaka,
--               (c) 2020-2021 Andrew Lelechenko,
--               (c) 2020-2021 Kevin Quick
-- License     : BSD3
-- Maintainer  : Andrew Lelechenko <andrew.lelechenko@gmail.com>
--
-- Adapted from the paper
-- <http://okmij.org/ftp/papers/LogicT.pdf Backtracking, Interleaving, and Terminating Monad Transformers>
-- by Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, Amr Sabry.
-- Note that the paper uses 'MonadPlus' vocabulary
-- ('mzero' and 'mplus'),
-- while examples below prefer 'empty' and '<|>'
-- from 'Alternative'.
-------------------------------------------------------------------------

{-# LANGUAGE CPP                   #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE UndecidableInstances  #-}

#if __GLASGOW_HASKELL__ >= 704
{-# 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 Trans
  ) where

import Control.Applicative

import Control.Monad
import qualified Control.Monad.Fail as Fail
import Control.Monad.Identity (Identity(..))
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Trans (MonadTrans(..))
import qualified Control.Monad.Trans as Trans

import Control.Monad.Reader.Class (MonadReader(..))
import Control.Monad.State.Class (MonadState(..))
import Control.Monad.Error.Class (MonadError(..))

#if !MIN_VERSION_base(4,8,0)
import Data.Monoid (Monoid (..))
#endif

#if MIN_VERSION_base(4,9,0)
import Data.Semigroup (Semigroup (..))
#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 { forall (m :: * -> *) a.
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 if there are no results at all.
#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 :: forall (m :: * -> *) a. MonadFail m => LogicT m a -> m a
observeT LogicT m a
lt = LogicT m a -> forall r. (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
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.")

-------------------------------------------------------------------------
-- | Extracts all results from a 'LogicT' computation, unless blocked by the
-- underlying monad.
--
-- For example, given
--
-- >>> let nats = pure 0 <|> fmap (+ 1) nats
--
-- some monads (like 'Identity', 'Control.Monad.Reader.Reader',
-- 'Control.Monad.Writer.Writer', and 'Control.Monad.State.State')
-- will be productive:
--
-- >>> take 5 $ runIdentity (observeAllT nats)
-- [0,1,2,3,4]
--
-- but others (like 'Control.Monad.Except.ExceptT',
-- and 'Control.Monad.Cont.ContT') will not:
--
-- >>> take 20 <$> runExcept (observeAllT nats)
--
-- In general, if the underlying monad manages control flow then
-- 'observeAllT' may be unproductive under infinite branching,
-- and 'observeManyT' should be used instead.
observeAllT :: Applicative m => LogicT m a -> m [a]
observeAllT :: forall (m :: * -> *) a. Applicative m => LogicT m a -> m [a]
observeAllT LogicT m a
m = LogicT m a -> forall r. (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 [a] -> m [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([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 (f :: * -> *) a. Applicative f => a -> f a
pure [])

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a 'LogicT' computation.
observeManyT :: Monad m => Int -> LogicT m a -> m [a]
observeManyT :: forall (m :: * -> *) a. Monad m => 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 -> forall r. (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 [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))
-> forall r. (Maybe (a, LogicT m 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 -> 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'

-------------------------------------------------------------------------
-- | Runs a 'LogicT' computation with the specified initial success and
-- failure continuations.
--
-- The second argument ("success continuation") takes one result of
-- the 'LogicT' computation and the monad to run for any subsequent
-- matches.
--
-- The third argument ("failure continuation") is called when the
-- 'LogicT' cannot produce any more results.
--
-- For example:
--
-- >>> yieldWords = foldr ((<|>) . pure) empty
-- >>> showEach wrd nxt = putStrLn wrd >> nxt
-- >>> runLogicT (yieldWords ["foo", "bar"]) showEach (putStrLn "none!")
-- foo
-- bar
-- none!
-- >>> runLogicT (yieldWords []) showEach (putStrLn "none!")
-- none!
-- >>> showFirst wrd _ = putStrLn wrd
-- >>> runLogicT (yieldWords ["foo", "bar"]) showFirst (putStrLn "none!")
-- foo
--
runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT :: forall (m :: * -> *) a r.
LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT (LogicT forall r. (a -> m r -> m r) -> m r -> m r
r) = (a -> m r -> m r) -> m r -> m r
forall r. (a -> m r -> m r) -> m r -> m r
r

-------------------------------------------------------------------------
-- | The basic 'Logic' monad, for performing backtracking computations
-- returning values (e.g. 'Logic' @a@ will return 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 a. (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)
-> LogicT Identity 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)
 -> LogicT Identity a)
-> (forall r.
    (a -> Identity r -> Identity r) -> Identity r -> Identity r)
-> LogicT Identity 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

-------------------------------------------------------------------------
-- | Extracts the first result from a 'Logic' computation, failing if
-- there are no results.
--
-- >>> observe (pure 5 <|> pure 3 <|> empty)
-- 5
--
-- >>> observe empty
-- *** Exception: No answer.
--
observe :: Logic a -> a
observe :: forall a. 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
-> forall r.
   (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
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 (f :: * -> *) a. Applicative f => a -> f a
pure) (String -> Identity a
forall a. HasCallStack => String -> a
error String
"No answer.")

-------------------------------------------------------------------------
-- | Extracts all results from a 'Logic' computation.
--
-- >>> observe (pure 5 <|> empty <|> empty <|> pure 3 <|> empty)
-- [5,3]
--
observeAll :: Logic a -> [a]
observeAll :: forall a. Logic a -> [a]
observeAll = Identity [a] -> [a]
forall a. Identity a -> a
runIdentity (Identity [a] -> [a])
-> (LogicT Identity a -> Identity [a]) -> LogicT Identity a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicT Identity a -> Identity [a]
forall (m :: * -> *) a. Applicative m => LogicT m a -> m [a]
observeAllT

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a 'Logic' computation.
--
-- >>> let nats = pure 0 <|> fmap (+ 1) nats
-- >>> observeMany 5 nats
-- [0,1,2,3,4]
--
observeMany :: Int -> Logic a -> [a]
observeMany :: forall a. 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
-- 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 empty (+) 0
-- 0
--
-- >>> runLogic (pure 5 <|> pure 3 <|> empty) (+) 0
-- 8
--
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic :: forall a r. 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
-> forall r.
   (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 :: forall a b. (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 -> forall r. (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 :: forall a. 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 <*> :: forall a b. 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)
-> forall r. ((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 -> forall r. (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 :: forall a. 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 <|> :: forall a. 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 -> forall r. (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 -> forall r. (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 :: forall a. a -> LogicT m a
return = a -> LogicT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    LogicT m a
m >>= :: forall a b. 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 -> forall r. (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 -> forall r. (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 :: forall a. 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 :: forall a. LogicT m a
mzero = LogicT m a
forall (f :: * -> *) a. Alternative f => f a
empty
  mplus :: forall a. LogicT m a -> LogicT m a -> LogicT m a
mplus = LogicT m a -> LogicT m a -> LogicT m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)

#if MIN_VERSION_base(4,9,0)
instance Semigroup (LogicT m a) where
  <> :: LogicT m a -> LogicT m a -> LogicT m a
(<>) = LogicT m a -> LogicT m a -> LogicT m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
  sconcat :: NonEmpty (LogicT m a) -> LogicT m a
sconcat = (LogicT m a -> LogicT m a -> LogicT m a)
-> NonEmpty (LogicT m a) -> LogicT m a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 LogicT m a -> LogicT m a -> LogicT m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
#endif

instance Monoid (LogicT m a) where
  mempty :: LogicT m a
mempty = LogicT m a
forall (f :: * -> *) a. Alternative f => f a
empty
  mappend :: LogicT m a -> LogicT m a -> LogicT m a
mappend = LogicT m a -> LogicT m a -> LogicT m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)
  mconcat :: [LogicT m a] -> LogicT m a
mconcat = [LogicT m a] -> LogicT m a
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
F.asum

instance MonadTrans LogicT where
    lift :: forall (m :: * -> *) a. Monad m => 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 :: forall a. 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 :: forall a. 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 -> forall r. (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 (Maybe (a, LogicT m a)) -> m (Maybe (a, LogicT m a))
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {m :: * -> *} {a}
       {b}.
(MonadTrans t, Monad m, Monad m, Monad (t m), Alternative (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. Alternative m => Maybe (a, m a) -> m a
reflect)
    once :: forall a. 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 -> forall r. (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 :: forall a. 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 -> forall r. (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 #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
    foldMap :: forall m a. Monoid m => (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 -> forall r. (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 -> m) -> m m -> m m
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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 (f :: * -> *) a. Applicative f => a -> f a
pure m
forall a. Monoid a => a
mempty)

instance {-# OVERLAPPING #-} F.Foldable (LogicT Identity) where
    foldr :: forall a b. (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 (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
    foldMap f m = F.fold $ unLogicT m (fmap . mappend . f) (pure mempty)

#endif

instance T.Traversable (LogicT Identity) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(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 {f :: * -> *} {a}. Alternative f => a -> f a -> f 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 (f :: * -> *) a. Alternative f => f a
empty)
    where
      cons :: a -> f a -> f a
cons a
a f a
l' = a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> f 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 :: forall a. (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)

-- 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 :: forall a. 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 :: forall a. 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 -> forall r. (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 -> forall r. (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