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

{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cat (tests) where

import           Prelude hiding ((.), id)
import           Control.Category
import           Data.Function (on)
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

instance (forall x y. Show (Tr x y)) => Show ArbListTr where
    show (ArbListTr listTr a b) =
         "ArbListTr "
      ++ show a
      ++ " -> "
      ++ show b
      ++ " "
      ++ show listTr

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

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)