-------------------------------------------------------------------------
-- |
-- Module      : Control.Monad.Logic.Class
-- 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  #-}

#if __GLASGOW_HASKELL__ >= 702
{-# LANGUAGE Safe #-}
#endif

module Control.Monad.Logic.Class (MonadLogic(..), reflect) where

import Control.Monad.Reader
import qualified Control.Monad.State.Lazy as LazyST
import qualified Control.Monad.State.Strict as StrictST

-------------------------------------------------------------------------------
-- | Minimal implementation: msplit
class (MonadPlus m) => MonadLogic m where
    -- | Attempts to split the computation, giving access to the first
    --   result. Satisfies the following laws:
    --
    --   > msplit mzero                == return Nothing
    --   > msplit (return a `mplus` m) == return (Just (a, m))
    msplit     :: m a -> m (Maybe (a, m a))

    -- | Fair disjunction. It is possible for a logical computation
    --   to have an infinite number of potential results, for instance:
    --
    --   > odds = return 1 `mplus` liftM (2+) odds
    --
    --   Such computations can cause problems in some circumstances. Consider:
    --
    --   > do x <- odds `mplus` return 2
    --   >    if even x then return x else mzero
    --
    --   Such a computation may never consider the 'return 2', and will
    --   therefore never terminate. By contrast, interleave ensures fair
    --   consideration of both branches of a disjunction
    interleave :: m a -> m a -> m a

    -- | Fair conjunction. Similarly to the previous function, consider
    --   the distributivity law for MonadPlus:
    --
    --   > (mplus a b) >>= k = (a >>= k) `mplus` (b >>= k)
    --
    --   If 'a >>= k' can backtrack arbitrarily many tmes, (b >>= k) may never
    --   be considered. (>>-) takes similar care to consider both branches of
    --   a disjunctive computation.
    (>>-)      :: m a -> (a -> m b) -> m b
    infixl 1 >>-

    -- | Logical conditional. The equivalent of Prolog's soft-cut. If its
    --   first argument succeeds at all, then the results will be fed into
    --   the success branch. Otherwise, the failure branch is taken.
    --   satisfies the following laws:
    --
    --   > ifte (return a) th el           == th a
    --   > ifte mzero th el                == el
    --   > ifte (return a `mplus` m) th el == th a `mplus` (m >>= th)
    ifte       :: m a -> (a -> m b) -> m b -> m b

    -- | Pruning. Selects one result out of many. Useful for when multiple
    --   results of a computation will be equivalent, or should be treated as
    --   such.
    once       :: m a -> m a

    -- | Inverts a logic computation. If @m@ succeeds with at least one value,
    -- @lnot m@ fails. If @m@ fails, then @lnot m@ succeeds the value @()@.
    lnot :: m a -> m ()

    -- All the class functions besides msplit can be derived from msplit, if
    -- desired
    interleave m a
m1 m a
m2 = m a -> m (Maybe (a, m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit m a
m1 m (Maybe (a, m a)) -> (Maybe (a, m a) -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                        m a -> ((a, m a) -> m a) -> Maybe (a, m a) -> m a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m a
m2 (\(a
a, m a
m1') -> 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 -> m a -> m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
interleave m a
m2 m a
m1')

    m a
m >>- a -> m b
f = do (a
a, m a
m') <- m (a, m a)
-> ((a, m a) -> m (a, m a)) -> Maybe (a, m a) -> m (a, m a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m (a, m a)
forall (m :: * -> *) a. MonadPlus m => m a
mzero (a, m a) -> m (a, m a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, m a) -> m (a, m a)) -> m (Maybe (a, m a)) -> m (a, m a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m a -> m (Maybe (a, m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit m a
m
                 m b -> m b -> m b
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
interleave (a -> m b
f a
a) (m a
m' m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- a -> m b
f)

    ifte m a
t a -> m b
th m b
el = m a -> m (Maybe (a, m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit m a
t m (Maybe (a, m a)) -> (Maybe (a, m a) -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m b -> ((a, m a) -> m b) -> Maybe (a, m a) -> m b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m b
el (\(a
a,m a
m) -> a -> m b
th a
a m b -> m b -> m b
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (m a
m m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
th))

    once m a
m = do (a
a, m a
_) <- m (a, m a)
-> ((a, m a) -> m (a, m a)) -> Maybe (a, m a) -> m (a, m a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m (a, m a)
forall (m :: * -> *) a. MonadPlus m => m a
mzero (a, m a) -> m (a, m a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, m a) -> m (a, m a)) -> m (Maybe (a, m a)) -> m (a, m a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m a -> m (Maybe (a, m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit m a
m
                a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

    lnot m a
m = m a -> (a -> m ()) -> m () -> m ()
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte (m a -> m a
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once m a
m) (m () -> a -> m ()
forall a b. a -> b -> a
const m ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero) (() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())


-------------------------------------------------------------------------------
-- | The inverse of msplit. Satisfies the following law:
--
-- > msplit m >>= reflect == m
reflect :: MonadLogic m => Maybe (a, m a) -> m a
reflect :: Maybe (a, m a) -> m a
reflect Maybe (a, m a)
Nothing = m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
reflect (Just (a
a, m a
m)) = 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
m

-- An instance of MonadLogic for lists
instance MonadLogic [] where
    msplit :: [a] -> [Maybe (a, [a])]
msplit []     = Maybe (a, [a]) -> [Maybe (a, [a])]
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, [a])
forall a. Maybe a
Nothing
    msplit (a
x:[a]
xs) = Maybe (a, [a]) -> [Maybe (a, [a])]
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, [a]) -> [Maybe (a, [a])])
-> Maybe (a, [a]) -> [Maybe (a, [a])]
forall a b. (a -> b) -> a -> b
$ (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
x, [a]
xs)

-- | Note that splitting a transformer does
-- not allow you to provide different input
-- to the monadic object returned.
-- For instance, in:
--
-- > let Just (_, rm') = runReaderT (msplit rm) r in runReaderT rm' r'
--
-- @r'@ will be ignored, because @r@ was already threaded through the
-- computation.
instance MonadLogic m => MonadLogic (ReaderT e m) where
    msplit :: ReaderT e m a -> ReaderT e m (Maybe (a, ReaderT e m a))
msplit ReaderT e m a
rm = (e -> m (Maybe (a, ReaderT e m a)))
-> ReaderT e m (Maybe (a, ReaderT e m a))
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((e -> m (Maybe (a, ReaderT e m a)))
 -> ReaderT e m (Maybe (a, ReaderT e m a)))
-> (e -> m (Maybe (a, ReaderT e m a)))
-> ReaderT e m (Maybe (a, ReaderT e m a))
forall a b. (a -> b) -> a -> b
$ \e
e -> do Maybe (a, m a)
r <- m a -> m (Maybe (a, m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit (m a -> m (Maybe (a, m a))) -> m a -> m (Maybe (a, m a))
forall a b. (a -> b) -> a -> b
$ ReaderT e m a -> e -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT e m a
rm e
e
                                   case Maybe (a, m a)
r of
                                     Maybe (a, m a)
Nothing -> Maybe (a, ReaderT e m a) -> m (Maybe (a, ReaderT e m a))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (a, ReaderT e m a)
forall a. Maybe a
Nothing
                                     Just (a
a, m a
m) -> Maybe (a, ReaderT e m a) -> m (Maybe (a, ReaderT e m a))
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, ReaderT e m a) -> Maybe (a, ReaderT e m a)
forall a. a -> Maybe a
Just (a
a, m a -> ReaderT e m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m a
m))

-- | See note on splitting above.
instance MonadLogic m => MonadLogic (StrictST.StateT s m) where
    msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a))
msplit StateT s m a
sm = (s -> m (Maybe (a, StateT s m a), s))
-> StateT s m (Maybe (a, StateT s m a))
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StrictST.StateT ((s -> m (Maybe (a, StateT s m a), s))
 -> StateT s m (Maybe (a, StateT s m a)))
-> (s -> m (Maybe (a, StateT s m a), s))
-> StateT s m (Maybe (a, StateT s m a))
forall a b. (a -> b) -> a -> b
$ \s
s ->
                    do Maybe ((a, s), m (a, s))
r <- m (a, s) -> m (Maybe ((a, s), m (a, s)))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit (StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m a
sm s
s)
                       case Maybe ((a, s), m (a, s))
r of
                            Maybe ((a, s), m (a, s))
Nothing          -> (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, StateT s m a)
forall a. Maybe a
Nothing, s
s)
                            Just ((a
a,s
s'), m (a, s)
m) ->
                                (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, StateT s m a) -> Maybe (a, StateT s m a)
forall a. a -> Maybe a
Just (a
a, (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StrictST.StateT (\s
_ -> m (a, s)
m)), s
s')

    interleave :: StateT s m a -> StateT s m a -> StateT s m a
interleave StateT s m a
ma StateT s m a
mb = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StrictST.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s ->
                        StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m a
ma s
s m (a, s) -> m (a, s) -> m (a, s)
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
`interleave` StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m a
mb s
s

    StateT s m a
ma >>- :: StateT s m a -> (a -> StateT s m b) -> StateT s m b
>>- a -> StateT s m b
f = (s -> m (b, s)) -> StateT s m b
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StrictST.StateT ((s -> m (b, s)) -> StateT s m b)
-> (s -> m (b, s)) -> StateT s m b
forall a b. (a -> b) -> a -> b
$ \s
s ->
                StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m a
ma s
s m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s)
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- \(a
a,s
s') -> StateT s m b -> s -> m (b, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT (a -> StateT s m b
f a
a) s
s'

    ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b
ifte StateT s m a
t a -> StateT s m b
th StateT s m b
el = (s -> m (b, s)) -> StateT s m b
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StrictST.StateT ((s -> m (b, s)) -> StateT s m b)
-> (s -> m (b, s)) -> StateT s m b
forall a b. (a -> b) -> a -> b
$ \s
s -> m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s) -> m (b, s)
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte (StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m a
t s
s)
                                                (\(a
a,s
s') -> StateT s m b -> s -> m (b, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT (a -> StateT s m b
th a
a) s
s')
                                                (StateT s m b -> s -> m (b, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m b
el s
s)

    once :: StateT s m a -> StateT s m a
once StateT s m a
ma = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StrictST.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> m (a, s) -> m (a, s)
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once (StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
StrictST.runStateT StateT s m a
ma s
s)

-- | See note on splitting above.
instance MonadLogic m => MonadLogic (LazyST.StateT s m) where
    msplit :: StateT s m a -> StateT s m (Maybe (a, StateT s m a))
msplit StateT s m a
sm = (s -> m (Maybe (a, StateT s m a), s))
-> StateT s m (Maybe (a, StateT s m a))
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
LazyST.StateT ((s -> m (Maybe (a, StateT s m a), s))
 -> StateT s m (Maybe (a, StateT s m a)))
-> (s -> m (Maybe (a, StateT s m a), s))
-> StateT s m (Maybe (a, StateT s m a))
forall a b. (a -> b) -> a -> b
$ \s
s ->
                    do Maybe ((a, s), m (a, s))
r <- m (a, s) -> m (Maybe ((a, s), m (a, s)))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit (StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m a
sm s
s)
                       case Maybe ((a, s), m (a, s))
r of
                            Maybe ((a, s), m (a, s))
Nothing -> (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (a, StateT s m a)
forall a. Maybe a
Nothing, s
s)
                            Just ((a
a,s
s'), m (a, s)
m) ->
                                (Maybe (a, StateT s m a), s) -> m (Maybe (a, StateT s m a), s)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, StateT s m a) -> Maybe (a, StateT s m a)
forall a. a -> Maybe a
Just (a
a, (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
LazyST.StateT (\s
_ -> m (a, s)
m)), s
s')

    interleave :: StateT s m a -> StateT s m a -> StateT s m a
interleave StateT s m a
ma StateT s m a
mb = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
LazyST.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s ->
                        StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m a
ma s
s m (a, s) -> m (a, s) -> m (a, s)
forall (m :: * -> *) a. MonadLogic m => m a -> m a -> m a
`interleave` StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m a
mb s
s

    StateT s m a
ma >>- :: StateT s m a -> (a -> StateT s m b) -> StateT s m b
>>- a -> StateT s m b
f = (s -> m (b, s)) -> StateT s m b
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
LazyST.StateT ((s -> m (b, s)) -> StateT s m b)
-> (s -> m (b, s)) -> StateT s m b
forall a b. (a -> b) -> a -> b
$ \s
s ->
                StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m a
ma s
s m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s)
forall (m :: * -> *) a b. MonadLogic m => m a -> (a -> m b) -> m b
>>- \(a
a,s
s') -> StateT s m b -> s -> m (b, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT (a -> StateT s m b
f a
a) s
s'

    ifte :: StateT s m a -> (a -> StateT s m b) -> StateT s m b -> StateT s m b
ifte StateT s m a
t a -> StateT s m b
th StateT s m b
el = (s -> m (b, s)) -> StateT s m b
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
LazyST.StateT ((s -> m (b, s)) -> StateT s m b)
-> (s -> m (b, s)) -> StateT s m b
forall a b. (a -> b) -> a -> b
$ \s
s -> m (a, s) -> ((a, s) -> m (b, s)) -> m (b, s) -> m (b, s)
forall (m :: * -> *) a b.
MonadLogic m =>
m a -> (a -> m b) -> m b -> m b
ifte (StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m a
t s
s)
                                              (\(a
a,s
s') -> StateT s m b -> s -> m (b, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT (a -> StateT s m b
th a
a) s
s')
                                              (StateT s m b -> s -> m (b, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m b
el s
s)

    once :: StateT s m a -> StateT s m a
once StateT s m a
ma = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
LazyST.StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> m (a, s) -> m (a, s)
forall (m :: * -> *) a. MonadLogic m => m a -> m a
once (StateT s m a -> s -> m (a, s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
LazyST.runStateT StateT s m a
ma s
s)