module Control.Effect.NonDet
  ( -- * Effects
    NonDet(..)
  , Cull(..)
  , Cut(..)
  , Split(..)
  , Logic

    -- * Actions
  , choose
  , lose
  , fromList

  , cull

  , cutfail
  , cut
  , call

  , split

    -- * Interpretations
  , runNonDet
  , runNonDet1

  , runCullCut

  , runLogic

    -- * Threading constraints
  , NonDetThreads

    -- * Carriers
  , NonDetC
  , CullCutC
  , LogicC
  ) where

import Control.Monad

import Control.Effect
import Control.Effect.Internal.NonDet
import Control.Effect.Internal.Utils

import Control.Effect.Type.Split

-- | Introduce new branches stemming from the current one using a list of values.
fromList :: Eff NonDet m => [a] -> m a
fromList :: [a] -> m a
fromList = NonDet m a -> m a
forall (e :: Effect) (m :: * -> *) a.
(Member e (Derivs m), Carrier m) =>
e m a -> m a
send (NonDet m a -> m a) -> ([a] -> NonDet m a) -> [a] -> m a
forall b a c. Coercible b a => (b -> c) -> (a -> b) -> a -> c
.# [a] -> NonDet m a
forall a (m :: * -> *). [a] -> NonDet m a
FromList

-- | Introduce two new branches stemming from the current one.
choose :: Eff NonDet m => m a -> m a -> m a
choose :: m a -> m a -> m a
choose m a
ma m a
mb = m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m a) -> m a) -> m (m a) -> m a
forall a b. (a -> b) -> a -> b
$ [m a] -> m (m a)
forall (m :: * -> *) a. Eff NonDet m => [a] -> m a
fromList [m a
ma, m a
mb]
{-# INLINE choose #-}

-- | Fail the current branch and proceed to the next branch,
-- backtracking to the nearest use of 'choose' or 'fromList' that
-- still has unprocessed branches.
lose :: Eff NonDet m => m a
lose :: m a
lose = [a] -> m a
forall (m :: * -> *) a. Eff NonDet m => [a] -> m a
fromList []
{-# INLINE lose #-}

-- | Cull nondeterminism in the argument, limiting the number of branches
-- it may introduce to be at most 1.
--
-- @'cull' (return True \`'choose'\` return False) == return True@
--
-- @'cull' ('lose' \`'choose'\` return False) == return False@
cull :: Eff Cull m => m a -> m a
cull :: m a -> m a
cull = Cull m a -> m a
forall (e :: Effect) (m :: * -> *) a.
(Member e (Derivs m), Carrier m) =>
e m a -> m a
send (Cull m a -> m a) -> (m a -> Cull m a) -> m a -> m a
forall b a c. Coercible b a => (b -> c) -> (a -> b) -> a -> c
.# m a -> Cull m a
forall (m :: * -> *) a. m a -> Cull m a
Cull
{-# INLINE cull #-}

-- | Fail the current branch, and prevent backtracking up until the nearest
-- enclosing use of 'call' (if any).
--
-- @'cutfail' \`'choose'\` m == 'cutfail'@
cutfail :: Eff Cut m => m a
cutfail :: m a
cutfail = Cut m a -> m a
forall (e :: Effect) (m :: * -> *) a.
(Member e (Derivs m), Carrier m) =>
e m a -> m a
send Cut m a
forall (m :: * -> *) a. Cut m a
Cutfail
{-# INLINE cutfail #-}

-- | Commit to the current branch: prevent all backtracking that would move
-- execution to before 'cut' was invoked, up until the nearest enclosing use
-- of 'call' (if any).
--
-- @'call' ('fromList' [1,2] >>= \\a -> 'cut' >> 'fromList' [a,a+3]) == 'fromList' [1,4]@
--
-- @'call' (('cut' >> return True) \`'choose'\` return False) == return True@
cut :: Effs '[NonDet, Cut] m => m ()
cut :: m ()
cut = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () m () -> m () -> m ()
forall (m :: * -> *) a. Eff NonDet m => m a -> m a -> m a
`choose` m ()
forall (m :: * -> *) a. Eff Cut m => m a
cutfail
{-# INLINE cut #-}

-- | Delimit the prevention of backtracking from uses of 'cut' and 'cutfail'.
--
-- @'call' 'cutfail' \`'choose'\` m = m@
call :: Eff Cut m => m a -> m a
call :: m a -> m a
call = Cut m a -> m a
forall (e :: Effect) (m :: * -> *) a.
(Member e (Derivs m), Carrier m) =>
e m a -> m a
send (Cut m a -> m a) -> (m a -> Cut m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> Cut m a
forall (m :: * -> *) a. m a -> Cut m a
Call
{-# INLINE call #-}

-- | Split a nondeterministic computation into its first result
-- and the rest of the computation, if possible.
--
-- Note that @'split' 'cutfail' == 'cutfail'@. If you don't want that behavior,
-- use @'split' ('call' m)@ instead of @'split' m@.
split :: Eff Split m => m a -> m (Maybe (a, m a))
split :: m a -> m (Maybe (a, m a))
split = Split m (Maybe (a, m a)) -> m (Maybe (a, m a))
forall (e :: Effect) (m :: * -> *) a.
(Member e (Derivs m), Carrier m) =>
e m a -> m a
send (Split m (Maybe (a, m a)) -> m (Maybe (a, m a)))
-> (m a -> Split m (Maybe (a, m a))) -> m a -> m (Maybe (a, m a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (a, m a) -> Maybe (a, m a))
-> m a -> Split m (Maybe (a, m a))
forall a (m :: * -> *) b. (Maybe (a, m a) -> b) -> m a -> Split m b
Split Maybe (a, m a) -> Maybe (a, m a)
forall a. a -> a
id
{-# INLINE split #-}