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

{-| Module  : FiniteCategories
Description : Selecting a full subcategory yields a finite category.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Selecting a 'FullSubcategory' in a 'Category' yields a 'FiniteCategory'.

We have to forget the generating set of morphisms of the original 'Category' as the generators are not always inheritable (see for example the full subcategory of __'Square'__ containing the objects A and D).

If the generators are inheritable, you can use the constructor 'InheritedFullSubcategory' to inherit the generators of the original 'Category'.
-}

module Math.FiniteCategories.FullSubcategory 
(
    FullSubcategory(..),
    InheritedFullSubcategory(..),
)
where
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint
    
    import              Data.WeakSet            (Set)
    import qualified    Data.WeakSet        as  Set
    import              Data.WeakSet.Safe
    import              Data.Simplifiable
    
    import              GHC.Generics
    
    -- | A 'FullSubcategory' needs an original category and a set of objects to select in the category.

    --

    -- The generators are forgotten, use 'InheritedFullSubcategory' if the generators are inheritable.

    data FullSubcategory c m o = FullSubcategory c (Set 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
$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
/= :: 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
$cshowsPrec :: forall c m o.
(Show c, Show o) =>
Int -> FullSubcategory c m o -> ShowS
showsPrec :: Int -> FullSubcategory c m o -> ShowS
$cshow :: forall c m o. (Show c, Show o) => FullSubcategory c m o -> String
show :: FullSubcategory c m o -> String
$cshowList :: forall c m o. (Show c, Show o) => [FullSubcategory c m o] -> ShowS
showList :: [FullSubcategory c m o] -> ShowS
Show, (forall x. FullSubcategory c m o -> Rep (FullSubcategory c m o) x)
-> (forall x.
    Rep (FullSubcategory c m o) x -> FullSubcategory c m o)
-> Generic (FullSubcategory c m o)
forall x. Rep (FullSubcategory c m o) x -> FullSubcategory c m o
forall x. FullSubcategory c m o -> Rep (FullSubcategory c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (FullSubcategory c m o) x -> FullSubcategory c m o
forall c m o x.
FullSubcategory c m o -> Rep (FullSubcategory c m o) x
$cfrom :: forall c m o x.
FullSubcategory c m o -> Rep (FullSubcategory c m o) x
from :: forall x. FullSubcategory c m o -> Rep (FullSubcategory c m o) x
$cto :: forall c m o x.
Rep (FullSubcategory c m o) x -> FullSubcategory c m o
to :: forall x. Rep (FullSubcategory c m o) x -> FullSubcategory c m o
Generic, Int -> Int -> String -> FullSubcategory c m o -> String
Int -> FullSubcategory c m o -> String
(Int -> FullSubcategory c m o -> String)
-> (Int -> Int -> String -> FullSubcategory c m o -> String)
-> (Int -> FullSubcategory c m o -> String)
-> PrettyPrint (FullSubcategory c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> Int -> String -> FullSubcategory c m o -> String
forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> FullSubcategory c m o -> String
$cpprint :: forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> FullSubcategory c m o -> String
pprint :: Int -> FullSubcategory c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> Int -> String -> FullSubcategory c m o -> String
pprintWithIndentations :: Int -> Int -> String -> FullSubcategory c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> FullSubcategory c m o -> String
pprintIndent :: Int -> FullSubcategory c m o -> String
PrettyPrint, FullSubcategory c m o -> FullSubcategory c m o
(FullSubcategory c m o -> FullSubcategory c m o)
-> Simplifiable (FullSubcategory c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable c, Simplifiable o, Eq o) =>
FullSubcategory c m o -> FullSubcategory c m o
$csimplify :: forall c m o.
(Simplifiable c, Simplifiable o, Eq o) =>
FullSubcategory c m o -> FullSubcategory c m o
simplify :: FullSubcategory c m o -> FullSubcategory c m o
Simplifiable)
    
    instance (Category c m o, Eq o) => Category (FullSubcategory c m o) m o where
        identity :: Morphism m o => FullSubcategory c m o -> o -> m
identity (FullSubcategory c
c Set o
objs) o
o
            | o
o o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
            | Bool
otherwise = String -> m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.FullSubcategory.identity: object not in the subcategory"
        ar :: Morphism m o => FullSubcategory c m o -> o -> o -> Set m
ar (FullSubcategory c
c Set o
objs) o
s o
t
            | o
s o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& o
t o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
            | Bool
otherwise = String -> Set m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.FullSubcategory.ar: source or target not in the subcategory"
    
    instance (Category c m o, Eq o) => FiniteCategory (FullSubcategory c m o) m o where
        ob :: FullSubcategory c m o -> Set o
ob (FullSubcategory c
_ Set o
s) = Set o
s

        
    -- | An 'InheritedFullSubcategory' is a 'FullSubcategory' where the generators are the same as in the original 'Category'.

    data InheritedFullSubcategory c m o = InheritedFullSubcategory c (Set o) deriving (InheritedFullSubcategory c m o
-> InheritedFullSubcategory c m o -> Bool
(InheritedFullSubcategory c m o
 -> InheritedFullSubcategory c m o -> Bool)
-> (InheritedFullSubcategory c m o
    -> InheritedFullSubcategory c m o -> Bool)
-> Eq (InheritedFullSubcategory c m o)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c m o.
(Eq c, Eq o) =>
InheritedFullSubcategory c m o
-> InheritedFullSubcategory c m o -> Bool
$c== :: forall c m o.
(Eq c, Eq o) =>
InheritedFullSubcategory c m o
-> InheritedFullSubcategory c m o -> Bool
== :: InheritedFullSubcategory c m o
-> InheritedFullSubcategory c m o -> Bool
$c/= :: forall c m o.
(Eq c, Eq o) =>
InheritedFullSubcategory c m o
-> InheritedFullSubcategory c m o -> Bool
/= :: InheritedFullSubcategory c m o
-> InheritedFullSubcategory c m o -> Bool
Eq, Int -> InheritedFullSubcategory c m o -> ShowS
[InheritedFullSubcategory c m o] -> ShowS
InheritedFullSubcategory c m o -> String
(Int -> InheritedFullSubcategory c m o -> ShowS)
-> (InheritedFullSubcategory c m o -> String)
-> ([InheritedFullSubcategory c m o] -> ShowS)
-> Show (InheritedFullSubcategory c m o)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall c m o.
(Show c, Show o) =>
Int -> InheritedFullSubcategory c m o -> ShowS
forall c m o.
(Show c, Show o) =>
[InheritedFullSubcategory c m o] -> ShowS
forall c m o.
(Show c, Show o) =>
InheritedFullSubcategory c m o -> String
$cshowsPrec :: forall c m o.
(Show c, Show o) =>
Int -> InheritedFullSubcategory c m o -> ShowS
showsPrec :: Int -> InheritedFullSubcategory c m o -> ShowS
$cshow :: forall c m o.
(Show c, Show o) =>
InheritedFullSubcategory c m o -> String
show :: InheritedFullSubcategory c m o -> String
$cshowList :: forall c m o.
(Show c, Show o) =>
[InheritedFullSubcategory c m o] -> ShowS
showList :: [InheritedFullSubcategory c m o] -> ShowS
Show, (forall x.
 InheritedFullSubcategory c m o
 -> Rep (InheritedFullSubcategory c m o) x)
-> (forall x.
    Rep (InheritedFullSubcategory c m o) x
    -> InheritedFullSubcategory c m o)
-> Generic (InheritedFullSubcategory c m o)
forall x.
Rep (InheritedFullSubcategory c m o) x
-> InheritedFullSubcategory c m o
forall x.
InheritedFullSubcategory c m o
-> Rep (InheritedFullSubcategory c m o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall c m o x.
Rep (InheritedFullSubcategory c m o) x
-> InheritedFullSubcategory c m o
forall c m o x.
InheritedFullSubcategory c m o
-> Rep (InheritedFullSubcategory c m o) x
$cfrom :: forall c m o x.
InheritedFullSubcategory c m o
-> Rep (InheritedFullSubcategory c m o) x
from :: forall x.
InheritedFullSubcategory c m o
-> Rep (InheritedFullSubcategory c m o) x
$cto :: forall c m o x.
Rep (InheritedFullSubcategory c m o) x
-> InheritedFullSubcategory c m o
to :: forall x.
Rep (InheritedFullSubcategory c m o) x
-> InheritedFullSubcategory c m o
Generic, Int -> Int -> String -> InheritedFullSubcategory c m o -> String
Int -> InheritedFullSubcategory c m o -> String
(Int -> InheritedFullSubcategory c m o -> String)
-> (Int
    -> Int -> String -> InheritedFullSubcategory c m o -> String)
-> (Int -> InheritedFullSubcategory c m o -> String)
-> PrettyPrint (InheritedFullSubcategory c m o)
forall a.
(Int -> a -> String)
-> (Int -> Int -> String -> a -> String)
-> (Int -> a -> String)
-> PrettyPrint a
forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> Int -> String -> InheritedFullSubcategory c m o -> String
forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> InheritedFullSubcategory c m o -> String
$cpprint :: forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> InheritedFullSubcategory c m o -> String
pprint :: Int -> InheritedFullSubcategory c m o -> String
$cpprintWithIndentations :: forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> Int -> String -> InheritedFullSubcategory c m o -> String
pprintWithIndentations :: Int -> Int -> String -> InheritedFullSubcategory c m o -> String
$cpprintIndent :: forall c m o.
(PrettyPrint c, PrettyPrint o, Eq o) =>
Int -> InheritedFullSubcategory c m o -> String
pprintIndent :: Int -> InheritedFullSubcategory c m o -> String
PrettyPrint, InheritedFullSubcategory c m o -> InheritedFullSubcategory c m o
(InheritedFullSubcategory c m o -> InheritedFullSubcategory c m o)
-> Simplifiable (InheritedFullSubcategory c m o)
forall a. (a -> a) -> Simplifiable a
forall c m o.
(Simplifiable c, Simplifiable o, Eq o) =>
InheritedFullSubcategory c m o -> InheritedFullSubcategory c m o
$csimplify :: forall c m o.
(Simplifiable c, Simplifiable o, Eq o) =>
InheritedFullSubcategory c m o -> InheritedFullSubcategory c m o
simplify :: InheritedFullSubcategory c m o -> InheritedFullSubcategory c m o
Simplifiable)
    
    instance (Category c m o, Eq o) => Category (InheritedFullSubcategory c m o) m o where
        identity :: Morphism m o => InheritedFullSubcategory c m o -> o -> m
identity (InheritedFullSubcategory c
c Set o
objs) o
o
            | o
o o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity c
c o
o
            | Bool
otherwise = String -> m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedFullSubcategory.identity: object not in the subcategory"
        ar :: Morphism m o => InheritedFullSubcategory c m o -> o -> o -> Set m
ar (InheritedFullSubcategory c
c Set o
objs) o
s o
t
            | o
s o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& o
t o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
ar c
c o
s o
t
            | Bool
otherwise = String -> Set m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedFullSubcategory.ar: source or target not in the subcategory"
        genAr :: Morphism m o => InheritedFullSubcategory c m o -> o -> o -> Set m
genAr (InheritedFullSubcategory c
c Set o
objs) o
s o
t
            | o
s o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& o
t o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> o -> o -> Set m
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr c
c o
s o
t
            | Bool
otherwise = String -> Set m
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedFullSubcategory.genAr: source or target not in the subcategory"
        decompose :: Morphism m o => InheritedFullSubcategory c m o -> m -> [m]
decompose (InheritedFullSubcategory c
c Set o
objs) m
m
            | m -> o
forall m o. Morphism m o => m -> o
source m
m o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs Bool -> Bool -> Bool
&& m -> o
forall m o. Morphism m o => m -> o
target m
m o -> Set o -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set o
objs = c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
c m
m
            | Bool
otherwise = String -> [m]
forall a. HasCallStack => String -> a
error String
"Math.FiniteCategories.InheritedFullSubcategory.decompose: morphism not in the subcategory"
        
    instance (Category c m o, Eq o) => FiniteCategory (InheritedFullSubcategory c m o) m o where
        ob :: InheritedFullSubcategory c m o -> Set o
ob (InheritedFullSubcategory c
_ Set o
s) = Set o
s