{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE Safe #-}
#endif

module Test.SmallCheck.SeriesMonad where

import Control.Applicative (Applicative(..), Alternative(..), (<$>))
import Control.Monad (MonadPlus(..))
import Control.Monad.Logic (MonadLogic(..), LogicT)
import Control.Monad.Reader (MonadTrans(..), ReaderT, runReaderT)
import Control.Arrow (second)

-- | 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 'Series' monad and can be extracted using
-- 'Test.SmallCheck.Series.getDepth' and changed using 'Test.SmallCheck.Series.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.
-- 'Test.SmallCheck.Series.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)

instance Functor (Series m) where
  fmap :: (a -> b) -> Series m a -> Series m b
fmap a -> b
f (Series ReaderT Depth (LogicT m) a
x) = ReaderT Depth (LogicT m) b -> Series m b
forall (m :: * -> *) a. ReaderT Depth (LogicT m) a -> Series m a
Series ((a -> b)
-> ReaderT Depth (LogicT m) a -> ReaderT Depth (LogicT m) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ReaderT Depth (LogicT m) a
x)

instance Monad (Series m) where
  Series ReaderT Depth (LogicT m) a
x >>= :: Series m a -> (a -> Series m b) -> Series m b
>>= a -> Series m b
f = ReaderT Depth (LogicT m) b -> Series m b
forall (m :: * -> *) a. ReaderT Depth (LogicT m) a -> Series m a
Series (ReaderT Depth (LogicT m) a
x ReaderT Depth (LogicT m) a
-> (a -> ReaderT Depth (LogicT m) b) -> ReaderT Depth (LogicT m) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Series m b -> ReaderT Depth (LogicT m) b
forall (m :: * -> *) a. Series m a -> ReaderT Depth (LogicT m) a
unSeries (Series m b -> ReaderT Depth (LogicT m) b)
-> (a -> Series m b) -> a -> ReaderT Depth (LogicT m) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Series m b
f)
    where
      unSeries :: Series m a -> ReaderT Depth (LogicT m) a
unSeries (Series ReaderT Depth (LogicT m) a
y) = ReaderT Depth (LogicT m) a
y
  return :: a -> Series m a
return = a -> Series m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Applicative (Series m) where
  pure :: a -> Series m a
pure = 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)
-> (a -> ReaderT Depth (LogicT m) a) -> a -> Series m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ReaderT Depth (LogicT m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Series ReaderT Depth (LogicT m) (a -> b)
x <*> :: Series m (a -> b) -> Series m a -> Series m b
<*> Series ReaderT Depth (LogicT m) a
y = ReaderT Depth (LogicT m) b -> Series m b
forall (m :: * -> *) a. ReaderT Depth (LogicT m) a -> Series m a
Series (ReaderT Depth (LogicT m) (a -> b)
x ReaderT Depth (LogicT m) (a -> b)
-> ReaderT Depth (LogicT m) a -> ReaderT Depth (LogicT m) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT Depth (LogicT m) a
y)

instance MonadPlus (Series m) where
  mzero :: Series m a
mzero = Series m a
forall (f :: * -> *) a. Alternative f => f a
empty
  mplus :: Series m a -> Series m a -> Series m a
mplus = Series m a -> Series m a -> Series m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)

instance Alternative (Series m) where
  empty :: Series m a
empty = 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
forall (f :: * -> *) a. Alternative f => f a
empty
  Series ReaderT Depth (LogicT m) a
x <|> :: Series m a -> Series m a -> Series m a
<|> Series ReaderT Depth (LogicT m) a
y = 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
x ReaderT Depth (LogicT m) a
-> ReaderT Depth (LogicT m) a -> ReaderT Depth (LogicT m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ReaderT Depth (LogicT m) a
y)

-- 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 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 (((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 ((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) (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
<$> 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 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 Depth
d (Series 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