{-# LANGUAGE RankNTypes #-}

module Control.Monad.Amb
       (
         -- * Overview
         -- $overview

         -- * Creating computations
         amb,
         aPartitionOfSize,
         aPartitionOf,
         aPermutationOf,
         aSplitOf,
         anIntegerBetween,
         aSubsetOf,
         aMemberOf,
         aBoolean,
         -- * Running computations
         isPossible,
         isPossibleT,
         isNecessary,
         isNecessaryT,
         allValues,
         allValuesT,
         oneValue,
         oneValueT,
         -- * Low-level internals
         tell',
         tellState,
         uponFailure,
         runAmbT,
         runAmbTI,
         ambCC,
         forEffects,
         -- * Types
         AmbT(..),
         AmbT',
         Amb,
         Amb',
         module Control.Applicative
       ) where
import Control.Monad.Cont
import Control.Monad.State.Lazy
import Control.Monad.Identity
import Control.Monad
import Control.Applicative
#if __GLASGOW_HASKELL__ < 709
import Data.Monoid
#endif

-- $overview
--
-- A nondeterministic computation makes a series of choices which it
-- can then backtrack to. You can select between computations with
-- '(<|>)' or 'mplus' and abort a line of computation with 'empty' or
-- 'mzero'
--
-- As an example, here is a program which computes Pythagorean triples
-- of a certain size.
--
-- @
--import Control.Monad
--import Control.Monad.Amb
--
--pyTriple :: (Num t, Ord t) => t -> Amb r (t, t, t)
--pyTriple n = do a <- 'anIntegerBetween' 1 n
--                b <- 'anIntegerBetween' (a + 1) n
--                c <- 'anIntegerBetween' (b + 1) n
--                when (a*a + b*b /= c*c) 'empty'
--                return (a,b,c)
-- @
--
-- You can run this computation and ask for one or more of its
-- possible values.
--
-- >>> oneValue $ pyTriple 20
-- (3,4,5)
--
-- >>> allValues $ pyTriple 20
-- [(3,4,5),(5,12,13),(6,8,10),(8,15,17),(9,12,15),(12,16,20)]

-- | @AmbT r m a@ is a computation whose current value is of type @a@
-- and which will ultimately return a value of type @r@. The same as
-- @ContT@.
data AmbT r m a = AmbT { 
  {- | From left to right:

       * the computation to run on failure
       
       * the continuation captured when making nondeterministic choices

       * record keeping of solutions found so far
 -}
  AmbT r m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
unAmbT ::
     StateT (AmbT r m r)
     (ContT r            
      (StateT [r] m))
     a }

type Amb r = AmbT r Identity
type AmbT' m a = forall r. AmbT r m a
type Amb' a = AmbT' Identity a

instance MonadTrans (AmbT r) where
    lift :: m a -> AmbT r m a
lift = StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a)
-> (m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> m a
-> AmbT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContT r (StateT [r] m) a
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ContT r (StateT [r] m) a
 -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> (m a -> ContT r (StateT [r] m) a)
-> m a
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT [r] m a -> ContT r (StateT [r] m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT [r] m a -> ContT r (StateT [r] m) a)
-> (m a -> StateT [r] m a) -> m a -> ContT r (StateT [r] m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT [r] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance Monad (AmbT r m) where
    AmbT StateT (AmbT r m r) (ContT r (StateT [r] m)) a
a >>= :: AmbT r m a -> (a -> AmbT r m b) -> AmbT r m b
>>= a -> AmbT r m b
b = StateT (AmbT r m r) (ContT r (StateT [r] m)) b -> AmbT r m b
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) b -> AmbT r m b)
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) b -> AmbT r m b
forall a b. (a -> b) -> a -> b
$ StateT (AmbT r m r) (ContT r (StateT [r] m)) a
a StateT (AmbT r m r) (ContT r (StateT [r] m)) a
-> (a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) b)
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AmbT r m b -> StateT (AmbT r m r) (ContT r (StateT [r] m)) b
forall r (m :: * -> *) a.
AmbT r m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
unAmbT (AmbT r m b -> StateT (AmbT r m r) (ContT r (StateT [r] m)) b)
-> (a -> AmbT r m b)
-> a
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AmbT r m b
b
    return :: a -> AmbT r m a
return = StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a)
-> (a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> a
-> AmbT r m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance MonadPlus (AmbT r m) where
  mzero :: AmbT r m a
mzero = AmbT r m a
forall r (m :: * -> *) a. AmbT r m a
fail'
  mplus :: AmbT r m a -> AmbT r m a -> AmbT r m a
mplus = AmbT r m a -> AmbT r m a -> AmbT r m a
forall r (m :: * -> *) a. AmbT r m a -> AmbT r m a -> AmbT r m a
either'

instance Functor (AmbT r m) where
  fmap :: (a -> b) -> AmbT r m a -> AmbT r m b
fmap = (a -> b) -> AmbT r m a -> AmbT r m b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative (AmbT r m) where
  pure :: a -> AmbT r m a
pure = a -> AmbT r m a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: AmbT r m (a -> b) -> AmbT r m a -> AmbT r m b
(<*>) = AmbT r m (a -> b) -> AmbT r m a -> AmbT r m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Alternative (AmbT r m) where
  <|> :: AmbT r m a -> AmbT r m a -> AmbT r m a
(<|>) = AmbT r m a -> AmbT r m a -> AmbT r m a
forall r (m :: * -> *) a. AmbT r m a -> AmbT r m a -> AmbT r m a
either'
  empty :: AmbT r m a
empty = AmbT r m a
forall r (m :: * -> *) a. AmbT r m a
fail'

-- Internals

-- | call/cc lifted into the nondeterministic monad. This implements
-- the backtracking behaviour which allows Amb to try different code
-- paths and return multiple results.
ambCC :: ((a -> AmbT r m a1) -> AmbT r m a) -> AmbT r m a
ambCC :: ((a -> AmbT r m a1) -> AmbT r m a) -> AmbT r m a
ambCC (a -> AmbT r m a1) -> AmbT r m a
f = StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a)
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
forall a b. (a -> b) -> a -> b
$ ((a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a1)
 -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall (m :: * -> *) a b. MonadCont m => ((a -> m b) -> m a) -> m a
callCC (((a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a1)
  -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
 -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> ((a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a1)
    -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall a b. (a -> b) -> a -> b
$ \a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a1
k -> AmbT r m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall r (m :: * -> *) a.
AmbT r m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
unAmbT (AmbT r m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a)
-> AmbT r m a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a
forall a b. (a -> b) -> a -> b
$ (a -> AmbT r m a1) -> AmbT r m a
f ((a -> AmbT r m a1) -> AmbT r m a)
-> (a -> AmbT r m a1) -> AmbT r m a
forall a b. (a -> b) -> a -> b
$ StateT (AmbT r m r) (ContT r (StateT [r] m)) a1 -> AmbT r m a1
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) a1 -> AmbT r m a1)
-> (a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a1)
-> a
-> AmbT r m a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> StateT (AmbT r m r) (ContT r (StateT [r] m)) a1
k

-- | Run the nondeterministic computation. This is internal.
runAmbTI :: (Monad m) => AmbT a m a -> AmbT a m a -> m (a, [a])
runAmbTI :: AmbT a m a -> AmbT a m a -> m (a, [a])
runAmbTI (AmbT StateT (AmbT a m a) (ContT a (StateT [a] m)) a
a) AmbT a m a
i = StateT [a] m a -> [a] -> m (a, [a])
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ContT a (StateT [a] m) a -> (a -> StateT [a] m a) -> StateT [a] m a
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT (StateT (AmbT a m a) (ContT a (StateT [a] m)) a
-> AmbT a m a -> ContT a (StateT [a] m) a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (AmbT a m a) (ContT a (StateT [a] m)) a
a AmbT a m a
i) a -> StateT [a] m a
forall (m :: * -> *) a. Monad m => a -> m a
return) []

-- | Run the nondeterministic computation. This is internal.
runAmbT :: (Monad m) => AmbT t m t -> m (t, [t])
runAmbT :: AmbT t m t -> m (t, [t])
runAmbT AmbT t m t
a = AmbT t m t -> AmbT t m t -> m (t, [t])
forall (m :: * -> *) a.
Monad m =>
AmbT a m a -> AmbT a m a -> m (a, [a])
runAmbTI AmbT t m t
a ([Char] -> AmbT t m t
forall a. HasCallStack => [Char] -> a
error [Char]
"top-level fail")

-- | When the nondeterministic computation backtracks past this state,
-- execute this nondeterministic computation. Generally used to undo
-- side effects.
uponFailure :: AmbT r m a -> AmbT r m ()
uponFailure :: AmbT r m a -> AmbT r m ()
uponFailure AmbT r m a
f = do
  AmbT r m r
old <- StateT (AmbT r m r) (ContT r (StateT [r] m)) (AmbT r m r)
-> AmbT r m (AmbT r m r)
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT StateT (AmbT r m r) (ContT r (StateT [r] m)) (AmbT r m r)
forall s (m :: * -> *). MonadState s m => m s
get
  StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ())
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall a b. (a -> b) -> a -> b
$ AmbT r m r -> StateT (AmbT r m r) (ContT r (StateT [r] m)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (AmbT r m a
f AmbT r m a -> AmbT r m r -> AmbT r m r
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AmbT r m r
old)

-- | A helper to inject state into the backtracking stack
tellState :: (Monoid s, MonadState s m) => s -> m ()
tellState :: s -> m ()
tellState s
b = do
  s
a <- m s
forall s (m :: * -> *). MonadState s m => m s
get
  s -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (s -> m ()) -> s -> m ()
forall a b. (a -> b) -> a -> b
$ s
a s -> s -> s
forall a. Monoid a => a -> a -> a
`mappend` s
b

-- | A helper to inject state into the backtracking stack
tell' :: (Monad m) => [r] -> AmbT r m ()
tell' :: [r] -> AmbT r m ()
tell' [r]
t = StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ())
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall a b. (a -> b) -> a -> b
$ (ContT r (StateT [r] m) ()
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ContT r (StateT [r] m) ()
 -> StateT (AmbT r m r) (ContT r (StateT [r] m)) ())
