{-# LANGUAGE MultiParamTypeClasses, MonadComprehensions #-}

{-| Module  : FiniteCategories
Description : A 'CommaCategory' is intuitively a category where objects are selected morphisms of another category /C/ and morphisms are selected commutative squares in /C/.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Each 'Category' has an opposite one where morphisms are reversed.

A 'CommaCategory' is intuitively a category where objects are selected morphisms of another category /C/ and morphisms are selected commutative squares in /C/.

More precisely, given two 'Diagram's @/T/ : /E/ -> /C/@ and @/S/ : /D/ -> /C/@, a `CommaObject` in the `CommaCategory` (/T/|/S/) is a triplet \<e,d,f\> where @f : /T/(e) -> /S/(d)@.

A `CommaMorphism` from \<e1,d1,f1\> to \<e2,d2,f2\> in the `CommaCategory` (/T/|/S/) is a couple \<k,h\> where @/T/(k) : /T/(e1) -> /T/(e2)@, @/S/(h) : /S/(d1) -> /S/(d2)@ such that @f2 \@ /T/(k) = /S/(h) \@ f1@.

See /Categories for the working mathematician/, Saunders Mac Lane, P.46.

If the category /C/ is a 'FiniteCategory', then the 'CommaCategory' of /C/ is also a 'FiniteCategory'. Otherwise it is only a 'Category'.
-}

module Math.Categories.CommaCategory
(
    -- * Comma object
    CommaObject,
    -- ** Getters
    indexSource,
    indexTarget,
    selectedArrow,
    -- ** Smart constructors
    commaObject,
    unsafeCommaObject,
    -- * Comma morphism
    CommaMorphism,
    -- ** Getters
    indexFirstArrow,
    indexSecondArrow,
    -- ** Smart constructors
    commaMorphism,
    unsafeCommaMorphism,
    CommaCategory(..),
    sliceCategory,
    cosliceCategory,
    arrowCategory, 
)
where
    import   qualified  Data.WeakSet        as Set
    import              Data.WeakSet          (Set)
    import              Data.WeakSet.Safe
    import   qualified  Data.WeakMap        as Map
    import              Data.WeakMap          (Map)
    import              Data.WeakMap.Safe
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.FinCat
    import              Math.Categories.FunctorCategory
    import              Math.FiniteCategories.One
    import              Math.IO.PrettyPrint
    
    -- | A `CommaObject` in the `CommaCategory` (/T/|/S/) is a triplet \<e,d,f\> where @f : /T/(e) -> /S/(d)@.
    --
    -- See "Categories for the working mathematician", Saunders Mac Lane, P.46.
    --
    -- The 'CommaObject' constructor is private, use the smart constructor 'commaObject' or the unsafe one 'unsafeCommaObject'.
    data CommaObject o1 o2 m3 = CommaObject { indexSource :: o1 -- ^ e, the indexing object of the source of the 'selectedArrow'.
                                            , indexTarget :: o2 -- ^ d, the indexing object of the target of the 'selectedArrow'.
                                            , selectedArrow :: m3 -- ^ f, the selected arrow of the target category.
                                            } deriving (Eq)
    
    instance (PrettyPrint o1, PrettyPrint o2, PrettyPrint m3) =>
             PrettyPrint (CommaObject o1 o2 m3) where
        pprint CommaObject{indexSource=e, indexTarget=d, selectedArrow=f} = "<"++pprint e++", "++pprint d++", "++pprint f++">"
        
    instance (Show o1, Show o2, Show m3) =>
            Show (CommaObject o1 o2 m3) where
        show CommaObject{indexSource=e, indexTarget=d, selectedArrow=f} = "(unsafeCommaObject ("++ show e ++ ") (" ++ show d ++ ") (" ++ show f ++ "))"        

    -- | Smart constructor of 'CommaObject' which checks the structure of the 'CommaObject'.
    commaObject :: (Morphism m3 o3, Eq o1, Eq o2, Eq o3) => Diagram c1 m1 o1 c3 m3 o3 -> Diagram c2 m2 o2 c3 m3 o3 -> o1 -> o2 -> m3 -> Maybe (CommaObject o1 o2 m3)
    commaObject d1 d2 iS iT arr
        | d1 ->$ iS == (source arr) && d2 ->$ iT == (target arr) = Just CommaObject{indexSource=iS, indexTarget=iT,selectedArrow=arr}
        | otherwise = Nothing
    
    -- | Unsafe way of constructing a 'CommaObject' : the structure of the 'CommaObject' 
    unsafeCommaObject :: o1 -> o2 -> m3 -> CommaObject o1 o2 m3
    unsafeCommaObject iS iT arr = CommaObject{indexSource=iS, indexTarget=iT,selectedArrow=arr}
        
    -- | A `CommaMorphism` from \<e1,d1,f1\> to \<e2,d2,f2\> in the `CommaCategory` (/T/|/S/) is a couple \<k,h\> where @/T/(k) : /T/(e1) -> /T/(e2)@, @/S/(h) : /S/(d1) -> /S/(d2)@ such that @f2 \@ /T/(k) = /S/(h) \@ f1@.
    --
    -- See "Categories for the working mathematician", Saunders Mac Lane, P.46.
    data CommaMorphism o1 o2 m1 m2 m3 = CommaMorphism {srcCM :: (CommaObject o1 o2 m3) -- ^ The source `CommaObject` (private, use 'source' instead).
                                                     , tgtCM :: (CommaObject o1 o2 m3) -- ^ The target `CommaObject`, (private, use 'target' instead).
                                                     , indexFirstArrow :: m1 -- ^ k, the indexing arrow of the first functor.
                                                     , indexSecondArrow :: m2} -- ^ h, the indexing arrow of the second functor.
                                                     deriving (Eq)
    
    -- | Smart constructor of 'CommaMorphism', checks the structure of the 'CommaMorphism' at construction.
    commaMorphism :: (Morphism m3 o3, Eq o1, Eq o2, Eq o3, Eq m1, Eq m2, Eq m3) => Diagram c1 m1 o1 c3 m3 o3 -> Diagram c2 m2 o2 c3 m3 o3 -> (CommaObject o1 o2 m3) -> (CommaObject o1 o2 m3) -> m1 -> m2 -> Maybe (CommaMorphism o1 o2 m1 m2 m3)
    commaMorphism d1 d2 s t firstArr secondArr
        | null m1 || null m2 || m1 /= m2 = Nothing
        | otherwise = Just CommaMorphism{srcCM=s, tgtCM=t, indexFirstArrow=firstArr, indexSecondArrow=secondArr}
        where
            m1 = (selectedArrow t) @? (d1 ->£ firstArr)
            m2 = (d2 ->£ secondArr) @? (selectedArrow s)
            
    -- | Unsafe constructor of 'CommaMorphism', does not check the structure of the 'CommaMorphism'.
    unsafeCommaMorphism :: (CommaObject o1 o2 m3) -> (CommaObject o1 o2 m3) -> m1 -> m2 -> CommaMorphism o1 o2 m1 m2 m3
    unsafeCommaMorphism s t firstArr secondArr = CommaMorphism{srcCM=s, tgtCM=t, indexFirstArrow=firstArr, indexSecondArrow=secondArr}
        
    instance (Show o1, Show o2, Show m1, Show m2, Show m3) => 
            Show (CommaMorphism o1 o2 m1 m2 m3) where
        show CommaMorphism{srcCM=s, tgtCM =t, indexFirstArrow=k, indexSecondArrow=h} = "(unsafeCommaMorphism ("++show s++") ("++show t++") ("++show k++") ("++show h++"))"
        
    instance (PrettyPrint m1, PrettyPrint m2) =>
              PrettyPrint (CommaMorphism o1 o2 m1 m2 m3) where
        pprint CommaMorphism{srcCM=_, tgtCM =_, indexFirstArrow=k, indexSecondArrow=h} = "<"++pprint k++", "++pprint h++">"
        
    instance (Morphism m1 o1, Morphism m2 o2, Eq o1, Eq o2, Eq m3) => Morphism (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        (@?) CommaMorphism{srcCM=s2,tgtCM=t2,indexFirstArrow=k2,indexSecondArrow=h2} CommaMorphism{srcCM=s1,tgtCM=t1,indexFirstArrow=k1,indexSecondArrow=h1}
            | t1 /= s2 = Nothing
            | null compoK = Nothing
            | null compoH = Nothing
            | otherwise = Just CommaMorphism{srcCM=s1,tgtCM=t2,indexFirstArrow=k,indexSecondArrow=h}
            where
                compoK = k2 @? k1
                Just k = compoK
                compoH = h2 @? h1
                Just h = compoH
        source = srcCM
        target = tgtCM
        
    -- | A `CommaCategory` is a couple (/T/|/S/) with /T/ and /S/ two diagrams with the same target.
    --
    -- See "Categories for the working mathematician", Saunders Mac Lane, P.46.
    data CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3 = CommaCategory {leftDiagram :: Diagram c1 m1 o1 c3 m3 o3 -- ^ /T/
                                                                 , rightDiagram :: Diagram c2 m2 o2 c3 m3 o3} -- ^ /S/
                                                    deriving (Eq, Show)
                                                    
    instance (Category c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
              Category c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2,
              Category c3 m3 o3, Morphism m3 o3, Eq m3, Eq o3) => Category (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        identity cc co = CommaMorphism{srcCM = co, tgtCM = co, indexFirstArrow = ((identity.src.leftDiagram $ cc) (indexSource co)), indexSecondArrow = ((identity.src.rightDiagram $ cc) (indexTarget co))}
        ar CommaCategory{leftDiagram = t, rightDiagram = s} obj1@CommaObject{indexSource=e1,indexTarget=d1,selectedArrow=f1} obj2@CommaObject{indexSource=e2,indexTarget=d2,selectedArrow=f2}
            = [CommaMorphism{srcCM=obj1,tgtCM=obj2,indexFirstArrow=k,indexSecondArrow=h}| k <- ar (src t) e1 e2, h <- ar (src s) d1 d2, f2 @ (t ->£ k) == (s ->£ h) @ f1]
            
        genAr CommaCategory{leftDiagram = t, rightDiagram = s} obj1@CommaObject{indexSource=e1,indexTarget=d1,selectedArrow=f1} obj2@CommaObject{indexSource=e2,indexTarget=d2,selectedArrow=f2}
            | d1 == d2 = [CommaMorphism{srcCM=obj1,tgtCM=obj2,indexFirstArrow=k,indexSecondArrow=identity (src s) d1}| k <- genAr (src t) e1 e2, f2 @ (t ->£ k) == f1]
            | e1 == e2 = [CommaMorphism{srcCM=obj1,tgtCM=obj2,indexFirstArrow=identity (src t) e1,indexSecondArrow=h}| h <- genAr (src s) d1 d2, f2 == (s ->£ h) @ f1]
            | otherwise = set []
            
        decompose cc cm
            | length hyp == 1 = hyp
            | otherwise = filter (isNotIdentity cc) hyp
            where
                hyp = decomposeHelper cc cm
                decomposeHelper cc@CommaCategory{leftDiagram = t, rightDiagram = s} cm@CommaMorphism{srcCM=xfy,tgtCM=x'gy',indexFirstArrow=h,indexSecondArrow=i}
                    | xfy == x'gy' = [identity cc xfy]
                    | indexTarget xfy == indexTarget x'gy' = resultT:(decompose cc (unsafeCommaMorphism xfy (source resultT) composeAboveH (identity (src s) (indexTarget xfy))))
                    | indexSource xfy == indexSource x'gy' = (decompose cc (unsafeCommaMorphism (target resultI) (target cm) (identity (src t) (indexSource xfy)) composeBelowI))++[resultI]
                    | otherwise = decompose cc (unsafeCommaMorphism (unsafeCommaObject (indexSource xfy) (indexTarget x'gy') (s ->£ i @ (selectedArrow xfy))) x'gy' h (identity (src s) (indexTarget x'gy'))) ++ decompose cc (unsafeCommaMorphism xfy (unsafeCommaObject (indexSource xfy) (indexTarget x'gy') (s ->£ i @ selectedArrow xfy)) (identity (src t) (indexSource xfy)) i)
                    where
                        decompH = decompose (src t) h ++ [identity (src t) (indexSource xfy)]
                        genH = head decompH
                        composeAboveH = compose.tail $ decompH
                        resultT = unsafeCommaMorphism (unsafeCommaObject (source genH) (indexTarget xfy) ((selectedArrow x'gy') @ (t ->£ genH))) x'gy' genH (identity (src s) (indexTarget xfy))
                        decompI = [identity (src s) (indexTarget x'gy')] ++ decompose (src s) i
                        genI = last decompI
                        composeBelowI = compose.init $ decompI
                        resultI = unsafeCommaMorphism xfy (unsafeCommaObject (indexSource xfy) (target genI) ((s ->£ genI) @ (selectedArrow xfy))) (identity (src t) (indexSource xfy)) genI
                
            
    instance (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, Eq m3, Eq o3) => FiniteCategory (CommaCategory c1 m1 o1 c2 m2 o2 c3 m3 o3) (CommaMorphism o1 o2 m1 m2 m3) (CommaObject o1 o2 m3) where
        ob CommaCategory{leftDiagram = t, rightDiagram = s} = [CommaObject{indexSource=e,indexTarget=d,selectedArrow=f}| e <- (ob (src t)), d <- (ob (src s)), f <- ar (tgt t) (t ->$ e) (s ->$ d)]
        
    
        
    -- | Construct the slice category of a category /C/ over an object /o/.
    --
    -- Return Nothing if the object is not in the category.
    sliceCategory :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => c -> o -> Maybe (CommaCategory c m o One One One c m o)
    sliceCategory c o
        | o `isIn` ob c = Just CommaCategory{leftDiagram=identity FinCat c, rightDiagram=selectObject c o}
        | otherwise = Nothing
        
    -- | Construct the coslice category of a category /C/ under an object /o/.
    
    -- Return Nothing if the object is not in the category.
    cosliceCategory :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => c -> o -> Maybe (CommaCategory One One One c m o c m o)
    cosliceCategory c o 
        | o `isIn` ob c = Just CommaCategory{leftDiagram=selectObject c o, rightDiagram=identity FinCat c}
        | otherwise = Nothing
        
    -- | Construct the arrow category of a category /C/.
    arrowCategory :: (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o) => c -> CommaCategory c m o c m o c m o
    arrowCategory c = CommaCategory{leftDiagram=identity FinCat c, rightDiagram=identity FinCat c}