{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Empty
( tests
, gen0
, test
) where

import qualified Control.Carrier.Empty.Church as C.Church
import qualified Control.Carrier.Empty.Maybe as C.Maybe
import qualified Control.Monad.Trans.Maybe as T.Maybe
import           Control.Effect.Empty
import           Data.Maybe (maybeToList)
import           Gen
import qualified Monad
import qualified MonadFix
import           Test.Tasty
import           Test.Tasty.Hedgehog

tests :: TestTree
tests = testGroup "Empty"
  [ testGroup "EmptyC (Church)" $
    [ testMonad
    , testMonadFix
    , testEmpty
    ] >>= ($ runL (fmap maybeToList . C.Church.runEmpty (pure Nothing) (pure . Just)))
  , testGroup "EmptyC (Maybe)" $
    [ testMonad
    , testMonadFix
    , testEmpty
    ] >>= ($ runL (fmap maybeToList . C.Maybe.runEmpty))
  , testGroup "MaybeT" $ testEmpty (runL (fmap maybeToList . T.Maybe.runMaybeT))
  , testGroup "Maybe"  $ testEmpty (runL (pure . maybeToList))
  ] where
  testMonad    run = Monad.test    (m gen0 (\ _ _ -> [])) a b c initial run
  testMonadFix run = MonadFix.test (m gen0 (\ _ _ -> [])) a b   initial run
  testEmpty    run = Empty.test    (m gen0 (\ _ _ -> [])) a b   initial run
  initial = identity <*> unit


gen0 :: Has Empty sig m => GenTerm a -> [GenTerm (m a)]
gen0 _ = [ label "empty" empty ]


test
  :: forall a b m f sig
  .  (Has Empty sig m, Arg a, Eq b, Show a, Show b, Vary a, Functor f)
  => GenM m
  -> GenTerm a
  -> GenTerm b
  -> GenTerm (f ())
  -> Run f [] m
  -> [TestTree]
test m _ b i (Run runEmpty) =
  [ testProperty "empty annihilates >>=" . forall (i :. fn @a (m b) :. Nil) $
    \ i k -> runEmpty ((empty >>= k) <$ i) === runEmpty (empty <$ i)
  ]