-> ContT r (StateT [r] m) ()
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) ()
forall a b. (a -> b) -> a -> b
$ StateT [r] m () -> ContT r (StateT [r] m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT [r] m () -> ContT r (StateT [r] m) ())
-> StateT [r] m () -> ContT r (StateT [r] m) ()
forall a b. (a -> b) -> a -> b
$ [r] -> StateT [r] m ()
forall s (m :: * -> *). (Monoid s, MonadState s m) => s -> m ()
tellState [r]
t)

-- | A low-level internal function which executes a nondeterministic
-- computation for its nondeterministic side-effects, such as its
-- ability to produce different results.
forEffects :: (Monad m) => ((t, [t]) -> r) -> (t1 -> AmbT t m t) -> AmbT t m t1 -> m r
forEffects :: ((t, [t]) -> r) -> (t1 -> AmbT t m t) -> AmbT t m t1 -> m r
forEffects (t, [t]) -> r
f t1 -> AmbT t m t
g AmbT t m t1
e = (t, [t]) -> r
f ((t, [t]) -> r) -> m (t, [t]) -> m r
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` AmbT t m t -> AmbT t m t -> m (t, [t])
forall (m :: * -> *) a.
Monad m =>
AmbT a m a -> AmbT a m a -> m (a, [a])
runAmbTI (do ((t -> AmbT t m t) -> AmbT t m t) -> AmbT t m t
forall a r (m :: * -> *) a1.
((a -> AmbT r m a1) -> AmbT r m a) -> AmbT r m a
ambCC (((t -> AmbT t m t) -> AmbT t m t) -> AmbT t m t)
-> ((t -> AmbT t m t) -> AmbT t m t) -> AmbT t m t
forall a b. (a -> b) -> a -> b
$ \t -> AmbT t m t
k -> do
                                            StateT (AmbT t m t) (ContT t (StateT [t] m)) () -> AmbT t m ()
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT t m t) (ContT t (StateT [t] m)) () -> AmbT t m ())
-> StateT (AmbT t m t) (ContT t (StateT [t] m)) () -> AmbT t m ()
forall a b. (a -> b) -> a -> b
$ AmbT t m t -> StateT (AmbT t m t) (ContT t (StateT [t] m)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (t -> AmbT t m t
k t
forall a. HasCallStack => a
undefined)
                                            t1
v <- AmbT t m t1
e
                                            t1 -> AmbT t m t
g t1
v)
                                      (t -> AmbT t m t
forall (m :: * -> *) a. Monad m => a -> m a
return t
forall a. HasCallStack => a
undefined)

-- Run nondeterministic computations

-- | Run a nondeterministic computation and return a result of that
-- computation.
oneValueT :: (Monad m) => AmbT b m b -> m b
oneValueT :: AmbT b m b -> m b
oneValueT AmbT b m b
c = (b, [b]) -> b
forall a b. (a, b) -> a
fst ((b, [b]) -> b) -> m (b, [b]) -> m b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` AmbT b m b -> m (b, [b])
forall (m :: * -> *) t. Monad m => AmbT t m t -> m (t, [t])
runAmbT AmbT b m b
c

