{-# LANGUAGE Trustworthy #-} -- GeneralizedNewtypeDeriving
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Test.SmallCheck.SeriesMonad where

import Control.Applicative
import Control.Monad
import Control.Monad.Logic
import Control.Monad.Reader
import Control.Arrow

-- | Maximum depth of generated test values.
--
-- For data values, it is the depth of nested constructor applications.
--
-- For functional values, it is both the depth of nested case analysis
-- and the depth of results.
type Depth = Int

-- | 'Series' is a `MonadLogic` action that enumerates values of a certain
-- type, up to some depth.
--
-- The depth bound is tracked in the 'SC' monad and can be extracted using
-- 'getDepth' and changed using 'localDepth'.
--
-- To manipulate series at the lowest level you can use its 'Monad',
-- 'MonadPlus' and 'MonadLogic' instances. This module provides some
-- higher-level combinators which simplify creating series.
--
-- A proper 'Series' should be monotonic with respect to the depth — i.e.
-- @localDepth (+1) s@ should emit all the values that @s@ emits (and
-- possibly some more).
--
-- It is also desirable that values of smaller depth come before the values
-- of greater depth.
newtype Series m a = Series (ReaderT Depth (LogicT m) a)
  deriving
    ( a -> Series m b -> Series m a
(a -> b) -> Series m a -> Series m b
(forall a b. (a -> b) -> Series m a -> Series m b)
-> (forall a b. a -> Series m b -> Series m a)
-> Functor (Series m)
forall a b. a -> Series m b -> Series m a
forall a b. (a -> b) -> Series m a -> Series 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 -> Series m b -> Series m a
forall (m :: * -> *) a b. (a -> b) -> Series m a -> Series m b
<$ :: a -> Series m b -> Series m a
$c<$ :: forall (m :: * -> *) a b. a -> Series m b -> Series m a
fmap :: (a -> b) -> Series m a -> Series m b
$cfmap :: forall (m :: * -> *) a b. (a -> b) -> Series m a -> Series m b
Functor
    , Applicative (Series m)
a -> Series m a
Applicative (Series m) =>
(forall a b. Series m a -> (a -> Series m b) -> Series m b)
-> (forall a b. Series m a -> Series m b -> Series m b)
-> (forall a. a -> Series m a)
-> Monad (Series m)
Series m a -> (a -> Series m b) -> Series m b
Series m a -> Series m b -> Series m b
forall a. a -> Series m a
forall a b. Series m a -> Series m b -> Series m b
forall a b. Series m a -> (a -> Series m b) -> Series m b
forall (m :: * -> *). Applicative (Series m)
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (m :: * -> *) a. a -> Series m a
forall (m :: * -> *) a b. Series m a -> Series m b -> Series m b
forall (m :: * -> *) a b.
Series m a -> (a -> Series m b) -> Series m b
return :: a -> Series m a
$creturn :: forall (m :: * -> *) a. a -> Series m a
>> :: Series m a -> Series m b -> Series m b
$c>> :: forall (m :: * -> *) a b. Series m a -> Series m b -> Series m b
>>= :: Series m a -> (a -> Series m b) -> Series m b
$c>>= :: forall (m :: * -> *) a b.
Series m a -> (a -> Series m b) -> Series m b
$cp1Monad :: forall (m :: * -> *). Applicative (Series m)
Monad
    , Functor (Series m)
a -> Series m a
Functor (Series m) =>
(forall a. a -> Series m a)
-> (forall a b. Series m (a -> b) -> Series m a -> Series m b)
-> (forall a b c.
    (a -> b -> c) -> Series m a -> Series m b -> Series m c)
-> (forall a b. Series m a -> Series m b -> Series m b)
-> (forall a b. Series m a -> Series m b -> Series m a)
-> Applicative (Series m)
Series m a -> Series m b -> Series m b
Series m a -> Series m b -> Series m a
Series m (a -> b) -> Series m a -> Series m b
(a -> b -> c) -> Series m a -> Series m b -> Series m c
forall a. a -> Series m a
forall a b. Series m a -> Series m b -> Series m a
forall a b. Series m a -> Series m b -> Series m b
forall a b. Series m (a -> b) -> Series m a -> Series m b
forall a b c.
(a -> b -> c) -> Series m a -> Series m b -> Series m c
forall (m :: * -> *). Functor (Series m)
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *) a. a -> Series m a
forall (m :: * -> *) a b. Series m a -> Series m b -> Series m a
forall (m :: * -> *) a b. Series m a -> Series m b -> Series m b
forall (m :: * -> *) a b.
Series m (a -> b) -> Series m a -> Series m b
forall (m :: * -> *) a b c.
(a -> b -> c) -> Series m a -> Series m b -> Series m c
<* :: Series m a -> Series m b -> Series m a
$c<* :: forall (m :: * -> *) a b. Series m a -> Series m b -> Series m a
*> :: Series m a -> Series m b -> Series m b
$c*> :: forall (m :: * -> *) a b. Series m a -> Series m b -> Series m b
liftA2 :: (a -> b -> c) -> Series m a -> Series m b -> Series m c
$cliftA2 :: forall (m :: * -> *) a b c.
(a -> b -> c) -> Series m a -> Series m b -> Series m c
<*> :: Series m (a -> b) -> Series m a -> Series m b
$c<*> :: forall (m :: * -> *) a b.
Series m (a -> b) -> Series m a -> Series m b
pure :: a -> Series m a
$cpure :: forall (m :: * -> *) a. a -> Series m a
$cp1Applicative :: forall (m :: * -> *). Functor (Series m)
Applicative
    , Monad (Series m)
Alternative (Series m)
Series m a
(Alternative (Series m), Monad (Series m)) =>
(forall a. Series m a)
-> (forall a. Series m a -> Series m a -> Series m a)
-> MonadPlus (Series m)
Series m a -> Series m a -> Series m a
forall a. Series m a
forall a. Series m a -> Series m a -> Series m a
forall (m :: * -> *). Monad (Series m)
forall (m :: * -> *). Alternative (Series m)
forall (m :: * -> *).
(Alternative m, Monad m) =>
(forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
forall (m :: * -> *) a. Series m a
forall (m :: * -> *) a. Series m a -> Series m a -> Series m a
mplus :: Series m a -> Series m a -> Series m a
$cmplus :: forall (m :: * -> *) a. Series m a -> Series m a -> Series m a
mzero :: Series m a
$cmzero :: forall (m :: * -> *) a. Series m a
$cp2MonadPlus :: forall (m :: * -> *). Monad (Series m)
$cp1MonadPlus :: forall (m :: * -> *). Alternative (Series m)
MonadPlus
    , Applicative (Series m)
Series m a
Applicative (Series m) =>
(forall a. Series m a)
-> (forall a. Series m a -> Series m a -> Series m a)
-> (forall a. Series m a -> Series m [a])
-> (forall a. Series m a -> Series m [a])
-> Alternative (Series m)
Series m a -> Series m a -> Series m a
Series m a -> Series m [a]
Series m a -> Series m [a]
forall a. Series m a
forall a. Series m a -> Series m [a]
forall a. Series m a -> Series m a -> Series m a
forall (m :: * -> *). Applicative (Series m)
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall (m :: * -> *) a. Series m a
forall (m :: * -> *) a. Series m a -> Series m [a]
forall (m :: * -> *) a. Series m a -> Series m a -> Series m a
many :: Series m a -> Series m [a]
$cmany :: forall (m :: * -> *) a. Series m a -> Series m [a]
some :: Series m a -> Series m [a]
$csome :: forall (m :: * -> *) a. Series m a -> Series m [a]
<|> :: Series m a -> Series m a -> Series m a
$c<|> :: forall (m :: * -> *) a. Series m a -> Series m a -> Series m a
empty :: Series m a
$cempty :: forall (m :: * -> *) a. Series m a
$cp1Alternative :: forall (m :: * -> *). Applicative (Series m)
Alternative
    )

-- This instance is written manually. Using the GND for it is not safe. 
instance Monad m => MonadLogic (Series m) where
  msplit :: Series m a -> Series m (Maybe (a, Series m a))
msplit (Series a :: ReaderT Depth (LogicT m) a
a) = ReaderT Depth (LogicT m) (Maybe (a, Series m a))
-> Series m (Maybe (a, Series m a))
forall (m :: * -> *) a. ReaderT Depth (LogicT m) a -> Series m a
Series (ReaderT Depth (LogicT m) (Maybe (a, Series m a))
 -> Series m (Maybe (a, Series m a)))
-> ReaderT Depth (LogicT m) (Maybe (a, Series m a))
-> Series m (Maybe (a, Series m a))
forall a b. (a -> b) -> a -> b
$ (Maybe (a, ReaderT Depth (LogicT m) a) -> Maybe (a, Series m a))
-> ReaderT Depth (LogicT m) (Maybe (a, ReaderT Depth (LogicT m) a))
-> ReaderT Depth (LogicT m) (Maybe (a, Series m a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((a, ReaderT Depth (LogicT m) a) -> (a, Series m a))
-> Maybe (a, ReaderT Depth (LogicT m) a) -> Maybe (a, Series m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((a, ReaderT Depth (LogicT m) a) -> (a, Series m a))
 -> Maybe (a, ReaderT Depth (LogicT m) a) -> Maybe (a, Series m a))
-> ((a, ReaderT Depth (LogicT m) a) -> (a, Series m a))
-> Maybe (a, ReaderT Depth (LogicT m) a)
-> Maybe (a, Series m a)
forall a b. (a -> b) -> a -> b
$ (ReaderT Depth (LogicT m) a -> Series m a)
-> (a, ReaderT Depth (LogicT m) a) -> (a, Series m a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ReaderT Depth (LogicT m) a -> Series m a
forall (m :: * -> *) a. ReaderT Depth (LogicT m) a -> Series m a
Series) (ReaderT Depth (LogicT m) (Maybe (a, ReaderT Depth (LogicT m) a))
 -> ReaderT Depth (LogicT m) (Maybe (a, Series m a)))
-> ReaderT Depth (LogicT m) (Maybe (a, ReaderT Depth (LogicT m) a))
-> ReaderT Depth (LogicT m) (Maybe (a, Series m a))
forall a b. (a -> b) -> a -> b
$ ReaderT Depth (LogicT m) a
-> ReaderT Depth (LogicT m) (Maybe (a, ReaderT Depth (LogicT m) a))
forall (m :: * -> *) a. MonadLogic m => m a -> m (Maybe (a, m a))
msplit ReaderT Depth (LogicT m) a
a

instance MonadTrans Series where
  lift :: m a -> Series m a
lift a :: m a
a = ReaderT Depth (LogicT m) a -> Series m a
forall (m :: * -> *) a. ReaderT Depth (LogicT m) a -> Series m a
Series (ReaderT Depth (LogicT m) a -> Series m a)
-> ReaderT Depth (LogicT m) a -> Series m a
forall a b. (a -> b) -> a -> b
$ LogicT m a -> ReaderT Depth (LogicT m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LogicT m a -> ReaderT Depth (LogicT m) a)
-> (m a -> LogicT m a) -> m a -> ReaderT Depth (LogicT m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> LogicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> ReaderT Depth (LogicT m) a)
-> m a -> ReaderT Depth (LogicT m) a
forall a b. (a -> b) -> a -> b
$ m a
a

runSeries :: Depth -> Series m a -> LogicT m a
runSeries :: Depth -> Series m a -> LogicT m a
runSeries d :: Depth
d (Series a :: ReaderT Depth (LogicT m) a
a) = ReaderT Depth (LogicT m) a -> Depth -> LogicT m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Depth (LogicT m) a
a Depth
d