{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}

module Data.IFunctor.ICofree
    ( ICofree (..)
    ) where

import           Data.IComonad         (IComonad (..))
import           Data.IFunctor         (IFunctor (..))
import           Data.IFunctor.Classes
import           Data.ITraversable     (ITraversable (..))
import           Data.Typeable         (Typeable)
import           GHC.Generics          (Generic, Generic1)
import           Singlethongs          (SingI)
import           Text.Read

infixr 5 ::<

-- | Cofree IComonad
data ICofree f a ix = a ix ::< f (ICofree f a) ix
    deriving (Typeable, (forall x. ICofree f a ix -> Rep (ICofree f a ix) x)
-> (forall x. Rep (ICofree f a ix) x -> ICofree f a ix)
-> Generic (ICofree f a ix)
forall x. Rep (ICofree f a ix) x -> ICofree f a ix
forall x. ICofree f a ix -> Rep (ICofree f a ix) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k) x.
Rep (ICofree f a ix) x -> ICofree f a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k) x.
ICofree f a ix -> Rep (ICofree f a ix) x
$cto :: forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k) x.
Rep (ICofree f a ix) x -> ICofree f a ix
$cfrom :: forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k) x.
ICofree f a ix -> Rep (ICofree f a ix) x
Generic, (forall (a :: k). ICofree f a a -> Rep1 (ICofree f a) a)
-> (forall (a :: k). Rep1 (ICofree f a) a -> ICofree f a a)
-> Generic1 (ICofree f a)
forall (a :: k). Rep1 (ICofree f a) a -> ICofree f a a
forall (a :: k). ICofree f a a -> Rep1 (ICofree f a) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (a :: k).
Rep1 (ICofree f a) a -> ICofree f a a
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (a :: k).
ICofree f a a -> Rep1 (ICofree f a) a
$cto1 :: forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (a :: k).
Rep1 (ICofree f a) a -> ICofree f a a
$cfrom1 :: forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (a :: k).
ICofree f a a -> Rep1 (ICofree f a) a
Generic1)

instance IFunctor f => IFunctor (ICofree f) where
    imap :: (a ~~> b) -> ICofree f a ~~> ICofree f b
imap f :: a ~~> b
f (a :: a ix
a ::< x :: f (ICofree f a) ix
x) = a ix -> b ix
a ~~> b
f a ix
a b ix -> f (ICofree f b) ix -> ICofree f b ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< (ICofree f a ~~> ICofree f b)
-> f (ICofree f a) ix -> f (ICofree f b) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap ((a ~~> b) -> ICofree f a ~~> ICofree f b
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> b
f) f (ICofree f a) ix
x

instance ITraversable f => ITraversable (ICofree f) where
    itraverse :: (forall (ix :: k). SingI ix => a ix -> m (b ix))
-> ICofree f a ix -> m (ICofree f b ix)
itraverse f :: forall (ix :: k). SingI ix => a ix -> m (b ix)
f (a :: a ix
a ::< x :: f (ICofree f a) ix
x) = b ix -> f (ICofree f b) ix -> ICofree f b ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
(::<) (b ix -> f (ICofree f b) ix -> ICofree f b ix)
-> m (b ix) -> m (f (ICofree f b) ix -> ICofree f b ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a ix -> m (b ix)
forall (ix :: k). SingI ix => a ix -> m (b ix)
f a ix
a m (f (ICofree f b) ix -> ICofree f b ix)
-> m (f (ICofree f b) ix) -> m (ICofree f b ix)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (ix :: k).
 SingI ix =>
 ICofree f a ix -> m (ICofree f b ix))
