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

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

Free subcategory generated by a subset of morphisms of a category @C@.
-}
module Subcategories.FreeSubcategory
(
FreeSubcategory(..)
)
where
    import FiniteCategory.FiniteCategory
    import Data.List (nub)
    import Utils.SetList
    
    -- | The free subcategory generated by a subset of morphisms of a category @C@.

    data FreeSubcategory c m o = FreeSubcategory c [m]
    
    -- | Compose a list of morphisms with generator morphisms to generated new morphisms.

    composeOnce :: (Morphism m o, Eq m, Eq o) => [m] -> [m] -> [m]
    composeOnce :: forall m o. (Morphism m o, Eq m, Eq o) => [m] -> [m] -> [m]
composeOnce [m]
m [m]
g = [m] -> [m]
forall a. Eq a => [a] -> [a]
nub [m
m2 m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
m1| m
m1 <- [m]
m, m
m2 <- [m]
g, (m -> o
forall m o. Morphism m o => m -> o
target m
m1) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== (m -> o
forall m o. Morphism m o => m -> o
source m
m2)]
    
    -- | Compose a list of generator morphisms until it's useless.

    composeUntilEnd :: (Morphism m o, Eq m, Eq o) => [m] -> [m]
    composeUntilEnd :: forall m o. (Morphism m o, Eq m, Eq o) => [m] -> [m]
composeUntilEnd [m]
g = [m] -> [m] -> [m]
forall m o. (Morphism m o, Eq m, Eq o) => [m] -> [m] -> [m]
composeRecursive [m]
g [m]
g
        where composeRecursive :: [a] -> [a] -> [a]
composeRecursive [a]
ms [a]
g
                | [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
doubleInclusion [a]
nextStep [a]
ms = [a]
ms
                | Bool
otherwise = [a] -> [a] -> [a]
composeRecursive [a]
nextStep [a]
g
                where
                    nextStep :: [a]
nextStep = [a] -> [a] -> [a]
forall m o. (Morphism m o, Eq m, Eq o) => [m] -> [m] -> [m]
composeOnce [a]
ms [a]
g
    allArrows :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FreeSubcategory c m o -> [m]
    allArrows :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
FreeSubcategory c m o -> [m]
allArrows sc :: FreeSubcategory c m o
sc@(FreeSubcategory c
c [m]
morphs) = [m] -> [m]
forall m o. (Morphism m o, Eq m, Eq o) => [m] -> [m]
composeUntilEnd ([m] -> [m]) -> [m] -> [m]
forall a b. (a -> b) -> a -> b
$ [m] -> [m]
forall a. Eq a => [a] -> [a]
nub ([m] -> [m]) -> [m] -> [m]
forall a b. (a -> b) -> a -> b
$ [m]
morphs[m] -> [m] -> [m]
forall a. [a] -> [a] -> [a]
++(FreeSubcategory c m o -> [m]
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> [m]
identities FreeSubcategory c m o
sc)
    
    instance (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => FiniteCategory (FreeSubcategory c m o) m o where
        ob :: FreeSubcategory c m o -> [o]
ob (FreeSubcategory c
_ [m]
morphs) = [o] -> [o]
forall a. Eq a => [a] -> [a]
nub ([o] -> [o]) -> [o] -> [o]
forall a b. (a -> b) -> a -> b
$ [m -> o
forall m o. Morphism m o => m -> o
source m
m | m
m <- [m]
morphs][o] -> [o] -> [o]
forall a. [a] -> [a] -> [a]
++[m -> o
forall m o. Morphism m o => m -> o
target m
m | m
m <- [m]
morphs]
        identity :: Morphism m o => FreeSubcategory c m o -> o -> m
identity (FreeSubcategory c
c [m]
morphs) o
obj = c -> o -> m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> o -> m
identity c
c o
obj
        ar :: Morphism m o => FreeSubcategory c m o -> o -> o -> [m]
ar FreeSubcategory c m o
sc o
s o
t = (m -> Bool) -> [m] -> [m]
forall a. (a -> Bool) -> [a] -> [a]
filter (\m
x -> (m -> o
forall m o. Morphism m o => m -> o
source m
x) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
s Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
x) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
t) (FreeSubcategory c m o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
FreeSubcategory c m o -> [m]
allArrows FreeSubcategory c m o
sc)
        arrows :: (FiniteCategory (FreeSubcategory c m o) m o, Morphism m o) =>
FreeSubcategory c m o -> [m]
arrows = FreeSubcategory c m o -> [m]
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
FreeSubcategory c m o -> [m]
allArrows
        
    instance (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => GeneratedFiniteCategory (FreeSubcategory c m o) m o where
        genAr :: Morphism m o => FreeSubcategory c m o -> o -> o -> [m]
genAr (FreeSubcategory c
_ [m]
morphs) o
s o
t = (m -> Bool) -> [m] -> [m]
forall a. (a -> Bool) -> [a] -> [a]
filter (\m
x -> (m -> o
forall m o. Morphism m o => m -> o
source m
x) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
s Bool -> Bool -> Bool
&& (m -> o
forall m o. Morphism m o => m -> o
target m
x) o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
t) [m]
morphs
        decompose :: Morphism m o => FreeSubcategory c m o -> m -> [m]
decompose = FreeSubcategory c m o -> m -> [m]
forall c m o.
(GeneratedFiniteCategory c m o, Morphism m o, Eq m) =>
c -> m -> [m]
bruteForceDecompose
        genArrows :: (GeneratedFiniteCategory (FreeSubcategory c m o) m o,
 Morphism m o) =>
FreeSubcategory c m o -> [m]
genArrows (FreeSubcategory c
_ [m]
morphs) = [m]
morphs