-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A backtracking logic-programming monad.
--   
--   Adapted from the paper <a>Backtracking, Interleaving, and Terminating
--   Monad Transformers</a> by Oleg Kiselyov, Chung-chieh Shan, Daniel P.
--   Friedman, Amr Sabry.
@package logict
@version 0.7.1.0


-- | Adapted from the paper <a>Backtracking, Interleaving, and Terminating
--   Monad Transformers</a> by Oleg Kiselyov, Chung-chieh Shan, Daniel P.
--   Friedman, Amr Sabry. Note that the paper uses <a>MonadPlus</a>
--   vocabulary (<a>mzero</a> and <a>mplus</a>), while examples below
--   prefer <a>empty</a> and <a>&lt;|&gt;</a> from <a>Alternative</a>.
module Control.Monad.Logic.Class

-- | A backtracking, logic programming monad.
class (Monad m, Alternative m) => MonadLogic m

-- | Attempts to <b>split</b> the computation, giving access to the first
--   result. Satisfies the following laws:
--   
--   <pre>
--   msplit empty          == pure Nothing
--   msplit (pure a &lt;|&gt; m) == pure (Just (a, m))
--   </pre>
msplit :: MonadLogic m => m a -> m (Maybe (a, m a))

-- | <b>Fair disjunction.</b> It is possible for a logical computation to
--   have an infinite number of potential results, for instance:
--   
--   <pre>
--   odds = pure 1 &lt;|&gt; fmap (+ 2) odds
--   </pre>
--   
--   Such computations can cause problems in some circumstances. Consider:
--   
--   <pre>
--   two = do x &lt;- odds &lt;|&gt; pure 2
--            if even x then pure x else empty
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observe two
--   ...never completes...
--   </pre>
--   
--   Such a computation may never consider <a>pure</a> <tt>2</tt>, and
--   therefore even <a>observe</a> <tt>two</tt> will never return any
--   results. By contrast, using <a>interleave</a> in place of
--   <a>&lt;|&gt;</a> ensures fair consideration of both branches of a
--   disjunction.
--   
--   <pre>
--   fairTwo = do x &lt;- odds `interleave` pure 2
--                if even x then pure x else empty
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observe fairTwo
--   2
--   </pre>
--   
--   Note that even with <a>interleave</a> this computation will never
--   terminate after returning 2: only the first value can be safely
--   observed, after which each odd value becomes <a>empty</a> (equivalent
--   to <a>Prolog's fail</a>) which does not stop the evaluation but
--   indicates there is no value to return yet.
--   
--   Unlike <a>&lt;|&gt;</a>, <a>interleave</a> is not associative:
--   
--   <pre>
--   &gt;&gt;&gt; let x = [1,2,3]; y = [4,5,6]; z = [7,8,9] :: [Int]
--   
--   &gt;&gt;&gt; x `interleave` y
--   [1,4,2,5,3,6]
--   
--   &gt;&gt;&gt; (x `interleave` y) `interleave` z
--   [1,7,4,8,2,9,5,3,6]
--   
--   &gt;&gt;&gt; y `interleave` z
--   [4,7,5,8,6,9]
--   
--   &gt;&gt;&gt; x `interleave` (y `interleave` z)
--   [1,4,2,7,3,5,8,6,9]
--   </pre>
interleave :: MonadLogic m => m a -> m a -> m a

-- | <b>Fair conjunction.</b> Similarly to the previous function, consider
--   the distributivity law, naturally expected from <a>MonadPlus</a>:
--   
--   <pre>
--   (a &lt;|&gt; b) &gt;&gt;= k = (a &gt;&gt;= k) &lt;|&gt; (b &gt;&gt;= k)
--   </pre>
--   
--   If <tt>a</tt> <a>&gt;&gt;=</a> <tt>k</tt> can backtrack arbitrarily
--   many times, <tt>b</tt> <a>&gt;&gt;=</a> <tt>k</tt> may never be
--   considered. In logic statements, "backtracking" is the process of
--   discarding the current possible solution value and returning to a
--   previous decision point where a new value can be obtained and tried.
--   For example:
--   
--   <pre>
--   &gt;&gt;&gt; do { x &lt;- pure 0 &lt;|&gt; pure 1 &lt;|&gt; pure 2; if even x then pure x else empty } :: [Int]
--   [0,2]
--   </pre>
--   
--   Here, the <tt>x</tt> value can be produced three times, where
--   <a>&lt;|&gt;</a> represents the decision points of that production.
--   The subsequent <tt>if</tt> statement specifies <a>empty</a> (fail) if
--   <tt>x</tt> is odd, causing it to be discarded and a return to an
--   <a>&lt;|&gt;</a> decision point to get the next <tt>x</tt>.
--   
--   The statement "<tt>a</tt> <a>&gt;&gt;=</a> <tt>k</tt> can backtrack
--   arbitrarily many times" means that the computation is resulting in
--   <a>empty</a> and that <tt>a</tt> has an infinite number of
--   <a>&lt;|&gt;</a> applications to return to. This is called a
--   conjunctive computation because the logic for <tt>a</tt> <i>and</i>
--   <tt>k</tt> must both succeed (i.e. <a>pure</a> a value instead of
--   <a>empty</a>).
--   
--   Similar to the way <a>interleave</a> allows both branches of a
--   disjunctive computation, the <a>&gt;&gt;-</a> operator takes care to
--   consider both branches of a conjunctive computation.
--   
--   Consider the operation:
--   
--   <pre>
--   odds = pure 1 &lt;|&gt; fmap (2 +) odds
--   
--   oddsPlus n = odds &gt;&gt;= \a -&gt; pure (a + n)
--   
--   g = do x &lt;- (pure 0 &lt;|&gt; pure 1) &gt;&gt;= oddsPlus
--          if even x then pure x else empty
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observeMany 3 g
--   ...never completes...
--   </pre>
--   
--   This will never produce any value because all values produced by the
--   <tt>do</tt> program come from the <a>pure</a> <tt>1</tt> driven
--   operation (adding one to the sequence of odd values, resulting in the
--   even values that are allowed by the test in the second line), but the
--   <a>pure</a> <tt>0</tt> input to <tt>oddsPlus</tt> generates an
--   infinite number of <a>empty</a> failures so the even values generated
--   by the <a>pure</a> <tt>1</tt> alternative are never seen. Using
--   <a>interleave</a> here instead of <a>&lt;|&gt;</a> does not help due
--   to the aforementioned distributivity law.
--   
--   Also note that the <tt>do</tt> notation desugars to <a>&gt;&gt;=</a>
--   bind operations, so the following would also fail:
--   
--   <pre>
--   do a &lt;- pure 0 &lt;|&gt; pure 1
--      x &lt;- oddsPlus a
--      if even x then pure x else empty
--   </pre>
--   
--   The solution is to use the <a>&gt;&gt;-</a> in place of the normal
--   monadic bind operation <a>&gt;&gt;=</a> when fairness between
--   alternative productions is needed in a conjunction of statements
--   (rules):
--   
--   <pre>
--   h = do x &lt;- (pure 0 &lt;|&gt; pure 1) &gt;&gt;- oddsPlus
--          if even x then pure x else empty
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observeMany 3 h
--   [2,4,6]
--   </pre>
--   
--   However, a bit of care is needed when using <a>&gt;&gt;-</a> because,
--   unlike <a>&gt;&gt;=</a>, it is not associative. For example:
--   
--   <pre>
--   &gt;&gt;&gt; let m = [2,7] :: [Int]
--   
--   &gt;&gt;&gt; let k x = [x, x + 1]
--   
--   &gt;&gt;&gt; let h x = [x, x * 2]
--   
--   &gt;&gt;&gt; m &gt;&gt;= (\x -&gt; k x &gt;&gt;= h)
--   [2,4,3,6,7,14,8,16]
--   
--   &gt;&gt;&gt; (m &gt;&gt;= k) &gt;&gt;= h -- same as above
--   [2,4,3,6,7,14,8,16]
--   
--   &gt;&gt;&gt; m &gt;&gt;- (\x -&gt; k x &gt;&gt;- h)
--   [2,7,3,8,4,14,6,16]
--   
--   &gt;&gt;&gt; (m &gt;&gt;- k) &gt;&gt;- h -- central elements are different
--   [2,7,4,3,14,8,6,16]
--   </pre>
--   
--   This means that the following will be productive:
--   
--   <pre>
--   (pure 0 &lt;|&gt; pure 1) &gt;&gt;-
--     oddsPlus &gt;&gt;-
--       \x -&gt; if even x then pure x else empty
--   </pre>
--   
--   Which is equivalent to
--   
--   <pre>
--   ((pure 0 &lt;|&gt; pure 1) &gt;&gt;- oddsPlus) &gt;&gt;-
--     (\x -&gt; if even x then pure x else empty)
--   </pre>
--   
--   But the following will <i>not</i> be productive:
--   
--   <pre>
--   (pure 0 &lt;|&gt; pure 1) &gt;&gt;-
--     (\a -&gt; (oddsPlus a &gt;&gt;- \x -&gt; if even x then pure x else empty))
--   </pre>
--   
--   Since do notation desugaring results in the latter, the
--   <tt>RebindableSyntax</tt> language pragma cannot easily be used
--   either. Instead, it is recommended to carefully use explicit
--   <a>&gt;&gt;-</a> only when needed.
(>>-) :: MonadLogic m => m a -> (a -> m b) -> m b

-- | <b>Pruning.</b> Selects one result out of many. Useful for when
--   multiple results of a computation will be equivalent, or should be
--   treated as such.
--   
--   As an example, here's a way to determine if a number is
--   <a>composite</a> (has non-trivial integer divisors, i.e. not a prime
--   number):
--   
--   <pre>
--   choose = foldr ((&lt;|&gt;) . pure) empty
--   
--   divisors n = do a &lt;- choose [2..n-1]
--                   b &lt;- choose [2..n-1]
--                   guard (a * b == n)
--                   pure (a, b)
--   
--   composite_ v = do _ &lt;- divisors v
--                     pure "Composite"
--   </pre>
--   
--   While this works as intended, it actually does too much work:
--   
--   <pre>
--   &gt;&gt;&gt; observeAll (composite_ 20)
--   ["Composite", "Composite", "Composite", "Composite"]
--   </pre>
--   
--   Because there are multiple divisors of 20, and they can also occur in
--   either order:
--   
--   <pre>
--   &gt;&gt;&gt; observeAll (divisors 20)
--   [(2,10), (4,5), (5,4), (10,2)]
--   </pre>
--   
--   Clearly one could just use <a>observe</a> here to get the first
--   non-prime result, but if the call to <tt>composite</tt> is in the
--   middle of other logic code then use <a>once</a> instead.
--   
--   <pre>
--   composite v = do _ &lt;- once (divisors v)
--                    pure "Composite"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observeAll (composite 20)
--   ["Composite"]
--   </pre>
once :: MonadLogic m => m a -> m a

-- | <b>Inverts</b> a logic computation. If <tt>m</tt> succeeds with at
--   least one value, <a>lnot</a> <tt>m</tt> fails. If <tt>m</tt> fails,
--   then <a>lnot</a> <tt>m</tt> succeeds with the value <tt>()</tt>.
--   
--   For example, evaluating if a number is prime can be based on the
--   failure to find divisors of a number:
--   
--   <pre>
--   choose = foldr ((&lt;|&gt;) . pure) empty
--   
--   divisors n = do d &lt;- choose [2..n-1]
--                   guard (n `rem` d == 0)
--                   pure d
--   
--   prime v = do _ &lt;- lnot (divisors v)
--                pure True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observeAll (prime 20)
--   []
--   
--   &gt;&gt;&gt; observeAll (prime 19)
--   [True]
--   </pre>
--   
--   Here if <tt>divisors</tt> never succeeds, then the <a>lnot</a> will
--   succeed and the number will be declared as prime.
lnot :: MonadLogic m => m a -> m ()

-- | Logical <b>conditional.</b> The equivalent of <a>Prolog's
--   soft-cut</a>. If its first argument succeeds at all, then the results
--   will be fed into the success branch. Otherwise, the failure branch is
--   taken. The failure branch is never considered if the first argument
--   has any successes. The <a>ifte</a> function satisfies the following
--   laws:
--   
--   <pre>
--   ifte (pure a) th el       == th a
--   ifte empty th el          == el
--   ifte (pure a &lt;|&gt; m) th el == th a &lt;|&gt; (m &gt;&gt;= th)
--   </pre>
--   
--   For example, the previous <tt>prime</tt> function returned nothing if
--   the number was not prime, but if it should return <a>False</a>
--   instead, the following can be used:
--   
--   <pre>
--   choose = foldr ((&lt;|&gt;) . pure) empty
--   
--   divisors n = do d &lt;- choose [2..n-1]
--                   guard (n `rem` d == 0)
--                   pure d
--   
--   prime v = once (ifte (divisors v)
--                     (const (pure True))
--                     (pure False))
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observeAll (prime 20)
--   [False]
--   
--   &gt;&gt;&gt; observeAll (prime 19)
--   [True]
--   </pre>
--   
--   Notice that this cannot be done with a simple <tt>if-then-else</tt>
--   because <tt>divisors</tt> either generates values or it does not, so
--   there's no "false" condition to check with a simple <tt>if</tt>
--   statement.
ifte :: MonadLogic m => m a -> (a -> m b) -> m b -> m b
infixl 1 >>-

-- | The inverse of <a>msplit</a>. Satisfies the following law:
--   
--   <pre>
--   msplit m &gt;&gt;= reflect == m
--   </pre>
reflect :: Alternative m => Maybe (a, m a) -> m a
instance Control.Monad.Logic.Class.MonadLogic []
instance Control.Monad.Logic.Class.MonadLogic m => Control.Monad.Logic.Class.MonadLogic (Control.Monad.Trans.Reader.ReaderT e m)
instance (Control.Monad.Logic.Class.MonadLogic m, GHC.Base.MonadPlus m) => Control.Monad.Logic.Class.MonadLogic (Control.Monad.Trans.State.Strict.StateT s m)
instance (Control.Monad.Logic.Class.MonadLogic m, GHC.Base.MonadPlus m) => Control.Monad.Logic.Class.MonadLogic (Control.Monad.Trans.State.Lazy.StateT s m)


-- | Adapted from the paper <a>Backtracking, Interleaving, and Terminating
--   Monad Transformers</a> by Oleg Kiselyov, Chung-chieh Shan, Daniel P.
--   Friedman, Amr Sabry. Note that the paper uses <a>MonadPlus</a>
--   vocabulary (<a>mzero</a> and <a>mplus</a>), while examples below
--   prefer <a>empty</a> and <a>&lt;|&gt;</a> from <a>Alternative</a>.
module Control.Monad.Logic

-- | The basic <a>Logic</a> monad, for performing backtracking computations
--   returning values (e.g. <a>Logic</a> <tt>a</tt> will return values of
--   type <tt>a</tt>).
type Logic = LogicT Identity

-- | A smart constructor for <a>Logic</a> computations.
logic :: (forall r. (a -> r -> r) -> r -> r) -> Logic a

-- | Runs a <a>Logic</a> computation with the specified initial success and
--   failure continuations.
--   
--   <pre>
--   &gt;&gt;&gt; runLogic empty (+) 0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; runLogic (pure 5 &lt;|&gt; pure 3 &lt;|&gt; empty) (+) 0
--   8
--   </pre>
runLogic :: Logic a -> (a -> r -> r) -> r -> r

-- | Extracts the first result from a <a>Logic</a> computation, failing if
--   there are no results.
--   
--   <pre>
--   &gt;&gt;&gt; observe (pure 5 &lt;|&gt; pure 3 &lt;|&gt; empty)
--   5
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; observe empty
--   *** Exception: No answer.
--   </pre>
observe :: Logic a -> a

-- | Extracts up to a given number of results from a <a>Logic</a>
--   computation.
--   
--   <pre>
--   &gt;&gt;&gt; let nats = pure 0 &lt;|&gt; fmap (+ 1) nats
--   
--   &gt;&gt;&gt; observeMany 5 nats
--   [0,1,2,3,4]
--   </pre>
observeMany :: Int -> Logic a -> [a]

-- | Extracts all results from a <a>Logic</a> computation.
--   
--   <pre>
--   &gt;&gt;&gt; observe (pure 5 &lt;|&gt; empty &lt;|&gt; empty &lt;|&gt; pure 3 &lt;|&gt; empty)
--   [5,3]
--   </pre>
observeAll :: Logic a -> [a]

-- | A monad transformer for performing backtracking computations layered
--   over another monad <tt>m</tt>.
newtype LogicT m a
LogicT :: (forall r. (a -> m r -> m r) -> m r -> m r) -> LogicT m a
[unLogicT] :: LogicT m a -> forall r. (a -> m r -> m r) -> m r -> m r

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

-- | Extracts the first result from a <a>LogicT</a> computation, failing if
--   there are no results at all.
observeT :: MonadFail m => LogicT m a -> m a

-- | Extracts up to a given number of results from a <a>LogicT</a>
--   computation.
observeManyT :: Monad m => Int -> LogicT m a -> m [a]

-- | Extracts all results from a <a>LogicT</a> computation, unless blocked
--   by the underlying monad.
--   
--   For example, given
--   
--   <pre>
--   &gt;&gt;&gt; let nats = pure 0 &lt;|&gt; fmap (+ 1) nats
--   </pre>
--   
--   some monads (like <a>Identity</a>, <a>Reader</a>, <a>Writer</a>, and
--   <a>State</a>) will be productive:
--   
--   <pre>
--   &gt;&gt;&gt; take 5 $ runIdentity (observeAllT nats)
--   [0,1,2,3,4]
--   </pre>
--   
--   but others (like <a>ExceptT</a>, and <a>ContT</a>) will not:
--   
--   <pre>
--   &gt;&gt;&gt; take 20 &lt;$&gt; runExcept (observeAllT nats)
--   </pre>
--   
--   In general, if the underlying monad manages control flow then
--   <a>observeAllT</a> may be unproductive under infinite branching, and
--   <a>observeManyT</a> should be used instead.
observeAllT :: Applicative m => LogicT m a -> m [a]
instance GHC.Base.Functor (Control.Monad.Logic.LogicT f)
instance GHC.Base.Applicative (Control.Monad.Logic.LogicT f)
instance GHC.Base.Alternative (Control.Monad.Logic.LogicT f)
instance GHC.Base.Monad (Control.Monad.Logic.LogicT m)
instance Control.Monad.Fail.MonadFail (Control.Monad.Logic.LogicT m)
instance GHC.Base.MonadPlus (Control.Monad.Logic.LogicT m)
instance GHC.Base.Semigroup (Control.Monad.Logic.LogicT m a)
instance GHC.Base.Monoid (Control.Monad.Logic.LogicT m a)
instance Control.Monad.Trans.Class.MonadTrans Control.Monad.Logic.LogicT
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Control.Monad.Logic.LogicT m)
instance GHC.Base.Monad m => Control.Monad.Logic.Class.MonadLogic (Control.Monad.Logic.LogicT m)
instance (GHC.Base.Applicative m, Data.Foldable.Foldable m) => Data.Foldable.Foldable (Control.Monad.Logic.LogicT m)
instance Data.Foldable.Foldable (Control.Monad.Logic.LogicT Data.Functor.Identity.Identity)
instance Data.Traversable.Traversable (Control.Monad.Logic.LogicT Data.Functor.Identity.Identity)
instance Control.Monad.Reader.Class.MonadReader r m => Control.Monad.Reader.Class.MonadReader r (Control.Monad.Logic.LogicT m)
instance Control.Monad.State.Class.MonadState s m => Control.Monad.State.Class.MonadState s (Control.Monad.Logic.LogicT m)
instance Control.Monad.Error.Class.MonadError e m => Control.Monad.Error.Class.MonadError e (Control.Monad.Logic.LogicT m)