-- | Run a nondeterministic computation and return a result of that
-- computation.
oneValue :: Amb a a -> a
oneValue :: Amb a a -> a
oneValue = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> (Amb a a -> Identity a) -> Amb a a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Amb a a -> Identity a
forall (m :: * -> *) b. Monad m => AmbT b m b -> m b
oneValueT

-- | Run a nondeterministic computation and return a list of all
-- results that the computation can produce. Note that this function
-- is not lazy its result.
allValuesT :: (Monad m) => AmbT t m t -> m [t]
allValuesT :: AmbT t m t -> m [t]
allValuesT = ((t, [t]) -> [t]) -> (t -> AmbT t m t) -> AmbT t m t -> m [t]
forall (m :: * -> *) t r t1.
Monad m =>
((t, [t]) -> r) -> (t1 -> AmbT t m t) -> AmbT t m t1 -> m r
forEffects (t, [t]) -> [t]
forall a b. (a, b) -> b
snd (\t
a -> [t] -> AmbT t m ()
forall (m :: * -> *) r. Monad m => [r] -> AmbT r m ()
tell' [t
a] AmbT t m () -> AmbT t m t -> AmbT t m t
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AmbT t m t
forall (f :: * -> *) a. Alternative f => f a
empty)

-- | Run a nondeterministic computation and return a list of all
-- results that the computation can produce. Note that this function
-- is not lazy its result.
allValues :: Amb t t -> [t]
allValues :: Amb t t -> [t]
allValues = Identity [t] -> [t]
forall a. Identity a -> a
runIdentity (Identity [t] -> [t])
-> (Amb t t -> Identity [t]) -> Amb t t -> [t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Amb t t -> Identity [t]
forall (m :: * -> *) t. Monad m => AmbT t m t -> m [t]
allValuesT

-- | Run a nondeterministic computation and return @True@
-- if any result is @True@, @False@ otherwise.
isPossibleT :: (Monad m) => AmbT Bool m Bool -> m Bool
isPossibleT :: AmbT Bool m Bool -> m Bool
isPossibleT = ((Bool, [Bool]) -> Bool)
-> (Bool -> AmbT Bool m Bool) -> AmbT Bool m Bool -> m Bool
forall (m :: * -> *) t r t1.
Monad m =>
((t, [t]) -> r) -> (t1 -> AmbT t m t) -> AmbT t m t1 -> m r
forEffects (([Bool
True] [Bool] -> [Bool] -> Bool
forall a. Eq a => a -> a -> Bool
==) ([Bool] -> Bool)
-> ((Bool, [Bool]) -> [Bool]) -> (Bool, [Bool]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, [Bool]) -> [Bool]
forall a b. (a, b) -> b
snd) (\Bool
a -> Bool -> AmbT Bool m () -> AmbT Bool m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False) AmbT Bool m ()
forall (f :: * -> *) a. Alternative f => f a
empty AmbT Bool m () -> AmbT Bool m () -> AmbT Bool m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Bool] -> AmbT Bool m ()
forall (m :: * -> *) r. Monad m => [r] -> AmbT r m ()
tell' [Bool
True] AmbT Bool m () -> AmbT Bool m Bool -> AmbT Bool m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AmbT Bool m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
forall a. HasCallStack => a
undefined)

-- | Run a nondeterministic computation and return @True@
-- if any result is @True@, @False@ otherwise.
isPossible :: Amb Bool Bool -> Bool
isPossible :: Amb Bool Bool -> Bool
isPossible = Identity Bool -> Bool
forall a. Identity a -> a
runIdentity (Identity Bool -> Bool)
-> (Amb Bool Bool -> Identity Bool) -> Amb Bool Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Amb Bool Bool -> Identity Bool
forall (m :: * -> *). Monad m => AmbT Bool m Bool -> m Bool
isPossibleT

