{-| Module  : FiniteCategories
Description : Functions to create usual and arbitrary diagrams.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A diagram is a heterogeneous FinFunctor, it is a shift of perspective : we view the functor not as a morphism of categories but as a selection in a category.
 
By heterogeneous, we mean that the type of the source category may be different from the target category.
 
To convert a `Diagram` into any other kind of functor, see @Diagram.Conversion@.

To enumerate all diagrams between two categories, see the `ob` function of /FunctorCategory/.
-}

module Diagram.Diagram
(
    -- * Diagram typeclass and useful functions
    Diagram(..),
    checkFunctoriality,
    completeMmap,
    composeDiag,
    objectImage,
    -- * Constructors of diagrams
    mkDiagram,
    mkIdentityDiagram,
    mkConstantDiagram,
    mkDiscreteDiagram,
    mkSelect0,
    mkSelect1,
    mkSelect2,
    mkSelect3,
    mkTriangle,
    mkParallel,
    mkV,
    mkHat,
)
where
    import Prelude                          hiding ((@))
    import FiniteCategory.FiniteCategory
    import Cat.FinCat
    import Cat.PartialFinCat
    import UsualCategories.DiscreteCategory
    import UsualCategories.Zero
    import UsualCategories.One
    import qualified UsualCategories.Two   as Two
    import qualified UsualCategories.Three as Three
    import qualified UsualCategories.Parallel as Par
    import qualified UsualCategories.V as V
    import qualified UsualCategories.Hat as Hat
    import Data.List (intercalate, nub)
    import Utils.SetList
    import Utils.AssociationList
    import IO.PrettyPrint
    import IO.Show
    
    -- | A diagram is a heterogeneous FinFunctor /F/, it is a shift of perspective : we view the FinFunctor not as a morphism of categories but as a selection in a category. It must obey the following rules :
    --
    -- prop> F (src f) = src (F f) 
    -- prop> F (tgt f) = tgt (F f)
    -- prop> F (f @ g) = F(f) @ F(g)
    -- prop> F (identity a) = identity (F a)
    --
    -- Unlike /FinFunctor/, a `Diagram` can have a source category and a target category with different types.
    --
    -- Using constructor functions `mkDiagram`, `mkConstantDiagram`, `mkDiscreteDiagram`, `mkSelect0`, `mkSelect1`, `mkSelect2`, `mkSelect3`, `mkTriangle` and `mkParallel` 
    -- is the safe way to instantiate a `Diagram` (FinFunctoriality is checked during construction).
    -- 
    -- Therefore, if you want to construct an arbitrary diagram, use the constructor function `mkDiagram` unless it is too long to check FinFunctoriality in which case
    -- you should use the `Diagram` constructor. It is then your responsability to ensure the FinFunctoriality property is verified.
    data Diagram c1 m1 o1 c2 m2 o2 = Diagram {src :: c1 -- ^ The source category of the `Diagram`
                                            , tgt :: c2 -- ^ The target category of the `Diagram`
                                            , omap :: AssociationList o1 o2 -- ^ The object map
                                            , mmap :: AssociationList m1 m2} -- ^ The morphism map
                                            deriving (Eq, Show)
    
    -- | Checks wether the properties of a Diagram are respected. Returns True if the diagram is well formed, else False.
    checkFunctoriality :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                           FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                          Diagram c1 m1 o1 c2 m2 o2 -> Bool
    checkFunctoriality Diagram{src=s,tgt=t,omap=om,mmap=fm}
        | not (foldr (&&) True imIdNotId) = False
        | not (foldr (&&) True 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))]
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, PrettyPrintable m1, PrettyPrintable o1, Eq m1, Eq o1, PrettyPrintable c1,
              FiniteCategory c2 m2 o2, Morphism m2 o2, PrettyPrintable m2, PrettyPrintable o2, PrettyPrintable c2) =>
              PrettyPrintable (Diagram c1 m1 o1 c2 m2 o2) where
        pprint Diagram{src=s,tgt=t,omap=om,mmap=fm} = "Diagram "++pprint s++" -> "++pprint t++"\n"++pprint om++"\n"++pprint fm
    
    -- | Constructor of an arbitrary `Diagram` that checks functoriality.
    --
    -- Use the `Diagram` constructor if the functoriality check is too slow. It is then your responsability to ensure the functoriality property is verified.
    mkDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
                  FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) =>
                  c1 -- ^ The source category of the diagram.
               -> c2 -- ^ The target category of the diagram.
               -> AssociationList o1 o2 -- ^ The object map of the diagram.
               -> AssociationList m1 m2 -- ^ The morphism map of the diagram.
               -> Maybe (Diagram c1 m1 o1 c2 m2 o2) -- ^ The constructor returns Nothing if the FinFunctoriality check failed.
    mkDiagram c1 c2 om fm = if checkFunctoriality diag then Just diag else Nothing
        where diag = Diagram {src=c1, tgt=c2, omap=om, mmap=fm}
    
    -- | Completes the function map `mmap` of a diagram so that you do not have to specify images of identites and composite arrows.
    completeMmap :: (GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq m1,
                              FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2, Eq m2) =>
                       c1 -- ^ The source category, it must be a generated category. 
                    -> c2 -- ^ The target category. 
                    -> AssociationList o1 o2 -- ^ The omap. 
                    -> AssociationList m1 m2 -- ^ The mmap to complete. 
                    -> AssociationList m1 m2 -- ^ The completed mmap.
    completeMmap c1 c2 om fm = nub fm2
        where
            fm1 = [(identity c1 o, identity c2 (om !-! o)) | o <- ob c1]++fm
            fm2 = [(a,compose $ (fm1 !-!) <$> decompose c1 a) | a <- arrows c1]++fm1
            
    -- | Compose two diagrams.
    composeDiag :: (FiniteCategory c1 m1 o1, Morphism m1 o1
           ,FiniteCategory c2 m2 o2, Morphism m2 o2
           ,FiniteCategory c3 m3 o3, Morphism m3 o3
           ,Eq m1, Eq o1, Eq m2, Eq o2) => 
           Diagram c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c3 m3 o3
    diag2 `composeDiag` diag1 = Diagram {src=(src diag1), tgt=(tgt diag2), omap=((omap diag2)!-.(omap diag1)), mmap=((mmap diag2)!-.(mmap diag1))} 
    
    -- | Returns the objects image of the diagram.
    objectImage :: (FiniteCategory c1 m1 o1, Morphism m1 o1
                   ,FiniteCategory c2 m2 o2, Morphism m2 o2) =>
                    Diagram c1 m1 o1 c2 m2 o2 -> [o2]
    objectImage diag = snd <$> (omap diag)
    
    -- | Constructs a diagram which maps a category to itself to that each object is mapped to itself and each morphism is mapped to itself too.
    mkIdentityDiagram :: (FiniteCategory c m o, Morphism m o) => c -> (Diagram c m o c m o)
    mkIdentityDiagram c = Diagram {src=c, tgt=c, omap=functToAssocList id (ob c),mmap=functToAssocList id (arrows c)}
    
    -- | Constructs a diagram where every object is mapped to a single object and every morphism is mapped to the identity of this single object.
    mkConstantDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1,
                          FiniteCategory c2 m2 o2, Morphism m2 o2, Eq o2) => c1 -> c2 -> o2 -> Maybe (Diagram c1 m1 o1 c2 m2 o2)
    mkConstantDiagram c1 c2 o2
        | elem o2 (ob c2) = Just Diagram {src=c1, tgt=c2, omap=functToAssocList (\x -> o2) (ob c1),mmap=functToAssocList (\x -> (identity c2 o2)) (arrows c1)}
        | otherwise = Nothing
    
    -- | Constructs a diagram that selects a list of objects of a category.
    mkDiscreteDiagram :: (FiniteCategory c m o, Morphism m o, Eq o) =>
                          c -> [o] -> Maybe (Diagram (DiscreteCategory o) (DiscreteIdentity o) (DiscreteObject o) c m o)
    mkDiscreteDiagram c objs
        | objs `isIncludedIn` (ob c) = Just Diagram {src=DiscreteCategory objs, tgt=c, omap=functToAssocList (\(DiscreteObject o) -> o) (ob (DiscreteCategory objs)),mmap=functToAssocList (\(DiscreteIdentity o) -> (identity c o)) (arrows (DiscreteCategory objs))}
        | otherwise = Nothing
    
    -- | Constructs a diagram that selects no object and no morphism.
    mkSelect0 :: (FiniteCategory c m o, Morphism m o) => c -> Diagram Zero Zero Zero c m o
    mkSelect0 c = Diagram {src=Zero, tgt=c, omap=[],mmap=[]}
    
    -- | Constructs a diagram that selects a single object and its identity.
    mkSelect1 :: (FiniteCategory c m o, Morphism m o, Eq o) => c -> o -> Maybe (Diagram One One One c m o)
    mkSelect1 c o
        | elem o (ob c) = Just Diagram {src=One, tgt=c, omap=[(One,o)],mmap=[(One,(identity c o))]}
        | otherwise = Nothing
    
    -- | Constructs a diagram that selects a single arrow.
    mkSelect2 :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Maybe (Diagram Two.Two Two.TwoAr Two.TwoOb c m o)
    mkSelect2 c m 
        | condition = Just Diagram {src=Two.Two, tgt=c, omap=om,mmap=(completeMmap Two.Two c om [(Two.F,m)])}
        | otherwise = Nothing
        where
            condition = elem (source m) (ob c) && elem (target m) (ob c) && elem m (ar c (source m) (target m))
            om = [(Two.A,source m),(Two.B,target m)]
            
    -- | Constructs a diagram that selects a triangle.
    --
    -- > B <-f- A
    -- > |     /
    -- > g   g\@f
    -- > |  /
    -- > v v 
    -- > C
    mkSelect3 :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -- ^ The target category.
                                                                  -> m -- ^ /f/
                                                                  -> m -- ^ /g/
                                                                  -> Maybe (Diagram Three.Three Three.ThreeAr Three.ThreeOb c m o)
    mkSelect3 c f g
        | condition = Just Diagram {src=Three.Three, tgt=c, omap=om,mmap=(completeMmap Three.Three c om [(Three.F,f),(Three.G,g)])}
        | otherwise = Nothing
        where
            condition = obInCat && arInCat && (source g) == (target f)
            obInCat =  elem (source f) (ob c) && elem (target f) (ob c) && elem (target g) (ob c)
            arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
            om = [(Three.A,source f),(Three.B,target f),(Three.C,target g)]
            
    -- | Constructs a diagram that selects a triangle. (Alias for `mkSelect3`).
    mkTriangle :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Three.Three Three.ThreeAr Three.ThreeOb c m o)
    mkTriangle = mkSelect3
    
    -- | Constructs a diagram that selects two parallel arrows.
    mkParallel :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Par.Parallel Par.ParallelAr Par.ParallelOb c m o)
    mkParallel c f g
        | condition = Just Diagram {src=Par.Parallel, tgt=c, omap=om,mmap=(completeMmap Par.Parallel c om [(Par.F,f),(Par.G,g)])}
        | otherwise = Nothing
        where
            condition = obInCat && arInCat && (source f) == (source g) && (target f) == (target g)
            obInCat =  elem (source f) (ob c) && elem (target f) (ob c)
            arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
            om = [(Par.A,source f), (Par.B, target f)]
           
    -- | Constructs a diagram that selects a V.
    mkV :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram V.V V.VAr V.VOb c m o)
    mkV c f g
        | condition = Just Diagram {src=V.V, tgt=c, omap=om,mmap=(completeMmap V.V c om [(V.F,f),(V.G,g)])}
        | otherwise = Nothing
        where
            condition = obInCat && arInCat && (target f) == (target g)
            obInCat =  elem (source f) (ob c) && elem (target f) (ob c)
            arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
            om = [(V.A,source f), (V.B, source g), (V.C, target g)]
            
    -- | Constructs a diagram that selects a Hat.
    mkHat :: (FiniteCategory c m o, Morphism m o, Eq o, Eq m) => c -> m -> m -> Maybe (Diagram Hat.Hat Hat.HatAr Hat.HatOb c m o)
    mkHat c f g
        | condition = Just Diagram {src=Hat.Hat, tgt=c, omap=om,mmap=(completeMmap Hat.Hat c om [(Hat.F,f),(Hat.G,g)])}
        | otherwise = Nothing
        where
            condition = obInCat && arInCat && (source f) == (source g)
            obInCat =  elem (source f) (ob c) && elem (target f) (ob c)
            arInCat = elem f (ar c (source f) (target f)) && elem g (ar c (source g) (target g))
            om = [(Hat.A,source f), (Hat.B, target f), (Hat.C, target g)]