{-# LANGUAGE DeriveFunctor, ExistentialQuantification, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, MultiParamTypeClasses, RankNTypes, StandaloneDeriving, TypeOperators, UndecidableInstances #-}
module Control.Effect.Cut
( -- * Cut effect
  Cut(..)
, cutfail
, call
, cut
  -- * Cut carrier
, runCut
, runCutAll
, CutC(..)
-- * Re-exports
, Carrier
, Member
, run
) where

import Control.Effect.Carrier
import Control.Effect.NonDet
import Control.Monad (MonadPlus(..))
import qualified Control.Monad.Fail as Fail
import Control.Monad.Fix
import Control.Monad.IO.Class
import Control.Monad.Trans.Class

-- | 'Cut' effects are used with 'NonDet' to provide control over backtracking.
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
  handle :: f () -> (forall x. f (m x) -> n (f x)) -> Cut m a -> Cut n (f a)
handle _     _       Cutfail    = Cut n (f a)
forall (m :: * -> *) k. Cut m k
Cutfail
  handle state :: f ()
state handler :: forall x. f (m x) -> n (f x)
handler (Call m :: m a
m k :: a -> m a
k) = n (f a) -> (f a -> n (f a)) -> Cut n (f a)
forall (m :: * -> *) k a. m a -> (a -> m k) -> Cut m k
Call (f (m a) -> n (f a)
forall x. f (m x) -> n (f x)
handler (m a
m m a -> f () -> f (m a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f ()
state)) (f (m a) -> n (f a)
forall x. f (m x) -> n (f x)
handler (f (m a) -> n (f a)) -> (f a -> f (m a)) -> f a -> n (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m a) -> f a -> f (m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> m a
k)
  {-# INLINE handle #-}

-- | 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.
--
--   prop> run (runNonDet (runCut (cutfail <|> pure a))) === []
--   prop> run (runNonDet (runCut (pure a <|> cutfail))) === [a]
cutfail :: (Carrier sig m, Member Cut sig) => m a
cutfail :: m a
cutfail = Cut m a -> m a
forall (effect :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member effect sig, Carrier sig m) =>
effect 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.
--
--   prop> run (runNonDet (runCut (call (cutfail <|> pure a) <|> pure b))) === [b]
call :: (Carrier sig m, Member Cut sig) => m a -> m a
call :: m a -> m a
call m :: m a
m = Cut m a -> m a
forall (effect :: (* -> *) -> * -> *) (sig :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(Member effect sig, Carrier sig m) =>
effect 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.
--
--   prop> run (runNonDet (runCut (pure a <|> cut *> pure b))) === [a, b]
--   prop> run (runNonDet (runCut (cut *> pure a <|> pure b))) === [a]
--   prop> run (runNonDet (runCut (cut *> empty <|> pure a))) === []
cut :: (Alternative m, Carrier sig m, Member Cut sig) => 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.
(Carrier sig m, Member Cut sig) =>
m a
cutfail
{-# INLINE cut #-}


-- | Run a 'Cut' effect within an underlying 'Alternative' instance (typically another 'Carrier' for a 'NonDet' effect).
--
--   prop> run (runNonDetOnce (runCut (pure a))) === Just a
runCut :: Alternative m => CutC m a -> m a
runCut :: CutC m a -> m a
runCut m :: CutC m a
m = CutC m a -> (a -> m a -> m a) -> m a -> m a -> m a
forall (m :: * -> *) a.
CutC m a -> forall b. (a -> m b -> m b) -> m b -> m b -> m b
runCutC CutC m a
m (m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (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 (f :: * -> *) a. Applicative f => a -> f a
pure) m a
forall (f :: * -> *) a. Alternative f => f a
empty m a
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Run a 'Cut' effect, returning all its results in an 'Alternative' collection.
runCutAll :: (Alternative f, Applicative m) => CutC m a -> m (f a)
runCutAll :: CutC m a -> m (f a)
runCutAll (CutC m :: forall b. (a -> m b -> m b) -> m b -> m b -> m b
m) = (a -> m (f a) -> m (f a)) -> m (f a) -> m (f a) -> m (f a)
forall b. (a -> m b -> m b) -> m b -> m b -> m b
m ((f a -> f a) -> m (f a) -> m (f a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f a -> f a) -> m (f a) -> m (f a))
-> (a -> f a -> f a) -> a -> m (f a) -> m (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (f a -> f a -> f a) -> (a -> f a) -> a -> f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) (f a -> m (f a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure f a
forall (f :: * -> *) a. Alternative f => f a
empty) (f a -> m (f a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure f a
forall (f :: * -> *) a. Alternative f => f a
empty)

newtype CutC m a = CutC
  { -- | A higher-order function receiving three parameters: a function to combine each solution with the rest of the solutions, an action to run when no results are produced (e.g. on 'empty'), and an action to run when no results are produced and backtrcking should not be attempted (e.g. on 'cutfail').
    CutC m a -> forall b. (a -> m b -> m b) -> m b -> m b -> m b
runCutC :: forall b . (a -> m b -> m b) -> m b -> m b -> m b
  }
  deriving (a -> CutC m b -> CutC m a
(a -> b) -> CutC m a -> CutC m b
(forall a b. (a -> b) -> CutC m a -> CutC m b)
-> (forall a b. a -> CutC m b -> CutC m a) -> Functor (CutC m)
forall a b. a -> CutC m b -> CutC m a
forall a b. (a -> b) -> CutC m a -> CutC m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) a b. a -> CutC m b -> CutC m a
forall (m :: * -> *) a b. (a -> b) -> CutC m a -> CutC m b
<$ :: a -> CutC m b -> CutC m a
$c<$ :: forall (m :: * -> *) a b. a -> CutC m b -> CutC m a
fmap :: (a -> b) -> CutC m a -> CutC m b
$cfmap :: forall (m :: * -> *) a b. (a -> b) -> CutC m a -> CutC m b
Functor)

instance Applicative (CutC m) where
  pure :: a -> CutC m a
pure a :: a
a = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ cons :: a -> m b -> m b
cons nil :: m b
nil _ -> a -> m b -> m b
cons a
a m b
nil)
  {-# INLINE pure #-}
  CutC f :: forall b. ((a -> b) -> m b -> m b) -> m b -> m b -> m b
f <*> :: CutC m (a -> b) -> CutC m a -> CutC m b
<*> CutC a :: forall b. (a -> m b -> m b) -> m b -> m b -> m b
a = (forall b. (b -> m b -> m b) -> m b -> m b -> m b) -> CutC m b
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC ((forall b. (b -> m b -> m b) -> m b -> m b -> m b) -> CutC m b)
-> (forall b. (b -> m b -> m b) -> m b -> m b -> m b) -> CutC m b
forall a b. (a -> b) -> a -> b
$ \ cons :: b -> m b -> m b
cons nil :: m b
nil fail :: m b
fail ->
    ((a -> b) -> m b -> m b) -> m b -> m b -> m b
forall b. ((a -> b) -> m b -> m b) -> m b -> m b -> m b
f (\ f' :: a -> b
f' fs :: m b
fs -> (a -> m b -> m b) -> m b -> m b -> m b
forall b. (a -> m b -> m b) -> m b -> m b -> m b
a (b -> m b -> m b
cons (b -> m b -> m b) -> (a -> b) -> a -> m b -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f') m b
fs m b
fail) m b
nil m b
fail
  {-# INLINE (<*>) #-}

instance Alternative (CutC m) where
  empty :: CutC m a
empty = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ _ nil :: m b
nil _ -> m b
nil)
  {-# INLINE empty #-}
  CutC l :: forall b. (a -> m b -> m b) -> m b -> m b -> m b
l <|> :: CutC m a -> CutC m a -> CutC m a
<|> CutC r :: forall b. (a -> m b -> m b) -> m b -> m b -> m b
r = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ cons :: a -> m b -> m b
cons nil :: m b
nil fail :: m b
fail -> (a -> m b -> m b) -> m b -> m b -> m b
forall b. (a -> m b -> m b) -> m b -> m b -> m b
l a -> m b -> m b
cons ((a -> m b -> m b) -> m b -> m b -> m b
forall b. (a -> m b -> m b) -> m b -> m b -> m b
r a -> m b -> m b
cons m b
nil m b
fail) m b
fail)
  {-# INLINE (<|>) #-}

instance Monad (CutC m) where
  CutC a :: forall b. (a -> m b -> m b) -> m b -> m b -> m b
a >>= :: CutC m a -> (a -> CutC m b) -> CutC m b
>>= f :: a -> CutC m b
f = (forall b. (b -> m b -> m b) -> m b -> m b -> m b) -> CutC m b
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC ((forall b. (b -> m b -> m b) -> m b -> m b -> m b) -> CutC m b)
-> (forall b. (b -> m b -> m b) -> m b -> m b -> m b) -> CutC m b
forall a b. (a -> b) -> a -> b
$ \ cons :: b -> m b -> m b
cons nil :: m b
nil fail :: m b
fail ->
    (a -> m b -> m b) -> m b -> m b -> m b
forall b. (a -> m b -> m b) -> m b -> m b -> m b
a (\ a' :: a
a' as :: m b
as -> CutC m b -> (b -> m b -> m b) -> m b -> m b -> m b
forall (m :: * -> *) a.
CutC m a -> forall b. (a -> m b -> m b) -> m b -> m b -> m b
runCutC (a -> CutC m b
f a
a') b -> m b -> m b
cons m b
as m b
fail) m b
nil m b
fail
  {-# INLINE (>>=) #-}

instance Fail.MonadFail m => Fail.MonadFail (CutC m) where
  fail :: String -> CutC m a
fail s :: String
s = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ _ _ _ -> String -> m b
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
s)
  {-# INLINE fail #-}

instance MonadFix m => MonadFix (CutC m) where
  mfix :: (a -> CutC m a) -> CutC m a
mfix f :: a -> CutC m a
f = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ cons :: a -> m b -> m b
cons nil :: m b
nil _ -> ([a] -> m [a]) -> m [a]
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (\ a :: [a]
a -> CutC m a -> (a -> m [a] -> m [a]) -> m [a] -> m [a] -> m [a]
forall (m :: * -> *) a.
CutC m a -> forall b. (a -> m b -> m b) -> m b -> m b -> m b
runCutC (a -> CutC m a
f ([a] -> a
forall a. [a] -> a
head [a]
a)) (([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 []) ([a] -> m [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])) m [a] -> ([a] -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> m b -> m b) -> m b -> [a] -> m b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> m b -> m b
cons m b
nil)
  {-# INLINE mfix #-}

instance MonadIO m => MonadIO (CutC m) where
  liftIO :: IO a -> CutC m a
liftIO io :: IO a
io = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ cons :: a -> m b -> m b
cons nil :: m b
nil _ -> IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO a
io m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> m b -> m b) -> m b -> a -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> m b -> m b
cons m b
nil)
  {-# INLINE liftIO #-}

instance MonadPlus (CutC m)

instance MonadTrans CutC where
  lift :: m a -> CutC m a
lift m :: m a
m = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC (\ cons :: a -> m b -> m b
cons nil :: m b
nil _ -> m a
m m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> m b -> m b) -> m b -> a -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> m b -> m b
cons m b
nil)
  {-# INLINE lift #-}

instance (Carrier sig m, Effect sig) => Carrier (Cut :+: NonDet :+: sig) (CutC m) where
  eff :: (:+:) Cut (NonDet :+: sig) (CutC m) a -> CutC m a
eff (L Cutfail)    = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC ((forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a)
-> (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall a b. (a -> b) -> a -> b
$ \ _    _   fail :: m b
fail -> m b
fail
  eff (L (Call m :: CutC m a
m k :: a -> CutC m a
k)) = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC ((forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a)
-> (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall a b. (a -> b) -> a -> b
$ \ cons :: a -> m b -> m b
cons nil :: m b
nil fail :: m b
fail -> CutC m a -> (a -> m b -> m b) -> m b -> m b -> m b
forall (m :: * -> *) a.
CutC m a -> forall b. (a -> m b -> m b) -> m b -> m b -> m b
runCutC CutC m a
m (\ a :: a
a as :: m b
as -> CutC m a -> (a -> m b -> m b) -> m b -> m b -> m b
forall (m :: * -> *) a.
CutC m a -> forall b. (a -> m b -> m b) -> m b -> m b -> m b
runCutC (a -> CutC m a
k a
a) a -> m b -> m b
cons m b
as m b
fail) m b
nil m b
nil
  eff (R (L Empty))      = CutC m a
forall (f :: * -> *) a. Alternative f => f a
empty
  eff (R (L (Choose k :: Bool -> CutC m a
k))) = Bool -> CutC m a
k Bool
True CutC m a -> CutC m a -> CutC m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> CutC m a
k Bool
False
  eff (R (R other :: sig (CutC m) a
other)) = (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
CutC ((forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a)
-> (forall b. (a -> m b -> m b) -> m b -> m b -> m b) -> CutC m a
forall a b. (a -> b) -> a -> b
$ \ cons :: a -> m b -> m b
cons nil :: m b
nil _ -> sig m [a] -> m [a]
forall (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Carrier sig m =>
sig m a -> m a
eff ([()]
-> (forall x. [CutC m x] -> m [x]) -> sig (CutC m) a -> sig m [a]
forall (sig :: (* -> *) -> * -> *) (f :: * -> *) (m :: * -> *)
       (n :: * -> *) a.
(Effect sig, Functor f, Monad m) =>
f () -> (forall x. f (m x) -> n (f x)) -> sig m a -> sig n (f a)
handle [()] (([[x]] -> [x]) -> m [[x]] -> m [x]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[x]] -> [x]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (m [[x]] -> m [x])
-> ([CutC m x] -> m [[x]]) -> [CutC m x] -> m [x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CutC m x -> m [x]) -> [CutC m x] -> m [[x]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CutC m x -> m [x]
forall (f :: * -> *) (m :: * -> *) a.
(Alternative f, Applicative m) =>
CutC m a -> m (f a)
runCutAll) sig (CutC m) a
other) m [a] -> ([a] -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (a -> m b -> m b) -> m b -> [a] -> m b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> m b -> m b
cons m b
nil
  {-# INLINE eff #-}


-- $setup
-- >>> :seti -XFlexibleContexts
-- >>> import Test.QuickCheck
-- >>> import Control.Effect.Cull
-- >>> import Control.Effect.Pure