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

{-| Module  : FiniteCategories
Description : A 'Subcategory' of a category /C/ is a category /D/ whose objects are objects in /C/ and whose morphisms are morphisms in /C/ with the same identities and composition of morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'Subcategory' of a category /C/ is a category /D/ whose objects are objects in /C/ and whose morphisms are morphisms in /C/ with the same identities and composition of morphisms.

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 'InheritedSubcategory' to inherit the generators of the original 'Category'.
-}

module Math.FiniteCategories.Subcategory
(
    -- * Subcategory
    Subcategory,
    -- ** Smart constructors
    unsafeSubcategory,
    subcategory,
    -- ** Getter
    originalCategory,
    -- ** Interaction with 'Diagram'
    embeddingToSubcategory,
    fullDiagram,
    fullNaturalTransformation,
    -- * InheritedSubcategory
    InheritedSubcategory,
    -- ** Smart constructors
    unsafeInheritedSubcategory,
    inheritedSubcategory,
    -- ** Getter
    originalCategory2,
    -- ** Interaction with 'Diagram'
    embeddingToInheritedSubcategory,
    fullDiagram2,
    fullNaturalTransformation2,
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategoryError
    import              Math.Categories.FunctorCategory
    import              Math.IO.PrettyPrint
    
    import              Data.WeakSet            (Set)
    import qualified    Data.WeakSet        as  Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap            (Map)
    import qualified    Data.WeakMap        as  Map
    import              Data.WeakMap.Safe
    
    -- | A 'Subcategory' needs an original category, a set of objects and a set of morphisms selected in the category.
    --
    -- The generators are forgotten, use 'InheritedSubcategory' if the generators are inheritable.
    --
    -- 'Subcategory' is private because the subset of morphisms might not yield a valid 'FiniteCategory' if a composite morphism does not belong in the subset.
    --
    -- Use the smart constructor 'subcategory' instead.
    data Subcategory c m o = Subcategory c (Set o) (Set m) deriving (Eq)
    
    instance (Show c, Show m, Show o) => Show (Subcategory c m o) where
        show (Subcategory c os ms) = "(unsafeSubcategory "++show c++" "++show os++" "++show ms++")"
    
    -- | Unsafe version of 'subcategory' which does not check the structure of the 'Subcategory' constructed.
    unsafeSubcategory :: c -> (Set o) -> (Set m) -> Subcategory c m o
    unsafeSubcategory c os ms = Subcategory c os ms
    
    -- | Smart constructor of 'Subcategory'.
    --
    -- If the 'Subcategory' constructed is valid, return 'Right' the subcategory, otherwise return Left a 'FiniteCategoryError'.
    subcategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (Set o) -> (Set m) -> Either (FiniteCategoryError m o) (Subcategory c m o)
    subcategory c ms os
        | null check = Right r
        | otherwise = Left err
        where
            r = Subcategory c ms os
            check = checkFiniteCategory r
            Just err = check
            
    -- | Return the original category the 'Subcategory' was taken from.
    originalCategory :: Subcategory c m o -> c
    originalCategory (Subcategory c _ _) = c
    
    instance (Category c m o, Eq o, Eq m) => Category (Subcategory c m o) m o where
        identity (Subcategory c objs _) o
            | o `isIn` objs = identity c o
            | otherwise = error "Math.FiniteCategories.Subcategory.identity: object not in the subcategory"
        ar (Subcategory c objs morphs) s t
            | s `isIn` objs && t `isIn` objs = Set.filter (`isIn` morphs) $ ar c s t
            | otherwise = error "Math.FiniteCategories.Subcategory.ar: source or target not in the subcategory"
    
    instance (Category c m o, Eq o, Eq m) => FiniteCategory (Subcategory c m o) m o where
        ob (Subcategory _ o _) = o
    
    instance (PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq o, Eq m) => PrettyPrint (Subcategory c m o) where
        pprint (Subcategory c o m) = "FullSubcategory("++ pprint c ++ ","++ pprint o ++ "," ++ pprint m ++")"
        
        
        
    -- | An 'InheritedSubcategory' needs an original category, a set of objects and a set of morphisms selected in the category.
    --
    -- The generators are inherited.
    --
    -- 'InheritedSubcategory' is private because the subset of morphisms might not yield a valid 'FiniteCategory' if a composite morphism does not belong in the subset.
    --
    -- Use the smart constructor 'inheritedSubcategory' instead.
    data InheritedSubcategory c m o = InheritedSubcategory c (Set o) (Set m) deriving (Eq)
    
    instance (Show c, Show m, Show o) => Show (InheritedSubcategory c m o) where
        show (InheritedSubcategory c os ms) = "(unsafeInheritedSubcategory "++show c++" "++show os++" "++show ms++")"
    
    -- | Unsafe version of 'inheritedSubcategory' which does not check the structure of the 'InheritedSubcategory' constructed.
    unsafeInheritedSubcategory :: c -> (Set o) -> (Set m) -> InheritedSubcategory c m o
    unsafeInheritedSubcategory c os ms = InheritedSubcategory c os ms
    
    -- | Smart constructor of 'InheritedSubcategory'.
    --
    -- If the 'InheritedSubcategory' constructed is valid, return 'Right' the subcategory, otherwise return Left a 'FiniteCategoryError'.
    inheritedSubcategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> (Set o) -> (Set m) -> Either (FiniteCategoryError m o) (InheritedSubcategory c m o)
    inheritedSubcategory c ms os
        | null check = Right r
        | otherwise = Left err
        where
            r = InheritedSubcategory c ms os
            check = checkFiniteCategory r
            Just err = check
            
    -- | Return the original category the 'InheritedSubcategory' was taken from.
    originalCategory2 :: InheritedSubcategory c m o -> c
    originalCategory2 (InheritedSubcategory c _ _) = c
    
    instance (Category c m o, Eq o, Eq m) => Category (InheritedSubcategory c m o) m o where
        identity (InheritedSubcategory c objs _) o
            | o `isIn` objs = identity c o
            | otherwise = error "Math.FiniteCategories.InheritedSubcategory.identity: object not in the subcategory"
        ar (InheritedSubcategory c objs morphs) s t
            | s `isIn` objs && t `isIn` objs = Set.filter (`isIn` morphs) $ ar c s t
            | otherwise = error "Math.FiniteCategories.InheritedSubcategory.ar: source or target not in the subcategory"
        genAr (InheritedSubcategory c objs morphs) s t
            | s `isIn` objs && t `isIn` objs = Set.filter (`isIn` morphs) $ genAr c s t
            | otherwise = error "Math.FiniteCategories.InheritedSubcategory.genAr: source or target not in the subcategory"
        decompose (InheritedSubcategory c _ morphs) m
            | m `isIn` morphs = decompose c m
            | otherwise = error "Math.FiniteCategories.InheritedSubcategory.decompose: morphism not in the subcategory"
    
    instance (Category c m o, Eq o, Eq m) => FiniteCategory (InheritedSubcategory c m o) m o where
        ob (InheritedSubcategory _ o _) = o
    
    instance (PrettyPrint c, PrettyPrint m, PrettyPrint o, Eq o, Eq m) => PrettyPrint (InheritedSubcategory c m o) where
        pprint (InheritedSubcategory c o m) = "InheritedFullSubcategory("++ pprint c ++ ","++ pprint o ++ "," ++ pprint m ++")"
            
    
    -- | Return the image 'Subcategory' of an embedding.
    --
    -- An embedding is a faithful 'Diagram' injective on objects.
    --
    -- Does not check that the 'Diagram' is an embedding.
    embeddingToSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> Subcategory c2 m2 o2
    embeddingToSubcategory diag = Subcategory (tgt diag) (image (omap diag)) (image (mmap diag))
    
    -- | Return the image 'InheritedSubcategory' of an embedding.
    --
    -- An embedding is a faithful 'Diagram' injective on objects.
    --
    -- Does not check that the 'Diagram' is an embedding.
    embeddingToInheritedSubcategory :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => Diagram c1 m1 o1 c2 m2 o2 -> InheritedSubcategory c2 m2 o2
    embeddingToInheritedSubcategory diag = InheritedSubcategory (tgt diag) (image (omap diag)) (image (mmap diag))
    
    -- | Extracts a full and faithful diagram out of a faithful 'Diagram' injective on objects.
    --
    -- Does not check that the 'Diagram' is an embedding.
    fullDiagram :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => 
                    Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
    fullDiagram diag = Diagram {src = src diag, tgt = embeddingToSubcategory diag, omap = omap diag, mmap = mmap diag}
    
    -- | Extracts a full and faithful diagram out of a faithful 'Diagram' injective on objects. The target subcategory is inherited (see 'InheritedFullSubcategory').
    --
    -- Does not check that the 'Diagram' is an embedding.
    fullDiagram2 :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1) => 
                    Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
    fullDiagram2 diag = Diagram {src = src diag, tgt = embeddingToInheritedSubcategory diag, omap = omap diag, mmap = mmap diag}
    
    -- | Extracts full and faithful diagrams out of the source and target 'Diagram's of a 'NaturalTransformation'. The 'Diagram's should be a faithful and injective on objects.
    --
    -- Does not check that the 'Diagram's are embeddings.
    fullNaturalTransformation :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                        Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 (Subcategory c2 m2 o2) m2 o2
    fullNaturalTransformation nat = unsafeNaturalTransformation sourceDiag targetDiag (components nat)
        where
            targetCat = Subcategory (tgt (source nat)) ((image (omap (source nat))) ||| (image (omap (target nat)))) ((image (mmap (source nat))) ||| (image (mmap (target nat))) ||| (image (components nat)))
            sourceDiag = Diagram{src=src (source nat), tgt=targetCat, omap=omap (source nat), mmap=mmap (source nat)}
            targetDiag = Diagram{src=src (target nat), tgt=targetCat, omap=omap (target nat), mmap=mmap (target nat)}
            
    -- | Extracts full and faithful diagrams out of the source and target 'Diagram's of a 'NaturalTransformation'. The 'Diagram's should be a faithful and injective on objects. The target subcategory is inherited (see 'InheritedFullSubcategory').
    --
    -- Does not check that the 'Diagram's are embeddings.
    fullNaturalTransformation2 :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
                                         Category c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => 
                    NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 (InheritedSubcategory c2 m2 o2) m2 o2
    fullNaturalTransformation2 nat = unsafeNaturalTransformation sourceDiag targetDiag (components nat)
        where
            targetCat = InheritedSubcategory (tgt (source nat)) ((image (omap (source nat))) ||| (image (omap (target nat)))) ((image (mmap (source nat))) ||| (image (mmap (target nat))) ||| (image (components nat)))
            sourceDiag = Diagram{src=src (source nat), tgt=targetCat, omap=omap (source nat), mmap=mmap (source nat)}
            targetDiag = Diagram{src=src (target nat), tgt=targetCat, omap=omap (target nat), mmap=mmap (target nat)}