{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : A left cone on I is I with another object called the cone point and a single morphism from the cone point to every other object of I. 
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A left cone on I is I with another object called the cone point and a single morphism from the cone point to every other object of I.

See Category Theory for the Sciences (2014) David I. Spivak for more details.

An usual cone on C is then a functor from a left cone on I to C.
-}

module ConeCategory.LeftCone
(
    -- * Cone related functions and types.
    LeftCone(..),
    inclusionFunctor,
    ConeCategory(..)
)
where
    import FiniteCategory.FiniteCategory
    import IO.PrettyPrint
    import Diagram.Diagram
    import FunctorCategory.FunctorCategory
    import Utils.AssociationList
    
    -- | Object in a `LeftCone` category, either an original object or the cone point.
    data LeftConeObject o =   OriginalObject o
                            | ConePoint
                            deriving (Eq, Show)
    
    instance (PrettyPrintable o) => PrettyPrintable (LeftConeObject o) where
        pprint (OriginalObject o) = pprint o
        pprint ConePoint = "Left cone point"
    
    -- | Morphism in a `LeftCone` category, it is either an original morphism, a cone leg or the cone point identity.
    data LeftConeMorphism m o = OriginalMorphism m
                              | ConeLeg o
                              | ConePointIdentity
                              deriving (Eq, Show)
                                
    instance (PrettyPrintable m, PrettyPrintable o) => PrettyPrintable (LeftConeMorphism m o) where
        pprint (OriginalMorphism m) = pprint m
        pprint (ConeLeg o) = "Leg "++(pprint o)
        pprint ConePointIdentity = "Id Cone Point"
        
    instance (Morphism m o, Eq o) => Morphism (LeftConeMorphism m o) (LeftConeObject o) where
        (@) (OriginalMorphism g) (OriginalMorphism f) = OriginalMorphism (g @ f)
        (@) (ConeLeg _) (OriginalMorphism _) = error "Cannot compose an original morphism with a cone leg."
        (@) ConePointIdentity (OriginalMorphism _) = error "Cannot compose an original morphism with a cone point identity."
        (@) (OriginalMorphism f) (ConeLeg o)
            | (source f) == o = (ConeLeg (target f))
            | otherwise = error "Source of original morphism is not target of cone leg."
        (@) (ConeLeg _) (ConeLeg _) = error "Cannot compose two cone legs."
        (@) ConePointIdentity (ConeLeg _) = error "Cannot compose a cone leg with a cone point identity"
        (@) (ConeLeg o) ConePointIdentity = ConeLeg o
        (@) ConePointIdentity ConePointIdentity = ConePointIdentity

                                    
        source (OriginalMorphism m) = OriginalObject (source m)
        source (ConeLeg _) = ConePoint
        source ConePointIdentity = ConePoint
        target (OriginalMorphism m) = OriginalObject (target m)
        target (ConeLeg o) = OriginalObject o
        target ConePointIdentity = ConePoint
    
    -- | The left cone category associated to a category.
    data LeftCone c m o = LeftCone c deriving (Eq, Show)
    
    instance (PrettyPrintable c) => PrettyPrintable (LeftCone c m o) where
        pprint (LeftCone cat) = "Left cone of "++pprint cat
    
    instance (FiniteCategory c m o, Morphism m o) => FiniteCategory (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o) where
        ob (LeftCone cat) = ConePoint: (OriginalObject <$> (ob cat))
        
        identity (LeftCone cat) (OriginalObject o) = OriginalMorphism (identity cat o)
        identity (LeftCone cat) ConePoint = ConePointIdentity
        
        ar (LeftCone cat) (OriginalObject s) (OriginalObject t) = OriginalMorphism <$> ar cat s t
        ar (LeftCone cat) (OriginalObject s) ConePoint = []
        ar (LeftCone cat) ConePoint (OriginalObject t) = [ConeLeg t]
        ar (LeftCone cat) ConePoint ConePoint = [ConePointIdentity]
        
    instance (GeneratedFiniteCategory c m o, Morphism m o) => GeneratedFiniteCategory (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o) where
        genAr (LeftCone cat) (OriginalObject s) (OriginalObject t) = OriginalMorphism <$> genAr cat s t
        genAr (LeftCone cat) (OriginalObject s) ConePoint = []
        genAr (LeftCone cat) ConePoint (OriginalObject t) = [ConeLeg t]
        genAr (LeftCone cat) ConePoint ConePoint = [ConePointIdentity]
        
        decompose (LeftCone cat) (OriginalMorphism m) = OriginalMorphism <$> (decompose cat m)
        decompose (LeftCone cat) (ConeLeg o) = [ConeLeg o]
        decompose (LeftCone cat) ConePointIdentity = [ConePointIdentity]
    
    -- | Inclusion functor from a category to its left cone category.
    inclusionFunctor :: (FiniteCategory c m o, Morphism m o) => LeftCone c m o -> Diagram c m o (LeftCone c m o) (LeftConeMorphism m o) (LeftConeObject o)
    inclusionFunctor lc@(LeftCone cat) = Diagram{ src=cat
                                                , tgt=lc
                                                , omap=functToAssocList OriginalObject (ob cat)
                                                , mmap=functToAssocList OriginalMorphism (arrows cat)
                                                }
    
    -- | The category of cones defined according to the left cone definition.
    --
    -- It is less efficient than the `ConeCategory.ConeCategory` implementation. This is only defined for pedagogical purposes.
    data ConeCategory c1 m1 o1 c2 m2 o2 =  ConeCategory (Diagram c1 m1 o1 c2 m2 o2) deriving (Eq, Show)
    
    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) => FiniteCategory 
        (ConeCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2)
        (Diagram (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2) where
        ob (ConeCategory diag) = [s | s <- ob FunctorCategory{sourceCat = lcone, targetCat = tgt diag}, s `composeDiag` (inclusionFunctor lcone) == diag]
            where lcone = LeftCone (src diag)
        
        identity (ConeCategory diag) cone = identity FunctorCategory{sourceCat = LeftCone (src diag), targetCat = tgt diag} cone
        
        ar (ConeCategory diag) cone1 cone2 = [nt | nt <- ar functCat cone1 cone2, preWhiskering nt (inclusionFunctor lcone) == (identity functCatDiag diag)]
            where 
                lcone =  LeftCone (src diag)
                functCat = FunctorCategory{sourceCat = lcone, targetCat = tgt diag}
                functCatDiag = FunctorCategory{sourceCat = src diag, targetCat = tgt diag}
        
    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) => GeneratedFiniteCategory 
        (ConeCategory c1 m1 o1 c2 m2 o2)
        (NaturalTransformation (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2)
        (Diagram (LeftCone c1 m1 o1) (LeftConeMorphism m1 o1) (LeftConeObject o1) c2 m2 o2) where
        genAr (ConeCategory diag) cone1 cone2 = genAr FunctorCategory{sourceCat = LeftCone (src diag), targetCat = tgt diag} cone1 cone2
        decompose (ConeCategory diag) cone = decompose FunctorCategory{sourceCat = LeftCone (src diag), targetCat = tgt diag} cone