-> f (ICofree f a) ix -> m (f (ICofree f b) ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse ((forall (ix :: k). SingI ix => a ix -> m (b ix))
-> ICofree f a ix -> m (ICofree f b ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse forall (ix :: k). SingI ix => a ix -> m (b ix)
f) f (ICofree f a) ix
x

instance IFunctor f => IComonad (ICofree f) where
    iextract :: ICofree f a ix -> a ix
iextract (a :: a ix
a ::< _) = a ix
a
    iduplicate :: ICofree f a ix -> ICofree f (ICofree f a) ix
iduplicate (a :: a ix
a ::< x :: f (ICofree f a) ix
x) = (a ix
a a ix -> f (ICofree f a) ix -> ICofree f a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< f (ICofree f a) ix
x) ICofree f a ix
-> f (ICofree f (ICofree f a)) ix -> ICofree f (ICofree f a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< (ICofree f a ~~> ICofree f (ICofree f a))
-> f (ICofree f a) ix -> f (ICofree f (ICofree f a)) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap ICofree f a ~~> ICofree f (ICofree f a)
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate f (ICofree f a) ix
x
    iextend :: (ICofree f a ~~> b) -> ICofree f a ~~> ICofree f b
iextend f :: ICofree f a ~~> b
f (a :: a ix
a ::< x :: f (ICofree f a) ix
x) = ICofree f a ix -> b ix
ICofree f a ~~> b
f (a ix
a a ix -> f (ICofree f a) ix -> ICofree f a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< f (ICofree f a) ix
x) b ix -> f (ICofree f b) ix -> ICofree f b ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< (ICofree f a ~~> ICofree f b)
-> f (ICofree f a) ix -> f (ICofree f b) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap ((ICofree f a ~~> b) -> ICofree f a ~~> ICofree f b
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IComonad f =>
(f a ~~> b) -> f a ~~> f b
iextend ICofree f a ~~> b
f) f (ICofree f a) ix
x

instance IShow f => IShow (ICofree f) where
    ishowsPrec :: (forall (ix :: k). SingI ix => Int -> a ix -> ShowS)
-> Int -> ICofree f a ix -> ShowS
ishowsPrec sp :: forall (ix :: k). SingI ix => Int -> a ix -> ShowS
sp p :: Int
p (a :: a ix
a ::< x :: f (ICofree f a) ix
x) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        Int -> a ix -> ShowS
forall (ix :: k). SingI ix => Int -> a ix -> ShowS
sp 6 a ix
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString " ::< " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (ix :: k). SingI ix => Int -> ICofree f a ix -> ShowS)
-> Int -> f (ICofree f a) ix -> ShowS
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IShow f, SingI ix) =>
(forall (ix :: k). SingI ix => Int -> a ix -> ShowS)
-> Int -> f a ix -> ShowS
ishowsPrec ((forall (ix :: k). SingI ix => Int -> a ix -> ShowS)
-> Int -> ICofree f a ix -> ShowS
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IShow f, SingI ix) =>
(forall (ix :: k). SingI ix => Int -> a ix -> ShowS)
-> Int -> f a ix -> ShowS
ishowsPrec forall (ix :: k). SingI ix => Int -> a ix -> ShowS
sp) 6 f (ICofree f a) ix
x

instance IRead f => IRead (ICofree f) where
    ireadPrec :: (forall (ix :: k). SingI ix => ReadPrec (a ix))
-> ReadPrec (ICofree f a ix)
ireadPrec rp :: forall (ix :: k). SingI ix => ReadPrec (a ix)
rp = ReadPrec (ICofree f a ix) -> ReadPrec (ICofree f a ix)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (ICofree f a ix) -> ReadPrec (ICofree f a ix))
-> ReadPrec (ICofree f a ix) -> ReadPrec (ICofree f a ix)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (ICofree f a ix) -> ReadPrec (ICofree f a ix)
forall a. Int -> ReadPrec a -> ReadPrec a
prec 5 (ReadPrec (ICofree f a ix) -> ReadPrec (ICofree f a ix))
-> ReadPrec (ICofree f a ix) -> ReadPrec (ICofree f a ix)
forall a b. (a -> b) -> a -> b
$ do
        a ix
a <- ReadPrec (a ix) -> ReadPrec (a ix)
forall a. ReadPrec a -> ReadPrec a
step ReadPrec (a ix)
forall (ix :: k). SingI ix => ReadPrec (a ix)
rp
        Symbol "::<" <- ReadPrec Lexeme
lexP
        f (ICofree f a) ix
x <- ReadPrec (f (ICofree f a) ix) -> ReadPrec (f (ICofree f a) ix)
forall a. ReadPrec a -> ReadPrec a
step ((forall (ix :: k). SingI ix => ReadPrec (ICofree f a ix))
-> ReadPrec (f (ICofree f a) ix)
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IRead f, SingI ix) =>
(forall (ix :: k). SingI ix => ReadPrec (a ix))
-> ReadPrec (f a ix)
ireadPrec ((forall (ix :: k). SingI ix => ReadPrec (a ix))
-> ReadPrec (ICofree f a ix)
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IRead f, SingI ix) =>
(forall (ix :: k). SingI ix => ReadPrec (a ix))
-> ReadPrec (f a ix)
ireadPrec forall (ix :: k). SingI ix => ReadPrec (a ix)
rp))
        ICofree f a ix -> ReadPrec (ICofree f a ix)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a ix
