{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, 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
    
    -- | 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 (Eq, Show)
    
    instance (Category c m o, Eq o) => Category (FullSubcategory c m o) m o where
        identity (FullSubcategory c objs) o
            | o `isIn` objs = identity c o
            | otherwise = error "Math.FiniteCategories.FullSubcategory.identity: object not in the subcategory"
        ar (FullSubcategory c objs) s t
            | s `isIn` objs && t `isIn` objs = ar c s t
            | otherwise = error "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 _ s) = s
    
    instance (PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq o) => PrettyPrint (FullSubcategory c m o)  where
        pprint (FullSubcategory c s) = "FullSubcategory("++ pprint c ++ ","++ pprint 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 (Eq, Show)
    
    instance (Category c m o, Eq o) => Category (InheritedFullSubcategory c m o) m o where
        identity (InheritedFullSubcategory c objs) o
            | o `isIn` objs = identity c o
            | otherwise = error "Math.FiniteCategories.InheritedFullSubcategory.identity: object not in the subcategory"
        ar (InheritedFullSubcategory c objs) s t
            | s `isIn` objs && t `isIn` objs = ar c s t
            | otherwise = error "Math.FiniteCategories.InheritedFullSubcategory.ar: source or target not in the subcategory"
        genAr (InheritedFullSubcategory c objs) s t
            | s `isIn` objs && t `isIn` objs = genAr c s t
            | otherwise = error "Math.FiniteCategories.InheritedFullSubcategory.genAr: source or target not in the subcategory"
        decompose (InheritedFullSubcategory c objs) m
            | source m `isIn` objs && target m `isIn` objs = decompose c m
            | otherwise = error "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 _ s) = s
        
    instance (PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq o) => PrettyPrint (InheritedFullSubcategory c m o)  where
        pprint (InheritedFullSubcategory c s) = "InheritedFullSubcategory("++ pprint c ++ ","++ pprint s ++")"