-------------------------------------------------------------------------
-- |
-- 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 Prelude (error, (-))

import Control.Applicative (Alternative(..), Applicative, liftA2, pure, (<*>))
import Control.Monad (join, MonadPlus(..), liftM, Monad(..), fail)
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,9,0)
import Data.Semigroup (Semigroup (..))
#endif

import Data.Bool (otherwise)
import Data.Eq ((==))
import qualified Data.Foldable as F
import Data.Function (($), (.), const)
import Data.Functor (Functor(..), (<$>))
import Data.Int
import qualified Data.List as L
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid (..))
import Data.Ord ((<=))
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.
--
-- @since 0.2
newtype LogicT m a =
    LogicT { forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }

-------------------------------------------------------------------------
-- | Extracts the first result from a 'LogicT' computation,
-- failing if there are no results at all.
--
-- @since 0.2
#if !MIN_VERSION_base(4,13,0)
observeT :: Monad m => LogicT m a -> m a
#else
observeT :: Fail.MonadFail m => LogicT m a -> m a
#endif
observeT :: forall (m :: * -> *) a. MonadFail m => LogicT m a -> m a
observeT LogicT m a
lt = forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
lt (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return) (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.
--
-- @since 0.2
observeAllT :: Applicative m => LogicT m a -> m [a]
observeAllT :: forall (m :: * -> *) a. Applicative m => LogicT m a -> m [a]
observeAllT LogicT m a
m = forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:)) (forall (f :: * -> *) a. Applicative f => a -> f a
pure [])

-------------------------------------------------------------------------
-- | Extracts up to a given number of results from a 'LogicT' computation.
--
-- @since 0.2
observeManyT :: Monad m => Int -> LogicT m a -> m [a]
observeManyT :: forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
observeManyT Int
n LogicT m a
m
    | Int
n forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return []
    | Int
n forall a. Eq a => a -> a -> Bool
== Int
1 = 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]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [a
a]) (forall (m :: * -> *) a. Monad m => a -> m a
return [])
    | Bool
