-------------------------------------------------------------------------
-- |
-- 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 DeriveFoldable        #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# 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,
    fromLogicT,
    fromLogicTWith,
    hoistLogicT,
    embedLogicT
  ) 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(..))
#if MIN_VERSION_base(4,8,0)
import Control.Monad.Zip (MonadZip (..))
#endif

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@.
--
-- When @m@ is 'Identity', 'LogicT' @m@ becomes isomorphic to a list
-- (see 'Logic'). Thus 'LogicT' @m@ for non-trivial @m@ can be imagined
-- as a list, pattern matching on which causes monadic effects.
--
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 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 :: LogicT m a -> m a
observeT LogicT m a
lt = LogicT m a -> (a -> m a -> m a) -> m a -> m a
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
lt (m a -> m a -> m a
forall a b. a -> b -> a
const (m a -> m a -> m a) -> (a -> m a) -> a -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return) (String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No answer.")

-------------------------------------------------------------------------
-- | 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 :: LogicT m a -> m [a]
observeAllT LogicT m a
m = LogicT m a -> (a -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (([a] -> [a]) -> m [a] -> m [a]
forall (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 :: Int -> LogicT m a -> m [a]
observeManyT Int
n LogicT m a
m
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = LogicT m a -> (a -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m [a]
_ -> [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a]) ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
    | Bool
otherwise = LogicT m (Maybe (a, LogicT m a))
-> (Maybe (a, LogicT m a) -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (LogicT m a -> LogicT m (Maybe (a, LogicT m a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit LogicT m a
m) Maybe (a, LogicT m a) -> m [a] -> m [a]
forall (m :: * -> *) a p.
Monad m =>
Maybe (a, LogicT m a) -> p -> m [a]
sk ([a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
 where
 sk :: Maybe (a, LogicT m a) -> p -> m [a]
sk Maybe (a, LogicT m a)
Nothing p
_ = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
 sk (Just (a
a, LogicT m a
m')) p
_ = (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([a] -> [a]) -> m [a] -> m [a]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` Int -> LogicT m a -> m [a]
forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
observeManyT (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) LogicT m a
m'

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

-- | Convert from 'LogicT' to an arbitrary logic-like monad transformer,
-- such as <https://hackage.haskell.org/package/list-t list-t>
-- or <https://hackage.haskell.org/package/logict-sequence logict-sequence>
--
-- For example, to show a representation of the structure of a `LogicT`
-- computation, @l@, over a data-like `Monad` (such as @[]@,
-- @Data.Sequence.Seq@, etc.), you could write
--
-- @
-- import ListT (ListT)
--
-- 'show' $ fromLogicT @ListT l
-- @
#if MIN_VERSION_base(4,8,0)
fromLogicT :: (Alternative (t m), MonadTrans t, Monad m, Monad (t m))
  => LogicT m a -> t m a
#else
fromLogicT :: (Alternative (t m), MonadTrans t, Applicative m, Monad m, Monad (t m))
  => LogicT m a -> t m a
#endif
fromLogicT :: LogicT m a -> t m a
fromLogicT = (forall x. m x -> t m x) -> LogicT m a -> t m a
forall (m :: * -> *) (n :: * -> *) a.
(Applicative m, Monad n, Alternative n) =>
(forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith forall x. m x -> t m x
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

-- | Convert from @'LogicT' m@ to an arbitrary logic-like monad,
-- such as @[]@.
--
-- Examples:
--
-- @
-- 'fromLogicT' = fromLogicTWith d
-- 'hoistLogicT' f = fromLogicTWith ('lift' . f)
-- 'embedLogicT' f = 'fromLogicTWith' f
-- @
--
-- The first argument should be a
-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
-- to produce sensible results.
fromLogicTWith :: (Applicative m, Monad n, Alternative n)
  => (forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith :: (forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith forall x. m x -> n x
p (LogicT forall r. (a -> m r -> m r) -> m r -> m r
f) = n (n a) -> n a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (n (n a) -> n a) -> (m (n a) -> n (n a)) -> m (n a) -> n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (n a) -> n (n a)
forall x. m x -> n x
p (m (n a) -> n a) -> m (n a) -> n a
forall a b. (a -> b) -> a -> b
$
  (a -> m (n a) -> m (n a)) -> m (n a) -> m (n a)
forall r. (a -> m r -> m r) -> m r -> m r
f (\a
a m (n a)
v -> n a -> m (n a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a n a -> n a -> n a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> n (n a) -> n a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (n a) -> n (n a)
forall x. m x -> n x
p m (n a)
v))) (n a -> m (n a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure n a
forall (f :: * -> *) a. Alternative f => f a
empty)

-- | Convert a 'LogicT' computation from one underlying monad to another.
-- For example,
--
-- @
-- hoistLogicT lift :: LogicT m a -> LogicT (StateT m) a
-- @
--
-- The first argument should be a
-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
-- to produce sensible results.
hoistLogicT :: (Applicative m, Monad n) => (forall x. m x -> n x) -> LogicT m a -> LogicT n a
hoistLogicT :: (forall x. m x -> n x) -> LogicT m a -> LogicT n a
hoistLogicT forall x. m x -> n x
f = (forall x. m x -> LogicT n x) -> LogicT m a -> LogicT n a
forall (m :: * -> *) (n :: * -> *) a.
(Applicative m, Monad n, Alternative n) =>
(forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith (n x -> LogicT n x
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n x -> LogicT n x) -> (m x -> n x) -> m x -> LogicT n x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m x -> n x
forall x. m x -> n x
f)

-- | Convert a 'LogicT' computation from one underlying monad to another.
--
-- The first argument should be a
-- <https://hackage.haskell.org/package/mmorph/docs/Control-Monad-Morph.html monad morphism>.
-- to produce sensible results.
embedLogicT :: Applicative m => (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
embedLogicT :: (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
embedLogicT forall a. m a -> LogicT n a
f = (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
forall (m :: * -> *) (n :: * -> *) a.
(Applicative m, Monad n, Alternative n) =>
(forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith forall a. m a -> LogicT n a
f

-------------------------------------------------------------------------
-- | The basic 'Logic' monad, for performing backtracking computations
-- returning values (e.g. 'Logic' @a@ will return values of type @a@).
--
-- __Technical perspective.__
-- 'Logic' is a
-- <http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html Boehm-Berarducci encoding>
-- of lists. Speaking plainly, its type is identical (up to 'Identity' wrappers)
-- to 'foldr' applied to a given list. And this list itself can be reconstructed
-- by supplying @(:)@ and @[]@.
--
-- > import Data.Functor.Identity
-- >
-- > fromList :: [a] -> Logic a
-- > fromList xs = LogicT $ \cons nil -> foldr cons nil xs
-- >
-- > toList :: Logic a -> [a]
-- > toList (LogicT fld) = runIdentity $ fld (\x (Identity xs) -> Identity (x : xs)) (Identity [])
--
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 forall r. (a -> r -> r) -> r -> r
f = (forall r.
 (a -> Identity r -> Identity r) -> Identity r -> Identity r)
-> Logic a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r.
  (a -> Identity r -> Identity r) -> Identity r -> Identity r)
 -> Logic a)
-> (forall r.
    (a -> Identity r -> Identity r) -> Identity r -> Identity r)
-> Logic a
forall a b. (a -> b) -> a -> b
$ \a -> Identity r -> Identity r
k -> r -> Identity r
forall a. a -> Identity a
Identity (r -> Identity r) -> (Identity r -> r) -> Identity r -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         (a -> r -> r) -> r -> r
forall r. (a -> r -> r) -> r -> r
f (\a
a -> Identity r -> r
forall a. Identity a -> a
runIdentity (Identity r -> r) -> (r -> Identity r) -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity r -> Identity r
k a
a (Identity r -> Identity r) -> (r -> Identity r) -> r -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> Identity r
forall a. a -> Identity a
Identity) (r -> r) -> (Identity r -> r) -> Identity r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         Identity r -> r
forall a. Identity a -> a
runIdentity

-------------------------------------------------------------------------
-- | 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.
--
-- Since 'Logic' is isomorphic to a list, 'observe' is analogous to 'head'.
--
observe :: Logic a -> a
observe :: Logic a -> a
observe Logic a
lt = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ Logic a
-> (a -> Identity a -> Identity a) -> Identity a -> Identity a
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT Logic a
lt (Identity a -> Identity a -> Identity a
forall a b. a -> b -> a
const (Identity a -> Identity a -> Identity a)
-> (a -> Identity a) -> a -> Identity a -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall (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.
--
-- >>> observeAll (pure 5 <|> empty <|> empty <|> pure 3 <|> empty)
-- [5,3]
--
-- 'observeAll' reveals a half of the isomorphism between 'Logic'
-- and lists. See description of 'runLogic' for the other half.
--
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. 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]
--
-- Since 'Logic' is isomorphic to a list, 'observeMany' is analogous to 'take'.
--
observeMany :: Int -> Logic a -> [a]
observeMany :: Int -> Logic a -> [a]
observeMany Int
i = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
i ([a] -> [a]) -> (Logic a -> [a]) -> Logic a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Logic a -> [a]
forall a. Logic a -> [a]
observeAll
-- 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
--
-- When invoked with @(:)@ and @[]@ as arguments, reveals
-- a half of the isomorphism between 'Logic' and lists.
-- See description of 'observeAll' for the other half.
--
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic Logic a
l a -> r -> r
s r
f = Identity r -> r
forall a. Identity a -> a
runIdentity (Identity r -> r) -> Identity r -> r
forall a b. (a -> b) -> a -> b
$ Logic a
-> (a -> Identity r -> Identity r) -> Identity r -> Identity r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT Logic a
l a -> Identity r -> Identity r
si Identity r
fi
 where
 si :: a -> Identity r -> Identity r
si = (r -> r) -> Identity r -> Identity r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((r -> r) -> Identity r -> Identity r)
-> (a -> r -> r) -> a -> Identity r -> Identity r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> r -> r
s
 fi :: Identity r
fi = r -> Identity r
forall a. a -> Identity a
Identity r
f

instance Functor (LogicT f) where
    fmap :: (a -> b) -> LogicT f a -> LogicT f b
fmap a -> b
f LogicT f a
lt = (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b)
-> (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall a b. (a -> b) -> a -> b
$ \b -> f r -> f r
sk f r
fk -> LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
lt (b -> f r -> f r
sk (b -> f r -> f r) -> (a -> b) -> a -> f r -> f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f r
fk

instance Applicative (LogicT f) where
    pure :: a -> LogicT f a
pure a
a = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
-> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall a b. (a -> b) -> a -> b
$ \a -> f r -> f r
sk f r
fk -> a -> f r -> f r
sk a
a f r
fk
    LogicT f (a -> b)
f <*> :: LogicT f (a -> b) -> LogicT f a -> LogicT f b
<*> LogicT f a
a = (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b)
-> (forall r. (b -> f r -> f r) -> f r -> f r) -> LogicT f b
forall a b. (a -> b) -> a -> b
$ \b -> f r -> f r
sk f r
fk -> LogicT f (a -> b) -> ((a -> b) -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f (a -> b)
f (\a -> b
g f r
fk' -> LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
a (b -> f r -> f r
sk (b -> f r -> f r) -> (a -> b) -> a -> f r -> f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g) f r
fk') f r
fk

instance Alternative (LogicT f) where
    empty :: LogicT f a
empty = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
-> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall a b. (a -> b) -> a -> b
$ \a -> f r -> f r
_ f r
fk -> f r
fk
    LogicT f a
f1 <|> :: LogicT f a -> LogicT f a -> LogicT f a
<|> LogicT f a
f2 = (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a)
-> (forall r. (a -> f r -> f r) -> f r -> f r) -> LogicT f a
forall a b. (a -> b) -> a -> b
$ \a -> f r -> f r
sk f r
fk -> LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
f1 a -> f r -> f r
sk (LogicT f a -> (a -> f r -> f r) -> f r -> f r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT f a
f2 a -> f r -> f r
sk f r
fk)

instance Monad (LogicT m) where
    return :: a -> LogicT m a
return = a -> LogicT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    LogicT m a
m >>= :: LogicT m a -> (a -> LogicT m b) -> LogicT m b
>>= a -> LogicT m b
f = (forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b)
-> (forall r. (b -> m r -> m r) -> m r -> m r) -> LogicT m b
forall a b. (a -> b) -> a -> b
$ \b -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m r
fk' -> LogicT m b -> (b -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (a -> LogicT m b
f a
a) b -> m r -> m r
sk m r
fk') m r
fk
#if !MIN_VERSION_base(4,13,0)
    fail = Fail.fail
#endif

instance Fail.MonadFail (LogicT m) where
    fail :: String -> LogicT m a
fail String
_ = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
_ m r
fk -> m r
fk

instance MonadPlus (LogicT m) where
  mzero :: LogicT m a
mzero = LogicT m a
forall (f :: * -> *) a. Alternative f => f a
empty
  mplus :: 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
#if MIN_VERSION_base(4,9,0)
  mappend :: LogicT m a -> LogicT m a -> LogicT m a
mappend = LogicT m a -> LogicT m a -> LogicT m a
forall a. Semigroup a => a -> a -> a
(<>)
#else
  mappend = (<|>)
#endif
  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 :: m a -> LogicT m a
lift m a
m = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> m a
m m a -> (a -> m r) -> m r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> a -> m r -> m r
sk a
a m r
fk

instance (MonadIO m) => MonadIO (LogicT m) where
    liftIO :: IO a -> LogicT m a
liftIO = m a -> LogicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> LogicT m a) -> (IO a -> m a) -> IO a -> LogicT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

instance (Monad m) => MonadLogic (LogicT m) where
    -- 'msplit' 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 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, 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 :: LogicT m a -> LogicT m a
once LogicT m a
m = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m r
_ -> a -> m r -> m r
sk a
a m r
fk) m r
fk
    lnot :: LogicT m a -> LogicT m ()
lnot LogicT m a
m = (forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ()
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ())
-> (forall r. (() -> m r -> m r) -> m r -> m r) -> LogicT m ()
forall a b. (a -> b) -> a -> b
$ \() -> m r -> m r
sk m r
fk -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
_ m r
_ -> m r
fk) (() -> m r -> m r
sk () m r
fk)

#if MIN_VERSION_base(4,8,0)

instance {-# OVERLAPPABLE #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
    foldMap :: (a -> m) -> LogicT m a -> m
foldMap a -> m
f LogicT m a
m = m m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
F.fold (m m -> m) -> m m -> m
forall a b. (a -> b) -> a -> b
$ LogicT m a -> (a -> m m -> m m) -> m m -> m m
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m ((m -> m) -> m m -> m m
forall (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 :: (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

-- A much simpler logic monad representation used to define the Traversable and
-- MonadZip instances. This is essentially the same as ListT from the list-t
-- package, but it uses a slightly more efficient representation: MLView m a is
-- more compact than Maybe (a, ML m a), and the additional laziness in the
-- latter appears to be incidental/historical.
newtype ML m a = ML (m (MLView m a))
  deriving (a -> ML m b -> ML m a
(a -> b) -> ML m a -> ML m b
(forall a b. (a -> b) -> ML m a -> ML m b)
-> (forall a b. a -> ML m b -> ML m a) -> Functor (ML m)
forall a b. a -> ML m b -> ML m a
forall a b. (a -> b) -> ML m a -> ML m b
forall (m :: * -> *) a b. Functor m => a -> ML m b -> ML m a
forall (m :: * -> *) a b. Functor m => (a -> b) -> ML m a -> ML m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ML m b -> ML m a
$c<$ :: forall (m :: * -> *) a b. Functor m => a -> ML m b -> ML m a
fmap :: (a -> b) -> ML m a -> ML m b
$cfmap :: forall (m :: * -> *) a b. Functor m => (a -> b) -> ML m a -> ML m b
Functor, ML m a -> Bool
(a -> m) -> ML m a -> m
(a -> b -> b) -> b -> ML m a -> b
(forall m. Monoid m => ML m m -> m)
-> (forall m a. Monoid m => (a -> m) -> ML m a -> m)
-> (forall m a. Monoid m => (a -> m) -> ML m a -> m)
-> (forall a b. (a -> b -> b) -> b -> ML m a -> b)
-> (forall a b. (a -> b -> b) -> b -> ML m a -> b)
-> (forall b a. (b -> a -> b) -> b -> ML m a -> b)
-> (forall b a. (b -> a -> b) -> b -> ML m a -> b)
-> (forall a. (a -> a -> a) -> ML m a -> a)
-> (forall a. (a -> a -> a) -> ML m a -> a)
-> (forall a. ML m a -> [a])
-> (forall a. ML m a -> Bool)
-> (forall a. ML m a -> Int)
-> (forall a. Eq a => a -> ML m a -> Bool)
-> (forall a. Ord a => ML m a -> a)
-> (forall a. Ord a => ML m a -> a)
-> (forall a. Num a => ML m a -> a)
-> (forall a. Num a => ML m a -> a)
-> Foldable (ML m)
forall a. Eq a => a -> ML m a -> Bool
forall a. Num a => ML m a -> a
forall a. Ord a => ML m a -> a
forall m. Monoid m => ML m m -> m
forall a. ML m a -> Bool
forall a. ML m a -> Int
forall a. ML m a -> [a]
forall a. (a -> a -> a) -> ML m a -> a
forall m a. Monoid m => (a -> m) -> ML m a -> m
forall b a. (b -> a -> b) -> b -> ML m a -> b
forall a b. (a -> b -> b) -> b -> ML m a -> b
forall (m :: * -> *) a. (Foldable m, Eq a) => a -> ML m a -> Bool
forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
forall (m :: * -> *) m. (Foldable m, Monoid m) => ML m m -> m
forall (m :: * -> *) a. Foldable m => ML m a -> Bool
forall (m :: * -> *) a. Foldable m => ML m a -> Int
forall (m :: * -> *) a. Foldable m => ML m a -> [a]
forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> ML m a -> m
forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> ML m a -> b
forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> ML m a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: ML m a -> a
$cproduct :: forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
sum :: ML m a -> a
$csum :: forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
minimum :: ML m a -> a
$cminimum :: forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
maximum :: ML m a -> a
$cmaximum :: forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
elem :: a -> ML m a -> Bool
$celem :: forall (m :: * -> *) a. (Foldable m, Eq a) => a -> ML m a -> Bool
length :: ML m a -> Int
$clength :: forall (m :: * -> *) a. Foldable m => ML m a -> Int
null :: ML m a -> Bool
$cnull :: forall (m :: * -> *) a. Foldable m => ML m a -> Bool
toList :: ML m a -> [a]
$ctoList :: forall (m :: * -> *) a. Foldable m => ML m a -> [a]
foldl1 :: (a -> a -> a) -> ML m a -> a
$cfoldl1 :: forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
foldr1 :: (a -> a -> a) -> ML m a -> a
$cfoldr1 :: forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
foldl' :: (b -> a -> b) -> b -> ML m a -> b
$cfoldl' :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> ML m a -> b
foldl :: (b -> a -> b) -> b -> ML m a -> b
$cfoldl :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> ML m a -> b
foldr' :: (a -> b -> b) -> b -> ML m a -> b
$cfoldr' :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> ML m a -> b
foldr :: (a -> b -> b) -> b -> ML m a -> b
$cfoldr :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> ML m a -> b
foldMap' :: (a -> m) -> ML m a -> m
$cfoldMap' :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> ML m a -> m
foldMap :: (a -> m) -> ML m a -> m
$cfoldMap :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> ML m a -> m
fold :: ML m m -> m
$cfold :: forall (m :: * -> *) m. (Foldable m, Monoid m) => ML m m -> m
F.Foldable, Functor (ML m)
Foldable (ML m)
Functor (ML m)
-> Foldable (ML m)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ML m a -> f (ML m b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    ML m (f a) -> f (ML m a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ML m a -> m (ML m b))
-> (forall (m :: * -> *) a. Monad m => ML m (m a) -> m (ML m a))
-> Traversable (ML m)
(a -> f b) -> ML m a -> f (ML m b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *). Traversable m => Functor (ML m)
forall (m :: * -> *). Traversable m => Foldable (ML m)
forall (m :: * -> *) (m :: * -> *) a.
(Traversable m, Monad m) =>
ML m (m a) -> m (ML m a)
forall (m :: * -> *) (f :: * -> *) a.
(Traversable m, Applicative f) =>
ML m (f a) -> f (ML m a)
forall (m :: * -> *) (m :: * -> *) a b.
(Traversable m, Monad m) =>
(a -> m b) -> ML m a -> m (ML m b)
forall (m :: * -> *) (f :: * -> *) a b.
(Traversable m, Applicative f) =>
(a -> f b) -> ML m a -> f (ML m b)
forall (m :: * -> *) a. Monad m => ML m (m a) -> m (ML m a)
forall (f :: * -> *) a. Applicative f => ML m (f a) -> f (ML m a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ML m a -> m (ML m b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ML m a -> f (ML m b)
sequence :: ML m (m a) -> m (ML m a)
$csequence :: forall (m :: * -> *) (m :: * -> *) a.
(Traversable m, Monad m) =>
ML m (m a) -> m (ML m a)
mapM :: (a -> m b) -> ML m a -> m (ML m b)
$cmapM :: forall (m :: * -> *) (m :: * -> *) a b.
(Traversable m, Monad m) =>
(a -> m b) -> ML m a -> m (ML m b)
sequenceA :: ML m (f a) -> f (ML m a)
$csequenceA :: forall (m :: * -> *) (f :: * -> *) a.
(Traversable m, Applicative f) =>
ML m (f a) -> f (ML m a)
traverse :: (a -> f b) -> ML m a -> f (ML m b)
$ctraverse :: forall (m :: * -> *) (f :: * -> *) a b.
(Traversable m, Applicative f) =>
(a -> f b) -> ML m a -> f (ML m b)
$cp2Traversable :: forall (m :: * -> *). Traversable m => Foldable (ML m)
$cp1Traversable :: forall (m :: * -> *). Traversable m => Functor (ML m)
T.Traversable)

data MLView m a = EmptyML | ConsML a (ML m a)
  deriving (a -> MLView m b -> MLView m a
(a -> b) -> MLView m a -> MLView m b
(forall a b. (a -> b) -> MLView m a -> MLView m b)
-> (forall a b. a -> MLView m b -> MLView m a)
-> Functor (MLView m)
forall a b. a -> MLView m b -> MLView m a
forall a b. (a -> b) -> MLView m a -> MLView m b
forall (m :: * -> *) a b.
Functor m =>
a -> MLView m b -> MLView m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> MLView m a -> MLView m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> MLView m b -> MLView m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> MLView m b -> MLView m a
fmap :: (a -> b) -> MLView m a -> MLView m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> MLView m a -> MLView m b
Functor, MLView m a -> Bool
(a -> m) -> MLView m a -> m
(a -> b -> b) -> b -> MLView m a -> b
(forall m. Monoid m => MLView m m -> m)
-> (forall m a. Monoid m => (a -> m) -> MLView m a -> m)
-> (forall m a. Monoid m => (a -> m) -> MLView m a -> m)
-> (forall a b. (a -> b -> b) -> b -> MLView m a -> b)
-> (forall a b. (a -> b -> b) -> b -> MLView m a -> b)
-> (forall b a. (b -> a -> b) -> b -> MLView m a -> b)
-> (forall b a. (b -> a -> b) -> b -> MLView m a -> b)
-> (forall a. (a -> a -> a) -> MLView m a -> a)
-> (forall a. (a -> a -> a) -> MLView m a -> a)
-> (forall a. MLView m a -> [a])
-> (forall a. MLView m a -> Bool)
-> (forall a. MLView m a -> Int)
-> (forall a. Eq a => a -> MLView m a -> Bool)
-> (forall a. Ord a => MLView m a -> a)
-> (forall a. Ord a => MLView m a -> a)
-> (forall a. Num a => MLView m a -> a)
-> (forall a. Num a => MLView m a -> a)
-> Foldable (MLView m)
forall a. Eq a => a -> MLView m a -> Bool
forall a. Num a => MLView m a -> a
forall a. Ord a => MLView m a -> a
forall m. Monoid m => MLView m m -> m
forall a. MLView m a -> Bool
forall a. MLView m a -> Int
forall a. MLView m a -> [a]
forall a. (a -> a -> a) -> MLView m a -> a
forall m a. Monoid m => (a -> m) -> MLView m a -> m
forall b a. (b -> a -> b) -> b -> MLView m a -> b
forall a b. (a -> b -> b) -> b -> MLView m a -> b
forall (m :: * -> *) a.
(Foldable m, Eq a) =>
a -> MLView m a -> Bool
forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
forall (m :: * -> *) m. (Foldable m, Monoid m) => MLView m m -> m
forall (m :: * -> *) a. Foldable m => MLView m a -> Bool
forall (m :: * -> *) a. Foldable m => MLView m a -> Int
forall (m :: * -> *) a. Foldable m => MLView m a -> [a]
forall (m :: * -> *) a.
Foldable m =>
(a -> a -> a) -> MLView m a -> a
forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> MLView m a -> m
forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> MLView m a -> b
forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> MLView m a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: MLView m a -> a
$cproduct :: forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
sum :: MLView m a -> a
$csum :: forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
minimum :: MLView m a -> a
$cminimum :: forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
maximum :: MLView m a -> a
$cmaximum :: forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
elem :: a -> MLView m a -> Bool
$celem :: forall (m :: * -> *) a.
(Foldable m, Eq a) =>
a -> MLView m a -> Bool
length :: MLView m a -> Int
$clength :: forall (m :: * -> *) a. Foldable m => MLView m a -> Int
null :: MLView m a -> Bool
$cnull :: forall (m :: * -> *) a. Foldable m => MLView m a -> Bool
toList :: MLView m a -> [a]
$ctoList :: forall (m :: * -> *) a. Foldable m => MLView m a -> [a]
foldl1 :: (a -> a -> a) -> MLView m a -> a
$cfoldl1 :: forall (m :: * -> *) a.
Foldable m =>
(a -> a -> a) -> MLView m a -> a
foldr1 :: (a -> a -> a) -> MLView m a -> a
$cfoldr1 :: forall (m :: * -> *) a.
Foldable m =>
(a -> a -> a) -> MLView m a -> a
foldl' :: (b -> a -> b) -> b -> MLView m a -> b
$cfoldl' :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> MLView m a -> b
foldl :: (b -> a -> b) -> b -> MLView m a -> b
$cfoldl :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> MLView m a -> b
foldr' :: (a -> b -> b) -> b -> MLView m a -> b
$cfoldr' :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> MLView m a -> b
foldr :: (a -> b -> b) -> b -> MLView m a -> b
$cfoldr :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> MLView m a -> b
foldMap' :: (a -> m) -> MLView m a -> m
$cfoldMap' :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> MLView m a -> m
foldMap :: (a -> m) -> MLView m a -> m
$cfoldMap :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> MLView m a -> m
fold :: MLView m m -> m
$cfold :: forall (m :: * -> *) m. (Foldable m, Monoid m) => MLView m m -> m
F.Foldable)

instance T.Traversable m => T.Traversable (MLView m) where
  traverse :: (a -> f b) -> MLView m a -> f (MLView m b)
traverse a -> f b
_ MLView m a
EmptyML = MLView m b -> f (MLView m b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure MLView m b
forall (m :: * -> *) a. MLView m a
EmptyML
  traverse a -> f b
f (ConsML a
x (ML m (MLView m a)
m))
    = (b -> m (MLView m b) -> MLView m b)
-> f b -> f (m (MLView m b)) -> f (MLView m b)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\b
y m (MLView m b)
ym -> b -> ML m b -> MLView m b
forall (m :: * -> *) a. a -> ML m a -> MLView m a
ConsML b
y (m (MLView m b) -> ML m b
forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m b)
ym)) (a -> f b
f a
x) ((MLView m a -> f (MLView m b))
-> m (MLView m a) -> f (m (MLView m b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse ((a -> f b) -> MLView m a -> f (MLView m b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse a -> f b
f) m (MLView m a)
m)
  {- The derived instance would write the second case as
   -
   -   traverse f (ConsML x xs) = liftA2 ConsML (f x) (traverse @(ML m) f xs)
   -
   - Inlining the inner traverse gives
   -
   -   traverse f (ConsML x (ML m)) = liftA2 ConsML (f x) (ML <$> traverse (traverse f) m)
   -
   - revealing fmap under liftA2. We fuse those into a single application of liftA2,
   - in case fmap isn't free.
  -}

toML :: Applicative m => LogicT m a -> ML m a
toML :: LogicT m a -> ML m a
toML (LogicT forall r. (a -> m r -> m r) -> m r -> m r
q) = m (MLView m a) -> ML m a
forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML (m (MLView m a) -> ML m a) -> m (MLView m a) -> ML m a
forall a b. (a -> b) -> a -> b
$ (a -> m (MLView m a) -> m (MLView m a))
-> m (MLView m a) -> m (MLView m a)
forall r. (a -> m r -> m r) -> m r -> m r
q (\a
a m (MLView m a)
m -> MLView m a -> m (MLView m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MLView m a -> m (MLView m a)) -> MLView m a -> m (MLView m a)
forall a b. (a -> b) -> a -> b
$ a -> ML m a -> MLView m a
forall (m :: * -> *) a. a -> ML m a -> MLView m a
ConsML a
a (m (MLView m a) -> ML m a
forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m a)
m)) (MLView m a -> m (MLView m a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure MLView m a
forall (m :: * -> *) a. MLView m a
EmptyML)

fromML :: Monad m => ML m a -> LogicT m a
fromML :: ML m a -> LogicT m a
fromML (ML m (MLView m a)
m) = m (MLView m a) -> LogicT m (MLView m a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (MLView m a)
m LogicT m (MLView m a) -> (MLView m a -> LogicT m a) -> LogicT m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \MLView m a
r -> case MLView m a
r of
  MLView m a
EmptyML -> LogicT m a
forall (f :: * -> *) a. Alternative f => f a
empty
  ConsML a
a ML m a
xs -> a -> LogicT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a LogicT m a -> LogicT m a -> LogicT m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ML m a -> LogicT m a
forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML ML m a
xs

#if MIN_VERSION_base(4,8,0)
instance {-# OVERLAPPING #-} T.Traversable (LogicT Identity) where
  traverse :: (a -> f b) -> LogicT Identity a -> f (LogicT Identity b)
traverse a -> f b
g LogicT Identity a
l = LogicT Identity a
-> (a -> f (LogicT Identity b) -> f (LogicT Identity b))
-> f (LogicT Identity b)
-> f (LogicT Identity b)
forall a r. Logic a -> (a -> r -> r) -> r -> r
runLogic LogicT Identity a
l (\a
a f (LogicT Identity b)
ft -> b -> LogicT Identity b -> LogicT Identity b
forall (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'
instance {-# OVERLAPPABLE #-} (Monad m, T.Traversable m) => T.Traversable (LogicT m) where
  traverse :: (a -> f b) -> LogicT m a -> f (LogicT m b)
traverse a -> f b
f = (ML m b -> LogicT m b) -> f (ML m b) -> f (LogicT m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ML m b -> LogicT m b
forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML (f (ML m b) -> f (LogicT m b))
-> (LogicT m a -> f (ML m b)) -> LogicT m a -> f (LogicT m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f b) -> ML m a -> f (ML m b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse a -> f b
f (ML m a -> f (ML m b))
-> (LogicT m a -> ML m a) -> LogicT m a -> f (ML m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicT m a -> ML m a
forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML
#else
instance (Monad m, Applicative m, T.Traversable m) => T.Traversable (LogicT m) where
  traverse f = fmap fromML . T.traverse f . toML
#endif

#if MIN_VERSION_base(4,8,0)
zipWithML :: MonadZip m => (a -> b -> c) -> ML m a -> ML m b -> ML m c
zipWithML :: (a -> b -> c) -> ML m a -> ML m b -> ML m c
zipWithML a -> b -> c
f = ML m a -> ML m b -> ML m c
forall (m :: * -> *). MonadZip m => ML m a -> ML m b -> ML m c
go
    where
      go :: ML m a -> ML m b -> ML m c
go (ML m (MLView m a)
m1) (ML m (MLView m b)
m2) =
        m (MLView m c) -> ML m c
forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML (m (MLView m c) -> ML m c) -> m (MLView m c) -> ML m c
forall a b. (a -> b) -> a -> b
$ (MLView m a -> MLView m b -> MLView m c)
-> m (MLView m a) -> m (MLView m b) -> m (MLView m c)
forall (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> m a -> m b -> m c
mzipWith MLView m a -> MLView m b -> MLView m c
zv m (MLView m a)
m1 m (MLView m b)
m2
      zv :: MLView m a -> MLView m b -> MLView m c
zv (a
a `ConsML` ML m a
as) (b
b `ConsML` ML m b
bs) = a -> b -> c
f a
a b
b c -> ML m c -> MLView m c
forall (m :: * -> *) a. a -> ML m a -> MLView m a
`ConsML` ML m a -> ML m b -> ML m c
go ML m a
as ML m b
bs
      zv MLView m a
_ MLView m b
_ = MLView m c
forall (m :: * -> *) a. MLView m a
EmptyML

unzipML :: MonadZip m => ML m (a, b) -> (ML m a, ML m b)
unzipML :: ML m (a, b) -> (ML m a, ML m b)
unzipML (ML m (MLView m (a, b))
m)
    | (m (MLView m a)
l, m (MLView m b)
r) <- m (MLView m a, MLView m b) -> (m (MLView m a), m (MLView m b))
forall (m :: * -> *) a b. MonadZip m => m (a, b) -> (m a, m b)
munzip ((MLView m (a, b) -> (MLView m a, MLView m b))
-> m (MLView m (a, b)) -> m (MLView m a, MLView m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MLView m (a, b) -> (MLView m a, MLView m b)
forall (m :: * -> *) a a.
MonadZip m =>
MLView m (a, a) -> (MLView m a, MLView m a)
go m (MLView m (a, b))
m)
    = (m (MLView m a) -> ML m a
forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m a)
l, m (MLView m b) -> ML m b
forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m b)
r)
    where
      go :: MLView m (a, a) -> (MLView m a, MLView m a)
go MLView m (a, a)
EmptyML = (MLView m a
forall (m :: * -> *) a. MLView m a
EmptyML, MLView m a
forall (m :: * -> *) a. MLView m a
EmptyML)
      go ((a
a, a
b) `ConsML` ML m (a, a)
listab)
        = (a
a a -> ML m a -> MLView m a
forall (m :: * -> *) a. a -> ML m a -> MLView m a
`ConsML` ML m a
la, a
b a -> ML m a -> MLView m a
forall (m :: * -> *) a. a -> ML m a -> MLView m a
`ConsML` ML m a
lb)
        where
          -- If the underlying munzip is careful not to leak memory, then we
          -- don't want to defeat it. We need to be sure that la and lb are
          -- realized as selector thunks. Hopefully the CPSish conversion
          -- doesn't muck anything up at another level.
          {-# NOINLINE remains #-}
          {-# NOINLINE la #-}
          {-# NOINLINE lb #-}
          remains :: (ML m a, ML m a)
remains = ML m (a, a) -> (ML m a, ML m a)
forall (m :: * -> *) a b.
MonadZip m =>
ML m (a, b) -> (ML m a, ML m b)
unzipML ML m (a, a)
listab
          (ML m a
la, ML m a
lb) = (ML m a, ML m a)
remains

instance MonadZip m => MonadZip (LogicT m) where
  mzipWith :: (a -> b -> c) -> LogicT m a -> LogicT m b -> LogicT m c
mzipWith a -> b -> c
f LogicT m a
xs LogicT m b
ys = ML m c -> LogicT m c
forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML (ML m c -> LogicT m c) -> ML m c -> LogicT m c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> ML m a -> ML m b -> ML m c
forall (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> ML m a -> ML m b -> ML m c
zipWithML a -> b -> c
f (LogicT m a -> ML m a
forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML LogicT m a
xs) (LogicT m b -> ML m b
forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML LogicT m b
ys)
  munzip :: LogicT m (a, b) -> (LogicT m a, LogicT m b)
munzip LogicT m (a, b)
xys = case ML m (a, b) -> (ML m a, ML m b)
forall (m :: * -> *) a b.
MonadZip m =>
ML m (a, b) -> (ML m a, ML m b)
unzipML (LogicT m (a, b) -> ML m (a, b)
forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML LogicT m (a, b)
xys) of
    (ML m a
xs, ML m b
ys) -> (ML m a -> LogicT m a
forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML ML m a
xs, ML m b -> LogicT m b
forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML ML m b
ys)
#endif

-- 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 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 :: e -> LogicT m a
throwError = m a -> LogicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> LogicT m a) -> (e -> m a) -> e -> LogicT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError
  catchError :: LogicT m a -> (e -> LogicT m a) -> LogicT m a
catchError LogicT m a
m e -> LogicT m a
h = (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT ((forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a)
-> (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> let
      handle :: m r -> m r
handle m r
r = m r
r m r -> (e -> m r) -> m r
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e
e -> LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (e -> LogicT m a
h e
e) a -> m r -> m r
sk m r
fk
    in m r -> m r
handle (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ LogicT m a -> (a -> m r -> m r) -> m r -> m r
forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a -> a -> m r -> m r
sk a
a (m r -> m r) -> (m r -> m r) -> m r -> m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m r -> m r
handle) m r
fk