{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test.Monad.Control.Checkers where
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Control (MonadTransControl, MonadBaseControl)
import Data.Functor.Identity
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import Data.Typeable (Typeable, typeRep)
import GHC.TypeLits
import Test.QuickCheck (Property, pattern Fn)
import Test.QuickCheck.HigherOrder
import Test.Monad.Instances ()
import Test.Monad.Control
import Test.SmallList
type family Replicate (n :: Nat) (xs :: [k]) :: [[k]] where
Replicate 0 _ = '[ '[] ]
Replicate n xs = Extend' xs (Replicate (n - 1) xs)
type Extend' xs ys = ys ++ Extend xs ys
type family Extend (xs :: [k]) (ys :: [[k]]) :: [[k]] where
Extend '[] ys = '[]
Extend (x ': xs) ys = MapCons x ys ++ Extend xs ys
type family MapCons (x :: k) (ys :: [[k]]) :: [[k]] where
MapCons x '[] = '[]
MapCons x (y ': ys) = (x ': y) ': MapCons x ys
type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': xs ++ ys
class TestControl (xs :: [[(Type -> Type) -> (Type -> Type)]]) (m :: Type -> Type) where
testControl :: [(String, [(String, Property)])]
instance TestControl '[] m where
testControl = []
instance
( TestTransControl ts m, TestBaseControl ts m, TestControl tss m
, Typeable (StackT ts m)
)
=> TestControl (ts ': tss) m where
testControl =
( show (typeRep (Proxy @(StackT ts m)))
, testTransControl @ts @m ++ testBaseControl @ts @m
) : testControl @tss @m
type family StackT (ts :: [(Type -> Type) -> (Type -> Type)]) (m :: Type -> Type) :: Type -> Type where
StackT '[] m = m
StackT (t ': ts) m = t (StackT ts m)
type Stack ts = StackT ts Identity
class TestTransControl (ts :: [(Type -> Type) -> (Type -> Type)]) (m :: Type -> Type) where
testTransControl :: [(String, Property)]
instance TestTransControl '[] m where
testTransControl = []
instance
( MonadTransControl t, Monad (StackT (t ': ts) m), Monad (StackT ts m)
, Constructible (StackT (t ': ts) m Int), Constructible (StackT ts m Int)
, TestEq (StackT (t ': ts) m Int))
=> TestTransControl (t ': ts) m where
testTransControl =
[ ok "liftWith-return" (liftWith_return @t @n @Int)
, ok "liftWith-bind" (\m (Fn k) -> liftWith_bind @t @n @Int @Int m k)
, ok "liftWith-lift" (liftWith_lift @t @n @Int)
, ok "liftWith-restoreT" (liftWith_restoreT @t @n @Int)
] :: forall n. (n ~ StackT ts m) => [(String, Property)]
{-# NOINLINE testTransControl #-}
class TestBaseControl (ts :: [(Type -> Type) -> (Type -> Type)]) (m :: Type -> Type) where
testBaseControl :: [(String, Property)]
instance
( MonadBaseControl m (StackT ts m)
, Constructible (StackT ts m Int), Constructible (m Int)
, TestEq (StackT ts m Int))
=> TestBaseControl ts m where
testBaseControl =
[ ok "liftBaseWith-liftBase" (liftBaseWith_liftBase @n @Int)
, ok "liftBaseWith-restoreM" (liftBaseWith_restoreM @n @Int)
] :: forall n. (n ~ StackT ts m) => [(String, Property)]
{-# NOINLINE testBaseControl #-}
type StdTrans = '[ ReaderT Int, StateT Int, ExceptT Int ]
type StdStacks = Replicate 2 StdTrans
checkControl :: [(String, [(String, Property)])]
checkControl =
testControl @StdStacks @Identity ++
testControl @StdStacks @SmallList