otherwise = forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT (forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit LogicT m a
m) forall {m :: * -> *} {a} {p}.
Monad m =>
Maybe (a, LogicT m a) -> p -> m [a]
sk (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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return []
 sk (Just (a
a, LogicT m a
m')) p
_ = (a
aforall a. a -> [a] -> [a]
:) forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
observeManyT (Int
nforall 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
--
-- @since 0.2
runLogicT :: LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT :: forall (m :: * -> *) a r.
LogicT m a -> (a -> m r -> m r) -> m r -> m r
runLogicT (LogicT forall r. (a -> m r -> m r) -> m r -> m r
r) = 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
-- @
--
-- @since 0.8.0.0
#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 :: forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(Alternative (t m), MonadTrans t, Monad m, Monad (t m)) =>
LogicT m a -> t m a
fromLogicT = forall (m :: * -> *) (n :: * -> *) a.
(Applicative m, Monad n, Alternative n) =>
(forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith 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.
--
-- @since 0.8.0.0
fromLogicTWith :: (Applicative m, Monad n, Alternative n)
  => (forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith :: 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 -> n x
p (LogicT forall r. (a -> m r -> m r) -> m r -> m r
f) = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. m x -> n x
p forall a b. (a -> b) -> a -> b
$
  forall r. (a -> m r -> m r) -> m r -> m r
f (\a
a m (n a)
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (forall x. m x -> n x
p m (n a)
v))) (forall (f :: * -> *) a. Applicative f => a -> f a
pure 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.
--
-- @since 0.8.0.0
hoistLogicT :: (Applicative m, Monad n) => (forall x. m x -> n x) -> LogicT m a -> LogicT n a
hoistLogicT :: forall (m :: * -> *) (n :: * -> *) a.
(Applicative m, Monad n) =>
(forall x. m x -> n x) -> LogicT m a -> LogicT n a
hoistLogicT forall x. m x -> n x
f = forall (m :: * -> *) (n :: * -> *) a.
(Applicative m, Monad n, Alternative n) =>
(forall x. m x -> n x) -> LogicT m a -> n a
fromLogicTWith (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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.
--
-- @since 0.8.0.0
embedLogicT :: Applicative m => (forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
embedLogicT :: forall (m :: * -> *) (n :: * -> *) b.
Applicative m =>
(forall a. m a -> LogicT n a) -> LogicT m b -> LogicT n b
embedLogicT forall a. m a -> LogicT n a
f = 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 [])
--
-- Here is a systematic derivation of the isomorphism. We start with observing
-- that @[a]@ is isomorphic to a fix point of a non-recursive
-- base algebra @Fix@ (@ListF@ @a@):
--
-- > newtype Fix f = Fix (f (Fix f))
-- > data ListF a r = ConsF a r | NilF deriving (Functor)
-- >
-- > cata :: Functor f => (f r -> r) -> Fix f -> r
-- > cata f = go where go (Fix x) = f (fmap go x)
-- >
-- > from :: [a] -> Fix (ListF a)
-- > from = foldr (\a acc -> Fix (ConsF a acc)) (Fix NilF)
-- >
-- > to :: Fix (ListF a) -> [a]
-- > to = cata (\case ConsF a r -> a : r; NilF -> [])
--
-- Further, @Fix@ (@ListF@ @a@) is isomorphic to Boehm-Berarducci encoding @ListC@ @a@:
--
-- > newtype ListC a = ListC (forall r. (ListF a r -> r) -> r)
-- >
-- > from :: Fix (ListF a) -> ListC a
-- > from xs = ListC (\f -> cata f xs)
-- >
-- > to :: ListC a -> Fix (ListF a)
-- > to (ListC f) = f Fix
--
-- Finally, @ListF@ @a@ @r@ → @r@ is isomorphic to a pair (@a@ → @r@ → @r@, @r@),
-- so @ListC@ is isomorphic to the 'Logic' type modulo 'Identity' wrappers:
--
-- > newtype Logic a = Logic (forall r. (a -> r -> r) -> r -> r)
--
-- And wrapping every occurence of @r@ into @m@ gives us 'LogicT':
--
-- > newtype LogicT m a = Logic (forall r. (a -> m r -> m r) -> m r -> m r)
--
-- @since 0.5.0
type Logic = LogicT Identity

-------------------------------------------------------------------------
-- | A smart constructor for 'Logic' computations.
--
-- @since 0.5.0
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic :: forall a. (forall r. (a -> r -> r) -> r -> r) -> Logic a
logic forall r. (a -> r -> r) -> r -> r
f = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \a -> Identity r -> Identity r
k -> forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         forall r. (a -> r -> r) -> r -> r
f (\a
a -> forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity r -> Identity r
k a
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         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'.
--
-- @since 0.2
observe :: Logic a -> a
observe :: forall a. Logic a -> a
observe Logic a
lt = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT Logic a
lt (forall a b. a -> b -> a
const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure) (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.
--
-- @since 0.2
observeAll :: Logic a -> [a]
observeAll :: forall a. Logic a -> [a]
observeAll = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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'.
--
-- @since 0.2
observeMany :: Int -> Logic a -> [a]
observeMany :: forall a. Int -> Logic a -> [a]
observeMany Int
i = forall a. Int -> [a] -> [a]
L.take Int
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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.
--
-- @since 0.2
runLogic :: Logic a -> (a -> r -> r) -> r -> r
runLogic :: forall a r. Logic a -> (a -> r -> r) -> r -> r
runLogic Logic a
l a -> r -> r
s r
f = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> r -> r
s
 fi :: Identity r
fi = forall a. a -> Identity a
Identity r
f

instance Functor (LogicT f) where
    fmap :: forall a b. (a -> b) -> LogicT f a -> LogicT f b
fmap a -> b
f LogicT f a
lt = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \b -> f r -> f r
sk f r
fk -> 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f r
fk

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

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

instance Monad (LogicT m) where
    return :: forall a. a -> LogicT m a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
    LogicT m a
m >>= :: forall a b. LogicT m a -> (a -> LogicT m b) -> LogicT m b
>>= a -> LogicT m b
f = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \b -> m r -> m r
sk m r
fk -> 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' -> 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

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

instance MonadPlus (LogicT m) where
  mzero :: forall a. LogicT m a
mzero = forall (f :: * -> *) a. Alternative f => f a
empty
  mplus :: forall a. LogicT m a -> LogicT m a -> LogicT m a
mplus = forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)

#if MIN_VERSION_base(4,9,0)
-- | @since 0.7.0.3
instance Semigroup (LogicT m a) where
  <> :: 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 = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
F.foldr1 forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus
#endif

-- | @since 0.7.0.3
instance Monoid (LogicT m a) where
  mempty :: LogicT m a
mempty = 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 = forall a. Semigroup a => a -> a -> a
(<>)
#else
  mappend = (<|>)
#endif
  mconcat :: [LogicT m a] -> LogicT m a
mconcat = forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
F.asum

instance MonadTrans LogicT where
    lift :: forall (m :: * -> *) a. Monad m => m a -> LogicT m a
lift m a
m = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> m a
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> a -> m r -> m r
sk a
a m r
fk

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

instance (Monad m) => MonadLogic (LogicT m) where
    -- 'msplit' is quite costly even if the base 'Monad' is 'Identity'.
    -- Try to avoid it.
    msplit :: forall a. LogicT m a -> LogicT m (Maybe (a, LogicT m a))
msplit LogicT m a
m = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m 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 (forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (a
a, forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Maybe (b, t m b))
fk forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Alternative m => Maybe (a, m a) -> m a
reflect)
    once :: forall a. LogicT m a -> LogicT m a
once LogicT m a
m = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (\a
a m r
_ -> a -> m r -> m r
sk a
a m r
fk) m r
fk
    lnot :: forall a. LogicT m a -> LogicT m ()
lnot LogicT m a
m = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \() -> m r -> m r
sk m r
fk -> 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)

-- | @since 0.5.0
instance {-# OVERLAPPABLE #-} (Applicative m, F.Foldable m) => F.Foldable (LogicT m) where
    foldMap :: forall m a. Monoid m => (a -> m) -> LogicT m a -> m
foldMap a -> m
f LogicT m a
m = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
F.fold forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r
unLogicT LogicT m a
m (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => a -> a -> a
mappend forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m
f) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty)

-- | @since 0.5.0
instance {-# OVERLAPPING #-} F.Foldable (LogicT Identity) where
    foldr :: forall a b. (a -> b -> b) -> b -> LogicT Identity a -> b
foldr a -> b -> b
f b
z LogicT Identity a
m = forall a r. Logic a -> (a -> r -> r) -> r -> r
runLogic LogicT Identity a
m a -> b -> b
f b
z

#else

-- | @since 0.5.0
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 (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
<$ :: forall a b. a -> ML m b -> ML m a
$c<$ :: forall (m :: * -> *) a b. Functor m => a -> ML m b -> ML m a
fmap :: forall a b. (a -> b) -> ML m a -> ML m b
$cfmap :: forall (m :: * -> *) a b. Functor m => (a -> b) -> ML m a -> ML m b
Functor, forall a. ML m a -> Bool
forall m a. Monoid m => (a -> m) -> ML m a -> m
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 :: forall a. Num a => ML m a -> a
$cproduct :: forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
sum :: forall a. Num a => ML m a -> a
$csum :: forall (m :: * -> *) a. (Foldable m, Num a) => ML m a -> a
minimum :: forall a. Ord a => ML m a -> a
$cminimum :: forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
maximum :: forall a. Ord a => ML m a -> a
$cmaximum :: forall (m :: * -> *) a. (Foldable m, Ord a) => ML m a -> a
elem :: forall a. Eq a => a -> ML m a -> Bool
$celem :: forall (m :: * -> *) a. (Foldable m, Eq a) => a -> ML m a -> Bool
length :: forall a. ML m a -> Int
$clength :: forall (m :: * -> *) a. Foldable m => ML m a -> Int
null :: forall a. ML m a -> Bool
$cnull :: forall (m :: * -> *) a. Foldable m => ML m a -> Bool
toList :: forall a. ML m a -> [a]
$ctoList :: forall (m :: * -> *) a. Foldable m => ML m a -> [a]
foldl1 :: forall a. (a -> a -> a) -> ML m a -> a
$cfoldl1 :: forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
foldr1 :: forall a. (a -> a -> a) -> ML m a -> a
$cfoldr1 :: forall (m :: * -> *) a. Foldable m => (a -> a -> a) -> ML m a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> ML m a -> b
$cfoldl' :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> ML m a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ML m a -> b
$cfoldl :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> ML m a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ML m a -> b
$cfoldr' :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> ML m a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ML m a -> b
$cfoldr :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> ML m a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> ML m a -> m
$cfoldMap' :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> ML m a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ML m a -> m
$cfoldMap :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> ML m a -> m
fold :: forall m. Monoid m => ML m m -> m
$cfold :: forall (m :: * -> *) m. (Foldable m, Monoid m) => ML m m -> m
F.Foldable, 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 (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ML m a -> f (ML m b)
sequence :: forall (m :: * -> *) a. Monad m => 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 :: forall (m :: * -> *) a b.
Monad m =>
(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 :: forall (f :: * -> *) a. Applicative f => 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 :: forall (f :: * -> *) a b.
Applicative f =>
(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)
T.Traversable)

data MLView m a = EmptyML | ConsML a (ML m a)
  deriving (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
<$ :: forall a b. a -> MLView m b -> MLView m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> MLView m b -> MLView m a
fmap :: forall a b. (a -> b) -> MLView m a -> MLView m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> MLView m a -> MLView m b
Functor, forall a. MLView m a -> Bool
forall m a. Monoid m => (a -> m) -> MLView m a -> m
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 :: forall a. Num a => MLView m a -> a
$cproduct :: forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
sum :: forall a. Num a => MLView m a -> a
$csum :: forall (m :: * -> *) a. (Foldable m, Num a) => MLView m a -> a
minimum :: forall a. Ord a => MLView m a -> a
$cminimum :: forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
maximum :: forall a. Ord a => MLView m a -> a
$cmaximum :: forall (m :: * -> *) a. (Foldable m, Ord a) => MLView m a -> a
elem :: forall a. Eq a => a -> MLView m a -> Bool
$celem :: forall (m :: * -> *) a.
(Foldable m, Eq a) =>
a -> MLView m a -> Bool
length :: forall a. MLView m a -> Int
$clength :: forall (m :: * -> *) a. Foldable m => MLView m a -> Int
null :: forall a. MLView m a -> Bool
$cnull :: forall (m :: * -> *) a. Foldable m => MLView m a -> Bool
toList :: forall a. MLView m a -> [a]
$ctoList :: forall (m :: * -> *) a. Foldable m => MLView m a -> [a]
foldl1 :: forall a. (a -> a -> a) -> MLView m a -> a
$cfoldl1 :: forall (m :: * -> *) a.
Foldable m =>
(a -> a -> a) -> MLView m a -> a
foldr1 :: forall a. (a -> a -> a) -> MLView m a -> a
$cfoldr1 :: forall (m :: * -> *) a.
Foldable m =>
(a -> a -> a) -> MLView m a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> MLView m a -> b
$cfoldl' :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> MLView m a -> b
foldl :: forall b a. (b -> a -> b) -> b -> MLView m a -> b
$cfoldl :: forall (m :: * -> *) b a.
Foldable m =>
(b -> a -> b) -> b -> MLView m a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> MLView m a -> b
$cfoldr' :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> MLView m a -> b
foldr :: forall a b. (a -> b -> b) -> b -> MLView m a -> b
$cfoldr :: forall (m :: * -> *) a b.
Foldable m =>
(a -> b -> b) -> b -> MLView m a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> MLView m a -> m
$cfoldMap' :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> MLView m a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> MLView m a -> m
$cfoldMap :: forall (m :: * -> *) m a.
(Foldable m, Monoid m) =>
(a -> m) -> MLView m a -> m
fold :: forall m. Monoid m => 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 :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MLView m a -> f (MLView m b)
traverse a -> f b
_ MLView m a
EmptyML = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *) a. MLView m a
EmptyML
  traverse a -> f b
f (ConsML a
x (ML m (MLView m a)
m))
    = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (\b
y m (MLView m b)
ym -> forall (m :: * -> *) a. a -> ML m a -> MLView m a
ConsML b
y (forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m b)
ym)) (a -> f b
f a
x) (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse (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 :: forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML (LogicT forall r. (a -> m r -> m r) -> m r -> m r
q) = forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML forall a b. (a -> b) -> a -> b
$ forall r. (a -> m r -> m r) -> m r -> m r
q (\a
a m (MLView m a)
m -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. a -> ML m a -> MLView m a
ConsML a
a (forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m a)
m)) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (m :: * -> *) a. MLView m a
EmptyML)

fromML :: Monad m => ML m a -> LogicT m a
fromML :: forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML (ML m (MLView m a)
m) = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (MLView m a)
m 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 -> forall (f :: * -> *) a. Alternative f => f a
empty
  ConsML a
a ML m a
xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML ML m a
xs

#if MIN_VERSION_base(4,8,0)
-- | @since 0.5.0
instance {-# OVERLAPPING #-} T.Traversable (LogicT Identity) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LogicT Identity a -> f (LogicT Identity b)
traverse a -> f b
g LogicT Identity a
l = forall a r. Logic a -> (a -> r -> r) -> r -> r
runLogic LogicT Identity a
l (\a
a f (LogicT Identity b)
ft -> forall {f :: * -> *} {a}. Alternative f => a -> f a -> f a
cons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
g a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (LogicT Identity b)
ft) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Alternative f => f a
empty)
    where
      cons :: a -> f a -> f a
cons a
a f a
l' = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> f a
l'

-- | @since 0.8.0.0
instance {-# OVERLAPPABLE #-} (Monad m, T.Traversable m) => T.Traversable (LogicT m) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> LogicT m a -> f (LogicT m b)
traverse a -> f b
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
T.traverse a -> f b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML
#else
-- | @since 0.8.0.0
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 :: forall (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> ML m a -> ML m b -> ML m c
zipWithML a -> b -> c
f = 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) =
        forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML forall a b. (a -> b) -> a -> b
$ 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 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
_ = forall (m :: * -> *) a. MLView m a
EmptyML

unzipML :: MonadZip m => ML m (a, b) -> (ML m a, ML m b)
unzipML :: forall (m :: * -> *) a b.
MonadZip m =>
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) <- forall (m :: * -> *) a b. MonadZip m => m (a, b) -> (m a, m b)
munzip (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {m :: * -> *} {a} {a}.
MonadZip m =>
MLView m (a, a) -> (MLView m a, MLView m a)
go m (MLView m (a, b))
m)
    = (forall (m :: * -> *) a. m (MLView m a) -> ML m a
ML m (MLView m a)
l, 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 = (forall (m :: * -> *) a. MLView m a
EmptyML, forall (m :: * -> *) a. MLView m a
EmptyML)
      go ((a
a, a
b) `ConsML` ML m (a, a)
listab)
        = (a
a forall (m :: * -> *) a. a -> ML m a -> MLView m a
`ConsML` ML m a
la, a
b 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 = 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

-- | @since 0.8.0.0
instance MonadZip m => MonadZip (LogicT m) where
  mzipWith :: forall a b c.
(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 = forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b c.
MonadZip m =>
(a -> b -> c) -> ML m a -> ML m b -> ML m c
zipWithML a -> b -> c
f (forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML LogicT m a
xs) (forall (m :: * -> *) a. Applicative m => LogicT m a -> ML m a
toML LogicT m b
ys)
  munzip :: forall a b. LogicT m (a, b) -> (LogicT m a, LogicT m b)
munzip LogicT m (a, b)
xys = case forall (m :: * -> *) a b.
MonadZip m =>
ML m (a, b) -> (ML m a, ML m b)
unzipML (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) -> (forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML ML m a
xs, forall (m :: * -> *) a. Monad m => ML m a -> LogicT m a
fromML ML m b
ys)
#endif

instance MonadReader r m => MonadReader r (LogicT m) where
    ask :: LogicT m r
ask = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: * -> *). MonadReader r m => m r
ask
    local :: forall a. (r -> r) -> LogicT m a -> LogicT m a
local r -> r
f (LogicT forall r. (a -> m r -> m r) -> m r -> m r
m) = forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
LogicT forall a b. (a -> b) -> a -> b
$ \a -> m r -> m r
sk m r
fk -> do
        r
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
        forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f forall a b. (a -> b) -> a -> b
$ forall r. (a -> m r -> m r) -> m r -> m r
m ((forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a b. a -> b -> a
const r
env) forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m r -> m r
sk) (forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a b. a -> b -> a
const r
env) m r
fk)

instance MonadState s m => MonadState s (LogicT m) where
    get :: LogicT m s
get = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall s (m :: * -> *). MonadState s m => m s
get
    put :: s -> LogicT m ()
put = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *). MonadState s m => s -> m ()
put

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