{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}

{- | Provides an effect to delimit backtracking in a given nondeterministic context. This effect is used in concert with 'Control.Effect.NonDet.NonDet'.

Computations that signal failure with 'cutfail' prevent backtracking within the nearest enclosing 'call'.

Predefined carriers:

* "Control.Carrier.Cut.Church"

@since 0.1.2.0
-}

module Control.Effect.Cut
( -- * Cut effect
  Cut(..)
, cutfail
, call
, cut
  -- * Re-exports
, Algebra
, Effect
, Has
, run
) where

import Control.Algebra
import Control.Applicative (Alternative(..))

-- | 'Cut' effects are used with 'Control.Effect.Choose' to provide control over backtracking.
--
-- @since 0.1.2.0
data Cut m k
  = Cutfail
  | forall a . Call (m a) (a -> m k)

deriving instance Functor m => Functor (Cut m)

instance HFunctor Cut where
  hmap :: (forall x. m x -> n x) -> Cut m a -> Cut n a
hmap _ Cutfail    = Cut n a
forall (m :: * -> *) k. Cut m k
Cutfail
  hmap f :: forall x. m x -> n x
f (Call m :: m a
m k :: a -> m a
k) = n a -> (a -> n a) -> Cut n a
forall (m :: * -> *) k a. m a -> (a -> m k) -> Cut m k
Call (m a -> n a
forall x. m x -> n x
f m a
m) (m a -> n a
forall x. m x -> n x
f (m a -> n a) -> (a -> m a) -> a -> n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m a
k)
  {-# INLINE hmap #-}

instance Effect Cut where
  thread :: ctx ()
-> (forall x. ctx (m x) -> n (ctx x)) -> Cut m a -> Cut n (ctx a)
thread _   _       Cutfail    = Cut n (ctx a)
forall (m :: * -> *) k. Cut m k
Cutfail
  thread ctx :: ctx ()
ctx handler :: forall x. ctx (m x) -> n (ctx x)
handler (Call m :: m a
m k :: a -> m a
k) = n (ctx a) -> (ctx a -> n (ctx a)) -> Cut n (ctx a)
forall (m :: * -> *) k a. m a -> (a -> m k) -> Cut m k
Call (ctx (m a) -> n (ctx a)
forall x. ctx (m x) -> n (ctx x)
handler (m a
m m a -> ctx () -> ctx (m a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ctx ()
ctx)) (ctx (m a) -> n (ctx a)
forall x. ctx (m x) -> n (ctx x)
handler (ctx (m a) -> n (ctx a))
-> (ctx a -> ctx (m a)) -> ctx a -> n (ctx a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m a) -> ctx a -> ctx (m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> m a
k)
  {-# INLINE thread #-}

-- | Fail the current branch, and prevent backtracking within the nearest enclosing 'call' (if any).
--
--   Contrast with 'empty', which fails the current branch but allows backtracking.
--
-- @
-- 'cutfail' '>>=' k = 'cutfail'
-- @
-- @
-- 'cutfail' '<|>' m = 'cutfail'
-- @
--
-- @since 0.1.2.0
cutfail :: Has Cut sig m => m a
cutfail :: m a
cutfail = Cut m a -> m a
forall (eff :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member eff sig, Algebra sig m) =>
eff m a -> m a
send Cut m a
forall (m :: * -> *) k. Cut m k
Cutfail
{-# INLINE cutfail #-}

-- | Delimit the effect of 'cutfail's, allowing backtracking to resume.
--
-- @
-- 'call' 'cutfail' '<|>' m = m
-- @
--
-- @since 0.1.2.0
call :: Has Cut sig m => m a -> m a
call :: m a -> m a
call m :: m a
m = Cut m a -> m a
forall (eff :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member eff sig, Algebra sig m) =>
eff m a -> m a
send (m a -> (a -> m a) -> Cut m a
forall (m :: * -> *) k a. m a -> (a -> m k) -> Cut m k
Call m a
m a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
{-# INLINE call #-}

-- | Commit to the current branch, preventing backtracking within the nearest enclosing 'call' (if any) on failure.
--
-- @
-- 'cut' '>>' 'empty' = 'cutfail'
-- @
--
-- @since 0.1.2.0
cut :: (Alternative m, Has Cut sig m) => m ()
cut :: m ()
cut = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () m () -> m () -> m ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m ()
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has Cut sig m =>
m a
cutfail
{-# INLINE cut #-}