    -------------------------------------------------------------------------
    -- |
    -- 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