a a ix -> f (ICofree f a) ix -> ICofree f a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< f (ICofree f a) ix
x)

instance IEq f => IEq (ICofree f) where
    ieq :: (forall (ix :: k). SingI ix => a ix -> a ix -> Bool)
-> ICofree f a ix -> ICofree f a ix -> Bool
ieq eq :: forall (ix :: k). SingI ix => a ix -> a ix -> Bool
eq (a :: a ix
a ::< x :: f (ICofree f a) ix
x) (a' :: a ix
a' ::< x' :: f (ICofree f a) ix
x') = a ix -> a ix -> Bool
forall (ix :: k). SingI ix => a ix -> a ix -> Bool
eq a ix
a a ix
a' Bool -> Bool -> Bool
&& (forall (ix :: k).
 SingI ix =>
 ICofree f a ix -> ICofree f a ix -> Bool)
-> f (ICofree f a) ix -> f (ICofree f a) ix -> Bool
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IEq f, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> a ix -> Bool)
-> f a ix -> f a ix -> Bool
ieq ((forall (ix :: k). SingI ix => a ix -> a ix -> Bool)
-> ICofree f a ix -> ICofree f a ix -> Bool
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IEq f, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> a ix -> Bool)
-> f a ix -> f a ix -> Bool
ieq forall (ix :: k). SingI ix => a ix -> a ix -> Bool
eq) f (ICofree f a) ix
x f (ICofree f a) ix
x'

instance IOrd f => IOrd (ICofree f) where
    icompare :: (forall (ix :: k). SingI ix => a ix -> a ix -> Ordering)
-> ICofree f a ix -> ICofree f a ix -> Ordering
icompare comp :: forall (ix :: k). SingI ix => a ix -> a ix -> Ordering
comp (a :: a ix
a ::< x :: f (ICofree f a) ix
x) (a' :: a ix
a' ::< x' :: f (ICofree f a) ix
x') = a ix -> a ix -> Ordering
forall (ix :: k). SingI ix => a ix -> a ix -> Ordering
comp a ix
a a ix
a' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (forall (ix :: k).
 SingI ix =>
 ICofree f a ix -> ICofree f a ix -> Ordering)
-> f (ICofree f a) ix -> f (ICofree f a) ix -> Ordering
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IOrd f, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> a ix -> Ordering)
-> f a ix -> f a ix -> Ordering
icompare ((forall (ix :: k). SingI ix => a ix -> a ix -> Ordering)
-> ICofree f a ix -> ICofree f a ix -> Ordering
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IOrd f, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> a ix -> Ordering)
-> f a ix -> f a ix -> Ordering
icompare forall (ix :: k). SingI ix => a ix -> a ix -> Ordering
comp) f (ICofree f a) ix
x f (ICofree f a) ix
x'

instance (IShow f, IShow2 a, SingI ix) => Show (ICofree f a ix) where
    showsPrec :: Int -> ICofree f a ix -> ShowS
showsPrec = Int -> ICofree f a ix -> ShowS
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *) (ix :: k2).
(IShow f, IShow2 a, SingI ix) =>
Int -> f a ix -> ShowS
ishowsPrec1

instance (IRead f, IRead2 a, SingI ix) => Read (ICofree f a ix) where
    readPrec :: ReadPrec (ICofree f a ix)
readPrec = ReadPrec (ICofree f a ix)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *) (ix :: k2).
(IRead f, IRead2 a, SingI ix) =>
ReadPrec (f a ix)
ireadPrec1

instance (IEq f, IEq2 a, SingI ix) => Eq (ICofree f a ix) where
    == :: ICofree f a ix -> ICofree f a ix -> Bool
(==) = ICofree f a ix -> ICofree f a ix -> Bool
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *) (ix :: k2).
(IEq f, IEq2 a, SingI ix) =>
f a ix -> f a ix -> Bool
ieq1

instance (IOrd f, IOrd2 a, SingI ix) => Ord (ICofree f a ix) where
    compare :: ICofree f a ix -> ICofree f a ix -> Ordering
compare = ICofree f a ix -> ICofree f a ix -> Ordering
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *) (ix :: k2).
(IOrd f, IOrd2 a, SingI ix) =>
f a ix -> f a ix -> Ordering
icompare1