{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : __FinCat__ is the category of finite categories, functors are the morphisms of __FinCat__.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __FinCat__ category has as objects finite categories and as morphisms functors between them.
It is itself a large category (therefore not a finite one),
we only construct finite full subcategories of the mathematical infinite __FinCat__ category.
`FinCat` is the type of full finite subcategories of __FinCat__.

To instantiate it, use the `FinCat` constructor on a list of categories.

For example, see ExampleCat.ExampleCat

The `FinCat` type should not be confused with the `FiniteCategory` typeclass.

The `FiniteCategory` typeclass describes axioms a structure should follow to be considered a finite category.

The `FinCat` type is itself a `FiniteCategory` and contains finite categories as objects.

To convert a `FinFunctor` into any other kind of functor, see @Diagram.Conversion@.
-}

module Cat.FinCat
(
    FinFunctor(..),
    FinCat(..)
)
where
    import FiniteCategory.FiniteCategory
    import Utils.EnumerateMaps
    import Utils.CartesianProduct
    import IO.PrettyPrint
    import IO.Show
    import Utils.AssociationList
    
    -- | A `FinFunctor` /F/ between two categories is a map between objects and a map between arrows of the two categories such that :
    --
    -- prop> F (srcF f) = srcF (F f) 
    -- prop> F (tgtF f) = tgtF (F f)
    -- prop> F (f @ g) = F(f) @ F(g)
    -- prop> F (identity a) = identity (F a)
    --
    -- It is meant to be a morphism between categories within `FinCat`, it is homogeneous, the type of the source category must be the same as the type of the target category.
    --
    -- See /Diagram/ for heterogeneous ones.
    --
    -- To convert a `FinFunctor` into any other kind of functor, see @Diagram.Conversion@.
    data FinFunctor c m o = FinFunctor {srcF :: c, tgtF :: c, omapF :: AssociationList o o, mmapF :: AssociationList m m} deriving (Eq, Show)
    
    instance (Eq c, Eq m, Eq o) => Morphism (FinFunctor c m o) c where
        (@) FinFunctor{srcF=s2,tgtF=t2,omapF=om2,mmapF=fm2} FinFunctor{srcF=s1,tgtF=t1,omapF=om1,mmapF=fm1}
            | t1 /= s2 = error "Illegal composition of FinFunctors."
            | otherwise = FinFunctor{srcF=s1,tgtF=t2,omapF=om2!-.om1,mmapF=fm2!-.fm1}
        source = srcF
        target = tgtF
                    
    instance (FiniteCategory c m o, Morphism m o, PrettyPrintable c, PrettyPrintable m, PrettyPrintable o, Eq m, Eq o) =>
              PrettyPrintable (FinFunctor c m o) where
        pprint FinFunctor{srcF=s,tgtF=t,omapF=om,mmapF=fm} = "FinFunctor ("++pprint s++") -> ("++pprint t++")\n"++pprint om++"\n"++pprint fm
        
    -- | Checks wether the properties of a FinFunctor are respected.
    checkFinFunctoriality :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FinFunctor c m o -> Bool
    checkFinFunctoriality FinFunctor {srcF=s,tgtF=t,omapF=om,mmapF=fm}
        | not (and imIdNotId) = False
        | not (and errFunct) = False
        | otherwise = True
        where
            imIdNotId = [fm !-! (identity s a) == identity t (om !-! a) | a <- ob s]
            errFunct = [fm !-! (g @ f) == (fm !-! g) @ (fm !-! f) | f <- (arrows s), g <- (arFrom s (target f))]
        
    -- | An instance of `FinCat` is a list of categories of interest.
    --
    -- Listing all arrows between two objects (i.e. listing FinFunctors between two categories) is slow (there are a lot of candidates).
    newtype FinCat c m o = FinCat [c]
    
    -- We are forced to use the language extension FlexibleInstances because of this instance declaration :
    -- The category 'c' could be itself a `FinCat` category therefore not respecting the uniqueness rule of instanciation.
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => FiniteCategory (FinCat c m o) (FinFunctor c m o) c where
        ob (FinCat xs) = xs
        identity finCat catObj = FinFunctor {srcF=catObj,tgtF=catObj,omapF=functToAssocList id (ob catObj),mmapF=functToAssocList id (arrows catObj)}
        ar finCat cat1 cat2 = [FinFunctor{srcF=cat1,tgtF=cat2,mmapF=appF, omapF=appO} | appO <- appObj, appF <- concat <$> cartesianProduct [twoObjToMaps a b appO| a <- ob cat1, b <- ob cat1], checkFinFunctoriality FinFunctor{srcF=cat1,tgtF=cat2,mmapF=appF, omapF=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 c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (FinCat c m o) (FinFunctor c m o) c where
        genAr = defaultGenAr
        decompose = defaultDecompose