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

{-| Module  : FiniteCategories
Description : The __'FinSet'__ category has finite sets as objects and functions as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'FinSet'__ category has finite sets as objects and functions as morphisms.

Finite sets are represented by weak sets from Data.WeakSet and functions by enriched weak maps from Data.WeakMap.

These structures are homogeneous, meaning you can only have sets containing one type of objects in a given 'FinSet' category.

See the category __'PureSet'__ for the category of sets which can be arbitrarily nested.
-}

module Math.Categories.FinSet
(
    -- * Function
    Function(..),
    (||!||),
    -- * __FinSet__
    FinSet(..),
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.FunctorCategory
    import              Math.FiniteCategories.DiscreteCategory
    import              Math.FiniteCategories.DiscreteTwo
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    import              Math.CartesianClosedCategory
    
    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           (nub)
    import              Data.Maybe          (fromJust)
    import              Data.Simplifiable
    
    import              GHC.Generics

    
    -- | A 'Function' (finite function) is a weak map enriched with a codomain.
    --
    -- We have to store the codomain to retrieve the target set of a morphism in __'FinSet'__.
    data Function a = Function 
                            {
                                function :: Map a a,
                                codomain :: Set a
                            }
                        deriving
                            (Eq, Show, Generic, Simplifiable)
    
    instance (PrettyPrint a, Eq a) => PrettyPrint (Function a) where
        pprint v a = pprint v (function a)
        
        -- pprintWithIndentations cv ov indent a = pprintWithIndentations cv ov indent (function a)
        
    instance (Eq a) => Morphism (Function a) (Set a) where
        source = domain.function
        target = codomain
        (@) f2 f1 = Function{function = (function f2) |.| (function f1), codomain = codomain f2}
            
    -- | A function to apply a 'Function' to an object in the domain of the 'Function'.
    (||!||) :: (Eq a) => Function a -> a -> a
    (||!||) f x = (function f) |!| x
    
    -- | __'FinSet'__ is the category of finite sets.
    data FinSet a = FinSet deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance (Eq a) => Category (FinSet a) (Function a) (Set a) where
        identity _ s = Function {function = idFromSet s, codomain = s}
        
        ar _ s t
            | Set.null s = set [Function{function = weakMap [], codomain = t}]
            | Set.null t = set []
            | otherwise = (\x -> Function{function = x, codomain = t}) <$> functions where
                domain = setToList s
                images = (t |^| (length domain))
                functions = weakMap <$> zip domain <$> images
                
    instance (Eq a, Eq oIndex) => HasProducts (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) oIndex where
        product discreteDiag = result
            where
                indexingCat = src discreteDiag
                prod = (ProductElement).weakMap <$> cartesianProductOfSets (setToList [(\x -> (i,x)) <$> (discreteDiag ->$ i) | i <- ob indexingCat])
                mapping i = memorizeFunction (\(ProductElement tuple) -> Projection (tuple |!| i)) prod
                constDiag = constantDiagram indexingCat FinSet prod
                transformObject x = [Projection e | e <- x]
                transformFunction Function{function = m, codomain = cod} = Function{function = weakMapFromSet [(Projection k, Projection v) | (k,v) <- Map.mapToSet m], codomain = transformObject cod}
                newDiag = Diagram{src = src discreteDiag, tgt = FinSet, omap = transformObject <$> (omap discreteDiag), mmap = transformFunction <$> (mmap discreteDiag)}
                result = unsafeCone prod (unsafeNaturalTransformation constDiag newDiag (weakMapFromSet [(i,Function {function=mapping i, codomain = newDiag ->$ i}) | i <- ob indexingCat]))
                
    instance (Eq a) => HasEqualizers (FinSet a) (Function a) (Set a) where
        equalize parallelDiag = result
            where
                equalizer = [e | e <- parallelDiag ->$ ParallelA, (parallelDiag ->£ ParallelF) ||!|| e == (parallelDiag ->£ ParallelG) ||!|| e]
                mapping i = memorizeFunction id equalizer
                constDiag = constantDiagram Parallel FinSet equalizer
                result = unsafeCone equalizer (unsafeNaturalTransformation constDiag parallelDiag (weakMap [(ParallelA,legA), (ParallelB, (parallelDiag ->£ ParallelF) @ legA) ]))
                legA = Function {function=mapping ParallelA, codomain = parallelDiag ->$ ParallelA}
    
    _projectMorphism m = Function{function = weakMapFromSet [(Projection k, Projection v) | (k,v) <- (Map.mapToSet.function) m], codomain = Projection <$> codomain m}
    
    instance (Eq a, Eq mIndex, Eq oIndex) => CompleteCategory (FinSet a) (Function a) (Set a) (FinSet (Limit oIndex a)) (Function (Limit oIndex a)) (Set (Limit oIndex a)) cIndex mIndex oIndex where
        limit = limitFromProductsAndEqualizers _projectMorphism
        
        projectBase diag = Diagram{src = FinSet, tgt = FinSet, omap = memorizeFunction (fmap Projection) (Map.values (omap diag)), mmap = memorizeFunction _projectMorphism (Map.values (mmap diag))}
        
    
    instance (Eq a, Eq oIndex) => HasCoproducts (FinSet a) (Function a) (Set a) (FinSet (Colimit oIndex a)) (Function (Colimit oIndex a)) (Set (Colimit oIndex a)) oIndex where
        coproduct discreteDiag = result
            where
                indexingCat = src discreteDiag
                coprod = Set.unions (setToList [CoproductElement i <$> (discreteDiag ->$ i) | i <- ob indexingCat])
                constDiag = constantDiagram indexingCat FinSet coprod
                transformObject x = [Coprojection e | e <- x]
                transformFunction Function{function = m, codomain = cod} = Function{function = weakMapFromSet [(Coprojection k, Coprojection v) | (k,v) <- Map.mapToSet m], codomain = transformObject cod}
                newDiag = Diagram{src = indexingCat, tgt = FinSet, omap = transformObject <$> (omap discreteDiag), mmap = transformFunction <$> (mmap discreteDiag)}
                mapping i = memorizeFunction (\(Coprojection x) -> CoproductElement i x) (newDiag ->$ i)
                result = unsafeCocone coprod (unsafeNaturalTransformation newDiag constDiag (weakMapFromSet [(i,Function {function=mapping i, codomain = coprod}) | i <- ob indexingCat]))
                
    instance (Eq a) => HasCoequalizers (FinSet a) (Function a) (Set a) where
        coequalize parallelDiag = result
            where
                glue x (s,mapping)
                    | (parallelDiag ->£ ParallelF) ||!|| x == (parallelDiag ->£ ParallelG) ||!|| x = (s,mapping)
                    | otherwise = (Set.delete ((parallelDiag ->£ ParallelF) ||!|| x) s, Map.adjust (const $ (parallelDiag ->£ ParallelG) ||!|| x) ((parallelDiag ->£ ParallelF) ||!|| x) mapping)
                (coequalizer,mapping) = Set.foldr glue ((parallelDiag ->$ ParallelB),memorizeFunction id (parallelDiag ->$ ParallelB)) (parallelDiag ->$ ParallelA) 
                constDiag = constantDiagram Parallel FinSet coequalizer
                result = unsafeCocone coequalizer (unsafeNaturalTransformation parallelDiag constDiag (weakMap [(ParallelA,Function {function=mapping, codomain = coequalizer} @ (parallelDiag ->£ ParallelF)), (ParallelB, Function {function=mapping, codomain = coequalizer}) ]))
                
    
    instance (Eq a, Eq mIndex, Eq oIndex) => CocompleteCategory (FinSet a) (Function a) (Set a) (FinSet (Colimit oIndex a)) (Function (Colimit oIndex a)) (Set (Colimit oIndex a)) cIndex mIndex oIndex where
        colimit = colimitFromCoproductsAndCoequalizers transformMorphismIntoColimMorphism
            where   
                transformMorphismIntoColimMorphism m = Function{function = weakMapFromSet [(Coprojection k, Coprojection v) | (k,v) <- (Map.mapToSet.function) m], codomain = Coprojection <$> codomain m}
                
        coprojectBase diag = Diagram{src = FinSet, tgt = FinSet, omap = memorizeFunction (fmap Coprojection) (Map.values (omap diag)), mmap = memorizeFunction transformMorphismIntoColimMorphism (Map.values (mmap diag))}
            where
                transformMorphismIntoColimMorphism m = Function{function = weakMapFromSet [(Coprojection k, Coprojection v) | (k,v) <- (Map.mapToSet.function) m], codomain = Coprojection <$> codomain m}
                
    instance (Eq a) => CartesianClosedCategory (FinSet a) (Function a) (Set a) (FinSet (TwoProduct a)) (Function (TwoProduct a)) (Set (TwoProduct a)) (FinSet (Cartesian a)) (Function (Cartesian a)) (Set (Cartesian a))  where
        internalHom twoBase = unsafeTripod twoLimit evalMap_
            where
                powerObject = [ExponentialElement (function m) | m <- ar FinSet (twoBase ->$ A) (twoBase ->$ B)]
                newInternalDomain = Exprojection <$> twoBase ->$ A
                baseTwoCone = completeDiagram Diagram{src = DiscreteTwo, tgt = FinSet, omap = weakMap [(A,powerObject),(B,newInternalDomain)], mmap = weakMap []}
                twoLimit = limit baseTwoCone
                eval tuple = (Projection (Exprojection $ m |!| x))
                    where
                        (ExponentialElement m) = tuple |!| A
                        (Exprojection x)  = tuple |!| B
                finalInternalCodomain = Projection <$> (Exprojection <$> twoBase ->$ A)
                evalMap_ = Function{function = Map.weakMapFromSet [(ProductElement tuple, eval tuple) | (ProductElement tuple) <- apex twoLimit], codomain = finalInternalCodomain}