{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Full subcategory a category C.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Full subcategory a category C.
-}
module Subcategories.FullSubcategory
(
FullSubcategory(..)
)
where
    import FiniteCategory.FiniteCategory
    import Data.List (nub)
    import Utils.SetList
    import IO.PrettyPrint
    
    -- | The datatype for full subcategories of a given category containing given objects.

    data FullSubcategory c m o = FullSubcategory c [o] deriving (FullSubcategory c m o -> FullSubcategory c m o -> Bool
(FullSubcategory c m o -> FullSubcategory c m o -> Bool)
-> (FullSubcategory c m o -> FullSubcategory c m o -> Bool)
-> Eq (FullSubcategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq o) =>
FullSubcategory c m o -> FullSubcategory c m o -> Bool
/= :: FullSubcategory c m o -> FullSubcategory c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq o) =>
FullSubcategory c m o -> FullSubcategory c m o -> Bool
== :: FullSubcategory c m o -> FullSubcategory c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq o) =>
FullSubcategory c m o -> FullSubcategory c m o -> Bool
Eq, Int -> FullSubcategory c m o -> ShowS
[FullSubcategory c m o] -> ShowS
FullSubcategory c m o -> String
(Int -> FullSubcategory c m o -> ShowS)
-> (FullSubcategory c m o -> String)
-> ([FullSubcategory c m o] -> ShowS)
-> Show (FullSubcategory c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show c, Show o) =>
Int -> FullSubcategory c m o -> ShowS
forall c m o. (Show c, Show o) => [FullSubcategory c m o] -> ShowS
forall c m o. (Show c, Show o) => FullSubcategory c m o -> String
showList :: [FullSubcategory c m o] -> ShowS
$cshowList :: forall c m o. (Show c, Show o) => [FullSubcategory c m o] -> ShowS
show :: FullSubcategory c m o -> String
$cshow :: forall c m o. (Show c, Show o) => FullSubcategory c m o -> String
showsPrec :: Int -> FullSubcategory c m o -> ShowS
$cshowsPrec :: forall c m o.
(Show c, Show o) =>
Int -> FullSubcategory c m o -> ShowS
Show)
    
    instance (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FiniteCategory (FullSubcategory c m o) m o where
        ob :: FullSubcategory c m o -> [o]
ob (FullSubcategory c
_ [o]
objs) = [o] -> [o]
forall a. Eq a => [a] -> [a]
nub ([o] -> [o]) -> [o] -> [o]
forall a b. (a -> b) -> a -> b
$ [o]
objs
        identity :: Morphism m o => FullSubcategory c m o -> o -> m
identity (FullSubcategory c
c [o]
objs) o
obj = if o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o
obj [o]
objs then c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c o
obj else String -> m
forall a. HasCallStack => String -> a
error String
"Cannot create identity of an object not in the category."
        ar :: Morphism m o => FullSubcategory c m o -> o -> o -> [m]
ar (FullSubcategory c
c [o]
objs) o
s o
t = if o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o
s [o]
objs Bool -> Bool -> Bool
&& o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o
t [o]
objs then c -> o -> o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
ar c
c o
s o
t else String -> [m]
forall a. HasCallStack => String -> a
error String
"Cannot create morphisms between objects not in the category."
        
    instance (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => GeneratedFiniteCategory (FullSubcategory c m o) m o where
        genAr :: Morphism m o => FullSubcategory c m o -> o -> o -> [m]
genAr = FullSubcategory c m o -> o -> o -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> o -> o -> [m]
defaultGenAr
        decompose :: Morphism m o => FullSubcategory c m o -> m -> [m]
decompose = FullSubcategory c m o -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o) =>
c -> m -> [m]
defaultDecompose
        
    instance (PrettyPrintable c, PrettyPrintable o) => PrettyPrintable (FullSubcategory c m o) where
        pprint :: FullSubcategory c m o -> String
pprint (FullSubcategory c
c [o]
o) = String
"Full subcategory of "String -> ShowS
forall a. [a] -> [a] -> [a]
++c -> String
forall a. PrettyPrintable a => a -> String
pprint c
cString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" containing "String -> ShowS
forall a. [a] -> [a] -> [a]
++[o] -> String
forall a. PrettyPrintable a => a -> String
pprint [o]
o