{-# LANGUAGE DeriveAnyClass, DeriveFunctor, DeriveGeneric, DerivingStrategies, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, RankNTypes, TypeOperators, UndecidableInstances #-}
module Control.Effect.NonDet
( -- * NonDet effect
  NonDet(..)
  -- * NonDet carrier
, runNonDet
, NonDetC(..)
  -- * Re-exports
, Alternative(..)
, Carrier
, Member
, run
) where

import Control.Applicative (Alternative(..))
import Control.Effect.Carrier
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
import GHC.Generics (Generic1)

data NonDet m k
  = Empty
  | Choose (Bool -> m k)
  deriving stock (a -> NonDet m b -> NonDet m a
(a -> b) -> NonDet m a -> NonDet m b
(forall a b. (a -> b) -> NonDet m a -> NonDet m b)
-> (forall a b. a -> NonDet m b -> NonDet m a)
-> Functor (NonDet m)
forall a b. a -> NonDet m b -> NonDet m a
forall a b. (a -> b) -> NonDet m a -> NonDet m b
forall (m :: * -> *) a b.
Functor m =>
a -> NonDet m b -> NonDet m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NonDet m a -> NonDet m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> NonDet m b -> NonDet m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> NonDet m b -> NonDet m a
fmap :: (a -> b) -> NonDet m a -> NonDet m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> NonDet m a -> NonDet m b
Functor, (forall a. NonDet m a -> Rep1 (NonDet m) a)
-> (forall a. Rep1 (NonDet m) a -> NonDet m a)
-> Generic1 (NonDet m)
forall a. Rep1 (NonDet m) a -> NonDet m a
forall a. NonDet m a -> Rep1 (NonDet m) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (m :: * -> *) a. Rep1 (NonDet m) a -> NonDet m a
forall (m :: * -> *) a. NonDet m a -> Rep1 (NonDet m) a
$cto1 :: forall (m :: * -> *) a. Rep1 (NonDet m) a -> NonDet m a
$cfrom1 :: forall (m :: * -> *) a. NonDet m a -> Rep1 (NonDet m) a
Generic1)
  deriving anyclass ((forall (f :: * -> *) a b.
 Functor (NonDet f) =>
 (a -> b) -> NonDet f a -> NonDet f b)
-> (forall (m :: * -> *) (n :: * -> *) a.
    Functor m =>
    (forall x. m x -> n x) -> NonDet m a -> NonDet n a)
-> HFunctor NonDet
forall (f :: * -> *) a b.
Functor (NonDet f) =>
(a -> b) -> NonDet f a -> NonDet f b
forall (m :: * -> *) (n :: * -> *) a.
Functor m =>
(forall x. m x -> n x) -> NonDet m a -> NonDet n a
forall (h :: (* -> *) -> * -> *).
(forall (f :: * -> *) a b.
 Functor (h f) =>
 (a -> b) -> h f a -> h f b)
-> (forall (m :: * -> *) (n :: * -> *) a.
    Functor m =>
    (forall x. m x -> n x) -> h m a -> h n a)
-> HFunctor h
hmap :: (forall x. m x -> n x) -> NonDet m a -> NonDet n a
$chmap :: forall (m :: * -> *) (n :: * -> *) a.
Functor m =>
(forall x. m x -> n x) -> NonDet m a -> NonDet n a
fmap' :: (a -> b) -> NonDet f a -> NonDet f b
$cfmap' :: forall (f :: * -> *) a b.
Functor (NonDet f) =>
(a -> b) -> NonDet f a -> NonDet f b
HFunctor, HFunctor NonDet
HFunctor NonDet =>
(forall (f :: * -> *) (m :: * -> *) (n :: * -> *) a.
 (Functor f, Monad m) =>
 f ()
 -> (forall x. f (m x) -> n (f x)) -> NonDet m a -> NonDet n (f a))
-> Effect NonDet
forall (f :: * -> *) (m :: * -> *) (n :: * -> *) a.
(Functor f, Monad m) =>
f ()
-> (forall x. f (m x) -> n (f x)) -> NonDet m a -> NonDet n (f a)
forall (sig :: (* -> *) -> * -> *).
HFunctor sig =>
(forall (f :: * -> *) (m :: * -> *) (n :: * -> *) a.
 (Functor f, Monad m) =>
 f () -> (forall x. f (m x) -> n (f x)) -> sig m a -> sig n (f a))
-> Effect sig
handle :: f ()
-> (forall x. f (m x) -> n (f x)) -> NonDet m a -> NonDet n (f a)
$chandle :: forall (f :: * -> *) (m :: * -> *) (n :: * -> *) a.
(Functor f, Monad m) =>
f ()
-> (forall x. f (m x) -> n (f x)) -> NonDet m a -> NonDet n (f a)
$cp1Effect :: HFunctor NonDet
Effect)


-- | Run a 'NonDet' effect, collecting all branches’ results into an 'Alternative' functor.
--
--   Using '[]' as the 'Alternative' functor will produce all results, while 'Maybe' will return only the first. However, unlike 'runNonDetOnce', this will still enumerate the entire search space before returning, meaning that it will diverge for infinite search spaces, even when using 'Maybe'.
--
--   prop> run (runNonDet (pure a)) === [a]
--   prop> run (runNonDet (pure a)) === Just a
runNonDet :: (Alternative f, Applicative m) => NonDetC m a -> m (f a)
runNonDet :: NonDetC m a -> m (f a)
runNonDet (NonDetC m :: forall b. (a -> m b -> m b) -> m b -> m b
m) = (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 ((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)

-- | A carrier for 'NonDet' effects based on Ralf Hinze’s design described in [Deriving Backtracking Monad Transformers](https://www.cs.ox.ac.uk/ralf.hinze/publications/#P12).
newtype NonDetC m a = NonDetC
  { -- | A higher-order function receiving two parameters: a function to combine each solution with the rest of the solutions, and an action to run when no results are produced.
    NonDetC m a -> forall b. (a -> m b -> m b) -> m b -> m b
runNonDetC :: forall b . (a -> m b -> m b) -> m b -> m b
  }
  deriving stock (a -> NonDetC m b -> NonDetC m a
(a -> b) -> NonDetC m a -> NonDetC m b
(forall a b. (a -> b) -> NonDetC m a -> NonDetC m b)
-> (forall a b. a -> NonDetC m b -> NonDetC m a)
-> Functor (NonDetC m)
forall a b. a -> NonDetC m b -> NonDetC m a
forall a b. (a -> b) -> NonDetC m a -> NonDetC 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 -> NonDetC m b -> NonDetC m a
forall (m :: * -> *) a b. (a -> b) -> NonDetC m a -> NonDetC m b
<$ :: a -> NonDetC m b -> NonDetC m a
$c<$ :: forall (m :: * -> *) a b. a -> NonDetC m b -> NonDetC m a
fmap :: (a -> b) -> NonDetC m a -> NonDetC m b
$cfmap :: forall (m :: * -> *) a b. (a -> b) -> NonDetC m a -> NonDetC m b
Functor)

instance Applicative (NonDetC m) where
  pure :: a -> NonDetC m a
pure a :: a
a = (forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC (\ cons :: a -> m b -> m b
cons -> a -> m b -> m b
cons a
a)
  {-# INLINE pure #-}
  NonDetC f :: forall b. ((a -> b) -> m b -> m b) -> m b -> m b
f <*> :: NonDetC m (a -> b) -> NonDetC m a -> NonDetC m b
<*> NonDetC a :: forall b. (a -> m b -> m b) -> m b -> m b
a = (forall b. (b -> m b -> m b) -> m b -> m b) -> NonDetC m b
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC ((forall b. (b -> m b -> m b) -> m b -> m b) -> NonDetC m b)
-> (forall b. (b -> m b -> m b) -> m b -> m b) -> NonDetC m b
forall a b. (a -> b) -> a -> b
$ \ cons :: b -> m b -> m b
cons ->
    ((a -> b) -> m b -> m b) -> m b -> m b
forall b. ((a -> b) -> m b -> m b) -> m b -> m b
f (\ f' :: a -> b
f' -> (a -> m b -> m b) -> m b -> m b
forall b. (a -> 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'))
  {-# INLINE (<*>) #-}

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

instance Monad (NonDetC m) where
  NonDetC a :: forall b. (a -> m b -> m b) -> m b -> m b
a >>= :: NonDetC m a -> (a -> NonDetC m b) -> NonDetC m b
>>= f :: a -> NonDetC m b
f = (forall b. (b -> m b -> m b) -> m b -> m b) -> NonDetC m b
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC ((forall b. (b -> m b -> m b) -> m b -> m b) -> NonDetC m b)
-> (forall b. (b -> m b -> m b) -> m b -> m b) -> NonDetC m b
forall a b. (a -> b) -> a -> b
$ \ cons :: b -> m b -> m b
cons ->
    (a -> m b -> m b) -> m b -> m b
forall b. (a -> m b -> m b) -> m b -> m b
a (\ a' :: a
a' -> NonDetC m b -> (b -> m b -> m b) -> m b -> m b
forall (m :: * -> *) a.
NonDetC m a -> forall b. (a -> m b -> m b) -> m b -> m b
runNonDetC (a -> NonDetC m b
f a
a') b -> m b -> m b
cons)
  {-# INLINE (>>=) #-}

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

instance MonadFix m => MonadFix (NonDetC m) where
  mfix :: (a -> NonDetC m a) -> NonDetC m a
mfix f :: a -> NonDetC m a
f = (forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC (\ 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 -> NonDetC m a -> (a -> m [a] -> m [a]) -> m [a] -> m [a]
forall (m :: * -> *) a.
NonDetC m a -> forall b. (a -> m b -> m b) -> m b -> m b
runNonDetC (a -> NonDetC 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 [])) 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 (NonDetC m) where
  liftIO :: IO a -> NonDetC m a
liftIO io :: IO a
io = (forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC (\ 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 (NonDetC m)

instance MonadTrans NonDetC where
  lift :: m a -> NonDetC m a
lift m :: m a
m = (forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC (\ 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 (NonDet :+: sig) (NonDetC m) where
  eff :: (:+:) NonDet sig (NonDetC m) a -> NonDetC m a
eff (L Empty)      = NonDetC m a
forall (f :: * -> *) a. Alternative f => f a
empty
  eff (L (Choose k :: Bool -> NonDetC m a
k)) = Bool -> NonDetC m a
k Bool
True NonDetC m a -> NonDetC m a -> NonDetC m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> NonDetC m a
k Bool
False
  eff (R other :: sig (NonDetC m) a
other)      = (forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
forall (m :: * -> *) a.
(forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a
NonDetC ((forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC m a)
-> (forall b. (a -> m b -> m b) -> m b -> m b) -> NonDetC 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. [NonDetC m x] -> m [x])
-> sig (NonDetC 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])
-> ([NonDetC m x] -> m [[x]]) -> [NonDetC m x] -> m [x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonDetC m x -> m [x]) -> [NonDetC m x] -> m [[x]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse NonDetC m x -> m [x]
forall (f :: * -> *) (m :: * -> *) a.
(Alternative f, Applicative m) =>
NonDetC m a -> m (f a)
runNonDet) sig (NonDetC 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.Pure
-- >>> import Data.Foldable (asum)