{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies  #-}

{-| Module  : FiniteCategories
Description : A 'FiniteCategory' is a 'Category' where the objects can be enumerated.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'FiniteCategory' is a 'Category' where the objects can be enumerated.

This module exports Math.Category so that you only have to import one of them.
-}

module Math.FiniteCategory
(
    -- * FiniteCategory
    FiniteCategory(..),
    -- ** Morphism enumeration
    arrows,
    arFrom,
    arTo,
    arFrom2,
    arTo2,
    identities,
    -- ** Morphism predicates
    isEpic,
    isMonic,
    -- ** Object predicates
    isTerminal,
    isInitial,
    -- ** Find special objects
    terminalObjects,
    initialObjects,
    -- * Generated finite category
    -- ** Generator enumeration
    genArrows,
    genArFrom,
    genArTo,
    genArFrom2,
    genArTo2,
    -- ** Helper
    bruteForceDecompose,
    module Math.Category
)
where
    import              Data.WeakSet                (Set)
    import qualified    Data.WeakSet           as   Set
    import              Data.WeakSet.Safe
    import              Data.List                   (elemIndex)
    
    import              Math.Category
    
    import              Control.Monad               (join)
    
        
    -- | A 'FiniteCategory' is a 'Category' which allows to enumerate its objects.
    --
    -- It is assumed that the set of objects of the category is finite.
    class (Category c m o) => FiniteCategory c m o | c -> m, m -> o where
        -- | `ob` should return a set of objects.
        ob :: c -> Set o
            
    -- | `arrows` returns the set of all unique morphisms of a category.
    arrows :: (FiniteCategory c m o, Morphism m o) => c -> Set m
    arrows c = join $ ar c <$> ob c <*> ob c
        
    -- | `arTo` returns the set of morphisms going to a specified target.
    arTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    arTo c t = join $ (\s -> ar c s t) <$> ob c

    -- | `arTo2` same as `arTo` but for multiple targets.
    arTo2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    arTo2 c ts = join $ ar c <$> ob c <*> ts

    -- | `arFrom` returns the list of unique morphisms going from a specified source.
    arFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    arFrom c s = join $ ar c s <$> ob c

    -- | `arFrom2` same as `arFrom` but for multiple sources.
    arFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    arFrom2 c ss = join $ ar c <$> ss <*> ob c

    -- | Same as `arrows` but only returns the generators. @genArrows c@ should be included in @arrows c@.  
    genArrows :: (FiniteCategory c m o, Morphism m o) => c -> Set m
    genArrows c = join $ genAr c <$> ob c <*> ob c

    -- | Same as `arTo` but only returns the generators. @genArTo c t@ should be included in @arTo c t@.       
    genArTo :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    genArTo c t = join $ (\s -> genAr c s t) <$> ob c 
        
    -- | Same as `arTo2` but only returns the generators. @genArTo2 c (set [t])@ should be included in @arTo2 c (set [t])@.  
    genArTo2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    genArTo2 c ts = join $ (genAr c) <$> ob c <*> ts 
        
    -- | Same as `arFrom` but only returns the generators. @genArFrom c s@ should be included in @arFrom c s@.  
    genArFrom :: (FiniteCategory c m o, Morphism m o) => c -> o -> Set m
    genArFrom c s = join $ (genAr c s) <$> ob c 
        
    -- | Same as `arFrom2` but only returns the generators. @genArFrom2 c (set [s])@ should be included in @arFrom2 c (set [s])@.  
    genArFrom2 :: (FiniteCategory c m o, Morphism m o) => c -> Set o -> Set m
    genArFrom2 c ss = join $ genAr c <$> ss <*> ob c 

    -- | `identities` returns all the identities of a category.
    identities :: (FiniteCategory c m o, Morphism m o) => c -> Set m
    identities c = identity c <$> ob c
    
    -- | Return wether an object is initial in the category.
    isInitial :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Bool
    isInitial cat obj = let
                            morphisms t = setToList $ ar cat obj t
                            condition t = (not.null $ morphisms t) && (null.tail $ morphisms t) -- we avoid the usage of cardinal to test that the size of (ar cat obj t) is 1 for speed purposes
                        in
                            Set.and $ condition <$> ob cat 
    
    -- | Return the set of intial objects in a category.
    initialObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o
    initialObjects cat = Set.filter (isInitial cat) (ob cat)
    
    -- | Return wether an object is terminal in the category.
    isTerminal :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> o -> Bool
    isTerminal cat obj = let
                            morphisms s = setToList $ ar cat s obj
                            condition s = (not.null $ morphisms s) && (null.tail $ morphisms s) -- we avoid the usage of cardinal to test that the size of (ar cat s obj) is 1 for speed purposes
                        in
                            Set.and $ condition <$> ob cat 
        
    -- | Return the set of terminal objects in a category.
    terminalObjects :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Set o
    terminalObjects cat = Set.filter (isTerminal cat) (ob cat)
    
    -- | Return wether a morphism is a monomorphism.
    isMonic :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isMonic c f = and [f @ g /= f @ h || g == h| x <- setToList $ ob c, g <- setToList $ ar c x (source f), h <- setToList $ ar c x (source f)]
    
    -- | Return wether a morphism is an epimorphism.
    isEpic :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> m -> Bool
    isEpic c f = and [g @ f /= h @ f || g == h | x <- setToList $ ob c, g <- setToList $ ar c (target f) x, h <- setToList $ ar c (target f) x]
    
    -- | Helper function for `bruteForceDecompose`.
    bruteForce :: (FiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [[m]] -> [m]
    bruteForce c m l = if index == Nothing then bruteForce c m (concat (pathToAugmentedPaths <$> l)) else l !! i where
        index = elemIndex m (compose <$> l)
        Just i = index
        leavingMorph path = (setToList.(genArFrom c)) $ target.head $ path
        pathToAugmentedPaths path = (leavingMorph path) >>= (\x -> [(x:path)] )   
    
    -- | If `genAr` is implemented, we can find the decomposition of a morphism by bruteforce search (we compose every arrow until we get the morphism we want).
    --
    -- This method is meant to be used temporarly until a proper decompose method is implemented. (It is very slow.)
    bruteForceDecompose :: (FiniteCategory c m o, Morphism m o, Eq m) => c -> m -> [m]
    bruteForceDecompose c m = bruteForce c m ((:[]) <$> (setToList $ genArFrom c (source m)))