{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE UndecidableInstances  #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE QuantifiedConstraints #-}
#endif

{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cat (tests) where

import           Prelude hiding ((.), id)
import           Control.Category
import           Data.Function (on)
#if __GLASGOW_HASKELL__ < 804
import           Data.Monoid (Monoid (..))
import           Data.Semigroup (Semigroup (..))
#endif
import           Text.Show.Functions ()
import           Numeric.Natural (Natural)

import           Control.Algebra.Free2
import           Control.Category.Free

import           Test.QuickCheck
import           Test.Tasty (TestTree, testGroup)
import           Test.Tasty.QuickCheck (testProperty)

tests :: TestTree
tests =
  testGroup "Control.Category.Free"
  [ testProperty "Queue" prop_Queue
  , testProperty "C"     prop_C
  , testGroup "Category laws"
    [ testProperty "ListTr id"            prop_id_ListTr
    , testProperty "ListTr associativity" prop_associativity_ListTr
    , testProperty "Queue id"            prop_id_Queue
    , testProperty "Queue associativity" prop_associativity_Queue
    , testProperty "C id"                 prop_id_C
    , testProperty "C associativity"      prop_associativity_C
    ]
  , testGroup "foldFree2 and foldMap"
    [ testProperty "foldFree ListTr" prop_foldListTr
    , testProperty "foldFree Queue"  prop_foldQueue
    , testProperty "foldFree C"      prop_foldC
    ]
  ]


data Tr a b where
    -- Num transition
    NumTr       :: Num a => (a -> a) -> Tr a a
    FromInteger :: Num b => Tr Integer b

    -- Integral transition
    ToInteger  :: Integral a => Tr a Integer


interpretTr :: Tr a b -> a -> b
interpretTr (NumTr f)   = f
interpretTr FromInteger = fromInteger
interpretTr ToInteger   = toInteger


instance (Show a, Show b) => Show (Tr a b) where
    show (NumTr f)   = "NumTr " ++ show f
    show FromInteger = "FromInteger"
    show ToInteger   = "ToInteger"


data SomeNumTr f a where
    SomeNumTr :: Num a
              => f Tr a a
              -> SomeNumTr f a

instance Show (f Tr a a) => Show (SomeNumTr f a) where
      show (SomeNumTr f) = "SomeNumTr " ++ show f


data SomeIntegralTr f a where
    SomeIntegralTr :: Integral a
                   => f Tr a a
                   -> SomeIntegralTr f a

instance Show (f Tr a a) => Show (SomeIntegralTr f a) where
      show (SomeIntegralTr f) = "SomeIntegralTr " ++ show f


-- A 'fromIntegral' transition in any free category @f@.
fromIntegralTr :: ( Integral a
                  , Num b
                  , Category     (f Tr)
                  , AlgebraType0 f Tr
                  , FreeAlgebra2 f
                  ) => f Tr a b
fromIntegralTr = liftFree2 FromInteger . liftFree2 ToInteger


data Sing a where
    SInt     :: Sing Int
    SInteger :: Sing Integer
    SNatural :: Sing Natural

instance Show (Sing a) where
    show SInt     = "SInt"
    show SInteger = "SInteger"
    show SNatural = "SNatural"

data AnySing where
    AnySing :: Eq a => Sing a -> AnySing

instance Eq AnySing where
    AnySing SInt     == AnySing SInt     = True
    AnySing SInteger == AnySing SInteger = True
    AnySing SNatural == AnySing SNatural = True
    _                == _                = False

instance Show AnySing where
    show (AnySing sing) = show sing

instance Arbitrary AnySing where
    arbitrary = oneof
      [ pure $ AnySing SInt
      , pure $ AnySing SInteger
      , pure $ AnySing SNatural
      ]


instance Arbitrary Natural where
    arbitrary =
      fromIntegral . getPositive <$> (arbitrary :: Gen (Positive Integer))

instance CoArbitrary Natural where
    coarbitrary a = variant (fromIntegral a :: Int)

data AnyListTr b where
    AnyListTr :: Eq c => ListTr Tr b c -> Sing c -> AnyListTr b


genNextTr :: Sing b
          -> Gen (AnyListTr b)
genNextTr b = do
    AnySing c <- arbitrary
    case (b, c) of
      (SInt, SInt) ->
        (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
      (SInteger, SInteger) ->
        (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary
      (SNatural, SNatural) ->
        (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary

      (SInt, SInteger) ->
        pure $ AnyListTr fromIntegralTr c
      (SInt, SNatural) ->
        pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c
      (SInteger, SInt) ->
        pure $ AnyListTr fromIntegralTr c
      (SNatural, SInt) ->
        pure $ AnyListTr fromIntegralTr c
      (SNatural, SInteger) ->
        pure $ AnyListTr fromIntegralTr c
      (SInteger, SNatural) ->
        pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c


data ArbListTr where
    ArbListTr :: Eq b => ListTr Tr a b -> Sing a -> Sing b -> ArbListTr

#if __GLASGOW_HASKELL__ >= 806
instance (forall x y. Show (Tr x y)) => Show ArbListTr where
    show (ArbListTr listTr a b) =
         "ArbListTr "
      ++ show a
      ++ " -> "
      ++ show b
      ++ " "
      ++ show listTr
#else
instance Show ArbListTr where
    show (ArbListTr _listTr a b) =
         "ArbListTr "
      ++ show a
      ++ " -> "
      ++ show b
#endif

instance Arbitrary ArbListTr where
    arbitrary = sized $ \n -> do
        k <- choose (0, n)
        AnySing a <- arbitrary
        go k a (AnyListTr NilTr a)
      where
        go 0 a (AnyListTr ab b) = pure $ ArbListTr ab a b
        go n a (AnyListTr ab b) = do
          AnyListTr bc c <- genNextTr b
          -- (.) can be used as (++) for ListTr
          go (n - 1) a $ AnyListTr (bc . ab) c


--
-- test 'Cat' and 'C' treating 'ListTr' as a model to compare to.
--
prop_Queue, prop_C
    :: Blind ArbListTr -> Bool


prop_Queue (Blind (ArbListTr listTr SInt _)) =
      foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
    ==
      foldNatFree2 interpretTr listTr 0
prop_Queue (Blind (ArbListTr listTr SInteger _)) =
      foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
    ==
      foldNatFree2 interpretTr listTr 0
prop_Queue (Blind (ArbListTr listTr SNatural _)) =
      foldNatFree2 interpretTr (hoistFreeH2 @_ @Queue listTr) 0
    ==
      foldNatFree2 interpretTr listTr 0


prop_C (Blind (ArbListTr listTr SInt _)) =
      foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
    ==
      foldNatFree2 interpretTr listTr 0
prop_C (Blind (ArbListTr listTr SInteger _)) =
      foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
    ==
      foldNatFree2 interpretTr listTr 0
prop_C (Blind (ArbListTr listTr SNatural _)) =
      foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0
    ==
      foldNatFree2 interpretTr listTr 0

--
-- Test Category Laws
-- @
--  f . id == f == id . f
--  f . g . h == (f . g) . h
-- @
--

prop_id :: Category c
        => (c a b -> c a b -> Bool)
        -> c a b
        -> Bool
prop_id eqCat f = eqCat (f . id) f && eqCat (id . f) f

prop_associativity :: Category c
                   => (c x w -> c x w -> Bool)
                   -> c z w -> c y z -> c x y
                   -> Bool
prop_associativity eqCat f g h =
    (f . g . h) `eqCat` ((f . g) . h)


-- | Integers form commutative monoid, and thus a category (a groupoid to be
-- precise) with a single object.
--
data IntCat (a :: ()) (b :: ()) where
     IntCat :: Int -> IntCat a a

instance Show (IntCat a b) where
    show (IntCat i) = "IntCat " ++ show i

instance Eq (IntCat a b) where
    IntCat i  == IntCat j = i == j

instance Category IntCat where
    id = IntCat 0
    IntCat a . IntCat b = IntCat (a + b)

instance Semigroup (IntCat '() '()) where
    IntCat a <> IntCat b = IntCat (a + b)

instance Monoid (IntCat '() '()) where
    mempty = IntCat 0
#if __GLASGOW_HASKELL__ < 804
    mappend = (<>)
#endif

instance Arbitrary (IntCat '() '()) where
    arbitrary = IntCat <$> arbitrary

fromList :: forall k (a :: k) m f.
            ( FreeAlgebra2 m
            , AlgebraType0 m f
            , Category    (m f)
            ) => [f a a] -> m f a a
fromList [] = id
fromList (f : fs) = liftFree2 f . fromList fs

toList :: ( FreeAlgebra2 m
          , AlgebraType0 m IntCat
          , AlgebraType  m (ListTr IntCat)
          )
       => m IntCat '() '()
       -> [IntCat '() '()]
toList c = go (hoistFreeH2 c)
  where
    go :: ListTr IntCat '() '() -> [IntCat '() '()]
    go NilTr = []
    go (ConsTr tr@IntCat{} xs) = tr : go xs

--
-- 'C' category laws
--

newtype ArbIntC = ArbIntC (C IntCat '() '())

instance Show ArbIntC where
    show (ArbIntC c) = show c

instance Arbitrary ArbIntC where
    arbitrary = ArbIntC . fromList <$> arbitrary
    shrink (ArbIntC c) =
      map (ArbIntC . fromList)
          $ shrinkList (const [])
          $ toList c

prop_id_C :: ArbIntC -> Bool
prop_id_C (ArbIntC f) =
    prop_id (on (==) toList) f

prop_associativity_C
    :: ArbIntC -> ArbIntC -> ArbIntC
    -> Bool
prop_associativity_C (ArbIntC f0)
                     (ArbIntC f1)
                     (ArbIntC f2) =
      prop_associativity (on (==) toList) f0 f1 f2

--
-- 'Queue' category laws
--

newtype ArbIntQueue = ArbIntQueue (Queue IntCat '() '())

instance Show ArbIntQueue where
    show (ArbIntQueue f) = show (toList f)

instance Arbitrary ArbIntQueue where
    arbitrary = ArbIntQueue . fromList <$> arbitrary
    shrink (ArbIntQueue c) =
      map (ArbIntQueue . fromList)
          $ shrinkList (const [])
          $ toList c

prop_id_Queue :: ArbIntQueue -> Bool
prop_id_Queue (ArbIntQueue f) =
    prop_id (on (==) toList) f

prop_associativity_Queue
    :: ArbIntQueue -> ArbIntQueue -> ArbIntQueue
    -> Bool
prop_associativity_Queue (ArbIntQueue f0)
                         (ArbIntQueue f1)
                         (ArbIntQueue f2) =
      prop_associativity (on (==) toList) f0 f1 f2

--
-- 'ListTr' category laws
--

newtype ArbIntListTr = ArbIntListTr (ListTr IntCat '() '())

instance Show ArbIntListTr where
    show (ArbIntListTr f) = show (toList f)

instance Arbitrary ArbIntListTr where
    arbitrary = ArbIntListTr . fromList <$> arbitrary
    shrink (ArbIntListTr c) =
      map (ArbIntListTr . fromList)
          $ shrinkList (const [])
          $ toList c

prop_id_ListTr :: ArbIntListTr -> Bool
prop_id_ListTr (ArbIntListTr f) =
    prop_id (on (==) toList) f

prop_associativity_ListTr
    :: ArbIntListTr -> ArbIntListTr -> ArbIntListTr
    -> Bool
prop_associativity_ListTr (ArbIntListTr f0)
                          (ArbIntListTr f1)
                          (ArbIntListTr f2) =
      prop_associativity (on (==) toList) f0 f1 f2


--
-- Compatibility between 'foldFree2' and 'foldMap' for 'IntCat'
--

prop_foldListTr :: ArbIntListTr -> Bool
prop_foldListTr (ArbIntListTr f)
    = foldFree2 f == foldMap id (toList f)

prop_foldQueue :: ArbIntQueue -> Bool
prop_foldQueue (ArbIntQueue f)
    = foldFree2 f == foldMap id (toList f)

prop_foldC :: (Blind ArbIntC) -> Bool
prop_foldC (Blind (ArbIntC f))
    = foldFree2 f == foldMap id (toList f)