-- | Run a nondeterministic computation and return @True@
-- if all possible results are @True@, @False@ otherwise.
isNecessaryT :: (Monad m) => AmbT Bool m Bool -> m Bool
isNecessaryT :: AmbT Bool m Bool -> m Bool
isNecessaryT = ((Bool, [Bool]) -> Bool)
-> (Bool -> AmbT Bool m Bool) -> AmbT Bool m Bool -> m Bool
forall (m :: * -> *) t r t1.
Monad m =>
((t, [t]) -> r) -> (t1 -> AmbT t m t) -> AmbT t m t1 -> m r
forEffects (([] [Bool] -> [Bool] -> Bool
forall a. Eq a => a -> a -> Bool
==) ([Bool] -> Bool)
-> ((Bool, [Bool]) -> [Bool]) -> (Bool, [Bool]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, [Bool]) -> [Bool]
forall a b. (a, b) -> b
snd) (\Bool
a -> Bool -> AmbT Bool m () -> AmbT Bool m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True) AmbT Bool m ()
forall (f :: * -> *) a. Alternative f => f a
empty AmbT Bool m () -> AmbT Bool m () -> AmbT Bool m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Bool] -> AmbT Bool m ()
forall (m :: * -> *) r. Monad m => [r] -> AmbT r m ()
tell' [Bool
True] AmbT Bool m () -> AmbT Bool m Bool -> AmbT Bool m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AmbT Bool m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
forall a. HasCallStack => a
undefined)

-- | Run a nondeterministic computation and return @True@
-- if all possible results are @True@, @False@ otherwise.
isNecessary :: Amb Bool Bool -> Bool
isNecessary :: Amb Bool Bool -> Bool
isNecessary = Identity Bool -> Bool
forall a. Identity a -> a
runIdentity (Identity Bool -> Bool)
-> (Amb Bool Bool -> Identity Bool) -> Amb Bool Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Amb Bool Bool -> Identity Bool
forall (m :: * -> *). Monad m => AmbT Bool m Bool -> m Bool
isNecessaryT

-- Generate nondeterministic computations

-- | Nondeterministically choose either of the two computations
either' :: AmbT r m b -> AmbT r m b -> AmbT r m b
either' :: AmbT r m b -> AmbT r m b -> AmbT r m b
either' AmbT r m b
a AmbT r m b
b = do Bool
r <- AmbT r m Bool
forall r (m :: * -> *). AmbT r m Bool
aBoolean
                 if Bool
r then AmbT r m b
a else AmbT r m b
b

-- | Terminate this branch of the computation.
fail' :: AmbT r m b
fail' :: AmbT r m b
fail' = StateT (AmbT r m r) (ContT r (StateT [r] m)) (AmbT r m r)
-> AmbT r m (AmbT r m r)
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT StateT (AmbT r m r) (ContT r (StateT [r] m)) (AmbT r m r)
forall s (m :: * -> *). MonadState s m => m s
get AmbT r m (AmbT r m r) -> (AmbT r m r -> AmbT r m b) -> AmbT r m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\AmbT r m r
a -> AmbT r m r
a AmbT r m r -> AmbT r m b -> AmbT r m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AmbT r m b
forall a. HasCallStack => a
undefined)

-- | The most basic primitive that everything else is built out
-- of. Generates @True@ and @False@.
aBoolean :: AmbT r m Bool
aBoolean :: AmbT r m Bool
aBoolean = ((Bool -> AmbT r m Any) -> AmbT r m Bool) -> AmbT r m Bool
forall a r (m :: * -> *) a1.
((a -> AmbT r m a1) -> AmbT r m a) -> AmbT r m a
ambCC (((Bool -> AmbT r m Any) -> AmbT r m Bool) -> AmbT r m Bool)
-> ((Bool -> AmbT r m Any) -> AmbT r m Bool) -> AmbT r m Bool
forall a b. (a -> b) -> a -> b
$ \Bool -> AmbT r m Any
k -> do
             AmbT r m r
old <- StateT (AmbT r m r) (ContT r (StateT [r] m)) (AmbT r m r)
-> AmbT r m (AmbT r m r)
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT StateT (AmbT r m r) (ContT r (StateT [r] m)) (AmbT r m r)
forall s (m :: * -> *). MonadState s m => m s
get
             StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ())
-> StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall a b. (a -> b) -> a -> b
$ AmbT r m r -> StateT (AmbT r m r) (ContT r (StateT [r] m)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (StateT (AmbT r m r) (ContT r (StateT [r] m)) () -> AmbT r m ()
forall r (m :: * -> *) a.
StateT (AmbT r m r) (ContT r (StateT [r] m)) a -> AmbT r m a
AmbT (AmbT r m r -> StateT (AmbT r m r) (ContT r (StateT [r] m)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put AmbT r m r
old) AmbT r m () -> AmbT r m Any -> AmbT r m Any
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Bool -> AmbT r m Any
k Bool
False) AmbT r m Any -> AmbT r m r -> AmbT r m r
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AmbT r m r
forall a. HasCallStack => a
undefined)
             Bool -> AmbT r m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | Generate each element of the given list.
aMemberOf :: [b] -> AmbT r m b
aMemberOf :: [b] -> AmbT r m b
aMemberOf [] = AmbT r m b
forall (f :: * -> *) a. Alternative f => f a
empty
aMemberOf (b
x:[b]
xs) =  b -> AmbT r m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
x AmbT r m b -> AmbT r m b -> AmbT r m b
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [b] -> AmbT r m b
forall b r (m :: * -> *). [b] -> AmbT r m b
aMemberOf [b]
xs

-- | Generate each subset of any size from the given list.
aSubsetOf :: [AmbT r m a] -> AmbT r m [a]
aSubsetOf :: [AmbT r m a] -> AmbT r m [a]
aSubsetOf [] = [a] -> AmbT r m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
aSubsetOf (AmbT r m a
x:[AmbT r m a]
xs) = [AmbT r m a] -> AmbT r m [a]
forall r (m :: * -> *) a. [AmbT r m a] -> AmbT r m [a]
aSubsetOf [AmbT r m a]
xs AmbT r m [a] -> AmbT r m [a] -> AmbT r m [a]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (a -> [a] -> [a]) -> AmbT r m a -> AmbT r m [a] -> AmbT r m [a]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (:) AmbT r m a
x ([AmbT r m a] -> AmbT r m [a]
forall r (m :: * -> *) a. [AmbT r m a] -> AmbT r m [a]
aSubsetOf [AmbT r m a]
xs)

-- | Generate all numbers between the given bounds, inclusive.
anIntegerBetween :: (Monad m, Num b, Ord b) => b -> b -> AmbT r m b
anIntegerBetween :: b -> b -> AmbT r m b
anIntegerBetween b
i b
j | b
i b -> b -> Bool
forall a. Ord a => a -> a -> Bool
> b
j = AmbT r m b
forall (f :: * -> *) a. Alternative f => f a
empty
                     | Bool
otherwise = AmbT r m b -> AmbT r m b -> AmbT r m b
forall r (m :: * -> *) a. AmbT r m a -> AmbT r m a -> AmbT r m a
either' (b -> AmbT r m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
i) (b -> b -> AmbT r m b
forall (m :: * -> *) b r.
(Monad m, Num b, Ord b) =>
b -> b -> AmbT r m b
anIntegerBetween (b
i b -> b -> b
forall a. Num a => a -> a -> a
+ b
1) b
j) 

-- | Generate all splits of a list.
aSplitOf :: [a] -> AmbT r m ([a],[a])
aSplitOf :: [a] -> AmbT r m ([a], [a])
aSplitOf [a]
l = [a] -> [a] -> AmbT r m ([a], [a])
forall a r (m :: * -> *). [a] -> [a] -> AmbT r m ([a], [a])
loop [] [a]
l
    where loop :: [a] -> [a] -> AmbT r m ([a], [a])
loop [a]
x [] = ([a], [a]) -> AmbT r m ([a], [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
x,[])
          loop [a]
x y :: [a]
y@(a
y0:[a]
ys)  = AmbT r m ([a], [a]) -> AmbT r m ([a], [a]) -> AmbT r m ([a], [a])
forall r (m :: * -> *) a. AmbT r m a -> AmbT r m a -> AmbT r m a
either' (([a], [a]) -> AmbT r m ([a], [a])
forall (m :: * -> *) a. Monad m => a -> m a
return ([a]
x,[a]
y)) ([a] -> [a] -> AmbT r m ([a], [a])
loop ([a]
x [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
y0]) [a]
ys)

