{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE MonadComprehensions  #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}

{-| Module  : FiniteCategories
Description : A 'LimitCategory' is the category in which lives the limit of a diagram in 'FinCat'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'LimitCategory' is the category in which the limit of a diagram in 'FinCat' lives. To compute limits in a usual category, see Math.CompleteCategory. To compute limits in a custom 'FiniteCategory', see 'limits' in Math.ConeCategory.
-}

module Math.FiniteCategories.LimitCategory
(
    -- * Limit category
    LimitCategory(..),
    
)
where
    import              Data.WeakSet             (Set)
    import qualified    Data.WeakSet           as Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap             (Map)
    import qualified    Data.WeakMap           as Map
    import              Data.WeakMap.Safe
    import              Data.List               (intercalate)
    import              Data.Simplifiable
    
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.CompleteCategory
    import              Math.CartesianClosedCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.IO.PrettyPrint
    
    import              GHC.Generics
    
    
        
    instance (Morphism m o, Eq m, Eq oIndex) => Morphism (Limit oIndex m) (Limit oIndex o) where
        source (Projection m) = Projection (source m)
        source (ProductElement tuple) = ProductElement (source <$> tuple)
        target (Projection m) = Projection (target m)
        target (ProductElement tuple) = ProductElement (target <$> tuple)
        (Projection m2) @ (Projection m1) = Projection $ m2 @ m1
        (ProductElement tuple2) @ (ProductElement tuple1) = ProductElement $ weakMapFromSet [(k1,(tuple2 |!| k1) @ v1) | (k1,v1) <- Map.mapToSet tuple1]
        _ @ _ = error "Incompatible composition of Limit morphisms."
    
    -- | A 'LimitCategory' is either a 'ProjectedCategory' (an original category) or a 'LimitCategory'.
    data LimitCategory cIndex mIndex oIndex c m o = ProjectedCategory c -- ^ An original category in 'FinCat' with the indexing object of the category.
                                                  | LimitCategory (Diagram cIndex mIndex oIndex (FinCat c m o) (FinFunctor c m o) c)     -- ^ The limit category of a given 'Diagram'.
        deriving (Eq, Show, Generic, Simplifiable, PrettyPrint)    

    
    instance (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex,
              Category c m o, Morphism m o, Eq m, Eq o) => Category (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o) where
        identity (ProjectedCategory c) (Projection o) = Projection $ identity c o
        identity (LimitCategory _) (Projection _) = error "Identity in a limit category on a projected object."
        identity (ProjectedCategory _) (ProductElement _) = error "Identity in a projected category on a limit object."
        identity (LimitCategory diag) (ProductElement tupleObj) 
            | topObjects /= domain tupleObj = error "Identity in a limit category on a limit object with different indexing objects."
            | otherwise = ProductElement $ weakMapFromSet [(k,identity (diag ->$ k) (tupleObj |!| k)) | k <- topObjects]
            where
                idxCat = (src diag)
                topObjects = Set.filter (\o -> Set.and [not $ Set.null $ ar idxCat o (source m) | m <- arTo idxCat o]) (ob idxCat)
         
        ar (ProjectedCategory c) (Projection s) (Projection t) = Projection <$> ar c s t
        ar (ProjectedCategory _) (Projection _) (ProductElement _) = error "Ar in a projected category where the target is a limit object."
        ar (ProjectedCategory _) (ProductElement _) (Projection _) = error "Ar in a projected category where the source is a limit object."
        ar (ProjectedCategory _) (ProductElement _) (ProductElement _) = error "Ar in a projected category where the source and the target are limit objects."
        ar (LimitCategory _) (Projection _) (Projection _) = error "Ar in a limit category where the source and target are projected objects."
        ar (LimitCategory _) (Projection _) (ProductElement _) = error "Ar in a limit category where the source is a projected object."
        ar (LimitCategory _) (ProductElement _) (Projection _) = error "Ar in a limit category where the target is a projected object."
        ar (LimitCategory diag) (ProductElement tupleSource) (ProductElement tupleTarget)
            | topObjects /= domain tupleSource || topObjects /= domain tupleTarget = error "Ar in a limit category where the source and target limit objects don't have the same indexing objects."
            | otherwise = Set.filter filterProduct products
            where
                products = ProductElement <$> weakMap <$> cartesianProductOfSets [(\x -> (k,x)) <$> ar (diag ->$ k) (tupleSource |!| k) (tupleTarget |!| k) | k <- Set.setToList topObjects]
                idxCat = (src diag)
                topObjects = Set.filter (\o -> Set.and [not $ Set.null $ ar idxCat o (source m) | m <- arTo idxCat o]) (ob idxCat)
                objectToAMorphismFromATopObject o
                    | o `Set.elem` topObjects = identity idxCat o
                    | otherwise = anElement [m | m <- arTo idxCat o, source m `Set.elem` topObjects]
                filterProduct (ProductElement tupleMorph) = Set.and [(diag ->£ (objectToAMorphismFromATopObject i)) ->£ (tupleMorph |!| (source $ objectToAMorphismFromATopObject i)) == (diag ->£ m) ->£ (tupleMorph |!| (source $ m)) | i <- (ob idxCat), s <- topObjects, m <- arWithoutId idxCat s (target $ objectToAMorphismFromATopObject i)]
            
            
    instance (FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq mIndex, Eq oIndex,
              FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FiniteCategory (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o) where
        ob (ProjectedCategory cat) = Projection <$> ob cat
        ob (LimitCategory diag) = Set.filter filterProduct products
            where
                products = ProductElement <$> weakMap <$> cartesianProductOfSets (Set.setToList [(\x -> (k,x)) <$> ob (diag ->$ k) | k <- topObjects])
                idxCat = (src diag)
                topObjects = Set.filter (\o -> Set.and [not $ Set.null $ ar idxCat o (source m) | m <- arTo idxCat o]) (ob idxCat)
                objectToAMorphismFromATopObject o
                    | o `Set.elem` topObjects = identity idxCat o
                    | otherwise = anElement [m | m <- arTo idxCat o, source m `Set.elem` topObjects]
                filterProduct (ProductElement tupleObj) = Set.and [(diag ->£ (objectToAMorphismFromATopObject i)) ->$ (tupleObj |!| (source $ objectToAMorphismFromATopObject i)) == (diag ->£ m) ->$ (tupleObj |!| (source $ m)) | i <- (ob idxCat), s <- topObjects, m <- arWithoutId idxCat s (target $ objectToAMorphismFromATopObject i)]
    
    instance (FiniteCategory c m o, Morphism m o, Eq c, Eq m, Eq o,
              FiniteCategory cIndex mIndex oIndex, Morphism mIndex oIndex, Eq cIndex, Eq mIndex, Eq oIndex) => 
        CompleteCategory (FinCat c m o) (FinFunctor c m o) c (FinCat (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (FinFunctor (LimitCategory cIndex mIndex oIndex c m o) (Limit oIndex m) (Limit oIndex o)) (LimitCategory cIndex mIndex oIndex c m o) cIndex mIndex oIndex where
        
        limit diag = unsafeCone apex nat
            where
                apex = LimitCategory diag
                newDiag = Diagram {src = src diag, tgt = FinCat, omap = newOmap, mmap = newMmap}
                newOmap = Map.weakMapFromSet [(k, ProjectedCategory v) | (k,v) <- (Map.mapToSet $ omap diag)]
                newMmap = Map.weakMapFromSet [(k, transformDiagramToProjectedDiagram v) | (k,v) <- (Map.mapToSet $ mmap diag)]
                transformDiagramToProjectedDiagram diag_ = Diagram{src = ProjectedCategory (src diag_), tgt = ProjectedCategory (tgt diag_), omap = transformOmapToProjectedOmap (omap diag_), mmap = transformMmapToProjectedMmap (mmap diag_)}
                transformOmapToProjectedOmap om = Map.weakMapFromSet [(Projection o1, Projection o2) | (o1,o2) <- (Map.mapToSet om)]
                transformMmapToProjectedMmap mm = Map.weakMapFromSet [(Projection m1, Projection m2) | (m1,m2) <- (Map.mapToSet mm)]
                nat = unsafeNaturalTransformation (constantDiagram (src diag) FinCat apex) newDiag components_
                components_ = Map.weakMapFromSet [(oIndex, leg oIndex) | oIndex <- (ob.src $ diag)]
                idxCat = (src diag)
                topObjects = Set.filter (\o -> Set.and [not $ Set.null $ ar idxCat o (source m) | m <- arTo idxCat o]) (ob idxCat)
                objectToAMorphismFromATopObject o
                    | o `Set.elem` topObjects = identity idxCat o
                    | otherwise = anElement [m | m <- arTo idxCat o, source m `Set.elem` topObjects]
                leg oIndex = Diagram{src = apex, tgt = ProjectedCategory (diag ->$ oIndex), omap = Map.weakMapFromSet [(tuple, (Projection ((diag ->£ (objectToAMorphismFromATopObject oIndex)) ->$ ((extractProductObj tuple) |!| (source (objectToAMorphismFromATopObject oIndex)))))) | tuple <- ob apex], mmap = Map.weakMapFromSet [(tuple, (Projection ((diag ->£ (objectToAMorphismFromATopObject oIndex)) ->£ ((extractProductMorph tuple) |!| (source (objectToAMorphismFromATopObject oIndex)))))) | tuple <- arrows apex]}
                extractProductObj (ProductElement m) = m  
                extractProductMorph (ProductElement m) = m

        projectBase diag = newDiag
            where
                newDiag = Diagram {src = FinCat, tgt = FinCat, omap = newOmap, mmap = newMmap}
                newOmap = Map.weakMapFromSet [(v, ProjectedCategory v) | (k,v) <- (Map.mapToSet $ omap diag)]
                newMmap = Map.weakMapFromSet [(v, transformDiagramToProjectedDiagram v) | (k,v) <- (Map.mapToSet $ mmap diag)]
                transformDiagramToProjectedDiagram diag_ = Diagram{src = ProjectedCategory (src diag_), tgt = ProjectedCategory (tgt diag_), omap = transformOmapToProjectedOmap (omap diag_), mmap = transformMmapToProjectedMmap (mmap diag_)}
                transformOmapToProjectedOmap om = Map.weakMapFromSet [(Projection o1, Projection o2) | (o1,o2) <- (Map.mapToSet om)]
                transformMmapToProjectedMmap mm = Map.weakMapFromSet [(Projection m1, Projection m2) | (m1,m2) <- (Map.mapToSet mm)]