{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
module Test.Verification
(
assuming
, (==>)
, property
, chooseBool
, chooseInt
, chooseInteger
, Gen
, getSize
, Verifiable(..)
, Property(..)
, Assumption(..)
, GenEnv(..)
, toNativeProperty
)
where
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Reader
data Property = BoolProperty Bool
| AssumptionProp Assumption
deriving Int -> Property -> ShowS
[Property] -> ShowS
Property -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Property] -> ShowS
$cshowList :: [Property] -> ShowS
show :: Property -> String
$cshow :: Property -> String
showsPrec :: Int -> Property -> ShowS
$cshowsPrec :: Int -> Property -> ShowS
Show
class Verifiable prop where
verifying :: prop -> Property
instance Verifiable Bool where verifying :: Bool -> Property
verifying = Bool -> Property
BoolProperty
property :: Bool -> Property
property :: Bool -> Property
property = forall prop. Verifiable prop => prop -> Property
verifying
data Assumption = Assuming { Assumption -> Bool
preCondition :: Bool,
Assumption -> Property
assumedProp :: Property }
deriving Int -> Assumption -> ShowS
[Assumption] -> ShowS
Assumption -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Assumption] -> ShowS
$cshowList :: [Assumption] -> ShowS
show :: Assumption -> String
$cshow :: Assumption -> String
showsPrec :: Int -> Assumption -> ShowS
$cshowsPrec :: Int -> Assumption -> ShowS
Show
assuming :: Verifiable t => Bool -> t -> Property
assuming :: forall t. Verifiable t => Bool -> t -> Property
assuming Bool
precond t
test = Assumption -> Property
AssumptionProp forall a b. (a -> b) -> a -> b
$ Bool -> Property -> Assumption
Assuming Bool
precond forall a b. (a -> b) -> a -> b
$ forall prop. Verifiable prop => prop -> Property
verifying t
test
(==>) :: Verifiable t => Bool -> t -> Property
==> :: forall t. Verifiable t => Bool -> t -> Property
(==>) = forall t. Verifiable t => Bool -> t -> Property
assuming
infixr 0 ==>
instance Verifiable Property where
verifying :: Property -> Property
verifying = forall a. a -> a
id
data GenEnv m = GenEnv { forall (m :: Type -> Type). GenEnv m -> m Bool
genChooseBool :: m Bool
, forall (m :: Type -> Type). GenEnv m -> (Int, Int) -> m Int
genChooseInt :: (Int, Int) -> m Int
, forall (m :: Type -> Type).
GenEnv m -> (Integer, Integer) -> m Integer
genChooseInteger :: (Integer, Integer) -> m Integer
, forall (m :: Type -> Type). GenEnv m -> m Int
genGetSize :: m Int
}
newtype Gen a =
Gen { forall a.
Gen a
-> forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
unGen :: forall m. Monad m => ReaderT (GenEnv m) m a }
instance Functor Gen where
fmap :: forall a b. (a -> b) -> Gen a -> Gen b
fmap a -> b
f (Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
m) = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
m)
instance Applicative Gen where
pure :: forall a. a -> Gen a
pure a
x = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (f :: Type -> Type) a. Applicative f => a -> f a
pure a
x)
(Gen forall (m :: Type -> Type).
Monad m =>
ReaderT (GenEnv m) m (a -> b)
f) <*> :: forall a b. Gen (a -> b) -> Gen a -> Gen b
<*> (Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
x) = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (m :: Type -> Type).
Monad m =>
ReaderT (GenEnv m) m (a -> b)
f forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
x)
instance Monad Gen where
Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
x >>= :: forall a b. Gen a -> (a -> Gen b) -> Gen b
>>= a -> Gen b
f = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
x forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x' -> forall a.
Gen a
-> forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a
unGen (a -> Gen b
f a
x'))
chooseBool :: Gen Bool
chooseBool :: Gen Bool
chooseBool = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (m :: Type -> Type) r a.
Monad m =>
(r -> a) -> ReaderT r m a
asks forall (m :: Type -> Type). GenEnv m -> m Bool
genChooseBool forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift)
chooseInt :: (Int, Int) -> Gen Int
chooseInt :: (Int, Int) -> Gen Int
chooseInt (Int, Int)
r = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (m :: Type -> Type) r a.
Monad m =>
(r -> a) -> ReaderT r m a
asks forall (m :: Type -> Type). GenEnv m -> (Int, Int) -> m Int
genChooseInt forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ (Int, Int)
r))
chooseInteger :: (Integer, Integer) -> Gen Integer
chooseInteger :: (Integer, Integer) -> Gen Integer
chooseInteger (Integer, Integer)
r = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (m :: Type -> Type) r a.
Monad m =>
(r -> a) -> ReaderT r m a
asks forall (m :: Type -> Type).
GenEnv m -> (Integer, Integer) -> m Integer
genChooseInteger forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> a -> b
$ (Integer, Integer)
r))
getSize :: Gen Int
getSize :: Gen Int
getSize = forall a.
(forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m a)
-> Gen a
Gen (forall (m :: Type -> Type) r a.
Monad m =>
(r -> a) -> ReaderT r m a
asks forall (m :: Type -> Type). GenEnv m -> m Int
genGetSize forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift)
toNativeProperty :: Monad m => GenEnv m -> Gen b -> m b
toNativeProperty :: forall (m :: Type -> Type) b. Monad m => GenEnv m -> Gen b -> m b
toNativeProperty GenEnv m
gens (Gen forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b
gprops) = forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT forall (m :: Type -> Type). Monad m => ReaderT (GenEnv m) m b
gprops GenEnv m
gens