-- | Generate all permutations of a list.
aPermutationOf :: [a] -> AmbT r m [a]
aPermutationOf :: [a] -> AmbT r m [a]
aPermutationOf [] = [a] -> AmbT r m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
aPermutationOf (a
l0:[a]
ls) = do ([a]
s1,[a]
s2) <- ([a] -> AmbT r m [a]
forall a r (m :: * -> *). [a] -> AmbT r m [a]
aPermutationOf [a]
ls AmbT r m [a] -> ([a] -> AmbT r m ([a], [a])) -> AmbT r m ([a], [a])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [a] -> AmbT r m ([a], [a])
forall a r (m :: * -> *). [a] -> AmbT r m ([a], [a])
aSplitOf)
                            [a] -> AmbT r m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> AmbT r m [a]) -> [a] -> AmbT r m [a]
forall a b. (a -> b) -> a -> b
$ [a]
s1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ (a
l0a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
s2)

-- | Generate all partitions of this list.
aPartitionOf :: (Eq t, Monad m) => [t] -> AmbT r m [[t]]
aPartitionOf :: [t] -> AmbT r m [[t]]
aPartitionOf [] = [[t]] -> AmbT r m [[t]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
aPartitionOf (t
x:[t]
xs) = do [[t]]
y <- [t] -> AmbT r m [[t]]
forall t (m :: * -> *) r. (Eq t, Monad m) => [t] -> AmbT r m [[t]]
aPartitionOf [t]
xs
                         AmbT r m [[t]] -> AmbT r m [[t]] -> AmbT r m [[t]]
forall r (m :: * -> *) a. AmbT r m a -> AmbT r m a -> AmbT r m a
either' ([[t]] -> AmbT r m [[t]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([t
x][t] -> [[t]] -> [[t]]
forall a. a -> [a] -> [a]
:[[t]]
y))
                                 (do [t]
z <- [[t]] -> AmbT r m [t]
forall b r (m :: * -> *). [b] -> AmbT r m b
aMemberOf [[t]]
y
                                     [[t]] -> AmbT r m [[t]]
forall (m :: * -> *) a. Monad m => a -> m a
return ((t
xt -> [t] -> [t]
forall a. a -> [a] -> [a]
:[t]
z) [t] -> [[t]] -> [[t]]
forall a. a -> [a] -> [a]
: ([t] -> Bool) -> [[t]] -> [[t]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([t]
z [t] -> [t] -> Bool
forall a. Eq a => a -> a -> Bool
/=) [[t]]
y))

-- | Generate all partitions of a given size of this list.
aPartitionOfSize :: (Eq a, Monad m) => Int -> [a] -> AmbT r m [[a]]
aPartitionOfSize :: Int -> [a] -> AmbT r m [[a]]
aPartitionOfSize Int
0 [a]
_ = [Char] -> AmbT r m [[a]]
forall a. HasCallStack => [Char] -> a
error [Char]
"Can't create a partition of size 0"
aPartitionOfSize Int
k [a]
l | [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k = AmbT r m [[a]]
forall (f :: * -> *) a. Alternative f => f a
empty
                     | Bool
otherwise = [a] -> AmbT r m [[a]]
forall a r (m :: * -> *). Eq a => [a] -> AmbT r m [[a]]
loop [a]
l
    where loop :: [a] -> AmbT r m [[a]]
loop x :: [a]
x@(a
x0:[a]
xs) | [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k = [[a]] -> AmbT r m [[a]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[a]] -> AmbT r m [[a]]) -> [[a]] -> AmbT r m [[a]]
forall a b. (a -> b) -> a -> b
$ (a -> [a]) -> [a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[]) [a]
x
                         | Bool
otherwise = do [[a]]
y <- [a] -> AmbT r m [[a]]
loop [a]
xs
                                          [a]
z <- [[a]] -> AmbT r m [a]
forall b r (m :: * -> *). [b] -> AmbT r m b
aMemberOf [[a]]
y
                                          [[a]] -> AmbT r m [[a]]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
x0a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
z)[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:([a] -> Bool) -> [[a]] -> [[a]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([a]
z [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
/=) [[a]]
y)
          loop [] = AmbT r m [[a]]
forall (f :: * -> *) a. Alternative f => f a
empty

-- | Just for fun. This is McCarthy's @amb@ operator and is a synonym
-- for @aMemberOf@.
amb :: [b] -> AmbT r m b
amb :: [b] -> AmbT r m b
amb = [b] -> AmbT r m b
forall b r (m :: * -> *). [b] -> AmbT r m b
aMemberOf