{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses #-}
module Subcategories.FreeSubcategory
(
FreeSubcategory(..)
)
where
import FiniteCategory.FiniteCategory
import Data.List (nub)
import Utils.SetList
data FreeSubcategory c m o = FreeSubcategory c [m]
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)]
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