{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Given two categories C and D, the `FunctorCategory` D^C has as objects functors from C to D and as morphisms natural transformations between functors.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Given two categories C and D, the `FunctorCategory` D^C has as objects functors from C to D and as morphisms natural transformations between functors.
-}

module FunctorCategory.FunctorCategory
(
    NaturalTransformation(..),
    preWhiskering,
    postWhiskering,
    FunctorCategory(..)
)
where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import Data.List                               (intercalate)
    import Utils.EnumerateMaps
    import Utils.CartesianProduct
    import Data.Maybe                              (isJust, fromJust)
    import IO.PrettyPrint
    import IO.Show
    import Utils.AssociationList
    
    -- | A `NaturalTransformation` between two heterogeneous functors from /C/ to /D/ is a mapping from objects of /C/ to morphism of /D/ such that naturality is respected.
    --
    -- Formally, let /F/ and /G/ be functors, and eta : Ob(/C/) -> Ar(/D/). The following property should be respected :
    --
    -- prop> source F = source G
    -- prop> target F = target G
    -- prop> Forall f in arrows (source F) : eta(target f) @ F(f) = G(f) @ eta(source f)
    data NaturalTransformation c1 m1 o1 c2 m2 o2 = NaturalTransformation {srcNT :: Diagram c1 m1 o1 c2 m2 o2
                                                                        , tgtNT :: Diagram c1 m1 o1 c2 m2 o2
                                                                        , component :: o1 -> m2}
    
    instance   (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                Morphism (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        (@) NaturalTransformation{srcNT=s2,tgtNT=t2,component=c2} NaturalTransformation{srcNT=s1,tgtNT=t1,component=c1}
            | t1 /= s2 = error "Illegal composition of natural transformations"
            | otherwise = NaturalTransformation{srcNT=s1,tgtNT=t2,component=(\x -> (c2 x) @ (c1 x))}
        source = srcNT
        target = tgtNT
        
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) =>
              Eq (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        NaturalTransformation{srcNT=s1,tgtNT=t1,component=c1} == NaturalTransformation{srcNT=s2,tgtNT=t2,component=c2}
            | s1 /= s2 = False
            | t1 /= t2 = False
            | otherwise = and [c1 o == c2 o | o <- (ob.src) s1]
            
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Show c1, Show m1, Show o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Show c2, Show m2, Show o2) =>
              Show (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        show NaturalTransformation{srcNT=s,tgtNT=t,component=c} = "NaturalTransformation{srcNT = "++show s++", tgtNT = "++show t++", component = "++showFunction c ((ob.src) s)++"}"
           
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, PrettyPrintable c1, PrettyPrintable m1, PrettyPrintable o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, PrettyPrintable c2, PrettyPrintable m2, PrettyPrintable o2) =>
              PrettyPrintable (NaturalTransformation c1 m1 o1 c2 m2 o2) where
        pprint NaturalTransformation{srcNT=s,tgtNT=t,component=c} = "Nat : "++pprint s++" -> "++pprint t++"\\n\\n"++pprintFunction c ((ob.src) s)
        
    -- | Checks wether the naturality property of a natural transformation is respected.
    checkNaturality :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                                                 Morphism m2 o2, Eq m2, Eq o2) => 
                        NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool
    checkNaturality NaturalTransformation{srcNT=s,tgtNT=t,component=c} = and [((mmap t) !-! f) @ (c (source f)) == (c (target f)) @ ((mmap s) !-! f)| f <- (arrows.src) s]
        
    -- | Pre-whiskering as defined in Category Theory for the Sciences (2014) by David I. Spivak
    preWhiskering :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                    , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2
                    , FiniteCategory c3 m3 o3, Morphism m3 o3) =>
        NaturalTransformation c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    preWhiskering nt d = NaturalTransformation{   srcNT = (srcNT nt) `composeDiag` d 
                                                , tgtNT = (tgtNT nt) `composeDiag` d
                                                , component = (component nt).(assocListToFunct (omap d))}
                                                
    -- | Pre-whiskering as defined in Category Theory for the Sciences (2014) by David I. Spivak
    postWhiskering ::   ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                        , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2
                        , FiniteCategory c3 m3 o3, Morphism m3 o3) =>
        Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3
    postWhiskering d nt = NaturalTransformation{  srcNT = d `composeDiag` (srcNT nt) 
                                                , tgtNT = d `composeDiag` (tgtNT nt)
                                                , component = (assocListToFunct (mmap d)).(component nt)}
        
        
    -- | `FunctorCategory` D^C.
    data FunctorCategory c1 m1 o1 c2 m2 o2 = FunctorCategory {sourceCat :: c1 -- ^ /C/
                                                            , targetCat :: c2} -- ^ /D/
                                                            deriving (Eq, Show)
    
    enumerateFunctors :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                          FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                          c1 -> c2 -> [Diagram c1 m1 o1 c2 m2 o2]
    enumerateFunctors cat1 cat2 = [Diagram{src=cat1,tgt=cat2,mmap=appF, omap=appO} | appO <- appObj, appF <- concat <$> cartesianProduct [twoObjToMaps a b appO| a <- ob cat1, b <- ob cat1], checkFunctoriality Diagram{src=cat1,tgt=cat2,mmap=appF, omap=appO}]
            where
                appObj = enumMaps (ob cat1) (ob cat2)
                twoObjToMaps a b appO = enumMaps (ar cat1 a b) (ar cat2 (appO !-! a) (appO !-! b))
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
              FiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        ob FunctorCategory{sourceCat=cat1, targetCat=cat2} = enumerateFunctors cat1 cat2
        
        identity c diag = NaturalTransformation{srcNT=diag,tgtNT=diag,component=(identity (tgt diag)).(assocListToFunct (omap diag))}
        
        ar c diag1 diag2 = [NaturalTransformation{srcNT=diag1,tgtNT=diag2,component=mapCompo} | mapCompo <- mapComponent, checkNaturality NaturalTransformation{srcNT=diag1,tgtNT=diag2,component=mapCompo}]
            where
                mapComponent = transformToFunction <$> cartesianProduct [(\x -> (o,x)) <$> (ar (tgt diag1) ((omap diag1) !-! o) ((omap diag2) !-! o)) | o <- (ob (src diag1))]
                transformToFunction ((o,f):xs) x = if o == x then f else transformToFunction xs x
                    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
              GeneratedFiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2) where
        genAr = defaultGenAr
        decompose = defaultDecompose
        
    instance (PrettyPrintable c1, PrettyPrintable c2) =>
              PrettyPrintable (FunctorCategory c1 m1 o1 c2 m2 o2) where
        pprint FunctorCategory{sourceCat=s, targetCat=t} = "Fonct("++pprint s++","++pprint t++")"