{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses  #-}

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

The __PartialFinCat__ category has as objects finite categories and as morphisms partial functors between them.

A partial functor is a functor where the object map and the morphism map can be partial functions.

It is itself a large category (therefore not a finite one),
we only construct finite full subcategories of the mathematical infinite __PartialFinCat__ category.
`PartialFinCat` is the type of full finite subcategories of __PartialFinCat__.

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

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

For example, see @ExampleCat.ExamplePartialFinCat@.
-}

module Cat.PartialFinCat
(
    PartialFunctor(..),
    PartialFinCat(..),
    domainObjects,
    domainArrows,
    codomainObjects,
    codomainArrows,
    objectsNotMapped,
    arrowsNotMapped,
    objectsNotMappedTo,
    arrowsNotMappedTo
)
where
    import FiniteCategory.FiniteCategory
    import Cat.FinCat
    import Utils.EnumerateMaps
    import Utils.CartesianProduct
    import Utils.AssociationList
    import IO.PrettyPrint
    import IO.Show
    import Utils.SetList
    import Data.List ((\\), nub)
    
    -- | A `PartialFunctor` /F/ between two categories is a partial map between objects and a partial map between arrows of the two categories such that :
    --
    -- prop> F (srcPF f) = srcPF (F f) 
    -- prop> F (tgtPF f) = tgtPF (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 `PartialFinCat`, it is homogeneous, the type of the source category must be the same as the type of the target category.
    --
    -- To convert a `PartialFunctor` into any other kind of functor, see @Diagram.Conversion@.
    data PartialFunctor c m o = PartialFunctor {srcPF :: c, tgtPF :: c, omapPF :: AssociationList o o, mmapPF :: AssociationList m m} deriving (Eq, Show)
    
    instance (Eq c, Eq m, Eq o) => Morphism (PartialFunctor c m o) c where
        (@) PartialFunctor{srcPF=s2,tgtPF=t2,omapPF=om2,mmapPF=fm2} PartialFunctor{srcPF=s1,tgtPF=t1,omapPF=om1,mmapPF=fm1}
            | t1 /= s2 = error "Illegal composition of PartialFunctors."
            | otherwise = PartialFunctor{srcPF=s1,tgtPF=t2,omapPF=om2 !-. om1,mmapPF=fm2 !-. fm1}
        source = srcPF
        target = tgtPF
            
    instance (FiniteCategory c m o, Morphism m o, PrettyPrintable c, PrettyPrintable m, PrettyPrintable o, Eq m, Eq o) =>
              PrettyPrintable (PartialFunctor c m o) where
        pprint PartialFunctor{srcPF=s,tgtPF=t,omapPF=om,mmapPF=fm} = "PartialFunctor ("++pprint s++") -> ("++pprint t++")\n\n"++pprint om++"\n\n"++pprint fm
        
    -- -- | Checks wether the properties of a functor are respected.
    checkPartialFunctoriality :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => PartialFunctor c m o -> Bool
    checkPartialFunctoriality PartialFunctor {srcPF=s,tgtPF=t,omapPF=om,mmapPF=fm}
        | not ((keys om) `isIncludedIn` (ob s)) = False
        | not ((keys fm) `isIncludedIn` (arrows s)) = False
        | not (and imSrcExists) = False
        | not (and imTgtExists) = False
        | not (and idMapped) = False
        | not (and imIdNotId) = False
        | not (and compNotMapped) = False
        | not (and errFunct) = False
        | otherwise = True
        where
            imSrcExists = [elem (source f) (keys om) | f <- keys fm]
            imTgtExists = [elem (target f) (keys om) | f <- keys fm]
            idMapped = [elem (identity s o) (keys fm) | o <- keys om]
            imIdNotId = [fm !-! (identity s a) == identity t (om !-! a) | a <- keys om]
            compNotMapped = [elem (g @ f) (keys fm) | f <- (arrows s), g <- (arFrom s (target f)), elem f (keys fm), elem g (keys fm)]
            errFunct = [fm !-! (g @ f) == (fm !-! g) @ (fm !-! f) | f <- (arrows s), g <- (arFrom s (target f)), elem f (keys fm), elem g (keys fm)]
      
    -- | An instance of `PartialFinCat` is a list of categories of interest.
    --
    -- Listing all arrows between two objects (i.e. listing PartialFunctors between two categories) is slow (there are a lot of candidates).
    newtype PartialFinCat c m o = PartialFinCat [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 (PartialFinCat c m o) (PartialFunctor c m o) c where
        ob (PartialFinCat xs) = xs
        identity (PartialFinCat xs) catObj
            | elem catObj xs = PartialFunctor {srcPF=catObj,tgtPF=catObj,omapPF=mkAssocListIdentity (ob catObj),mmapPF=mkAssocListIdentity (arrows catObj)}
            | otherwise = error "Category not in PartialFinCat"
        ar (PartialFinCat xs) cat1 cat2
            | elem cat1 xs && elem cat2 xs = [PartialFunctor{srcPF=cat1,tgtPF=cat2,mmapPF=appF, omapPF=appO} | appO <- appObj, appF <- appMorph, checkPartialFunctoriality PartialFunctor{srcPF=cat1,tgtPF=cat2,mmapPF=appF, omapPF=appO}]
            | otherwise = error "Category not in PartialFinCat"
            where
                appObj = concat $ (\x -> enumAssocLists x (ob cat2)) <$> (powerList (ob cat1))
                appMorph = concat $ (\x -> enumAssocLists x (arrows cat2)) <$> (powerList (arrows cat1))
                    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => GeneratedFiniteCategory (PartialFinCat c m o) (PartialFunctor c m o) c where
        genAr = defaultGenAr
        decompose = defaultDecompose
    
    -- | Returns the objects mapped by a partial functor.
    domainObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    domainObjects funct = keys (omapPF funct)
    
    -- | Returns the objects not mapped by a partial functor.
    objectsNotMapped :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    objectsNotMapped funct = (ob (source funct))\\(domainObjects funct)
    
    -- | Returns the arrows mapped by a partial functor.
    domainArrows :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    domainArrows funct = keys (mmapPF funct)
    
    -- | Returns the arrows not mapped by a partial functor.
    arrowsNotMapped :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    arrowsNotMapped funct = (arrows (source funct))\\(domainArrows funct)

    -- | Returns the objects mapped onto by a partial functor.
    codomainObjects :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    codomainObjects funct = nub $ values (omapPF funct)

    -- | Returns the objects not mapped onto by a partial functor.
    objectsNotMappedTo :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [o]
    objectsNotMappedTo funct = (ob (target funct))\\(codomainObjects funct)
    
    -- | Returns the arrows mapped onto by a partial functor.
    codomainArrows :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    codomainArrows funct = nub $ values (mmapPF funct)

    -- | Returns the arrows not mapped onto by a partial functor.
    arrowsNotMappedTo :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => PartialFunctor c m o -> [m]
    arrowsNotMappedTo funct = (arrows (target funct))\\(codomainArrows funct)