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

{-| Module  : FiniteCategories
Description : The __'Galaxy'__ category has every objects and no morphism other than identities.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'Galaxy'__ category has every objects and no morphism other than identities.

It is called __'Galaxy'__ because its underlying graph is composed of a lot of points with no arrow between them.

It is the biggest 'DiscreteCategory'.
-}

module Math.Categories.Galaxy
(
    StarIdentity(..),
    Galaxy(..),   
)
where
    import          Math.Category
    import          Math.IO.PrettyPrint
    
    import          Data.WeakSet.Safe
    import              Data.Simplifiable
    
    import          GHC.Generics
    
    -- | 'StarIdentity' is the identity of a star (an object) in a 'Galaxy'.
    data StarIdentity a = StarIdentity a deriving (Eq, Show, Generic, Simplifiable)
    
    instance Morphism (StarIdentity a) a where
        (StarIdentity x) @ _ = (StarIdentity x)
        source (StarIdentity x) = x
        target = source
    
    -- | The __'Galaxy'__ category has every objects and no morphism other than identities.
    data Galaxy a = Galaxy deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance (Eq a) => Category (Galaxy a) (StarIdentity a) a where
        identity _ = StarIdentity
        ar _ x y
            | x == y = set [StarIdentity x]
            | otherwise = set []
    
    instance (PrettyPrint a) => PrettyPrint (StarIdentity a) where
        pprint 0 _ = "Id"
        pprint v (StarIdentity x) = "Id_" ++ pprint (v-1) x
        
        -- pprintWithIndentations 0 ov indent _ = indentation ov indent ++ "Id\n"
        -- pprintWithIndentations cv ov indent (StarIdentity x) = indentation (ov - cv) indent ++ "Id_" ++ pprint (cv-1) x ++ "\n"