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

{-| Module  : FiniteCategories
Description : A subcategory is the image of a faithful functor.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A subcategory is the image of a faithful functor.
-}

module Subcategories.Subcategory where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import Utils.AssociationList
    import Data.List (nub)
    import Subcategories.FullSubcategory
    
    -- | The type to view a faithful diagram as a subcategory.
    --
    -- It is your responsability to check that the diagram is faithful.
    data Subcategory c1 m1 o1 c2 m2 o2 = Subcategory (Diagram c1 m1 o1 c2 m2 o2)
    
    instance (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
            , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => 
            FiniteCategory (Subcategory c1 m1 o1 c2 m2 o2) m2 o2 where
        ob (Subcategory diag) = nub $ ((omap diag) !-!) <$> (ob (src diag))
        identity (Subcategory diag) o = identity (tgt diag) o
        ar (Subcategory diag) s t = nub $ ((mmap diag) !-!) <$> ar (src diag) ((inverse.omap $ diag) !-! s) ((inverse.omap $ diag) !-! t)
        
    instance (GeneratedFiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
            , GeneratedFiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => 
              GeneratedFiniteCategory (Subcategory c1 m1 o1 c2 m2 o2) m2 o2 where
        genAr (Subcategory diag) s t = nub $ ((mmap diag) !-!) <$> genAr (src diag) ((inverse.omap $ diag) !-! s) ((inverse.omap $ diag) !-! t)
        decompose (Subcategory diag) m = nub $ ((mmap diag) !-!) <$> decompose (src diag) ((inverse.mmap $ diag) !-! m)
        
    -- | Extracts a full and faithful diagram out of a faithful diagram.
    fullDiagram :: (  FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                    , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => 
                    Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 (Subcategory c1 m1 o1 c2 m2 o2) m2 o2
    fullDiagram diag = Diagram {src = src diag, tgt = Subcategory diag, omap = omap diag, mmap = mmap diag}
    
    -- | Strips the target of a diagram so that only given objects remain.
    stripDiagram :: ( FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1
                    , FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => 
                      Diagram c1 m1 o1 c2 m2 o2 -> [o2] -> Diagram c1 m1 o1 (FullSubcategory c2 m2 o2) m2 o2
    stripDiagram diag keep = Diagram {
                            src = src diag,
                            tgt = FullSubcategory (tgt diag) keep,
                            omap = omap diag,
                            mmap = mmap diag
                                }