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

{-| Module  : FiniteCategories
Description : Composition graphs are the simpliest way to create simple small categories by hand. See 'readCGFile'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

A 'CompositionGraph' is the free category generated by a multidigraph quotiented by an equivalence relation on the paths of the graphs.
A multidigraph is a directed multigraph which means that edges are oriented and there can be multiple arrows between two objects.

The equivalence relation is given by a map on paths of the graph.

Morphisms from different composition graphs should not be composed or compared, if they are, the behavior is undefined.

When taking subcategories of a composition graph, the composition law might lead to morphisms not existing anymore.
It is not a problem because they are equivalent, it is only counterintuitive for human readability.  
-}


module Math.FiniteCategories.CompositionGraph
(
    -- * Types for composition graph morphism

    RawPath(..),
    Path(..),
    CGMorphism(..),
    -- ** Functions for composition graph morphism

    getLabel,
    cgmorphismToArrow,
    arrowToCGMorphism,
    unsafeCGMorphismToArrow,
    unsafeArrowToCGMorphism,
    -- * Composition graph

    CompositionLaw(..),
    CompositionGraph,
    support,
    law,
    -- * Construction

    compositionGraph,
    unsafeCompositionGraph,
    emptyCompositionGraph,
    finiteCategoryToCompositionGraph,
    unsafeReadCGString,
    readCGString,
    unsafeReadCGFile,
    readCGFile,
    coproductOfCompositionGraphs,
    coproductOfStringCompositionGraphs,
    coproductOfTextCompositionGraphs,
    glueObjects,
    glueMorphisms,
    coequalizeCompositionGraphDiagrams,
    colimitOfCompositionGraphs,
    -- * Serialization

    writeCGString,
    writeCGFile,
    -- * Construction of diagrams

    unsafeReadCGDString,
    readCGDString,
    unsafeReadCGDFile,
    readCGDFile,
    -- * Serialization of diagrams

    writeCGDString,
    writeCGDFile,
    -- * Random composition graph

    constructRandomCompositionGraph,
    defaultConstructRandomCompositionGraph,
    defaultConstructRandomDiagram,
)    
where
    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
    import              Data.List                   (intercalate, elemIndex, splitAt)
    import              Data.Maybe                  (fromJust, isNothing)
    import              Data.Text                   (Text, cons, singleton, unpack, pack)
    
    import              Math.Categories.FinGrph
    import              Math.Categories.FunctorCategory
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.FiniteCategoryError
    import              Math.FiniteCategories.One
    import              Math.Categories.ConeCategory
    import              Math.Categories.FinCat
    import              Math.Categories.CommaCategory
    import              Math.IO.PrettyPrint
    
    import              System.Directory            (createDirectoryIfMissing)
    import              System.FilePath.Posix       (takeDirectory)
    import              System.Random               (RandomGen, uniformR)
    
    
    
    -- | A `RawPath` is a list of arrows, arrows should be compatible.

    type RawPath a b = [Arrow a b]
    
    -- | A `Path` is a `RawPath` with a source specified.

    --

    -- An empty path is an identity in a free category. 

    -- Therefore, it is useful to keep the source when the path is empty

    -- because there is one identity for each node of the graph. (We need to differentiate identites for each node.)

    type Path a b = (a, RawPath a b)
    
    -- | A `CompositionLaw` is a `Map` that maps raw paths to smaller raw paths in order to simplify paths

    -- so that they don't compose infinitely many times when there is a cycle.

    --

    -- prop> length (law |!| p) <= length p 

    type CompositionLaw a b = Map (RawPath a b) (RawPath a b)
    
    -- | The datatype `CGMorphism` is the type of composition graph morphisms.

    --

    -- It is a path with a composition law, it is necessary to keep the composition law of the composition graph

    -- in every morphism of the graph because we need it to compose two morphisms and the morphisms compose 

    -- independently of the composition graph.

    data CGMorphism a b = CGMorphism {forall a b. CGMorphism a b -> Path a b
path :: Path a b, 
                                      forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw :: CompositionLaw a b} deriving (Int -> CGMorphism a b -> ShowS
[CGMorphism a b] -> ShowS
CGMorphism a b -> String
(Int -> CGMorphism a b -> ShowS)
-> (CGMorphism a b -> String)
-> ([CGMorphism a b] -> ShowS)
-> Show (CGMorphism a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> CGMorphism a b -> ShowS
forall a b. (Show a, Show b) => [CGMorphism a b] -> ShowS
forall a b. (Show a, Show b) => CGMorphism a b -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> CGMorphism a b -> ShowS
showsPrec :: Int -> CGMorphism a b -> ShowS
$cshow :: forall a b. (Show a, Show b) => CGMorphism a b -> String
show :: CGMorphism a b -> String
$cshowList :: forall a b. (Show a, Show b) => [CGMorphism a b] -> ShowS
showList :: [CGMorphism a b] -> ShowS
Show, CGMorphism a b -> CGMorphism a b -> Bool
(CGMorphism a b -> CGMorphism a b -> Bool)
-> (CGMorphism a b -> CGMorphism a b -> Bool)
-> Eq (CGMorphism a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b.
(Eq a, Eq b) =>
CGMorphism a b -> CGMorphism a b -> Bool
$c== :: forall a b.
(Eq a, Eq b) =>
CGMorphism a b -> CGMorphism a b -> Bool
== :: CGMorphism a b -> CGMorphism a b -> Bool
$c/= :: forall a b.
(Eq a, Eq b) =>
CGMorphism a b -> CGMorphism a b -> Bool
/= :: CGMorphism a b -> CGMorphism a b -> Bool
Eq)
    
    instance (PrettyPrint a, PrettyPrint b, Eq a, Eq b) => PrettyPrint (CGMorphism a b) where
        pprint :: CGMorphism a b -> String
pprint CGMorphism {path :: forall a b. CGMorphism a b -> Path a b
path=(a
s,[]),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
cl} = String
"Id"String -> ShowS
forall a. [a] -> [a] -> [a]
++(a -> String
forall a. PrettyPrint a => a -> String
pprint a
s)
        pprint CGMorphism {path :: forall a b. CGMorphism a b -> Path a b
path=(a
_,RawPath a b
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
cl} = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" o " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (b -> String
forall a. PrettyPrint a => a -> String
pprint(b -> String) -> (Arrow a b -> b) -> Arrow a b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a b -> b
forall n e. Arrow n e -> e
labelArrow) (Arrow a b -> String) -> RawPath a b -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
rp

    -- | Helper function for `simplify`. Returns a simplified raw path.

    simplifyOnce :: (Eq a, Eq b) => CompositionLaw a b -> RawPath a b -> RawPath a b
    simplifyOnce :: forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplifyOnce CompositionLaw a b
_ [] = [] 
    simplifyOnce CompositionLaw a b
_ [Arrow a b
e] = [Arrow a b
e]
    simplifyOnce CompositionLaw a b
cl RawPath a b
list 
        | RawPath a b
new_list RawPath a b -> RawPath a b -> Bool
forall a. Eq a => a -> a -> Bool
== [] = []
        | RawPath a b
new_list RawPath a b -> RawPath a b -> Bool
forall a. Eq a => a -> a -> Bool
/= RawPath a b
list = RawPath a b
new_list
        | RawPath a b
simple_tail RawPath a b -> RawPath a b -> Bool
forall a. Eq a => a -> a -> Bool
/= (RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
tail RawPath a b
list) = (RawPath a b -> Arrow a b
forall a. HasCallStack => [a] -> a
head RawPath a b
list)Arrow a b -> RawPath a b -> RawPath a b
forall a. a -> [a] -> [a]
:RawPath a b
simple_tail
        | RawPath a b
simple_init RawPath a b -> RawPath a b -> Bool
forall a. Eq a => a -> a -> Bool
/= (RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
init RawPath a b
list) = RawPath a b
simple_initRawPath a b -> RawPath a b -> RawPath a b
forall a. [a] -> [a] -> [a]
++[(RawPath a b -> Arrow a b
forall a. HasCallStack => [a] -> a
last RawPath a b
list)]
        | Bool
otherwise = RawPath a b
list
        where
        new_list :: RawPath a b
new_list = RawPath a b -> RawPath a b -> CompositionLaw a b -> RawPath a b
forall k a. Eq k => a -> k -> Map k a -> a
Map.findWithDefault RawPath a b
list RawPath a b
list CompositionLaw a b
cl
        simple_tail :: RawPath a b
simple_tail = CompositionLaw a b -> RawPath a b -> RawPath a b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplifyOnce CompositionLaw a b
cl (RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
tail RawPath a b
list)
        simple_init :: RawPath a b
simple_init = CompositionLaw a b -> RawPath a b -> RawPath a b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplifyOnce CompositionLaw a b
cl (RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
init RawPath a b
list)
    
    -- | Return a completely simplified raw path.

    simplify :: (Eq a, Eq b) => CompositionLaw a b -> RawPath a b -> RawPath a b
    simplify :: forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify CompositionLaw a b
_ [] = []
    simplify CompositionLaw a b
cl RawPath a b
rp 
        | RawPath a b
simple_one RawPath a b -> RawPath a b -> Bool
forall a. Eq a => a -> a -> Bool
== RawPath a b
rp = RawPath a b
rp 
        | Bool
otherwise = CompositionLaw a b -> RawPath a b -> RawPath a b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify CompositionLaw a b
cl RawPath a b
simple_one 
            where simple_one :: RawPath a b
simple_one = CompositionLaw a b -> RawPath a b -> RawPath a b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplifyOnce CompositionLaw a b
cl RawPath a b
rp

    instance (Eq a, Eq b) => Morphism (CGMorphism a b) a where
        @? :: CGMorphism a b -> CGMorphism a b -> Maybe (CGMorphism a b)
(@?) m2 :: CGMorphism a b
m2@CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
s2,[Arrow a b]
rp2), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
cl2} m1 :: CGMorphism a b
m1@CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
s1,[Arrow a b]
rp1), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
cl1}
            | CompositionLaw a b
cl1 CompositionLaw a b -> CompositionLaw a b -> Bool
forall a. Eq a => a -> a -> Bool
/= CompositionLaw a b
cl2 = Maybe (CGMorphism a b)
forall a. Maybe a
Nothing
            | CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
m2 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
m1 = Maybe (CGMorphism a b)
forall a. Maybe a
Nothing
            | Bool
otherwise = CGMorphism a b -> Maybe (CGMorphism a b)
forall a. a -> Maybe a
Just CGMorphism{path :: (a, [Arrow a b])
path=(a
s1,(CompositionLaw a b -> [Arrow a b] -> [Arrow a b]
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify CompositionLaw a b
cl1 ([Arrow a b]
rp2[Arrow a b] -> [Arrow a b] -> [Arrow a b]
forall a. [a] -> [a] -> [a]
++[Arrow a b]
rp1))), compositionLaw :: CompositionLaw a b
compositionLaw=CompositionLaw a b
cl1}

                                    
        source :: CGMorphism a b -> a
source CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
s,[Arrow a b]
_), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
_} = a
s
        target :: CGMorphism a b -> a
target CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
s,[]), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
_} = a
s
        target CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
_,[Arrow a b]
rp), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
_} = Arrow a b -> a
forall n e. Arrow n e -> n
targetArrow ([Arrow a b] -> Arrow a b
forall a. HasCallStack => [a] -> a
head [Arrow a b]
rp)
                                    
        
    -- | Constructs a `CGMorphism` from a composition law and an arrow.

    mkCGMorphism :: CompositionLaw a b -> Arrow a b -> CGMorphism a b
    mkCGMorphism :: forall a b. CompositionLaw a b -> Arrow a b -> CGMorphism a b
mkCGMorphism CompositionLaw a b
cl Arrow a b
e = CGMorphism {path :: Path a b
path=(Arrow a b -> a
forall n e. Arrow n e -> n
sourceArrow Arrow a b
e,[Arrow a b
e]),compositionLaw :: CompositionLaw a b
compositionLaw=CompositionLaw a b
cl}

    -- | Returns the list of arrows of a graph with a given target.

    findInwardEdges :: (Eq a) => Graph a b -> a -> Set (Arrow a b)
    findInwardEdges :: forall a b. Eq a => Graph a b -> a -> Set (Arrow a b)
findInwardEdges Graph a b
g a
o = (Arrow a b -> Bool) -> Set (Arrow a b) -> Set (Arrow a b)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow a b
e -> (Arrow a b -> a
forall n e. Arrow n e -> n
targetArrow Arrow a b
e) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
o Bool -> Bool -> Bool
&& (Arrow a b -> a
forall n e. Arrow n e -> n
sourceArrow Arrow a b
e) a -> Set a -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes Graph a b
g)) (Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a b
g)

    -- | Find all acyclic raw paths between two nodes in a graph.

    findAcyclicRawPaths :: (Eq a, Eq b) => Graph a b -> a -> a -> Set (RawPath a b)
    findAcyclicRawPaths :: forall a b.
(Eq a, Eq b) =>
Graph a b -> a -> a -> Set (RawPath a b)
findAcyclicRawPaths Graph a b
g a
s a
t = Graph a b -> a -> a -> Set a -> Set [Arrow a b]
forall {t} {e}.
(Eq t, Eq e) =>
Graph t e -> t -> t -> Set t -> Set [Arrow t e]
findAcyclicRawPathsVisitedNodes Graph a b
g a
s a
t Set a
forall a. Set a
Set.empty where
        findAcyclicRawPathsVisitedNodes :: Graph t e -> t -> t -> Set t -> Set [Arrow t e]
findAcyclicRawPathsVisitedNodes Graph t e
g t
s t
t Set t
v
            | t
t t -> Set t -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` Set t
v = Set [Arrow t e]
forall a. Set a
Set.empty
            | t
s t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
t = [[Arrow t e]] -> Set [Arrow t e]
forall a. [a] -> Set a
set [[]]
            | Bool
otherwise = [[Arrow t e]] -> Set [Arrow t e]
forall a. [a] -> Set a
set ([[[Arrow t e]]] -> [[Arrow t e]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((([[Arrow t e]] -> [[Arrow t e]])
 -> [[Arrow t e]] -> [[Arrow t e]])
-> [[[Arrow t e]] -> [[Arrow t e]]]
-> [[[Arrow t e]]]
-> [[[Arrow t e]]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ([[Arrow t e]] -> [[Arrow t e]]) -> [[Arrow t e]] -> [[Arrow t e]]
forall a b. (a -> b) -> a -> b
($) ((([Arrow t e] -> [Arrow t e]) -> [[Arrow t e]] -> [[Arrow t e]])
-> [[Arrow t e] -> [Arrow t e]] -> [[[Arrow t e]] -> [[Arrow t e]]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Arrow t e] -> [Arrow t e]) -> [[Arrow t e]] -> [[Arrow t e]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arrow t e -> [Arrow t e] -> [Arrow t e])
-> [Arrow t e] -> [[Arrow t e] -> [Arrow t e]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (:) [Arrow t e]
inwardEdges)) ((Arrow t e -> [[Arrow t e]]) -> [Arrow t e] -> [[[Arrow t e]]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Arrow t e
x -> Set [Arrow t e] -> [[Arrow t e]]
forall a. Eq a => Set a -> [a]
setToList (Graph t e -> t -> t -> Set t -> Set [Arrow t e]
findAcyclicRawPathsVisitedNodes Graph t e
g t
s (Arrow t e -> t
forall n e. Arrow n e -> n
sourceArrow Arrow t e
x) (t -> Set t -> Set t
forall a. a -> Set a -> Set a
Set.insert t
t Set t
v))) [Arrow t e]
inwardEdges)))
            where
                inwardEdges :: [Arrow t e]
inwardEdges = (Set (Arrow t e) -> [Arrow t e]
forall a. Eq a => Set a -> [a]
setToList (Graph t e -> t -> Set (Arrow t e)
forall a b. Eq a => Graph a b -> a -> Set (Arrow a b)
findInwardEdges Graph t e
g t
t)) 
    
    -- | An elementary cycle is a cycle which is not composed of any other cycle.

    findElementaryCycles :: (Eq a, Eq b) => Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
    findElementaryCycles :: forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findElementaryCycles Graph a b
g CompositionLaw a b
cl a
o = [[Arrow a b]] -> Set [Arrow a b]
forall a. [a] -> Set a
set ([[Arrow a b]] -> Set [Arrow a b])
-> [[Arrow a b]] -> Set [Arrow a b]
forall a b. (a -> b) -> a -> b
$ (CompositionLaw a b -> [Arrow a b] -> [Arrow a b]
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify CompositionLaw a b
cl ([Arrow a b] -> [Arrow a b]) -> [[Arrow a b]] -> [[Arrow a b]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [][Arrow a b] -> [[Arrow a b]] -> [[Arrow a b]]
forall a. a -> [a] -> [a]
:([[[Arrow a b]]] -> [[Arrow a b]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (([Arrow a b -> [Arrow a b]] -> Arrow a b -> [[Arrow a b]])
-> [[Arrow a b -> [Arrow a b]]] -> [Arrow a b] -> [[[Arrow a b]]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Arrow a b -> [Arrow a b]] -> Arrow a b -> [[Arrow a b]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (([[Arrow a b]] -> [Arrow a b -> [Arrow a b]])
-> [[[Arrow a b]]] -> [[Arrow a b -> [Arrow a b]]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Arrow a b] -> Arrow a b -> [Arrow a b])
-> [[Arrow a b]] -> [Arrow a b -> [Arrow a b]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Arrow a b]
x Arrow a b
y -> (Arrow a b
yArrow a b -> [Arrow a b] -> [Arrow a b]
forall a. a -> [a] -> [a]
:[Arrow a b]
x))) ((Arrow a b -> [[Arrow a b]]) -> [Arrow a b] -> [[[Arrow a b]]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Arrow a b
x ->  Set [Arrow a b] -> [[Arrow a b]]
forall a. Eq a => Set a -> [a]
setToList (Graph a b -> a -> a -> Set [Arrow a b]
forall a b.
(Eq a, Eq b) =>
Graph a b -> a -> a -> Set (RawPath a b)
findAcyclicRawPaths Graph a b
g a
o (Arrow a b -> a
forall n e. Arrow n e -> n
sourceArrow Arrow a b
x))) [Arrow a b]
inEdges)) [Arrow a b]
inEdges)))
        where 
            inEdges :: [Arrow a b]
inEdges = (Set (Arrow a b) -> [Arrow a b]
forall a. Eq a => Set a -> [a]
setToList (Graph a b -> a -> Set (Arrow a b)
forall a b. Eq a => Graph a b -> a -> Set (Arrow a b)
findInwardEdges Graph a b
g a
o))
    
    -- | Composes every elementary cycles of a node until they simplify into a fixed set of cycles.

    --

    -- Warning : this function can do an infinite loop if the composition law does not simplify a cycle or all of its child cycles.

    findCycles :: (Eq a, Eq b) => Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
    findCycles :: forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findCycles Graph a b
g CompositionLaw a b
cl a
o = Graph a b
-> CompositionLaw a b
-> a
-> Set (RawPath a b)
-> Set (RawPath a b)
forall {t} {b}.
(Eq t, Eq b) =>
Graph t b
-> Map (RawPath t b) (RawPath t b)
-> t
-> Set (RawPath t b)
-> Set (RawPath t b)
findCyclesWithPreviousCycles Graph a b
g CompositionLaw a b
cl a
o (Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findElementaryCycles Graph a b
g CompositionLaw a b
cl a
o)
        where 
            findCyclesWithPreviousCycles :: Graph t b
-> Map (RawPath t b) (RawPath t b)
-> t
-> Set (RawPath t b)
-> Set (RawPath t b)
findCyclesWithPreviousCycles Graph t b
g Map (RawPath t b) (RawPath t b)
cl t
o Set (RawPath t b)
p
                | Set (RawPath t b)
newCycles Set (RawPath t b) -> Set (RawPath t b) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (RawPath t b)
p = Set (RawPath t b)
newCycles
                | Bool
otherwise = Graph t b
-> Map (RawPath t b) (RawPath t b)
-> t
-> Set (RawPath t b)
-> Set (RawPath t b)
findCyclesWithPreviousCycles Graph t b
g Map (RawPath t b) (RawPath t b)
cl t
o Set (RawPath t b)
newCycles
                where
                    newCycles :: Set (RawPath t b)
newCycles = (Map (RawPath t b) (RawPath t b) -> RawPath t b -> RawPath t b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify Map (RawPath t b) (RawPath t b)
cl) (RawPath t b -> RawPath t b)
-> Set (RawPath t b) -> Set (RawPath t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RawPath t b -> RawPath t b -> RawPath t b
forall a. [a] -> [a] -> [a]
(++) (RawPath t b -> RawPath t b -> RawPath t b)
-> Set (RawPath t b) -> Set (RawPath t b -> RawPath t b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (RawPath t b)
p Set (RawPath t b -> RawPath t b)
-> Set (RawPath t b) -> Set (RawPath t b)
forall a b. Set (a -> b) -> Set a -> Set b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Graph t b
-> Map (RawPath t b) (RawPath t b) -> t -> Set (RawPath t b)
forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findElementaryCycles Graph t b
g Map (RawPath t b) (RawPath t b)
cl t
o)
    
    -- | Helper function which intertwine the second list in the first list.

    --

    -- Example : intertwine [1,2,3] [4,5] = [1,4,2,5,3]

    intertwine :: [a] -> [a] -> [a]
    intertwine :: forall a. [a] -> [a] -> [a]
intertwine [] [a]
l = [a]
l
    intertwine [a]
l [] = [a]
l
    intertwine l1 :: [a]
l1@(a
x1:[a]
xs1) l2 :: [a]
l2@(a
x2:[a]
xs2) = (a
x1a -> [a] -> [a]
forall a. a -> [a] -> [a]
:(a
x2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:([a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
intertwine [a]
xs1 [a]
xs2)))
    
    -- | Takes a path and intertwine every cycles possible along its path.

    intertwineWithCycles :: (Eq a, Eq b) => Graph a b -> CompositionLaw a b -> a -> RawPath a b -> Set (RawPath a b)
    intertwineWithCycles :: forall a b.
(Eq a, Eq b) =>
Graph a b
-> CompositionLaw a b -> a -> RawPath a b -> Set (RawPath a b)
intertwineWithCycles Graph a b
g CompositionLaw a b
cl a
_ p :: [Arrow a b]
p@(Arrow a b
x:[Arrow a b]
xs) = [[Arrow a b]] -> Set [Arrow a b]
forall a. [a] -> Set a
set ([[Arrow a b]] -> Set [Arrow a b])
-> [[Arrow a b]] -> Set [Arrow a b]
forall a b. (a -> b) -> a -> b
$ [[Arrow a b]] -> [Arrow a b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Arrow a b]] -> [Arrow a b]) -> [[[Arrow a b]]] -> [[Arrow a b]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((([[Arrow a b]] -> [[Arrow a b]] -> [[Arrow a b]])
-> ([[Arrow a b]], [[Arrow a b]]) -> [[Arrow a b]]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [[Arrow a b]] -> [[Arrow a b]] -> [[Arrow a b]]
forall a. [a] -> [a] -> [a]
intertwine) (([[Arrow a b]], [[Arrow a b]]) -> [[Arrow a b]])
-> [([[Arrow a b]], [[Arrow a b]])] -> [[[Arrow a b]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[[Arrow a b]]]
-> [[[Arrow a b]]] -> [([[Arrow a b]], [[Arrow a b]])]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set [[Arrow a b]] -> [[[Arrow a b]]]
forall a. Eq a => Set a -> [a]
setToList Set [[Arrow a b]]
prodCycles) ([[Arrow a b]] -> [[[Arrow a b]]]
forall a. a -> [a]
repeat ((Arrow a b -> [Arrow a b] -> [Arrow a b]
forall a. a -> [a] -> [a]
:[]) (Arrow a b -> [Arrow a b]) -> [Arrow a b] -> [[Arrow a b]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
p))) where
        prodCycles :: Set [[Arrow a b]]
prodCycles = [Set [Arrow a b]] -> Set [[Arrow a b]]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets [Set [Arrow a b]]
cycles
        cycles :: [Set [Arrow a b]]
cycles = ((Graph a b -> CompositionLaw a b -> a -> Set [Arrow a b]
forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findCycles Graph a b
g CompositionLaw a b
cl (Arrow a b -> a
forall n e. Arrow n e -> n
targetArrow Arrow a b
x)))Set [Arrow a b] -> [Set [Arrow a b]] -> [Set [Arrow a b]]
forall a. a -> [a] -> [a]
:(((\Arrow a b
y -> (Graph a b -> CompositionLaw a b -> a -> Set [Arrow a b]
forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findCycles Graph a b
g CompositionLaw a b
cl (Arrow a b -> a
forall n e. Arrow n e -> n
sourceArrow Arrow a b
y)))) (Arrow a b -> Set [Arrow a b]) -> [Arrow a b] -> [Set [Arrow a b]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
p)
    intertwineWithCycles Graph a b
g CompositionLaw a b
cl a
s [] = (Graph a b -> CompositionLaw a b -> a -> Set [Arrow a b]
forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> Set (RawPath a b)
findCycles Graph a b
g CompositionLaw a b
cl a
s)
        
    -- | Enumerates all paths between two nodes and construct composition graph morphisms with them.

    mkAr :: (Eq a, Eq b) => Graph a b -> CompositionLaw a b -> a -> a -> Set (CGMorphism a b)
    mkAr :: forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> a -> Set (CGMorphism a b)
mkAr Graph a b
g CompositionLaw a b
cl a
s a
t = (\RawPath a b
p -> CGMorphism{path :: Path a b
path=(a
s,RawPath a b
p),compositionLaw :: CompositionLaw a b
compositionLaw=CompositionLaw a b
cl}) (RawPath a b -> CGMorphism a b)
-> Set (RawPath a b) -> Set (CGMorphism a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (RawPath a b)
allPaths where
        acyclicPaths :: Set (RawPath a b)
acyclicPaths = (CompositionLaw a b -> RawPath a b -> RawPath a b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify CompositionLaw a b
cl) (RawPath a b -> RawPath a b)
-> Set (RawPath a b) -> Set (RawPath a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Graph a b -> a -> a -> Set (RawPath a b)
forall a b.
(Eq a, Eq b) =>
Graph a b -> a -> a -> Set (RawPath a b)
findAcyclicRawPaths Graph a b
g a
s a
t)
        allPaths :: Set (RawPath a b)
allPaths = (CompositionLaw a b -> RawPath a b -> RawPath a b
forall a b.
(Eq a, Eq b) =>
CompositionLaw a b -> RawPath a b -> RawPath a b
simplify CompositionLaw a b
cl (RawPath a b -> RawPath a b)
-> Set (RawPath a b) -> Set (RawPath a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (RawPath a b)] -> Set (RawPath a b)
forall (f :: * -> *) a. Foldable f => f (Set a) -> Set a
Set.unions (Set (Set (RawPath a b)) -> [Set (RawPath a b)]
forall a. Eq a => Set a -> [a]
setToList ((Graph a b
-> CompositionLaw a b -> a -> RawPath a b -> Set (RawPath a b)
forall a b.
(Eq a, Eq b) =>
Graph a b
-> CompositionLaw a b -> a -> RawPath a b -> Set (RawPath a b)
intertwineWithCycles Graph a b
g CompositionLaw a b
cl a
s) (RawPath a b -> Set (RawPath a b))
-> Set (RawPath a b) -> Set (Set (RawPath a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (RawPath a b)
acyclicPaths)))
    
    -- | Return Just the label of a 'CompositionGraph' non identity generator, Nothing if the morphism is not a non identity generator.

    getLabel :: CGMorphism a b -> Maybe b
    getLabel :: forall a b. CGMorphism a b -> Maybe b
getLabel CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
_,RawPath a b
rp), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
_}
        | RawPath a b -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null RawPath a b
rp = Maybe b
forall a. Maybe a
Nothing
        | RawPath a b -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null(RawPath a b -> Bool)
-> (RawPath a b -> RawPath a b) -> RawPath a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
tail (RawPath a b -> Bool) -> RawPath a b -> Bool
forall a b. (a -> b) -> a -> b
$ RawPath a b
rp = b -> Maybe b
forall a. a -> Maybe a
Just (Arrow a b -> b
forall n e. Arrow n e -> e
labelArrow(Arrow a b -> b) -> (RawPath a b -> Arrow a b) -> RawPath a b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.RawPath a b -> Arrow a b
forall a. HasCallStack => [a] -> a
head (RawPath a b -> b) -> RawPath a b -> b
forall a b. (a -> b) -> a -> b
$ RawPath a b
rp)
        | Bool
otherwise = Maybe b
forall a. Maybe a
Nothing
        
    -- | Return Just the 'Arrow' of a 'CompositionGraph' non identity generator, Nothing if the morphism is not a non identity generator.

    cgmorphismToArrow :: CGMorphism a b -> Maybe (Arrow a b)
    cgmorphismToArrow :: forall a b. CGMorphism a b -> Maybe (Arrow a b)
cgmorphismToArrow CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
_,RawPath a b
rp), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
_}
        | RawPath a b -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null RawPath a b
rp = Maybe (Arrow a b)
forall a. Maybe a
Nothing
        | RawPath a b -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null(RawPath a b -> Bool)
-> (RawPath a b -> RawPath a b) -> RawPath a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
tail (RawPath a b -> Bool) -> RawPath a b -> Bool
forall a b. (a -> b) -> a -> b
$ RawPath a b
rp = Arrow a b -> Maybe (Arrow a b)
forall a. a -> Maybe a
Just (RawPath a b -> Arrow a b
forall a. HasCallStack => [a] -> a
head (RawPath a b -> Arrow a b) -> RawPath a b -> Arrow a b
forall a b. (a -> b) -> a -> b
$ RawPath a b
rp)
        | Bool
otherwise = Maybe (Arrow a b)
forall a. Maybe a
Nothing
        
    -- | Given a composition graph, transform an 'Arrow' into a 'CGMorphism' if this 'CGMorphism' is in the composition graph, return Nothing otherwise. 

    arrowToCGMorphism :: (Eq a, Eq b) => CompositionGraph a b -> Arrow a b -> Maybe (CGMorphism a b)
    arrowToCGMorphism :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> Arrow a b -> Maybe (CGMorphism a b)
arrowToCGMorphism CompositionGraph a b
cg Arrow a b
arr
        | Arrow a b
arr Arrow a b -> Set (Arrow a b) -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph a b -> Set (Arrow a b))
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set (Arrow a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set (Arrow a b))
-> CompositionGraph a b -> Set (Arrow a b)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg) = CGMorphism a b -> Maybe (CGMorphism a b)
forall a. a -> Maybe a
Just (CGMorphism a b -> Maybe (CGMorphism a b))
-> CGMorphism a b -> Maybe (CGMorphism a b)
forall a b. (a -> b) -> a -> b
$ CompositionLaw a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionLaw a b -> Arrow a b -> CGMorphism a b
mkCGMorphism (CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
cg) Arrow a b
arr
        | Bool
otherwise = Maybe (CGMorphism a b)
forall a. Maybe a
Nothing
        
        
    -- | Unsafe version of 'cgmorphismToArrow'.

    unsafeCGMorphismToArrow :: CGMorphism a b -> (Arrow a b)
    unsafeCGMorphismToArrow :: forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
_,RawPath a b
rp), compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
_}
        | RawPath a b -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null RawPath a b
rp = String -> Arrow a b
forall a. HasCallStack => String -> a
error String
"no arrow in CGMorphism"
        | RawPath a b -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null(RawPath a b -> Bool)
-> (RawPath a b -> RawPath a b) -> RawPath a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.RawPath a b -> RawPath a b
forall a. HasCallStack => [a] -> [a]
tail (RawPath a b -> Bool) -> RawPath a b -> Bool
forall a b. (a -> b) -> a -> b
$ RawPath a b
rp = RawPath a b -> Arrow a b
forall a. HasCallStack => [a] -> a
head RawPath a b
rp
        | Bool
otherwise = String -> Arrow a b
forall a. HasCallStack => String -> a
error String
"several arrows in CGMorphism"
        
    -- | Unsafe version of 'arrowToCGMorphism'.

    unsafeArrowToCGMorphism :: CompositionGraph a b -> Arrow a b -> CGMorphism a b
    unsafeArrowToCGMorphism :: forall a b. CompositionGraph a b -> Arrow a b -> CGMorphism a b
unsafeArrowToCGMorphism CompositionGraph a b
cg Arrow a b
arr = CompositionLaw a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionLaw a b -> Arrow a b -> CGMorphism a b
mkCGMorphism (CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
cg) Arrow a b
arr
    
    -- | A 'CompositionGraph' is a graph with a composition law such that the free category generated by the graph quotiented out by the composition law gives a 'FiniteCategory'.

    -- 

    -- 'CompositionGraph' is private, use the smart constructors 'compositionGraph' or 'unsafeCompositionGraph' to instantiate one.

    data CompositionGraph a b = CompositionGraph {
                                                    forall a b. CompositionGraph a b -> Graph a b
support :: Graph a b, -- ^ The generating graph (or support) of the composition graph.

                                                    forall a b. CompositionGraph a b -> CompositionLaw a b
law :: CompositionLaw a b -- ^ The composition law of the composition graph.

                                                 } deriving (CompositionGraph a b -> CompositionGraph a b -> Bool
(CompositionGraph a b -> CompositionGraph a b -> Bool)
-> (CompositionGraph a b -> CompositionGraph a b -> Bool)
-> Eq (CompositionGraph a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> CompositionGraph a b -> Bool
$c== :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> CompositionGraph a b -> Bool
== :: CompositionGraph a b -> CompositionGraph a b -> Bool
$c/= :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> CompositionGraph a b -> Bool
/= :: CompositionGraph a b -> CompositionGraph a b -> Bool
Eq)
 
    instance (Show a, Show b) => Show (CompositionGraph a b) where
        show :: CompositionGraph a b -> String
show CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph a b
g, law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw a b
l} = String
"(unsafeCompositionGraph "String -> ShowS
forall a. [a] -> [a] -> [a]
++ Graph a b -> String
forall a. Show a => a -> String
show Graph a b
g String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CompositionLaw a b -> String
forall a. Show a => a -> String
show CompositionLaw a b
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
 
    instance (Eq a, Eq b) => Category (CompositionGraph a b) (CGMorphism a b) a where
        identity :: Morphism (CGMorphism a b) a =>
CompositionGraph a b -> a -> CGMorphism a b
identity CompositionGraph a b
c a
x
            | a
x a -> Set a -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes (CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a b
c)) = CGMorphism {path :: Path a b
path=(a
x,[]),compositionLaw :: CompositionLaw a b
compositionLaw=(CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
c)}
            | Bool
otherwise = String -> CGMorphism a b
forall a. HasCallStack => String -> a
error (String
"Math.FiniteCategories.CompositionGraph.identity: Trying to construct identity of an unknown object.")
        ar :: Morphism (CGMorphism a b) a =>
CompositionGraph a b -> a -> a -> Set (CGMorphism a b)
ar CompositionGraph a b
c a
s a
t = Graph a b -> CompositionLaw a b -> a -> a -> Set (CGMorphism a b)
forall a b.
(Eq a, Eq b) =>
Graph a b -> CompositionLaw a b -> a -> a -> Set (CGMorphism a b)
mkAr (CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a b
c) (CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
c) a
s a
t
        genAr :: Morphism (CGMorphism a b) a =>
CompositionGraph a b -> a -> a -> Set (CGMorphism a b)
genAr c :: CompositionGraph a b
c@CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph a b
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw a b
l} a
s a
t
            | a
s a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
t = CGMorphism a b -> Set (CGMorphism a b) -> Set (CGMorphism a b)
forall a. a -> Set a -> Set a
Set.insert (CompositionGraph a b -> a -> CGMorphism a b
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity CompositionGraph a b
c a
s) Set (CGMorphism a b)
gen
            | Bool
otherwise = Set (CGMorphism a b)
gen 
            where gen :: Set (CGMorphism a b)
gen = CompositionLaw a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionLaw a b -> Arrow a b -> CGMorphism a b
mkCGMorphism CompositionLaw a b
l (Arrow a b -> CGMorphism a b)
-> Set (Arrow a b) -> Set (CGMorphism a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Arrow a b -> Bool) -> Set (Arrow a b) -> Set (Arrow a b)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow a b
a -> a
s a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (Arrow a b -> a
forall n e. Arrow n e -> n
sourceArrow Arrow a b
a) Bool -> Bool -> Bool
&& a
t a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (Arrow a b -> a
forall n e. Arrow n e -> n
targetArrow Arrow a b
a)) (Set (Arrow a b) -> Set (Arrow a b))
-> Set (Arrow a b) -> Set (Arrow a b)
forall a b. (a -> b) -> a -> b
$ (Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a b
g))
            
        decompose :: Morphism (CGMorphism a b) a =>
CompositionGraph a b -> CGMorphism a b -> [CGMorphism a b]
decompose CompositionGraph a b
c m :: CGMorphism a b
m@CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=(a
_,[Arrow a b]
rp),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
l}
            | CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity CompositionGraph a b
c CGMorphism a b
m = [CGMorphism a b
m]
            | Bool
otherwise = CompositionLaw a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionLaw a b -> Arrow a b -> CGMorphism a b
mkCGMorphism CompositionLaw a b
l (Arrow a b -> CGMorphism a b) -> [Arrow a b] -> [CGMorphism a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
rp
    
    instance (Eq a, Eq b) => FiniteCategory (CompositionGraph a b) (CGMorphism a b) a where
        ob :: CompositionGraph a b -> Set a
ob = (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support)
            
    instance (PrettyPrint a, PrettyPrint b, Eq a, Eq b) => PrettyPrint (CompositionGraph a b) where
        pprint :: CompositionGraph a b -> String
pprint CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph a b
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw a b
l} = String
"CompositionGraph("String -> ShowS
forall a. [a] -> [a] -> [a]
++Graph a b -> String
forall a. PrettyPrint a => a -> String
pprint Graph a b
gString -> ShowS
forall a. [a] -> [a] -> [a]
++String
","String -> ShowS
forall a. [a] -> [a] -> [a]
++CompositionLaw a b -> String
forall a. PrettyPrint a => a -> String
pprint CompositionLaw a b
lString -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"         
    
    -- | Smart constructor of `CompositionGraph`.

    --

    -- If the 'CompositionGraph' constructed is valid, return 'Right' the composition graph, otherwise return Left a 'FiniteCategoryError'.

    compositionGraph :: (Eq a, Eq b) => Graph a b -> CompositionLaw a b -> Either (FiniteCategoryError (CGMorphism a b) a) (CompositionGraph a b) 
    compositionGraph :: forall a b.
(Eq a, Eq b) =>
Graph a b
-> CompositionLaw a b
-> Either
     (FiniteCategoryError (CGMorphism a b) a) (CompositionGraph a b)
compositionGraph Graph a b
g CompositionLaw a b
l
        | Maybe (FiniteCategoryError (CGMorphism a b) a) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (FiniteCategoryError (CGMorphism a b) a)
check = CompositionGraph a b
-> Either
     (FiniteCategoryError (CGMorphism a b) a) (CompositionGraph a b)
forall a b. b -> Either a b
Right CompositionGraph a b
c_g
        | Bool
otherwise = FiniteCategoryError (CGMorphism a b) a
-> Either
     (FiniteCategoryError (CGMorphism a b) a) (CompositionGraph a b)
forall a b. a -> Either a b
Left FiniteCategoryError (CGMorphism a b) a
err
        where
            c_g :: CompositionGraph a b
c_g = CompositionGraph{support :: Graph a b
support = Graph a b
g, law :: CompositionLaw a b
law = CompositionLaw a b
l}
            check :: Maybe (FiniteCategoryError (CGMorphism a b) a)
check = CompositionGraph a b
-> Maybe (FiniteCategoryError (CGMorphism a b) a)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategory CompositionGraph a b
c_g
            Just FiniteCategoryError (CGMorphism a b) a
err = Maybe (FiniteCategoryError (CGMorphism a b) a)
check
    
    -- | Unsafe constructor of 'CompositionGraph' for performance purposes. It does not check the structure of the 'CompositionGraph'.

    --

    -- Use this constructor only if the 'CompositionGraph' is necessarily well formed.

    unsafeCompositionGraph :: Graph a b -> CompositionLaw a b -> CompositionGraph a b
    unsafeCompositionGraph :: forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph Graph a b
g CompositionLaw a b
l = CompositionGraph{support :: Graph a b
support = Graph a b
g, law :: CompositionLaw a b
law = CompositionLaw a b
l}
            
                                                                            
    -- | Transforms any 'FiniteCategory' into a 'CompositionGraph'.

    --

    -- The 'CompositionGraph' will take more space in memory compared to the original category because the composition law is stored as a 'Map'.

    --

    -- Returns an isofunctor as a `Diagram` from the original category to the created 'CompositionGraph'.

    --

    -- If you only want the 'CompositionGraph', take the 'tgt' of the 'Diagram'.

    finiteCategoryToCompositionGraph :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
    finiteCategoryToCompositionGraph :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
finiteCategoryToCompositionGraph c
cat = Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
isofunct
        where
            morphToArrow :: e -> Arrow n e
morphToArrow e
f = Arrow{sourceArrow :: n
sourceArrow = e -> n
forall m o. Morphism m o => m -> o
source e
f, targetArrow :: n
targetArrow = e -> n
forall m o. Morphism m o => m -> o
target e
f, labelArrow :: e
labelArrow = e
f}
            catLaw :: Map [Arrow o m] [Arrow o m]
catLaw = Set ([Arrow o m], [Arrow o m]) -> Map [Arrow o m] [Arrow o m]
forall k v. Set (k, v) -> Map k v
weakMapFromSet [
                if c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
cat (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f) then
                    ((m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow (m -> Arrow o m) -> [m] -> [Arrow o m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
cat m
g))[Arrow o m] -> [Arrow o m] -> [Arrow o m]
forall a. [a] -> [a] -> [a]
++(m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow (m -> Arrow o m) -> [m] -> [Arrow o m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
cat m
f)), m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow (m -> Arrow o m) -> [m] -> [Arrow o m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
cat (m
g m -> m -> m
forall m o. Morphism m o => m -> m -> m
@ m
f)))
                else
                    ((m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow (m -> Arrow o m) -> [m] -> [Arrow o m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
cat m
g))[Arrow o m] -> [Arrow o m] -> [Arrow o m]
forall a. [a] -> [a] -> [a]
++(m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow (m -> Arrow o m) -> [m] -> [Arrow o m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
cat m
f)),[]) |
                m
f <- (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
cat), m
g <- (c -> o -> Set m
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
arFrom c
cat (m -> o
forall m o. Morphism m o => m -> o
target m
f)), c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
cat m
f, c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
cat m
g]
            cg :: CompositionGraph o m
cg = CompositionGraph{support :: Graph o m
support=(Set o -> Set (Arrow o m) -> Graph o m
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat) [m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow m
f | m
f <- (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows c
cat), c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
cat m
f])
                                , law :: Map [Arrow o m] [Arrow o m]
law=Map [Arrow o m] [Arrow o m]
catLaw}
            isofunct :: Diagram c m o (CompositionGraph o m) (CGMorphism o m) o
isofunct = Diagram{src :: c
src=c
cat,tgt :: CompositionGraph o m
tgt=CompositionGraph o m
cg,omap :: Map o o
omap=(o -> o) -> Set o -> Map o o
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction o -> o
forall a. a -> a
id (c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
cat),mmap :: Map m (CGMorphism o m)
mmap=(m -> CGMorphism o m) -> Set m -> Map m (CGMorphism o m)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (\m
f -> if c -> m -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity c
cat m
f
                                                                        then
                                                                            CGMorphism {path :: Path o m
path=(m -> o
forall m o. Morphism m o => m -> o
source m
f,(m -> Arrow o m
forall {e} {n}. Morphism e n => e -> Arrow n e
morphToArrow (m -> Arrow o m) -> [m] -> [Arrow o m]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c -> m -> [m]
forall c m o. (Category c m o, Morphism m o) => c -> m -> [m]
decompose c
cat m
f))),compositionLaw :: Map [Arrow o m] [Arrow o m]
compositionLaw=Map [Arrow o m] [Arrow o m]
catLaw}
                                                                        else
                                                                            CompositionGraph o m -> o -> CGMorphism o m
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity CompositionGraph o m
cg (m -> o
forall m o. Morphism m o => m -> o
source m
f)) (c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
cat)}



    -- | The empty 'CompositionGraph'.

    emptyCompositionGraph :: CompositionGraph a b
    emptyCompositionGraph :: forall a b. CompositionGraph a b
emptyCompositionGraph = CompositionGraph{support :: Graph a b
support=Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph Set a
forall a. Set a
Set.empty Set (Arrow a b)
forall a. Set a
Set.empty, law :: CompositionLaw a b
law=CompositionLaw a b
forall k a. Map k a
Map.empty}

    -----------------------

    -- CG FILE

    -----------------------



    -- | A token for a .cg file.

    data Token = Name Text | BeginArrow | EndArrow | Equals | Identity | BeginSrc | EndSrc | BeginTgt | EndTgt | MapsTo deriving (Token -> Token -> Bool
(Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Token -> Token -> Bool
== :: Token -> Token -> Bool
$c/= :: Token -> Token -> Bool
/= :: Token -> Token -> Bool
Eq, Int -> Token -> ShowS
[Token] -> ShowS
Token -> String
(Int -> Token -> ShowS)
-> (Token -> String) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Token -> ShowS
showsPrec :: Int -> Token -> ShowS
$cshow :: Token -> String
show :: Token -> String
$cshowList :: [Token] -> ShowS
showList :: [Token] -> ShowS
Show)
    
    -- | Strip a token of unnecessary spaces.

    strip :: Token -> Token
    strip :: Token -> Token
strip (Name Text
txt) = Text -> Token
Name (String -> Text
pack(String -> Text) -> ShowS -> String -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ShowS
forall a. [a] -> [a]
reverseShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ShowS
stripLeftShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ShowS
forall a. [a] -> [a]
reverseShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ShowS
stripLeft (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
str)
        where
            str :: String
str = Text -> String
unpack Text
txt
            stripLeft :: ShowS
stripLeft (Char
' ':String
s) = String
s 
            stripLeft String
s = String
s 
    strip Token
x = Token
x
        
    -- | Transforms a string into a list of tokens.

    parserLex :: String -> [Token]
    parserLex :: String -> [Token]
parserLex String
str = Token -> Token
strip (Token -> Token) -> [Token] -> [Token]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> [Token]
parserLexHelper String
str
        where
            parserLexHelper :: String -> [Token]
parserLexHelper [] = [] 
            parserLexHelper (Char
'#':String
str) = []
            parserLexHelper (Char
' ':Char
'-':String
str) = Token
BeginArrow Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'-':Char
'>':Char
' ':String
str) = Token
EndArrow Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
' ':Char
'=':Char
' ':String
str) = Token
Equals Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'<':Char
'I':Char
'D':Char
'/':Char
'>':String
str) = Token
Identity Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'<':Char
'I':Char
'D':Char
'>':String
str) = Token
Identity Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'<':Char
'S':Char
'R':Char
'C':Char
'>':String
str) = Token
BeginSrc Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'<':Char
'T':Char
'G':Char
'T':Char
'>':String
str) = Token
BeginTgt Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'<':Char
'/':Char
'S':Char
'R':Char
'C':Char
'>':String
str) = Token
EndSrc Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
'<':Char
'/':Char
'T':Char
'G':Char
'T':Char
'>':String
str) = Token
EndTgt Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
' ':Char
'=':Char
'>':Char
' ':String
str) = Token
MapsTo Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: (String -> [Token]
parserLexHelper String
str)
            parserLexHelper (Char
c:String
str) =  ([Token] -> [Token]
result [Token]
restLexed)
                where
                    restLexed :: [Token]
restLexed = (String -> [Token]
parserLexHelper String
str)
                    result :: [Token] -> [Token]
result (Name Text
txt:[Token]
xs) = (Text -> Token
Name (Char -> Text -> Text
cons Char
c Text
txt)Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
:[Token]
xs)
                    result [Token]
a = ((Text -> Token
Name (Char -> Text
singleton Char
c))Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
:[Token]
a)

    type CG = CompositionGraph Text Text
    
    addObject :: [Token] -> CG -> CG
    addObject :: [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addObject [Name Text
str] cg :: CompositionGraph Text Text
cg@CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph Text Text
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw Text Text
l} = CompositionGraph{support :: Graph Text Text
support=Set Text -> Set (Arrow Text Text) -> Graph Text Text
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Text -> Set Text -> Set Text
forall a. a -> Set a -> Set a
Set.insert Text
str (Graph Text Text -> Set Text
forall n e. Graph n e -> Set n
nodes Graph Text Text
g)) (Graph Text Text -> Set (Arrow Text Text)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph Text Text
g),law :: CompositionLaw Text Text
law=CompositionLaw Text Text
l}
    addObject [Token]
otherTokens CompositionGraph Text Text
_ = String -> CompositionGraph Text Text
forall a. HasCallStack => String -> a
error (String -> CompositionGraph Text Text)
-> String -> CompositionGraph Text Text
forall a b. (a -> b) -> a -> b
$ String
"addObject on invalid tokens : "String -> ShowS
forall a. [a] -> [a] -> [a]
++[Token] -> String
forall a. Show a => a -> String
show [Token]
otherTokens
    
    addMorphism :: [Token] -> CG -> CG
    addMorphism :: [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addMorphism [Name Text
src, Token
BeginArrow, Name Text
arr, Token
EndArrow, Name Text
tgt] CompositionGraph Text Text
cg = CompositionGraph{support :: Graph Text Text
support=(Set Text -> Set (Arrow Text Text) -> Graph Text Text
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Graph Text Text -> Set Text
forall n e. Graph n e -> Set n
nodes Graph Text Text
g) (Arrow Text Text -> Set (Arrow Text Text) -> Set (Arrow Text Text)
forall a. a -> Set a -> Set a
Set.insert Arrow{sourceArrow :: Text
sourceArrow=Text
src, targetArrow :: Text
targetArrow=Text
tgt, labelArrow :: Text
labelArrow=Text
arr} (Graph Text Text -> Set (Arrow Text Text)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph Text Text
g))),law :: CompositionLaw Text Text
law=CompositionLaw Text Text
l}
        where
            newCG1 :: CompositionGraph Text Text
newCG1 = [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addObject [Text -> Token
Name Text
src] CompositionGraph Text Text
cg
            newCG2 :: CompositionGraph Text Text
newCG2@CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph Text Text
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw Text Text
l} = [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addObject [Text -> Token
Name Text
tgt] CompositionGraph Text Text
newCG1
    addMorphism [Token]
otherTokens CompositionGraph Text Text
_ = String -> CompositionGraph Text Text
forall a. HasCallStack => String -> a
error (String -> CompositionGraph Text Text)
-> String -> CompositionGraph Text Text
forall a b. (a -> b) -> a -> b
$ String
"addMorphism on invalid tokens : "String -> ShowS
forall a. [a] -> [a] -> [a]
++[Token] -> String
forall a. Show a => a -> String
show [Token]
otherTokens
    
    extractPath :: [Token] -> RawPath Text Text
    extractPath :: [Token] -> RawPath Text Text
extractPath [] = []
    extractPath [Token
Identity] = []
    extractPath [(Name Text
_)] = []
    extractPath ((Name Text
src) : (Token
BeginArrow : ((Name Text
arr) : (Token
EndArrow : ((Name Text
tgt) : [Token]
ts))))) = ([Token] -> RawPath Text Text
extractPath ((Text -> Token
Name Text
tgt) Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ts)) RawPath Text Text -> RawPath Text Text -> RawPath Text Text
forall a. [a] -> [a] -> [a]
++ [Arrow{sourceArrow :: Text
sourceArrow=Text
src, targetArrow :: Text
targetArrow=Text
tgt, labelArrow :: Text
labelArrow=Text
arr}]
    extractPath [Token]
otherTokens = String -> RawPath Text Text
forall a. HasCallStack => String -> a
error (String -> RawPath Text Text) -> String -> RawPath Text Text
forall a b. (a -> b) -> a -> b
$ String
"extractPath on invalid tokens : "String -> ShowS
forall a. [a] -> [a] -> [a]
++[Token] -> String
forall a. Show a => a -> String
show [Token]
otherTokens
    
    addCompositionLawEntry :: [Token] -> CG -> CG
    addCompositionLawEntry :: [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addCompositionLawEntry [Token]
tokens cg :: CompositionGraph Text Text
cg@CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph Text Text
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw Text Text
l} = CompositionGraph{support :: Graph Text Text
support=(Set Text -> Set (Arrow Text Text) -> Graph Text Text
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((Graph Text Text -> Set Text
forall n e. Graph n e -> Set n
nodes Graph Text Text
g) Set Text -> Set Text -> Set Text
forall a. Set a -> Set a -> Set a
||| Set Text
newObj) ((Graph Text Text -> Set (Arrow Text Text)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph Text Text
g) Set (Arrow Text Text)
-> Set (Arrow Text Text) -> Set (Arrow Text Text)
forall a. Set a -> Set a -> Set a
||| Set (Arrow Text Text)
newMorph)),law :: CompositionLaw Text Text
law=RawPath Text Text
-> RawPath Text Text
-> CompositionLaw Text Text
-> CompositionLaw Text Text
forall k a. k -> a -> Map k a -> Map k a
Map.insert RawPath Text Text
pathLeft RawPath Text Text
pathRight CompositionLaw Text Text
l}
        where
            Just Int
indexEquals = Token -> [Token] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Token
Equals [Token]
tokens
            ([Token]
tokensLeft,(Token
_:[Token]
tokensRight)) = Int -> [Token] -> ([Token], [Token])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
indexEquals [Token]
tokens
            pathLeft :: RawPath Text Text
pathLeft = [Token] -> RawPath Text Text
extractPath [Token]
tokensLeft
            pathRight :: RawPath Text Text
pathRight = [Token] -> RawPath Text Text
extractPath [Token]
tokensRight
            newObj :: Set Text
newObj = [Text] -> Set Text
forall a. [a] -> Set a
set ([Text] -> Set Text) -> [Text] -> Set Text
forall a b. (a -> b) -> a -> b
$ (Arrow Text Text -> Text
forall n e. Arrow n e -> n
sourceArrow (Arrow Text Text -> Text) -> RawPath Text Text -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath Text Text
pathLeftRawPath Text Text -> RawPath Text Text -> RawPath Text Text
forall a. [a] -> [a] -> [a]
++RawPath Text Text
pathRight)[Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++(Arrow Text Text -> Text
forall n e. Arrow n e -> n
targetArrow (Arrow Text Text -> Text) -> RawPath Text Text -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath Text Text
pathLeftRawPath Text Text -> RawPath Text Text -> RawPath Text Text
forall a. [a] -> [a] -> [a]
++RawPath Text Text
pathRight)
            newMorph :: Set (Arrow Text Text)
newMorph = RawPath Text Text -> Set (Arrow Text Text)
forall a. [a] -> Set a
set (RawPath Text Text -> Set (Arrow Text Text))
-> RawPath Text Text -> Set (Arrow Text Text)
forall a b. (a -> b) -> a -> b
$ RawPath Text Text
pathLeftRawPath Text Text -> RawPath Text Text -> RawPath Text Text
forall a. [a] -> [a] -> [a]
++RawPath Text Text
pathRight
    
    readLine :: String -> CG -> CG
    readLine :: String -> CompositionGraph Text Text -> CompositionGraph Text Text
readLine String
line CompositionGraph Text Text
cg
        | [Token] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
lexedLine = CompositionGraph Text Text
cg
        | Token -> [Token] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Token
Equals [Token]
lexedLine = [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addCompositionLawEntry [Token]
lexedLine CompositionGraph Text Text
cg
        | Token -> [Token] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Token
BeginArrow [Token]
lexedLine = [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addMorphism [Token]
lexedLine CompositionGraph Text Text
cg
        | Bool
otherwise = [Token] -> CompositionGraph Text Text -> CompositionGraph Text Text
addObject [Token]
lexedLine CompositionGraph Text Text
cg
        where
            lexedLine :: [Token]
lexedLine = (String -> [Token]
parserLex String
line)
    
    -- | Unsafe version of 'readCGString' which does not check the structure of the result 'CompositionGraph'.

    unsafeReadCGString :: String -> CG
    unsafeReadCGString :: String -> CompositionGraph Text Text
unsafeReadCGString String
str = CompositionGraph Text Text
newCG
        where
            ls :: [String]
ls = String -> [String]
lines String
str
            cg :: CompositionGraph a b
cg = CompositionGraph a b
forall a b. CompositionGraph a b
emptyCompositionGraph
            newCG :: CompositionGraph Text Text
newCG = (String
 -> CompositionGraph Text Text -> CompositionGraph Text Text)
-> CompositionGraph Text Text
-> [String]
-> CompositionGraph Text Text
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> CompositionGraph Text Text -> CompositionGraph Text Text
readLine CompositionGraph Text Text
forall a b. CompositionGraph a b
cg [String]
ls
    
    -- | Read a .cg string to create a 'CompositionGraph'.

    --

    -- A .cg string follows the following rules :

    --

    -- 0. Every character of a line following a "#" character are ignored.

    --

    -- 1. Each line defines either an object, a morphism or a composition law entry.

    --

    -- 2. The following strings are reserved : " -","-> "," = ", "\<ID/\>", "\<SRC\>", "\</SRC\>", "\<TGT\>", "\</TGT\>", " => "

    --

    -- 3. To define an object, write a line containing its name.

    --

    -- 4. To define an arrow, the syntax "source_object -name_of_morphism-> target_object" is used, where "source_object", "target_object" and "name_of_morphism" should be replaced.

    --

    -- 4.1. If an object mentionned in an arrow does not exist, it is created.

    --

    -- 4.2. The spaces are important. 

    --

    -- 5. To define a composition law entry, the syntax "source_object1 -name_of_first_morphism-> middle_object -name_of_second_morphism-> target_object1 = source_object2 -name_of_composite_morphism-> target_object2" is used, where "source_object1", "name_of_first_morphism", "middle_object", "name_of_second_morphism", "target_object1", "source_object2", "name_of_composite_morphism", "target_object2" should be replaced.

    --

    -- 5.1 If an object mentionned does not exist, it is created.

    --

    -- 5.2 If a morphism mentionned does not exist, it is created.

    --

    -- 5.3 You can use the tag \<ID/\> in order to map a morphism to an identity.    

    readCGString :: String -> Either (FiniteCategoryError (CGMorphism Text Text) Text) CG
    readCGString :: String
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
readCGString String
str
        | Maybe (FiniteCategoryError (CGMorphism Text Text) Text) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
check = CompositionGraph Text Text
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
forall a b. b -> Either a b
Right CompositionGraph Text Text
c_g
        | Bool
otherwise = FiniteCategoryError (CGMorphism Text Text) Text
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
forall a b. a -> Either a b
Left FiniteCategoryError (CGMorphism Text Text) Text
err
        where
            c_g :: CompositionGraph Text Text
c_g = String -> CompositionGraph Text Text
unsafeReadCGString String
str
            check :: Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
check = CompositionGraph Text Text
-> Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategory CompositionGraph Text Text
c_g
            Just FiniteCategoryError (CGMorphism Text Text) Text
err = Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
check
            
    
    -- | Unsafe version of 'readCGFile' which does not check the structure of the resulting 'CompositionGraph'.

    unsafeReadCGFile :: String -> IO CG
    unsafeReadCGFile :: String -> IO (CompositionGraph Text Text)
unsafeReadCGFile String
path = do
        String
file <- String -> IO String
readFile String
path
        CompositionGraph Text Text -> IO (CompositionGraph Text Text)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CompositionGraph Text Text -> IO (CompositionGraph Text Text))
-> CompositionGraph Text Text -> IO (CompositionGraph Text Text)
forall a b. (a -> b) -> a -> b
$ String -> CompositionGraph Text Text
unsafeReadCGString String
file
    
    
    -- | Read a .cg file to create a 'CompositionGraph'.

    --

    -- A .cg file follows the following rules :

    --

    -- 0. Every character of a line following a "#" character are ignored.

    --

    -- 1. Each line defines either an object, a morphism or a composition law entry.

    --

    -- 2. The following strings are reserved : " -","-> "," = ", "\<ID/\>", "\<SRC\>", "\</SRC\>", "\<TGT\>", "\</TGT\>", " => "

    --

    -- 3. To define an object, write a line containing its name.

    --

    -- 4. To define an arrow, the syntax "source_object -name_of_morphism-> target_object" is used, where "source_object", "target_object" and "name_of_morphism" should be replaced.

    --

    -- 4.1. If an object mentionned in an arrow does not exist, it is created.

    --

    -- 4.2. The spaces are important. 

    --

    -- 5. To define a composition law entry, the syntax "source_object1 -name_of_first_morphism-> middle_object -name_of_second_morphism-> target_object1 = source_object2 -name_of_composite_morphism-> target_object2" is used, where "source_object1", "name_of_first_morphism", "middle_object", "name_of_second_morphism", "target_object1", "source_object2", "name_of_composite_morphism", "target_object2" should be replaced.

    --

    -- 5.1 If an object mentionned does not exist, it is created.

    --

    -- 5.2 If a morphism mentionned does not exist, it is created.

    --

    -- 5.3 You can use the tag \<ID/\> in order to map a morphism to an identity.

    readCGFile :: String -> IO (Either (FiniteCategoryError (CGMorphism Text Text) Text) CG)
    readCGFile :: String
-> IO
     (Either
        (FiniteCategoryError (CGMorphism Text Text) Text)
        (CompositionGraph Text Text))
readCGFile String
str = do
        CompositionGraph Text Text
cg <- String -> IO (CompositionGraph Text Text)
unsafeReadCGFile String
str
        let check :: Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
check = CompositionGraph Text Text
-> Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Maybe (FiniteCategoryError m o)
checkFiniteCategory CompositionGraph Text Text
cg
        Either
  (FiniteCategoryError (CGMorphism Text Text) Text)
  (CompositionGraph Text Text)
-> IO
     (Either
        (FiniteCategoryError (CGMorphism Text Text) Text)
        (CompositionGraph Text Text))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Maybe (FiniteCategoryError (CGMorphism Text Text) Text) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
check then CompositionGraph Text Text
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
forall a b. b -> Either a b
Right CompositionGraph Text Text
cg else FiniteCategoryError (CGMorphism Text Text) Text
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
forall a b. a -> Either a b
Left (FiniteCategoryError (CGMorphism Text Text) Text
 -> Either
      (FiniteCategoryError (CGMorphism Text Text) Text)
      (CompositionGraph Text Text))
-> FiniteCategoryError (CGMorphism Text Text) Text
-> Either
     (FiniteCategoryError (CGMorphism Text Text) Text)
     (CompositionGraph Text Text)
forall a b. (a -> b) -> a -> b
$ Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
-> FiniteCategoryError (CGMorphism Text Text) Text
forall {a}. Maybe a -> a
fromJust (Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
 -> FiniteCategoryError (CGMorphism Text Text) Text)
-> Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
-> FiniteCategoryError (CGMorphism Text Text) Text
forall a b. (a -> b) -> a -> b
$ Maybe (FiniteCategoryError (CGMorphism Text Text) Text)
check)
        where
            fromJust :: Maybe a -> a
fromJust (Just a
x) = a
x
        
    reversedRawPathToString :: (PrettyPrint a, PrettyPrint b) => RawPath a b -> String
    reversedRawPathToString :: forall a b. (PrettyPrint a, PrettyPrint b) => RawPath a b -> String
reversedRawPathToString [] = String
"<ID>"
    reversedRawPathToString [Arrow{sourceArrow :: forall n e. Arrow n e -> n
sourceArrow = a
s, targetArrow :: forall n e. Arrow n e -> n
targetArrow = a
t,labelArrow :: forall n e. Arrow n e -> e
labelArrow = b
l}] = a -> String
forall a. PrettyPrint a => a -> String
pprint a
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -" String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. PrettyPrint a => a -> String
pprint b
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. PrettyPrint a => a -> String
pprint a
t
    reversedRawPathToString (Arrow{sourceArrow :: forall n e. Arrow n e -> n
sourceArrow = a
s, targetArrow :: forall n e. Arrow n e -> n
targetArrow = a
t,labelArrow :: forall n e. Arrow n e -> e
labelArrow = b
l}:[Arrow a b]
xs) = a -> String
forall a. PrettyPrint a => a -> String
pprint a
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -" String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. PrettyPrint a => a -> String
pprint b
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Arrow a b] -> String
forall a b. (PrettyPrint a, PrettyPrint b) => RawPath a b -> String
reversedRawPathToString [Arrow a b]
xs
    
    -- | Transform a composition graph into a string following the .cg convention.

    writeCGString :: (PrettyPrint a, PrettyPrint b, Eq a, Eq b) => CompositionGraph a b -> String
    writeCGString :: forall a b.
(PrettyPrint a, PrettyPrint b, Eq a, Eq b) =>
CompositionGraph a b -> String
writeCGString CompositionGraph a b
cg = String
finalString
        where
            obString :: String
obString = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. PrettyPrint a => a -> String
pprint (a -> String) -> [a] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList(Set a -> [a])
-> (CompositionGraph a b -> Set a) -> CompositionGraph a b -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob (CompositionGraph a b -> [a]) -> CompositionGraph a b -> [a]
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            arNotIdentityAndNotComposite :: [CGMorphism a b]
arNotIdentityAndNotComposite = Set (CGMorphism a b) -> [CGMorphism a b]
forall a. Eq a => Set a -> [a]
setToList (Set (CGMorphism a b) -> [CGMorphism a b])
-> Set (CGMorphism a b) -> [CGMorphism a b]
forall a b. (a -> b) -> a -> b
$ (CGMorphism a b -> Bool)
-> Set (CGMorphism a b) -> Set (CGMorphism a b)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator CompositionGraph a b
cg) (Set (CGMorphism a b) -> Set (CGMorphism a b))
-> Set (CGMorphism a b) -> Set (CGMorphism a b)
forall a b. (a -> b) -> a -> b
$ (CGMorphism a b -> Bool)
-> Set (CGMorphism a b) -> Set (CGMorphism a b)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity CompositionGraph a b
cg) (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows CompositionGraph a b
cg)
            reversedRawPaths :: [[Arrow a b]]
reversedRawPaths = ([Arrow a b] -> [Arrow a b]
forall a. [a] -> [a]
reverse([Arrow a b] -> [Arrow a b])
-> (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path) (CGMorphism a b -> [Arrow a b])
-> [CGMorphism a b] -> [[Arrow a b]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CGMorphism a b]
arNotIdentityAndNotComposite
            arString :: String
arString = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Arrow a b] -> String
forall a b. (PrettyPrint a, PrettyPrint b) => RawPath a b -> String
reversedRawPathToString ([Arrow a b] -> String) -> [[Arrow a b]] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Arrow a b]]
reversedRawPaths
            lawString :: String
lawString = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (\([Arrow a b]
rp1,[Arrow a b]
rp2) -> ([Arrow a b] -> String
forall a b. (PrettyPrint a, PrettyPrint b) => RawPath a b -> String
reversedRawPathToString ([Arrow a b] -> [Arrow a b]
forall a. [a] -> [a]
reverse [Arrow a b]
rp1)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Arrow a b] -> String
forall a b. (PrettyPrint a, PrettyPrint b) => RawPath a b -> String
reversedRawPathToString ([Arrow a b] -> [Arrow a b]
forall a. [a] -> [a]
reverse [Arrow a b]
rp2))) (([Arrow a b], [Arrow a b]) -> String)
-> [([Arrow a b], [Arrow a b])] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map [Arrow a b] [Arrow a b] -> [([Arrow a b], [Arrow a b])]
forall k a. Eq k => Map k a -> [(k, a)]
Map.toList)(Map [Arrow a b] [Arrow a b] -> [([Arrow a b], [Arrow a b])])
-> (CompositionGraph a b -> Map [Arrow a b] [Arrow a b])
-> CompositionGraph a b
-> [([Arrow a b], [Arrow a b])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Map [Arrow a b] [Arrow a b]
forall a b. CompositionGraph a b -> CompositionLaw a b
law (CompositionGraph a b -> [([Arrow a b], [Arrow a b])])
-> CompositionGraph a b -> [([Arrow a b], [Arrow a b])]
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            finalString :: String
finalString = String
"#Objects :\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++String
obStringString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n\n# Arrows :\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++String
arStringString -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n\n# Composition law :\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++String
lawString
        
    -- | Saves a composition graph into a file located at a given path.

    writeCGFile :: (PrettyPrint a, PrettyPrint b, Eq a, Eq b) => CompositionGraph a b -> String -> IO ()
    writeCGFile :: forall a b.
(PrettyPrint a, PrettyPrint b, Eq a, Eq b) =>
CompositionGraph a b -> String -> IO ()
writeCGFile CompositionGraph a b
cg String
filepath = do
        Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ ShowS
takeDirectory String
filepath
        String -> String -> IO ()
writeFile String
filepath (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b -> String
forall a b.
(PrettyPrint a, PrettyPrint b, Eq a, Eq b) =>
CompositionGraph a b -> String
writeCGString CompositionGraph a b
cg
        
        
    -----------------------

    -- CGD FILE

    -----------------------


    type CGD = Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (CompositionGraph Text Text) (CGMorphism Text Text) Text 
    
    addOMapEntry :: [Token] -> CGD -> CGD
    addOMapEntry :: [Token] -> CGD -> CGD
addOMapEntry [Name Text
x, Token
MapsTo, Name Text
y] CGD
diag
        | Text
x Text -> Set Text -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (Map Text Text -> Set Text
forall k a. Map k a -> Set k
domain (CGD -> Map Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap CGD
diag)) = if Text
y Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== (CGD
diag CGD -> Text -> Text
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ Text
x) then CGD
diag else String -> CGD
forall a. HasCallStack => String -> a
error (String
"Incoherent maps of object : F("String -> ShowS
forall a. [a] -> [a] -> [a]
++Text -> String
forall a. Show a => a -> String
show Text
xString -> ShowS
forall a. [a] -> [a] -> [a]
++String
") = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Text -> String
forall a. Show a => a -> String
show Text
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and "String -> ShowS
forall a. [a] -> [a] -> [a]
++Text -> String
forall a. Show a => a -> String
show (CGD
diag CGD -> Text -> Text
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ Text
x))
        | Bool
otherwise = Diagram{src :: CompositionGraph Text Text
src=CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src CGD
diag, tgt :: CompositionGraph Text Text
tgt=CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt CGD
diag, omap :: Map Text Text
omap=Text -> Text -> Map Text Text -> Map Text Text
forall k a. k -> a -> Map k a -> Map k a
Map.insert Text
x Text
y (CGD -> Map Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap CGD
diag), mmap :: Map (CGMorphism Text Text) (CGMorphism Text Text)
mmap=CGD -> Map (CGMorphism Text Text) (CGMorphism Text Text)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap CGD
diag}
    addOMapEntry [Token]
otherTokens CGD
_ = String -> CGD
forall a. HasCallStack => String -> a
error (String -> CGD) -> String -> CGD
forall a b. (a -> b) -> a -> b
$ String
"addOMapEntry on invalid tokens : "String -> ShowS
forall a. [a] -> [a] -> [a]
++[Token] -> String
forall a. Show a => a -> String
show [Token]
otherTokens
    
    addMMapEntry :: [Token] -> CGD -> CGD
    addMMapEntry :: [Token] -> CGD -> CGD
addMMapEntry tks :: [Token]
tks@[Name Text
sx, Token
BeginArrow, Name Text
lx, Token
EndArrow, Name Text
tx, Token
MapsTo, Token
Identity] CGD
diag = if Text
sx Text -> Set Text -> Bool
forall a. Eq a => a -> Set a -> Bool
`isIn` (Map Text Text -> Set Text
forall k a. Map k a -> Set k
domain (CGD -> Map Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap CGD
diag)) then Diagram{src :: CompositionGraph Text Text
src=CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src CGD
diag, tgt :: CompositionGraph Text Text
tgt=CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt CGD
diag, omap :: Map Text Text
omap=CGD -> Map Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap CGD
diag, mmap :: Map (CGMorphism Text Text) (CGMorphism Text Text)
mmap=CGMorphism Text Text
-> CGMorphism Text Text
-> Map (CGMorphism Text Text) (CGMorphism Text Text)
-> Map (CGMorphism Text Text) (CGMorphism Text Text)
forall k a. k -> a -> Map k a -> Map k a
Map.insert CGMorphism Text Text
sourceMorph (CompositionGraph Text Text -> Text -> CGMorphism Text Text
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity (CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt CGD
diag) (CGD
diag CGD -> Text -> Text
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ Text
sx)) (CGD -> Map (CGMorphism Text Text) (CGMorphism Text Text)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap CGD
diag)} else String -> CGD
forall a. HasCallStack => String -> a
error (String
"You must specify the image of the source of the morphism before mapping to an identity : "String -> ShowS
forall a. [a] -> [a] -> [a]
++[Token] -> String
forall a. Show a => a -> String
show [Token]
tks)
        where
            sourceMorphCand :: Set (CGMorphism Text Text)
sourceMorphCand = (CGMorphism Text Text -> Bool)
-> Set (CGMorphism Text Text) -> Set (CGMorphism Text Text)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\CGMorphism Text Text
e -> CGMorphism Text Text -> Maybe Text
forall a b. CGMorphism a b -> Maybe b
getLabel CGMorphism Text Text
e Maybe Text -> Maybe Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> Maybe Text
forall a. a -> Maybe a
Just Text
lx) (CompositionGraph Text Text
-> Text -> Text -> Set (CGMorphism Text Text)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr (CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src CGD
diag) Text
sx Text
tx)
            sourceMorph :: CGMorphism Text Text
sourceMorph = if Set (CGMorphism Text Text) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism Text Text)
sourceMorphCand then String -> CGMorphism Text Text
forall a. HasCallStack => String -> a
error (String -> CGMorphism Text Text) -> String -> CGMorphism Text Text
forall a b. (a -> b) -> a -> b
$ String
"addMMapEntry : morphism not found in source category for the following map : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
tks else Set (CGMorphism Text Text) -> CGMorphism Text Text
forall a. Set a -> a
anElement Set (CGMorphism Text Text)
sourceMorphCand
    addMMapEntry tks :: [Token]
tks@[Name Text
sx, Token
BeginArrow, Name Text
lx, Token
EndArrow, Name Text
tx, Token
MapsTo, Name Text
sy, Token
BeginArrow, Name Text
ly, Token
EndArrow, Name Text
ty] CGD
diag = Diagram{src :: CompositionGraph Text Text
src=CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src CGD
newDiag2, tgt :: CompositionGraph Text Text
tgt=CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt CGD
newDiag2, omap :: Map Text Text
omap=CGD -> Map Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap CGD
newDiag2, mmap :: Map (CGMorphism Text Text) (CGMorphism Text Text)
mmap=CGMorphism Text Text
-> CGMorphism Text Text
-> Map (CGMorphism Text Text) (CGMorphism Text Text)
-> Map (CGMorphism Text Text) (CGMorphism Text Text)
forall k a. k -> a -> Map k a -> Map k a
Map.insert CGMorphism Text Text
sourceMorph CGMorphism Text Text
targetMorph (CGD -> Map (CGMorphism Text Text) (CGMorphism Text Text)
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap CGD
newDiag2)}
        where
            sourceMorphCand :: Set (CGMorphism Text Text)
sourceMorphCand = (CGMorphism Text Text -> Bool)
-> Set (CGMorphism Text Text) -> Set (CGMorphism Text Text)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\CGMorphism Text Text
e -> CGMorphism Text Text -> Maybe Text
forall a b. CGMorphism a b -> Maybe b
getLabel CGMorphism Text Text
e Maybe Text -> Maybe Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> Maybe Text
forall a. a -> Maybe a
Just Text
lx) (CompositionGraph Text Text
-> Text -> Text -> Set (CGMorphism Text Text)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr (CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src CGD
diag) Text
sx Text
tx)
            targetMorphCand :: Set (CGMorphism Text Text)
targetMorphCand = (CGMorphism Text Text -> Bool)
-> Set (CGMorphism Text Text) -> Set (CGMorphism Text Text)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\CGMorphism Text Text
e -> CGMorphism Text Text -> Maybe Text
forall a b. CGMorphism a b -> Maybe b
getLabel CGMorphism Text Text
e Maybe Text -> Maybe Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text -> Maybe Text
forall a. a -> Maybe a
Just Text
ly) (CompositionGraph Text Text
-> Text -> Text -> Set (CGMorphism Text Text)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr (CGD -> CompositionGraph Text Text
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt CGD
diag) Text
sy Text
ty)
            sourceMorph :: CGMorphism Text Text
sourceMorph = if Set (CGMorphism Text Text) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism Text Text)
sourceMorphCand then String -> CGMorphism Text Text
forall a. HasCallStack => String -> a
error (String -> CGMorphism Text Text) -> String -> CGMorphism Text Text
forall a b. (a -> b) -> a -> b
$ String
"addMMapEntry : morphism not found in source category for the following map : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
tks else Set (CGMorphism Text Text) -> CGMorphism Text Text
forall a. Set a -> a
anElement Set (CGMorphism Text Text)
sourceMorphCand
            targetMorph :: CGMorphism Text Text
targetMorph = if Set (CGMorphism Text Text) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism Text Text)
targetMorphCand then String -> CGMorphism Text Text
forall a. HasCallStack => String -> a
error (String -> CGMorphism Text Text) -> String -> CGMorphism Text Text
forall a b. (a -> b) -> a -> b
$ String
"addMMapEntry : morphism not found in target category for the following map : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Token] -> String
forall a. Show a => a -> String
show [Token]
tks else Set (CGMorphism Text Text) -> CGMorphism Text Text
forall a. Set a -> a
anElement Set (CGMorphism Text Text)
targetMorphCand
            newDiag1 :: CGD
newDiag1 = [Token] -> CGD -> CGD
addOMapEntry [Text -> Token
Name Text
sx, Token
MapsTo, Text -> Token
Name Text
sy] CGD
diag
            newDiag2 :: CGD
newDiag2 = [Token] -> CGD -> CGD
addOMapEntry [Text -> Token
Name Text
tx, Token
MapsTo, Text -> Token
Name Text
ty] CGD
newDiag1    
    addMMapEntry [Token]
otherTokens CGD
_ = String -> CGD
forall a. HasCallStack => String -> a
error (String -> CGD) -> String -> CGD
forall a b. (a -> b) -> a -> b
$ String
"addMMapEntry on invalid tokens : "String -> ShowS
forall a. [a] -> [a] -> [a]
++[Token] -> String
forall a. Show a => a -> String
show [Token]
otherTokens
    
    readLineD :: String -> CGD -> CGD
    readLineD :: String -> CGD -> CGD
readLineD String
line diag :: CGD
diag@Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=CompositionGraph Text Text
s, tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=CompositionGraph Text Text
t, omap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map o1 o2
omap=Map Text Text
om, mmap :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> Map m1 m2
mmap=Map (CGMorphism Text Text) (CGMorphism Text Text)
mm}
        | [Token] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
lexedLine = CGD
diag
        | Token -> [Token] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Token
MapsTo [Token]
lexedLine = if Token -> [Token] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Token
BeginArrow [Token]
lexedLine
            then [Token] -> CGD -> CGD
addMMapEntry [Token]
lexedLine CGD
diag
            else [Token] -> CGD -> CGD
addOMapEntry [Token]
lexedLine CGD
diag
        | Bool
otherwise = CGD
diag
        where
            lexedLine :: [Token]
lexedLine = (String -> [Token]
parserLex String
line)

    extractSrcSection :: [String] -> [String]
    extractSrcSection :: [String] -> [String]
extractSrcSection [String]
lines
        | Bool -> Bool
not ([Token] -> [[Token]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Token
BeginSrc] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines)) = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"No <SRC> section or malformed <SRC> section in file : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
lines
        | Bool -> Bool
not ([Token] -> [[Token]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Token
EndSrc] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines)) = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"No <SRC> section or malformed <SRC> section in file : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
lines
        | Int
indexEndSrc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
indexBeginSrc = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Malformed <SRC> section in file : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
lines
        | Bool
otherwise = [String]
c
        where
            Just Int
indexBeginSrc = ([Token] -> [[Token]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex [Token
BeginSrc] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines))
            Just Int
indexEndSrc = ([Token] -> [[Token]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex [Token
EndSrc] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines))
            ([String]
a,[String]
b) = Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
indexBeginSrcInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [String]
lines
            ([String]
c,[String]
d) = Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
indexEndSrcInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
indexBeginSrcInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [String]
b
            
    extractTgtSection :: [String] -> [String]
    extractTgtSection :: [String] -> [String]
extractTgtSection [String]
lines
        | Bool -> Bool
not ([Token] -> [[Token]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Token
BeginTgt] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines)) = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"No <TGT> section or malformed <TGT> section in file : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
lines
        | Bool -> Bool
not ([Token] -> [[Token]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Token
EndTgt] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines)) = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"No <TGT> section or malformed <TGT> section in file : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
lines
        | Int
indexEndTgt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
indexBeginTgt = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Malformed <TGT> section in file : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
lines
        | Bool
otherwise = [String]
c
        where
            Just Int
indexBeginTgt = ([Token] -> [[Token]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex [Token
BeginTgt] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines))
            Just Int
indexEndTgt = ([Token] -> [[Token]] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex [Token
EndTgt] (String -> [Token]
parserLex (String -> [Token]) -> [String] -> [[Token]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
lines))
            ([String]
a,[String]
b) = Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
indexBeginTgtInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [String]
lines
            ([String]
c,[String]
d) = Int -> [String] -> ([String], [String])
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
indexEndTgtInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
indexBeginTgtInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [String]
b
          
        
    -- | Unsafe version of 'readCGDString' which does not check the structure of the resulting 'Diagram'.

    unsafeReadCGDString :: String -> CGD
    unsafeReadCGDString :: String -> CGD
unsafeReadCGDString String
str = CGD -> CGD
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram CGD
finalDiag
        where
            ls :: [String]
ls = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not(Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Token] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null([Token] -> Bool) -> (String -> [Token]) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.String -> [Token]
parserLex) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
str
            s :: CompositionGraph Text Text
s = String -> CompositionGraph Text Text
unsafeReadCGString (String -> CompositionGraph Text Text)
-> String -> CompositionGraph Text Text
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> [String]
extractSrcSection [String]
ls)
            t :: CompositionGraph Text Text
t = String -> CompositionGraph Text Text
unsafeReadCGString (String -> CompositionGraph Text Text)
-> String -> CompositionGraph Text Text
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> [String]
extractTgtSection [String]
ls)
            diag :: Diagram
  (CompositionGraph Text Text)
  m1
  o1
  (CompositionGraph Text Text)
  m2
  o2
diag = Diagram{src :: CompositionGraph Text Text
src=CompositionGraph Text Text
s, tgt :: CompositionGraph Text Text
tgt=CompositionGraph Text Text
t,omap :: Map o1 o2
omap=AssociationList o1 o2 -> Map o1 o2
forall k v. AssociationList k v -> Map k v
weakMap [], mmap :: Map m1 m2
mmap=AssociationList m1 m2 -> Map m1 m2
forall k v. AssociationList k v -> Map k v
weakMap []}
            finalDiag :: CGD
finalDiag = (String -> CGD -> CGD) -> CGD -> [String] -> CGD
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> CGD -> CGD
readLineD CGD
forall {m1} {o1} {m2} {o2}.
Diagram
  (CompositionGraph Text Text)
  m1
  o1
  (CompositionGraph Text Text)
  m2
  o2
diag [String]
ls
        
    -- | Read a .cgd string and returns a diagram. A .cgd string obeys the following rules :

    --

    -- 1. There is a line "\<SRC\>" and a line "\</SRC\>".

    --

    -- 1.1 Between these two lines, the source composition graph is defined as in a cg file.

    --

    -- 2. There is a line "\<TGT\>" and a line "\</TGT\>".

    --

    -- 2.1 Between these two lines, the target composition graph is defined as in a cg file.

    --

    -- 3. Outside of the two previously described sections, you can declare the maps between objects and morphisms.

    --

    -- 3.1 You map an object to another with the following syntax : "object1 => object2".

    --

    -- 3.2 You map a morphism to another with the following syntax : "objSrc1 -arrowSrc1-> objSrc2 => objTgt1 -arrowTgt1-> objTgt2".

    --

    -- 4. You don't have to (and you shouldn't) specify maps from identities, nor maps from composite arrows.

    readCGDString :: String -> Either (DiagramError CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text) CGD
    readCGDString :: String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
str
        | Maybe
  (DiagramError
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text)
-> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Maybe
  (DiagramError
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text)
check = CGD
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
forall a b. b -> Either a b
Right CGD
diag
        | Bool
otherwise = DiagramError
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
forall a b. a -> Either a b
Left DiagramError
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
err
        where
            diag :: CGD
diag = String -> CGD
unsafeReadCGDString String
str
            check :: Maybe
  (DiagramError
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text)
check = CGD
-> Maybe
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
forall c1 m1 o1 c2 m2 o2.
(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 -> Maybe (DiagramError c1 m1 o1 c2 m2 o2)
checkFiniteDiagram CGD
diag
            Just DiagramError
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
  (CompositionGraph Text Text)
  (CGMorphism Text Text)
  Text
err = Maybe
  (DiagramError
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text)
check
            
    -- | Unsafe version 'readCGDFile' which does not check the structure of the resulting 'Diagram'.

    unsafeReadCGDFile :: String -> IO CGD
    unsafeReadCGDFile :: String -> IO CGD
unsafeReadCGDFile String
path = do
        String
raw <- String -> IO String
readFile String
path
        CGD -> IO CGD
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> CGD
unsafeReadCGDString String
raw)
        
    -- | Read a .cgd file and returns a diagram. A .cgd file obeys the following rules :

    --

    -- 1. There is a line "\<SRC\>" and a line "\</SRC\>".

    --

    -- 1.1 Between these two lines, the source composition graph is defined as in a cg file.

    --

    -- 2. There is a line "\<TGT\>" and a line "\</TGT\>".

    --

    -- 2.1 Between these two lines, the target composition graph is defined as in a cg file.

    --

    -- 3. Outside of the two previously described sections, you can declare the maps between objects and morphisms.

    --

    -- 3.1 You map an object to another with the following syntax : "object1 => object2".

    --

    -- 3.2 You map a morphism to another with the following syntax : "objSrc1 -arrowSrc1-> objSrc2 => objTgt1 -arrowTgt1-> objTgt2".

    --

    -- 4. You don't have to (and you shouldn't) specify maps from identities, nor maps from composite arrows.

    readCGDFile :: String -> IO (Either (DiagramError CG (CGMorphism Text Text) Text CG (CGMorphism Text Text) Text) CGD)
    readCGDFile :: String
-> IO
     (Either
        (DiagramError
           (CompositionGraph Text Text)
           (CGMorphism Text Text)
           Text
           (CompositionGraph Text Text)
           (CGMorphism Text Text)
           Text)
        CGD)
readCGDFile String
path = do
        String
raw <- String -> IO String
readFile String
path
        Either
  (DiagramError
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text
     (CompositionGraph Text Text)
     (CGMorphism Text Text)
     Text)
  CGD
-> IO
     (Either
        (DiagramError
           (CompositionGraph Text Text)
           (CGMorphism Text Text)
           Text
           (CompositionGraph Text Text)
           (CGMorphism Text Text)
           Text)
        CGD)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
-> Either
     (DiagramError
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text
        (CompositionGraph Text Text)
        (CGMorphism Text Text)
        Text)
     CGD
readCGDString String
raw)
        
    -- | Transform a composition graph diagram into a string following the .cgd convention.

    writeCGDString :: (PrettyPrint a1, PrettyPrint b1, Eq a1, Eq b1,
                       PrettyPrint a2, PrettyPrint b2, Eq a2, Eq b2) => 
                    Diagram (CompositionGraph a1 b1) (CGMorphism a1 b1) a1 (CompositionGraph a2 b2) (CGMorphism a2 b2) a2 -> String
    writeCGDString :: forall a1 b1 a2 b2.
(PrettyPrint a1, PrettyPrint b1, Eq a1, Eq b1, PrettyPrint a2,
 PrettyPrint b2, Eq a2, Eq b2) =>
Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> String
writeCGDString Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag = String
srcString String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
tgtString String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
omapString String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
mmapString
        where
            srcString :: String
srcString = String
"<SRC>\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++CompositionGraph a1 b1 -> String
forall a b.
(PrettyPrint a, PrettyPrint b, Eq a, Eq b) =>
CompositionGraph a b -> String
writeCGString (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CompositionGraph a1 b1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"\n</SRC>\n"
            tgtString :: String
tgtString = String
"<TGT>\n"String -> ShowS
forall a. [a] -> [a] -> [a]
++CompositionGraph a2 b2 -> String
forall a b.
(PrettyPrint a, PrettyPrint b, Eq a, Eq b) =>
CompositionGraph a b -> String
writeCGString (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CompositionGraph a2 b2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"</TGT>\n"
            omapString :: String
omapString = String
"#Object mapping\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (\a1
o -> (a1 -> String
forall a. PrettyPrint a => a -> String
pprint a1
o) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" => " String -> ShowS
forall a. [a] -> [a] -> [a]
++  (a2 -> String
forall a. PrettyPrint a => a -> String
pprint (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> a1 -> a2
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ a1
o)) )(a1 -> String) -> [a1] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set a1 -> [a1]
forall a. Eq a => Set a -> [a]
setToList(Set a1 -> [a1])
-> (Diagram
      (CompositionGraph a1 b1)
      (CGMorphism a1 b1)
      a1
      (CompositionGraph a2 b2)
      (CGMorphism a2 b2)
      a2
    -> Set a1)
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> [a1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a1 b1 -> Set a1
forall c m o. FiniteCategory c m o => c -> Set o
ob(CompositionGraph a1 b1 -> Set a1)
-> (Diagram
      (CompositionGraph a1 b1)
      (CGMorphism a1 b1)
      a1
      (CompositionGraph a2 b2)
      (CGMorphism a2 b2)
      a2
    -> CompositionGraph a1 b1)
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> Set a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CompositionGraph a1 b1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram
   (CompositionGraph a1 b1)
   (CGMorphism a1 b1)
   a1
   (CompositionGraph a2 b2)
   (CGMorphism a2 b2)
   a2
 -> [a1])
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> [a1]
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
            mmapString :: String
mmapString = String
"#Morphism mapping\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (\CGMorphism a1 b1
m -> a1 -> String
forall a. PrettyPrint a => a -> String
pprint (CGMorphism a1 b1 -> a1
forall m o. Morphism m o => m -> o
source CGMorphism a1 b1
m) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CGMorphism a1 b1 -> String
forall a. PrettyPrint a => a -> String
pprint CGMorphism a1 b1
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a1 -> String
forall a. PrettyPrint a => a -> String
pprint (CGMorphism a1 b1 -> a1
forall m o. Morphism m o => m -> o
target CGMorphism a1 b1
m)String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" => " String -> ShowS
forall a. [a] -> [a] -> [a]
++ if CompositionGraph a2 b2 -> CGMorphism a2 b2 -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isIdentity (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CompositionGraph a2 b2
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag) (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CGMorphism a1 b1 -> CGMorphism a2 b2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ CGMorphism a1 b1
m) then String
"<ID/>" else a2 -> String
forall a. PrettyPrint a => a -> String
pprint (CGMorphism a2 b2 -> a2
forall m o. Morphism m o => m -> o
source (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CGMorphism a1 b1 -> CGMorphism a2 b2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ CGMorphism a1 b1
m)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CGMorphism a2 b2 -> String
forall a. PrettyPrint a => a -> String
pprint (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CGMorphism a1 b1 -> CGMorphism a2 b2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ CGMorphism a1 b1
m) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a2 -> String
forall a. PrettyPrint a => a -> String
pprint (CGMorphism a2 b2 -> a2
forall m o. Morphism m o => m -> o
target (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CGMorphism a1 b1 -> CGMorphism a2 b2
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ CGMorphism a1 b1
m)))(CGMorphism a1 b1 -> String) -> [CGMorphism a1 b1] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Set (CGMorphism a1 b1) -> [CGMorphism a1 b1]
forall a. Eq a => Set a -> [a]
setToList(Set (CGMorphism a1 b1) -> [CGMorphism a1 b1])
-> (Diagram
      (CompositionGraph a1 b1)
      (CGMorphism a1 b1)
      a1
      (CompositionGraph a2 b2)
      (CGMorphism a2 b2)
      a2
    -> Set (CGMorphism a1 b1))
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> [CGMorphism a1 b1]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.((CGMorphism a1 b1 -> Bool)
-> Set (CGMorphism a1 b1) -> Set (CGMorphism a1 b1)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (CompositionGraph a1 b1 -> CGMorphism a1 b1 -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m, Eq o) =>
c -> m -> Bool
isNotIdentity (Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CompositionGraph a1 b1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag)))(Set (CGMorphism a1 b1) -> Set (CGMorphism a1 b1))
-> (Diagram
      (CompositionGraph a1 b1)
      (CGMorphism a1 b1)
      a1
      (CompositionGraph a2 b2)
      (CGMorphism a2 b2)
      a2
    -> Set (CGMorphism a1 b1))
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> Set (CGMorphism a1 b1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a1 b1 -> Set (CGMorphism a1 b1)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows(CompositionGraph a1 b1 -> Set (CGMorphism a1 b1))
-> (Diagram
      (CompositionGraph a1 b1)
      (CGMorphism a1 b1)
      a1
      (CompositionGraph a2 b2)
      (CGMorphism a2 b2)
      a2
    -> CompositionGraph a1 b1)
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> Set (CGMorphism a1 b1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> CompositionGraph a1 b1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (Diagram
   (CompositionGraph a1 b1)
   (CGMorphism a1 b1)
   a1
   (CompositionGraph a2 b2)
   (CGMorphism a2 b2)
   a2
 -> [CGMorphism a1 b1])
-> Diagram
     (CompositionGraph a1 b1)
     (CGMorphism a1 b1)
     a1
     (CompositionGraph a2 b2)
     (CGMorphism a2 b2)
     a2
-> [CGMorphism a1 b1]
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
        
    -- | Saves a composition graph diagram into a file located at a given path.

    writeCGDFile :: (PrettyPrint a1, PrettyPrint b1, Eq a1, Eq b1,
                     PrettyPrint a2, PrettyPrint b2, Eq a2, Eq b2) => 
                    Diagram (CompositionGraph a1 b1) (CGMorphism a1 b1) a1 (CompositionGraph a2 b2) (CGMorphism a2 b2) a2 -> String -> IO ()
    writeCGDFile :: forall a1 b1 a2 b2.
(PrettyPrint a1, PrettyPrint b1, Eq a1, Eq b1, PrettyPrint a2,
 PrettyPrint b2, Eq a2, Eq b2) =>
Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> String -> IO ()
writeCGDFile Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag String
filepath = do
        Bool -> String -> IO ()
createDirectoryIfMissing Bool
True (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ ShowS
takeDirectory String
filepath
        String -> String -> IO ()
writeFile String
filepath (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> String
forall a1 b1 a2 b2.
(PrettyPrint a1, PrettyPrint b1, Eq a1, Eq b1, PrettyPrint a2,
 PrettyPrint b2, Eq a2, Eq b2) =>
Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
-> String
writeCGDString Diagram
  (CompositionGraph a1 b1)
  (CGMorphism a1 b1)
  a1
  (CompositionGraph a2 b2)
  (CGMorphism a2 b2)
  a2
diag
        
        

-----------------------

-- Random CompositionGraph

-----------------------

        
        
        
        
        
    -- | Find first order composites arrows in a composition graph.

    compositeMorphisms :: (Eq a, Eq b, Show a) => CompositionGraph a b -> [CGMorphism a b]
    compositeMorphisms :: forall a b.
(Eq a, Eq b, Show a) =>
CompositionGraph a b -> [CGMorphism a b]
compositeMorphisms CompositionGraph a b
c = Set (CGMorphism a b) -> [CGMorphism a b]
forall a. Eq a => Set a -> [a]
setToList [CGMorphism a b
g CGMorphism a b -> CGMorphism a b -> CGMorphism a b
forall m o. Morphism m o => m -> m -> m
@ CGMorphism a b
f | CGMorphism a b
f <- CompositionGraph a b -> Set (CGMorphism a b)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows CompositionGraph a b
c, CGMorphism a b
g <- CompositionGraph a b -> a -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom CompositionGraph a b
c (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
f), Bool -> Bool
not (CGMorphism a b -> Set (CGMorphism a b) -> Bool
forall a. Eq a => a -> Set a -> Bool
isIn (CGMorphism a b
g CGMorphism a b -> CGMorphism a b -> CGMorphism a b
forall m o. Morphism m o => m -> m -> m
@ CGMorphism a b
f) (CompositionGraph a b -> a -> a -> Set (CGMorphism a b)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr CompositionGraph a b
c (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
f) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
g)))]

    -- | Merge two nodes.

    mergeNodes :: (Eq a, Eq b) => CompositionGraph a b -> a -> a -> CompositionGraph a b
    mergeNodes :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes cg :: CompositionGraph a b
cg@CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph a b
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw a b
l} a
s a
t
        | Bool -> Bool
not (a -> Set a -> Bool
forall a. Eq a => a -> Set a -> Bool
isIn a
s (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes Graph a b
g)) = String -> CompositionGraph a b
forall a. HasCallStack => String -> a
error String
"mapped but not in rcg."
        | Bool -> Bool
not (a -> Set a -> Bool
forall a. Eq a => a -> Set a -> Bool
isIn a
t (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes Graph a b
g)) = String -> CompositionGraph a b
forall a. HasCallStack => String -> a
error String
"mapped to but not in rcg."
        | a
s a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
t = CompositionGraph a b
cg
        | Bool
otherwise = CompositionGraph {support :: Graph a b
support=Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ((a -> Bool) -> Set a -> Set a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/=a
s) (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes Graph a b
g)) (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> Set (Arrow a b) -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph a b
g)), law :: CompositionLaw a b
law=CompositionLaw a b
newLaw}
        where
            replace :: a -> a
replace a
x = if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
s then a
t else a
x
            replaceArrow :: Arrow a e -> Arrow a e
replaceArrow Arrow{sourceArrow :: forall n e. Arrow n e -> n
sourceArrow=a
s3,targetArrow :: forall n e. Arrow n e -> n
targetArrow=a
t3,labelArrow :: forall n e. Arrow n e -> e
labelArrow=e
l3} = Arrow{sourceArrow :: a
sourceArrow=a -> a
replace a
s3,targetArrow :: a
targetArrow=a -> a
replace a
t3,labelArrow :: e
labelArrow=e
l3}
            newLaw :: CompositionLaw a b
newLaw = AssociationList [Arrow a b] [Arrow a b] -> CompositionLaw a b
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList [Arrow a b] [Arrow a b] -> CompositionLaw a b)
-> AssociationList [Arrow a b] [Arrow a b] -> CompositionLaw a b
forall a b. (a -> b) -> a -> b
$ (\([Arrow a b]
k,[Arrow a b]
v) -> (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> [Arrow a b] -> [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
k, Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> [Arrow a b] -> [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
v)) (([Arrow a b], [Arrow a b]) -> ([Arrow a b], [Arrow a b]))
-> AssociationList [Arrow a b] [Arrow a b]
-> AssociationList [Arrow a b] [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompositionLaw a b -> AssociationList [Arrow a b] [Arrow a b]
forall k a. Eq k => Map k a -> [(k, a)]
Map.mapToList CompositionLaw a b
l)
    
    -- | Merge two morphisms of a composition graph, the morphism mapped should be composite, the morphism mapped to should be a generator.

    mergeMorphisms :: (Eq a, Eq b) => CompositionGraph a b -> CGMorphism a b -> CGMorphism a b -> CompositionGraph a b
    mergeMorphisms :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b -> CGMorphism a b -> CompositionGraph a b
mergeMorphisms cg :: CompositionGraph a b
cg@CompositionGraph{support :: forall a b. CompositionGraph a b -> Graph a b
support=Graph a b
g,law :: forall a b. CompositionGraph a b -> CompositionLaw a b
law=CompositionLaw a b
l} s :: CGMorphism a b
s@CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=p1 :: Path a b
p1@(a
s1,RawPath a b
rp1),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
l1} t :: CGMorphism a b
t@CGMorphism{path :: forall a b. CGMorphism a b -> Path a b
path=p2 :: Path a b
p2@(a
s2,RawPath a b
rp2),compositionLaw :: forall a b. CGMorphism a b -> CompositionLaw a b
compositionLaw=CompositionLaw a b
l2}
        | (CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator CompositionGraph a b
cg CGMorphism a b
s) = String -> CompositionGraph a b
forall a. HasCallStack => String -> a
error String
"Generator at the start of a merge"
        | (CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isComposite CompositionGraph a b
cg CGMorphism a b
t) = String -> CompositionGraph a b
forall a. HasCallStack => String -> a
error String
"Composite at the end of a merge"
        | a
s1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Path a b -> a
forall {a} {e}. (a, [Arrow a e]) -> a
targetPath Path a b
p1 =  CompositionGraph a b -> a -> a -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes CompositionGraph{support :: Graph a b
support=Graph a b
g, law :: CompositionLaw a b
law=CompositionLaw a b
newLaw} (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
s) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
t)
        | a
s1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Path a b -> a
forall {a} {e}. (a, [Arrow a e]) -> a
targetPath Path a b
p2 = CompositionGraph a b -> a -> a -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes (CompositionGraph a b -> a -> a -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes CompositionGraph{support :: Graph a b
support=Graph a b
g, law :: CompositionLaw a b
law=CompositionLaw a b
newLaw} (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
s) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
t)) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
s) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
t)
        | Bool
otherwise = CompositionGraph a b -> a -> a -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes (CompositionGraph a b -> a -> a -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes CompositionGraph{support :: Graph a b
support=Graph a b
g, law :: CompositionLaw a b
law=CompositionLaw a b
newLaw} (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
s) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
t)) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
s) (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
t) where
        targetPath :: (a, [Arrow a e]) -> a
targetPath (a, [Arrow a e])
path = if [Arrow a e] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((a, [Arrow a e]) -> [Arrow a e]
forall a b. (a, b) -> b
snd (a, [Arrow a e])
path) then (a, [Arrow a e]) -> a
forall a b. (a, b) -> a
fst (a, [Arrow a e])
path else (Arrow a e -> a
forall n e. Arrow n e -> n
targetArrow ([Arrow a e] -> Arrow a e
forall a. HasCallStack => [a] -> a
head ((a, [Arrow a e]) -> [Arrow a e]
forall a b. (a, b) -> b
snd (a, [Arrow a e])
path)))
        newLaw :: CompositionLaw a b
newLaw = RawPath a b
-> RawPath a b -> CompositionLaw a b -> CompositionLaw a b
forall k a. k -> a -> Map k a -> Map k a
Map.insert (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> RawPath a b -> RawPath a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
rp1) (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> RawPath a b -> RawPath a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
rp2) (AssociationList (RawPath a b) (RawPath a b) -> CompositionLaw a b
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList (RawPath a b) (RawPath a b) -> CompositionLaw a b)
-> AssociationList (RawPath a b) (RawPath a b)
-> CompositionLaw a b
forall a b. (a -> b) -> a -> b
$ (\(RawPath a b
k,RawPath a b
v) -> (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> RawPath a b -> RawPath a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
k, Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
replaceArrow (Arrow a b -> Arrow a b) -> RawPath a b -> RawPath a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
v)) ((RawPath a b, RawPath a b) -> (RawPath a b, RawPath a b))
-> AssociationList (RawPath a b) (RawPath a b)
-> AssociationList (RawPath a b) (RawPath a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompositionLaw a b -> AssociationList (RawPath a b) (RawPath a b)
forall k a. Eq k => Map k a -> [(k, a)]
Map.mapToList CompositionLaw a b
l))
            where
                replace :: a -> a
replace a
x = if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
s1 then a
s2 else (if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== Path a b -> a
forall {a} {e}. (a, [Arrow a e]) -> a
targetPath Path a b
p1 then Path a b -> a
forall {a} {e}. (a, [Arrow a e]) -> a
targetPath Path a b
p2 else a
x)
                replaceArrow :: Arrow a e -> Arrow a e
replaceArrow Arrow{sourceArrow :: forall n e. Arrow n e -> n
sourceArrow=a
s3,targetArrow :: forall n e. Arrow n e -> n
targetArrow=a
t3,labelArrow :: forall n e. Arrow n e -> e
labelArrow=e
l3} = Arrow{sourceArrow :: a
sourceArrow=a -> a
replace a
s3,targetArrow :: a
targetArrow=a -> a
replace a
t3,labelArrow :: e
labelArrow=e
l3}
    
    -- | Checks associativity of a composition graph.

    checkAssociativity :: (Eq a, Eq b, Show a) => CompositionGraph a b -> Bool
    checkAssociativity :: forall a b. (Eq a, Eq b, Show a) => CompositionGraph a b -> Bool
checkAssociativity CompositionGraph a b
cg = (Bool -> Bool -> Bool) -> Bool -> Set Bool -> Bool
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr Bool -> Bool -> Bool
(&&) Bool
True [(CGMorphism a b, CGMorphism a b, CGMorphism a b) -> Bool
forall {a} {o}. (Eq a, Morphism a o) => (a, a, a) -> Bool
checkTriplet (CGMorphism a b
f,CGMorphism a b
g,CGMorphism a b
h) | CGMorphism a b
f <- CompositionGraph a b -> Set (CGMorphism a b)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows CompositionGraph a b
cg, CGMorphism a b
g <- CompositionGraph a b -> a -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom CompositionGraph a b
cg (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
f), CGMorphism a b
h <- CompositionGraph a b -> a -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom CompositionGraph a b
cg (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
g)]
        where
            checkTriplet :: (a, a, a) -> Bool
checkTriplet (a
f,a
g,a
h) = (a
h a -> a -> a
forall m o. Morphism m o => m -> m -> m
@ a
g) a -> a -> a
forall m o. Morphism m o => m -> m -> m
@ a
f a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
h a -> a -> a
forall m o. Morphism m o => m -> m -> m
@ (a
g a -> a -> a
forall m o. Morphism m o => m -> m -> m
@ a
f)
        
    -- | Find all composite arrows and try to map them to generating arrows. 

    identifyCompositeToGen :: (RandomGen g, Eq a, Eq b, Show a) => CompositionGraph a b -> Int -> g -> (Maybe (CompositionGraph a b), g)
    identifyCompositeToGen :: forall g a b.
(RandomGen g, Eq a, Eq b, Show a) =>
CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
identifyCompositeToGen CompositionGraph a b
_ Int
0 g
rGen = (Maybe (CompositionGraph a b)
forall a. Maybe a
Nothing, g
rGen)
    identifyCompositeToGen CompositionGraph a b
cg Int
n g
rGen
        | Bool -> Bool
not (CompositionGraph a b -> Bool
forall a b. (Eq a, Eq b, Show a) => CompositionGraph a b -> Bool
checkAssociativity CompositionGraph a b
cg) = (Maybe (CompositionGraph a b)
forall a. Maybe a
Nothing, g
rGen)
        | [CGMorphism a b] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CGMorphism a b]
compositeMorphs = (CompositionGraph a b -> Maybe (CompositionGraph a b)
forall a. a -> Maybe a
Just CompositionGraph a b
cg, g
rGen)
        | Bool
otherwise = if Maybe (CompositionGraph a b) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (CompositionGraph a b)
newCG then CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
forall g a b.
(RandomGen g, Eq a, Eq b, Show a) =>
CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
identifyCompositeToGen CompositionGraph a b
cg (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) g
newGen2 else (Maybe (CompositionGraph a b)
newCG, g
newGen2)
        where
            compositeMorphs :: [CGMorphism a b]
compositeMorphs = CompositionGraph a b -> [CGMorphism a b]
forall a b.
(Eq a, Eq b, Show a) =>
CompositionGraph a b -> [CGMorphism a b]
compositeMorphisms CompositionGraph a b
cg
            morphToMap :: CGMorphism a b
morphToMap = ([CGMorphism a b] -> CGMorphism a b
forall a. HasCallStack => [a] -> a
head [CGMorphism a b]
compositeMorphs)
            (CGMorphism a b
selectedGen,g
newGen1) = if (CGMorphism a b -> a
forall m o. Morphism m o => m -> o
source CGMorphism a b
morphToMap a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== CGMorphism a b -> a
forall m o. Morphism m o => m -> o
target CGMorphism a b
morphToMap) then [CGMorphism a b] -> g -> (CGMorphism a b, g)
forall g a. RandomGen g => [a] -> g -> (a, g)
pickOne [CGMorphism a b
fs | a
obj <- (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList (CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob CompositionGraph a b
cg)), CGMorphism a b
fs <- (Set (CGMorphism a b) -> [CGMorphism a b]
forall a. Eq a => Set a -> [a]
setToList (CompositionGraph a b -> a -> a -> Set (CGMorphism a b)
forall c m o.
(Category c m o, Morphism m o) =>
c -> o -> o -> Set m
genAr CompositionGraph a b
cg a
obj a
obj))] g
rGen else [CGMorphism a b] -> g -> (CGMorphism a b, g)
forall g a. RandomGen g => [a] -> g -> (a, g)
pickOne (Set (CGMorphism a b) -> [CGMorphism a b]
forall a. Eq a => Set a -> [a]
setToList (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
genArrows CompositionGraph a b
cg)) g
rGen
            (Maybe (CompositionGraph a b)
newCG,g
newGen2) = CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
forall g a b.
(RandomGen g, Eq a, Eq b, Show a) =>
CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
identifyCompositeToGen (CompositionGraph a b
-> CGMorphism a b -> CGMorphism a b -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b -> CGMorphism a b -> CompositionGraph a b
mergeMorphisms CompositionGraph a b
cg CGMorphism a b
morphToMap CGMorphism a b
selectedGen) Int
n g
newGen1 
            
    -- | Pick one element of a list randomly.

    pickOne :: (RandomGen g) => [a] -> g -> (a,g)
    pickOne :: forall g a. RandomGen g => [a] -> g -> (a, g)
pickOne [] g
g = String -> (a, g)
forall a. HasCallStack => String -> a
error String
"pickOne in an empty list."
    pickOne [a]
l g
g = (([a]
l [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
index),g
newGen) where
        (Int
index,g
newGen) = ((Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
0,([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
l)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) g
g)
        
    listWithoutNthElem :: [a] -> Int -> [a]
    listWithoutNthElem :: forall a. [a] -> Int -> [a]
listWithoutNthElem [] Int
_ = []
    listWithoutNthElem (a
x:[a]
xs) Int
0 = [a]
xs
    listWithoutNthElem (a
x:[a]
xs) Int
k = a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:([a] -> Int -> [a]
forall a. [a] -> Int -> [a]
listWithoutNthElem [a]
xs (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
        
    -- | Sample /n/ elements of a list randomly.

    sample :: (RandomGen g) => [a] -> Int -> g -> ([a],g)
    sample :: forall g a. RandomGen g => [a] -> Int -> g -> ([a], g)
sample [a]
_ Int
0 g
g = ([],g
g)
    sample [] Int
k g
g = String -> ([a], g)
forall a. HasCallStack => String -> a
error String
"Sample size bigger than the list size."
    sample [a]
l Int
n g
g = ((([a]
l [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
index)a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rest),g
finalGen) where
        (Int
index,g
newGen) = ((Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
0,([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
l)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) g
g)
        new_l :: [a]
new_l = [a] -> Int -> [a]
forall a. [a] -> Int -> [a]
listWithoutNthElem [a]
l Int
index
        ([a]
rest,g
finalGen) = [a] -> Int -> g -> ([a], g)
forall g a. RandomGen g => [a] -> Int -> g -> ([a], g)
sample [a]
new_l (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) g
newGen
            
    -- | Algorithm described in `mkRandomCompositionGraph`.

    monoidificationAttempt :: (RandomGen g, Eq a, Eq b, Show a) => CompositionGraph a b -> Int -> g -> (CompositionGraph a b, g, [a])
    monoidificationAttempt :: forall g a b.
(RandomGen g, Eq a, Eq b, Show a) =>
CompositionGraph a b -> Int -> g -> (CompositionGraph a b, g, [a])
monoidificationAttempt CompositionGraph a b
cg Int
p g
g = if Maybe (CompositionGraph a b) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (CompositionGraph a b)
result then (CompositionGraph a b
cg,g
finalGen,[]) else (Maybe (CompositionGraph a b) -> CompositionGraph a b
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (CompositionGraph a b)
result, g
finalGen, [a
s,a
t])
        where
            ([a
s,a
t],g
newGen) = if ((Set a -> Int
forall a. Eq a => Set a -> Int
cardinal (CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob CompositionGraph a b
cg)) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) then [a] -> Int -> g -> ([a], g)
forall g a. RandomGen g => [a] -> Int -> g -> ([a], g)
sample (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList(Set a -> [a])
-> (CompositionGraph a b -> Set a) -> CompositionGraph a b -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob (CompositionGraph a b -> [a]) -> CompositionGraph a b -> [a]
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg) Int
2 g
g else (Set a -> [a]
forall a. Eq a => Set a -> [a]
setToList (CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob CompositionGraph a b
cg Set a -> Set a -> Set a
forall a. Set a -> Set a -> Set a
||| CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob CompositionGraph a b
cg),g
g)
            newCG :: CompositionGraph a b
newCG = CompositionGraph a b -> a -> a -> CompositionGraph a b
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b -> a -> a -> CompositionGraph a b
mergeNodes CompositionGraph a b
cg a
s a
t
            (Maybe (CompositionGraph a b)
result,g
finalGen) = CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
forall g a b.
(RandomGen g, Eq a, Eq b, Show a) =>
CompositionGraph a b
-> Int -> g -> (Maybe (CompositionGraph a b), g)
identifyCompositeToGen CompositionGraph a b
newCG Int
p g
newGen
    
    -- | Initialize a composition graph with all arrows seperated.

    initRandomCG :: Int -> CompositionGraph Int Int
    initRandomCG :: Int -> CompositionGraph Int Int
initRandomCG Int
n = CompositionGraph{support :: Graph Int Int
support=Set Int -> Set (Arrow Int Int) -> Graph Int Int
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph ([Int] -> Set Int
forall a. [a] -> Set a
set [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]) ([Arrow Int Int] -> Set (Arrow Int Int)
forall a. [a] -> Set a
set [Arrow{sourceArrow :: Int
sourceArrow=(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i), targetArrow :: Int
targetArrow=(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1), labelArrow :: Int
labelArrow=Int
i} | Int
i <- [Int
0..Int
n]]),law :: CompositionLaw Int Int
law=AssociationList [Arrow Int Int] [Arrow Int Int]
-> CompositionLaw Int Int
forall k v. AssociationList k v -> Map k v
weakMap []}
    
    -- | Generates a random composition graph.

    --

    -- We use the fact that a category is a generalized monoid.

    --

    -- We try to create a composition law of a monoid greedily.

    --

    -- To get a category, we begin with a category with all arrows seperated and not composing with each other. 

    -- It is equivalent to the monoid with an empty composition law.

    --

    -- Then, a monoidification attempt is the following algorihm :

    --

    -- 1. Pick two objects, merge them.

    -- 2. While there are composite morphisms, try to merge them with generating arrows.

    -- 3. If it fails, don't change the composition graph.

    -- 4. Else return the new composition graph

    -- 

    -- A monoidification attempt takes a valid category and outputs a valid category, furthermore, the number of arrows is constant

    -- and the number of objects is decreasing (not strictly).

    constructRandomCompositionGraph :: (RandomGen g) => Int -- ^ Number of arrows of the random composition graph.

                                              -> Int -- ^ Number of monoidification attempts, a bigger number will produce more morphisms that will compose but the function will be slower.

                                              -> Int -- ^ Perseverance : how much we pursure an attempt far away to find a law that works, a bigger number will make the attemps more successful, but slower. (When in doubt put 4.)

                                              -> g   -- ^ Random generator.

                                              -> (CompositionGraph Int Int, g)
    constructRandomCompositionGraph :: forall g.
RandomGen g =>
Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
constructRandomCompositionGraph Int
nbAr Int
nbAttempts Int
perseverance g
gen = CompositionGraph Int Int
-> Int -> Int -> g -> (CompositionGraph Int Int, g)
forall {t} {t} {a} {b}.
(Num t, RandomGen t, Eq t, Eq a, Eq b, Show a) =>
CompositionGraph a b -> t -> Int -> t -> (CompositionGraph a b, t)
attempt (Int -> CompositionGraph Int Int
initRandomCG Int
nbAr) Int
nbAttempts Int
perseverance g
gen
        where
            attempt :: CompositionGraph a b -> t -> Int -> t -> (CompositionGraph a b, t)
attempt CompositionGraph a b
cg t
0 Int
_ t
gen = (CompositionGraph a b
cg, t
gen)
            attempt CompositionGraph a b
cg t
n Int
p t
gen = CompositionGraph a b -> t -> Int -> t -> (CompositionGraph a b, t)
attempt CompositionGraph a b
newCG (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) Int
p t
newGen
                where
                    (CompositionGraph a b
newCG, t
newGen,[a]
_) = (CompositionGraph a b -> Int -> t -> (CompositionGraph a b, t, [a])
forall g a b.
(RandomGen g, Eq a, Eq b, Show a) =>
CompositionGraph a b -> Int -> g -> (CompositionGraph a b, g, [a])
monoidificationAttempt CompositionGraph a b
cg Int
p t
gen)
    
    -- | Creates a random composition graph with default random values.

    --

    -- The number of arrows will be in the interval [1, 20].

    defaultConstructRandomCompositionGraph  :: (RandomGen g) => g -> (CompositionGraph Int Int, g)
    defaultConstructRandomCompositionGraph :: forall g. RandomGen g => g -> (CompositionGraph Int Int, g)
defaultConstructRandomCompositionGraph g
g1 = Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
forall g.
RandomGen g =>
Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
constructRandomCompositionGraph Int
nbArrows (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
nbAttempts Int
20) Int
4 g
g3
        where 
            (Int
nbArrows, g
g2) = (Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
1,Int
20) g
g1
            (Int
nbAttempts, g
g3) = (Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
0,Int
nbArrowsInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbArrows) g
g2
    
    
    -- | Constructs two random composition graphs and choose a random diagram between the two.

    defaultConstructRandomDiagram  :: (RandomGen g) => g ->  (Diagram (CompositionGraph Int Int) (CGMorphism Int Int) Int (CompositionGraph Int Int) (CGMorphism Int Int) Int, g)
    defaultConstructRandomDiagram :: forall g.
RandomGen g =>
g
-> (Diagram
      (CompositionGraph Int Int)
      (CGMorphism Int Int)
      Int
      (CompositionGraph Int Int)
      (CGMorphism Int Int)
      Int,
    g)
defaultConstructRandomDiagram g
g1 = CompositionGraph Int Int
-> CompositionGraph Int Int
-> g
-> (Diagram
      (CompositionGraph Int Int)
      (CGMorphism Int Int)
      Int
      (CompositionGraph Int Int)
      (CGMorphism Int Int)
      Int,
    g)
forall c1 m1 o1 c2 m2 o2 g.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2,
 RandomGen g) =>
c1 -> c2 -> g -> (Diagram c1 m1 o1 c2 m2 o2, g)
pickRandomDiagram CompositionGraph Int Int
cat1 CompositionGraph Int Int
cat2 g
g3
        where 
            (Int
nbArrows1, g
g2) = (Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
1,Int
8) g
g1
            (Int
nbAttempts1, g
g3) = (Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
0,Int
nbArrows1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbArrows1) g
g2
            (CompositionGraph Int Int
cat1, g
g4) = Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
forall g.
RandomGen g =>
Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
constructRandomCompositionGraph Int
nbArrows1 Int
nbAttempts1 Int
5 g
g3
            (Int
nbArrows2, g
g5) = (Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
1,Int
11Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
nbArrows1) g
g4
            (Int
nbAttempts2, g
g6) = (Int, Int) -> g -> (Int, g)
forall g a. (RandomGen g, UniformRange a) => (a, a) -> g -> (a, g)
uniformR (Int
0,Int
nbArrows2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
nbArrows2) g
g5
            (CompositionGraph Int Int
cat2, g
g7) = Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
forall g.
RandomGen g =>
Int -> Int -> Int -> g -> (CompositionGraph Int Int, g)
constructRandomCompositionGraph Int
nbArrows2 Int
nbAttempts2 Int
5 g
g6
    
    
    
    
    
    -- | Takes a discrete diagram of composition graphs and two functions and returns a colimit cocone object of this diagram. The two functions are used to combine an object (an arrow) of the indexing category with an object (an arrow) of a composition graph in order to distinguish an object (an arrow) with same identifier in the disjunct union constructed.

    --

    -- Two properties should be met and are not verified at runtime : the diagram given should be discrete and the two functions should be injective.

    --

    -- Moreover, the base of the diagram should not be empty. This function throws an error if this condition is not verified.

    coproductOfCompositionGraphs :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq a, Eq b) => Diagram c1 m1 o1 (FinCat (CompositionGraph a b) (CGMorphism a b) a) (FinFunctor (CompositionGraph a b) (CGMorphism a b) a) (CompositionGraph a b) -> (o1 -> a -> a) -> (o1 -> b -> b) -> Cocone c1 m1 o1 (FinCat (CompositionGraph a b) (CGMorphism a b) a) (FinFunctor (CompositionGraph a b) (CGMorphism a b) a) (CompositionGraph a b)
    coproductOfCompositionGraphs :: forall c1 m1 o1 a b.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq a, Eq b) =>
Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> (o1 -> a -> a)
-> (o1 -> b -> b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
coproductOfCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG o1 -> a -> a
combObj o1 -> b -> b
combArr
        | Set o1 -> Bool
forall a. Set a -> Bool
Set.null (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory) = String
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall a. HasCallStack => String -> a
error String
"The base should not be empty."
        | Bool
otherwise = One
-> CompositionGraph a b
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One CompositionGraph a b
coproduct NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
natCoproduct
        where
            indexingCategory :: c1
indexingCategory = Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG
            coproduct :: CompositionGraph a b
coproduct = Graph a b -> CompositionLaw a b -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph Graph a b
coproduct_graph ([CompositionLaw a b] -> CompositionLaw a b
forall k a. Eq k => [Map k a] -> Map k a
Map.unions [AssociationList (RawPath a b) (RawPath a b) -> CompositionLaw a b
forall k v. AssociationList k v -> Map k v
weakMap (AssociationList (RawPath a b) (RawPath a b) -> CompositionLaw a b)
-> AssociationList (RawPath a b) (RawPath a b)
-> CompositionLaw a b
forall a b. (a -> b) -> a -> b
$ (\(RawPath a b
rp1,RawPath a b
rp2) -> (o1 -> Arrow a b -> Arrow a b
transformArrowIntoArrowCoproduct o1
i (Arrow a b -> Arrow a b) -> RawPath a b -> RawPath a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
rp1, o1 -> Arrow a b -> Arrow a b
transformArrowIntoArrowCoproduct o1
i (Arrow a b -> Arrow a b) -> RawPath a b -> RawPath a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RawPath a b
rp2)) ((RawPath a b, RawPath a b) -> (RawPath a b, RawPath a b))
-> AssociationList (RawPath a b) (RawPath a b)
-> AssociationList (RawPath a b) (RawPath a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompositionLaw a b -> AssociationList (RawPath a b) (RawPath a b)
forall k a. Eq k => Map k a -> [(k, a)]
Map.mapToList (CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law (Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> CompositionGraph a b
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i))) | o1
i <- (Set o1 -> [o1]
forall a. Eq a => Set a -> [a]
setToList (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory))])
            transformObjectIntoObjectCoproduct :: o1 -> a -> a
transformObjectIntoObjectCoproduct o1
i a
x = o1 -> a -> a
combObj o1
i a
x
            transformArrowIntoArrowCoproduct :: o1 -> Arrow a b -> Arrow a b
transformArrowIntoArrowCoproduct o1
i Arrow a b
a = Arrow{sourceArrow :: a
sourceArrow = o1 -> a -> a
combObj o1
i (Arrow a b -> a
forall n e. Arrow n e -> n
sourceArrow Arrow a b
a), targetArrow :: a
targetArrow = o1 -> a -> a
combObj o1
i (Arrow a b -> a
forall n e. Arrow n e -> n
targetArrow Arrow a b
a), labelArrow :: b
labelArrow = o1 -> b -> b
combArr o1
i (Arrow a b -> b
forall n e. Arrow n e -> e
labelArrow Arrow a b
a)}
            coproduct_graph :: Graph a b
coproduct_graph = Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Set (Set a) -> Set a
forall a. Set (Set a) -> Set a
Set.concat2 ((\o1
i -> o1 -> a -> a
transformObjectIntoObjectCoproduct o1
i (a -> a) -> Set a -> Set a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> CompositionGraph a b
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i))) (o1 -> Set a) -> Set o1 -> Set (Set a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory))) (Set (Set (Arrow a b)) -> Set (Arrow a b)
forall a. Set (Set a) -> Set a
Set.concat2 ((\o1
i -> (o1 -> Arrow a b -> Arrow a b
transformArrowIntoArrowCoproduct o1
i) (Arrow a b -> Arrow a b) -> Set (Arrow a b) -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow (CGMorphism a b -> Arrow a b)
-> Set (CGMorphism a b) -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId (Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> CompositionGraph a b
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i))) (o1 -> Set (Arrow a b)) -> Set o1 -> Set (Set (Arrow a b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory)))
            natCoproduct :: NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
natCoproduct = Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> Diagram
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
-> Map o1 (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG (c1
-> FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> Diagram
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
indexingCategory FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
coproduct) (Set (o1, FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> Map o1 (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(o1
i, o1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
insertionFunctor o1
i)| o1
i <- c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory])
            insertionFunctor :: o1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
insertionFunctor o1
i = FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph a b
src = Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> CompositionGraph a b
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i, tgt :: CompositionGraph a b
tgt = CompositionGraph a b
coproduct, omap :: Map a a
omap = Set (a, a) -> Map a a
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(a
o, o1 -> a -> a
transformObjectIntoObjectCoproduct o1
i a
o)| a
o <- CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob (Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> CompositionGraph a b
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i)], mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap = Set (CGMorphism a b, CGMorphism a b)
-> Map (CGMorphism a b) (CGMorphism a b)
forall k v. Set (k, v) -> Map k v
weakMapFromSet [(CGMorphism a b
m, (CompositionGraph a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionGraph a b -> Arrow a b -> CGMorphism a b
unsafeArrowToCGMorphism CompositionGraph a b
coproduct (o1 -> Arrow a b -> Arrow a b
transformArrowIntoArrowCoproduct o1
i (CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m)))) | CGMorphism a b
m <- (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId (Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> CompositionGraph a b
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ o1
i))]}
    
    
    -- | Specialized version of 'coproductOfCompositionGraphs' to CompositionGraph String String.

    coproductOfStringCompositionGraphs :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Show o1) => Diagram c1 m1 o1 (FinCat (CompositionGraph String String) (CGMorphism String String) String) (FinFunctor (CompositionGraph String String) (CGMorphism String String) String) (CompositionGraph String String) -> Cocone c1 m1 o1 (FinCat (CompositionGraph String String) (CGMorphism String String) String) (FinFunctor (CompositionGraph String String) (CGMorphism String String) String) (CompositionGraph String String)
    coproductOfStringCompositionGraphs :: forall c1 m1 o1.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Show o1) =>
Diagram
  c1
  m1
  o1
  (FinCat
     (CompositionGraph String String) (CGMorphism String String) String)
  (FinFunctor
     (CompositionGraph String String) (CGMorphism String String) String)
  (CompositionGraph String String)
-> Cocone
     c1
     m1
     o1
     (FinCat
        (CompositionGraph String String) (CGMorphism String String) String)
     (FinFunctor
        (CompositionGraph String String) (CGMorphism String String) String)
     (CompositionGraph String String)
coproductOfStringCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat
     (CompositionGraph String String) (CGMorphism String String) String)
  (FinFunctor
     (CompositionGraph String String) (CGMorphism String String) String)
  (CompositionGraph String String)
diag = Diagram
  c1
  m1
  o1
  (FinCat
     (CompositionGraph String String) (CGMorphism String String) String)
  (FinFunctor
     (CompositionGraph String String) (CGMorphism String String) String)
  (CompositionGraph String String)
-> (o1 -> ShowS)
-> (o1 -> ShowS)
-> Cocone
     c1
     m1
     o1
     (FinCat
        (CompositionGraph String String) (CGMorphism String String) String)
     (FinFunctor
        (CompositionGraph String String) (CGMorphism String String) String)
     (CompositionGraph String String)
forall c1 m1 o1 a b.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq a, Eq b) =>
Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> (o1 -> a -> a)
-> (o1 -> b -> b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
coproductOfCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat
     (CompositionGraph String String) (CGMorphism String String) String)
  (FinFunctor
     (CompositionGraph String String) (CGMorphism String String) String)
  (CompositionGraph String String)
diag (\o1
x String
o -> (o1 -> String
forall a. Show a => a -> String
show (o1 -> String) -> o1 -> String
forall a b. (a -> b) -> a -> b
$ o1
x) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"." String -> ShowS
forall a. Semigroup a => a -> a -> a
<>String
o) (\o1
x String
m -> (o1 -> String
forall a. Show a => a -> String
show o1
x) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"." String -> ShowS
forall a. Semigroup a => a -> a -> a
<>String
m)
    
    
    -- | Specialized version of 'coproductOfCompositionGraphs' to CompositionGraph Text Text.

    coproductOfTextCompositionGraphs :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Show o1) => Diagram c1 m1 o1 (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text) (FinFunctor (CompositionGraph Text Text) (CGMorphism Text Text) Text) (CompositionGraph Text Text) -> Cocone c1 m1 o1 (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text) (FinFunctor (CompositionGraph Text Text) (CGMorphism Text Text) Text) (CompositionGraph Text Text)
    coproductOfTextCompositionGraphs :: forall c1 m1 o1.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Show o1) =>
Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph Text Text)
coproductOfTextCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
diag = Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
-> (o1 -> Text -> Text)
-> (o1 -> Text -> Text)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
     CGD
     (CompositionGraph Text Text)
forall c1 m1 o1 a b.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq a, Eq b) =>
Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> (o1 -> a -> a)
-> (o1 -> b -> b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
coproductOfCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text)
  CGD
  (CompositionGraph Text Text)
diag (\o1
x Text
o -> (String -> Text
pack(String -> Text) -> (o1 -> String) -> o1 -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> String
forall a. Show a => a -> String
show (o1 -> Text) -> o1 -> Text
forall a b. (a -> b) -> a -> b
$ o1
x) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String -> Text
pack String
".")Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>Text
o) (\o1
x Text
m -> (String -> Text
pack(String -> Text) -> (o1 -> String) -> o1 -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
.o1 -> String
forall a. Show a => a -> String
show(o1 -> Text) -> o1 -> Text
forall a b. (a -> b) -> a -> b
$ o1
x) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>(String -> Text
pack String
".")Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>Text
m)
    
    
    -- | Glue two objects of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    glueObject :: (Eq a, Eq b) => CompositionGraph a b -> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueObject :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObject CompositionGraph a b
cg a
a a
b = Diagram
  (CompositionGraph a b)
  (CGMorphism a b)
  a
  (CompositionGraph a b)
  (CGMorphism a b)
  a
-> Diagram
     (CompositionGraph a b)
     (CGMorphism a b)
     a
     (CompositionGraph a b)
     (CGMorphism a b)
     a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram (Diagram
   (CompositionGraph a b)
   (CGMorphism a b)
   a
   (CompositionGraph a b)
   (CGMorphism a b)
   a
 -> Diagram
      (CompositionGraph a b)
      (CGMorphism a b)
      a
      (CompositionGraph a b)
      (CGMorphism a b)
      a)
-> Diagram
     (CompositionGraph a b)
     (CGMorphism a b)
     a
     (CompositionGraph a b)
     (CGMorphism a b)
     a
-> Diagram
     (CompositionGraph a b)
     (CGMorphism a b)
     a
     (CompositionGraph a b)
     (CGMorphism a b)
     a
forall a b. (a -> b) -> a -> b
$ Diagram{src :: CompositionGraph a b
src=CompositionGraph a b
cg,tgt :: CompositionGraph a b
tgt=CompositionGraph a b
newCG, omap :: Map a a
omap = Map a a
omapD, mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap = Map (CGMorphism a b) (CGMorphism a b)
mmapD}
        where
            glueObj :: a -> a
glueObj a
obj = if a
obj a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b then a
a else a
obj
            omapD :: Map a a
omapD = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
glueObj (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set a) -> CompositionGraph a b -> Set a
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            glueArr :: Arrow a e -> Arrow a e
glueArr Arrow a e
arr = Arrow{sourceArrow :: a
sourceArrow = a -> a
glueObj(a -> a) -> (Arrow a e -> a) -> Arrow a e -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a e -> a
forall n e. Arrow n e -> n
sourceArrow (Arrow a e -> a) -> Arrow a e -> a
forall a b. (a -> b) -> a -> b
$ Arrow a e
arr, targetArrow :: a
targetArrow = a -> a
glueObj(a -> a) -> (Arrow a e -> a) -> Arrow a e -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a e -> a
forall n e. Arrow n e -> n
targetArrow (Arrow a e -> a) -> Arrow a e -> a
forall a b. (a -> b) -> a -> b
$ Arrow a e
arr, labelArrow :: e
labelArrow = Arrow a e -> e
forall n e. Arrow n e -> e
labelArrow Arrow a e
arr}
            mmapD :: Map (CGMorphism a b) (CGMorphism a b)
mmapD = (CGMorphism a b -> CGMorphism a b)
-> Set (CGMorphism a b) -> Map (CGMorphism a b) (CGMorphism a b)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction ((CompositionGraph a b -> Arrow a b -> CGMorphism a b
forall a b. CompositionGraph a b -> Arrow a b -> CGMorphism a b
unsafeArrowToCGMorphism CompositionGraph a b
cg)(Arrow a b -> CGMorphism a b)
-> (CGMorphism a b -> Arrow a b)
-> CGMorphism a b
-> CGMorphism a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
glueArr(Arrow a b -> Arrow a b)
-> (CGMorphism a b -> Arrow a b) -> CGMorphism a b -> Arrow a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow) (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId CompositionGraph a b
cg)
            newCG :: CompositionGraph a b
newCG = Graph a b -> CompositionLaw a b -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Map a a -> Set a
forall k a. Eq k => Map k a -> Set a
Map.values Map a a
omapD) (Arrow a b -> Arrow a b
forall {e}. Arrow a e -> Arrow a e
glueArr (Arrow a b -> Arrow a b) -> Set (Arrow a b) -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph a b -> Set (Arrow a b))
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set (Arrow a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set (Arrow a b))
-> CompositionGraph a b -> Set (Arrow a b)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg))) (CompositionGraph a b -> CompositionLaw a b
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
cg)
    
    -- | Glue objects of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    glueObjects :: (Eq a, Eq b) => CompositionGraph a b -> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueObjects :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObjects CompositionGraph a b
cg Set a
objects
        | Set a -> Bool
forall a. Set a -> Bool
Set.null Set a
objects = String -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => String -> a
error String
"glue 0 object"
        | Bool
otherwise = (a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\a
obj FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> a -> a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObject (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) a
representant a
obj) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg) Set a
objects
        where
            representant :: a
representant = Set a -> a
forall a. Set a -> a
anElement Set a
objects
            
    
    -- | Change the law of a CGMorphism

    updateCGMorphismWithNewLaw :: CompositionLaw a b -> CGMorphism a b -> CGMorphism a b
    updateCGMorphismWithNewLaw :: forall a b. CompositionLaw a b -> CGMorphism a b -> CGMorphism a b
updateCGMorphismWithNewLaw CompositionLaw a b
l CGMorphism a b
m = CGMorphism{path :: Path a b
path=CGMorphism a b -> Path a b
forall a b. CGMorphism a b -> Path a b
path CGMorphism a b
m, compositionLaw :: CompositionLaw a b
compositionLaw=CompositionLaw a b
l}
    
    -- | Glue two morphisms with same source and target of a 'Compositiongraph' and return an insertion diagram into the new CompositionGraph.

    -- The first argument should not be composite if the second is a generator.

    glueMorphism :: (Eq a, Eq b) => CompositionGraph a b -> CGMorphism a b -> CGMorphism a b -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueMorphism :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphism CompositionGraph a b
cg CGMorphism a b
m1 CGMorphism a b
m2
        | CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isComposite_ CGMorphism a b
m1 Bool -> Bool -> Bool
&& CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m2 = String -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => String -> a
error String
"Glue composite to generator."
        | CGMorphism a b
m1 CGMorphism a b -> CGMorphism a b -> Bool
forall a. Eq a => a -> a -> Bool
== CGMorphism a b
m2 = FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg
        | CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m1 Bool -> Bool -> Bool
&& CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m2 = FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph a b
src=CompositionGraph a b
cg,tgt :: CompositionGraph a b
tgt=CompositionGraph a b
newCGGG,omap :: Map a a
omap=Map a a
omapGG,mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap=Map (CGMorphism a b) (CGMorphism a b)
mmapGG}
        | Bool
otherwise = FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1,
 Category c2 m2 o2, Morphism m2 o2) =>
Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2
completeDiagram Diagram{src :: CompositionGraph a b
src=CompositionGraph a b
cg,tgt :: CompositionGraph a b
tgt=CompositionGraph a b
newCG,omap :: Map a a
omap=Map a a
omapGG,mmap :: Map (CGMorphism a b) (CGMorphism a b)
mmap=Map (CGMorphism a b) (CGMorphism a b)
mmapId}
        where
            isGenerator_ :: CGMorphism a b -> Bool
isGenerator_ CGMorphism a b
m = [Arrow a b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall a b. (a -> b) -> a -> b
$ CGMorphism a b
m) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
            isComposite_ :: CGMorphism a b -> Bool
isComposite_ = Bool -> Bool
not(Bool -> Bool)
-> (CGMorphism a b -> Bool) -> CGMorphism a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> Bool
forall {a} {b}. CGMorphism a b -> Bool
isGenerator_
            glueMorph :: CGMorphism a b -> CGMorphism a b
glueMorph CGMorphism a b
m = if CGMorphism a b
m CGMorphism a b -> CGMorphism a b -> Bool
forall a. Eq a => a -> a -> Bool
== CGMorphism a b
m2 then CGMorphism a b
m1 else CGMorphism a b
m
            glueArr :: Arrow a b -> Arrow a b
glueArr Arrow a b
a = if Arrow a b
a Arrow a b -> Arrow a b -> Bool
forall a. Eq a => a -> a -> Bool
== (CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m2) then CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m1 else Arrow a b
a
            omapGG :: Map a a
omapGG = (a -> a) -> Set a -> Map a a
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction a -> a
forall a. a -> a
id (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set a) -> CompositionGraph a b -> Set a
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            mmapGG :: Map (CGMorphism a b) (CGMorphism a b)
mmapGG = (CGMorphism a b -> CGMorphism a b)
-> Set (CGMorphism a b) -> Map (CGMorphism a b) (CGMorphism a b)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction CGMorphism a b -> CGMorphism a b
glueMorph (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId CompositionGraph a b
cg)
            newLawGG :: Map [Arrow a b] [Arrow a b]
newLawGG =  Set ([Arrow a b], [Arrow a b]) -> Map [Arrow a b] [Arrow a b]
forall k v. Set (k, v) -> Map k v
weakMapFromSet (Set ([Arrow a b], [Arrow a b]) -> Map [Arrow a b] [Arrow a b])
-> Set ([Arrow a b], [Arrow a b]) -> Map [Arrow a b] [Arrow a b]
forall a b. (a -> b) -> a -> b
$ (\([Arrow a b]
x,[Arrow a b]
y) -> (Arrow a b -> Arrow a b
glueArr (Arrow a b -> Arrow a b) -> [Arrow a b] -> [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
x, Arrow a b -> Arrow a b
glueArr (Arrow a b -> Arrow a b) -> [Arrow a b] -> [Arrow a b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arrow a b]
y)) (([Arrow a b], [Arrow a b]) -> ([Arrow a b], [Arrow a b]))
-> Set ([Arrow a b], [Arrow a b]) -> Set ([Arrow a b], [Arrow a b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Map [Arrow a b] [Arrow a b] -> Set ([Arrow a b], [Arrow a b])
forall k v. Eq k => Map k v -> Set (k, v)
Map.mapToSet)(Map [Arrow a b] [Arrow a b] -> Set ([Arrow a b], [Arrow a b]))
-> (CompositionGraph a b -> Map [Arrow a b] [Arrow a b])
-> CompositionGraph a b
-> Set ([Arrow a b], [Arrow a b])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Map [Arrow a b] [Arrow a b]
forall a b. CompositionGraph a b -> CompositionLaw a b
law (CompositionGraph a b -> Set ([Arrow a b], [Arrow a b]))
-> CompositionGraph a b -> Set ([Arrow a b], [Arrow a b])
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg)
            newCGGG :: CompositionGraph a b
newCGGG = Graph a b -> Map [Arrow a b] [Arrow a b] -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (Set a -> Set (Arrow a b) -> Graph a b
forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph (Graph a b -> Set a
forall n e. Graph n e -> Set n
nodes(Graph a b -> Set a)
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set a) -> CompositionGraph a b -> Set a
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg) ((Graph a b -> Set (Arrow a b)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph a b -> Set (Arrow a b))
-> (CompositionGraph a b -> Graph a b)
-> CompositionGraph a b
-> Set (Arrow a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support (CompositionGraph a b -> Set (Arrow a b))
-> CompositionGraph a b -> Set (Arrow a b)
forall a b. (a -> b) -> a -> b
$ CompositionGraph a b
cg) Set (Arrow a b) -> Set (Arrow a b) -> Set (Arrow a b)
forall a. Eq a => Set a -> Set a -> Set a
`Set.difference` ([Arrow a b] -> Set (Arrow a b)
forall a. [a] -> Set a
set [CGMorphism a b -> Arrow a b
forall a b. CGMorphism a b -> Arrow a b
unsafeCGMorphismToArrow CGMorphism a b
m2]))) Map [Arrow a b] [Arrow a b]
newLawGG
            newLaw :: Map [Arrow a b] [Arrow a b]
newLaw = [Arrow a b]
-> [Arrow a b]
-> Map [Arrow a b] [Arrow a b]
-> Map [Arrow a b] [Arrow a b]
forall k a. k -> a -> Map k a -> Map k a
Map.insert ((a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall a b. (a -> b) -> a -> b
$ CGMorphism a b
m2) ((a, [Arrow a b]) -> [Arrow a b]
forall a b. (a, b) -> b
snd((a, [Arrow a b]) -> [Arrow a b])
-> (CGMorphism a b -> (a, [Arrow a b]))
-> CGMorphism a b
-> [Arrow a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.CGMorphism a b -> (a, [Arrow a b])
forall a b. CGMorphism a b -> Path a b
path (CGMorphism a b -> [Arrow a b]) -> CGMorphism a b -> [Arrow a b]
forall a b. (a -> b) -> a -> b
$ CGMorphism a b
m1) (CompositionGraph a b -> Map [Arrow a b] [Arrow a b]
forall a b. CompositionGraph a b -> CompositionLaw a b
law CompositionGraph a b
cg)
            mmapId :: Map (CGMorphism a b) (CGMorphism a b)
mmapId = (CGMorphism a b -> CGMorphism a b)
-> Set (CGMorphism a b) -> Map (CGMorphism a b) (CGMorphism a b)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction CGMorphism a b -> CGMorphism a b
forall a. a -> a
id (CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId CompositionGraph a b
cg)
            newCG :: CompositionGraph a b
newCG = Graph a b -> Map [Arrow a b] [Arrow a b] -> CompositionGraph a b
forall a b. Graph a b -> CompositionLaw a b -> CompositionGraph a b
unsafeCompositionGraph (CompositionGraph a b -> Graph a b
forall a b. CompositionGraph a b -> Graph a b
support CompositionGraph a b
cg) Map [Arrow a b] [Arrow a b]
newLaw
            
    -- | Glue morphisms with same source and target of a 'CompositionGraph' and return an insertion diagram into the new CompositionGraph.

    glueMorphisms :: (Eq a, Eq b) => CompositionGraph a b -> Set (CGMorphism a b) -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    glueMorphisms :: forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphisms CompositionGraph a b
cg Set (CGMorphism a b)
morphisms
        | Set (CGMorphism a b) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism a b)
morphisms = String -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => String -> a
error String
"glue 0 morphism"
        | Set (CGMorphism a b) -> Bool
forall a. Set a -> Bool
Set.null Set (CGMorphism a b)
generators = (CGMorphism a b
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\CGMorphism a b
morph FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphism (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (Set (CGMorphism a b) -> CGMorphism a b
forall a. Set a -> a
anElement Set (CGMorphism a b)
morphisms) CGMorphism a b
morph) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg) Set (CGMorphism a b)
morphisms
        | Bool
otherwise = (CGMorphism a b
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\CGMorphism a b
morph FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> CGMorphism a b
-> CGMorphism a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphism (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (Set (CGMorphism a b) -> CGMorphism a b
forall a. Set a -> a
anElement Set (CGMorphism a b)
generators) CGMorphism a b
morph) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat CompositionGraph a b
cg) Set (CGMorphism a b)
morphisms
        where
            generators :: Set (CGMorphism a b)
generators = (CGMorphism a b -> Bool)
-> Set (CGMorphism a b) -> Set (CGMorphism a b)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (CompositionGraph a b -> CGMorphism a b -> Bool
forall c m o.
(Category c m o, Morphism m o, Eq m) =>
c -> m -> Bool
isGenerator CompositionGraph a b
cg) Set (CGMorphism a b)
morphisms
            
    
    -- | Takes diagrams with same source and target composition graphs and returns a diagram from the target to the coequalizer of the diagrams. The set of diagrams should not be empty

    coequalizeCompositionGraphDiagrams :: (Eq a, Eq b) => Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a) -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    coequalizeCompositionGraphDiagrams :: forall a b.
(Eq a, Eq b) =>
Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
coequalizeCompositionGraphDiagrams Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
diags
        | Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a) -> Bool
forall a. Set a -> Bool
Set.null Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
diags = String -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. HasCallStack => String -> a
error String
"coequalize no diagram"
        | Bool
otherwise = FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueArrowsFunctor
        where
            aDiagram :: FinFunctor (CompositionGraph a b) (CGMorphism a b) a
aDiagram = Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a. Set a -> a
anElement Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
diags
            selectingObjects :: Set a
selectingObjects = CompositionGraph a b -> Set a
forall c m o. FiniteCategory c m o => c -> Set o
ob(CompositionGraph a b -> Set a)
-> (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    -> CompositionGraph a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (FinFunctor (CompositionGraph a b) (CGMorphism a b) a -> Set a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a -> Set a
forall a b. (a -> b) -> a -> b
$ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
aDiagram
            glueObjectsFunctor :: FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObjectsFunctor = (a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\a
obj FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set a -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObjects (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) [(FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
diag) FinFunctor (CompositionGraph a b) (CGMorphism a b) a -> a -> a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
Diagram c1 m1 o1 c2 m2 o2 -> o1 -> o2
->$ a
obj | FinFunctor (CompositionGraph a b) (CGMorphism a b) a
diag <- Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
diags]) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) (FinCat (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall c m o. (Category c m o, Morphism m o) => c -> o -> m
identity FinCat (CompositionGraph a b) (CGMorphism a b) a
forall c m o. FinCat c m o
FinCat (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
aDiagram)) Set a
selectingObjects
            selectingArrows :: Set (CGMorphism a b)
selectingArrows = CompositionGraph a b -> Set (CGMorphism a b)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> Set m
genArrowsWithoutId(CompositionGraph a b -> Set (CGMorphism a b))
-> (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
    -> CompositionGraph a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> Set (CGMorphism a b))
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
forall a b. (a -> b) -> a -> b
$ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
aDiagram
            glueArrowsFunctor :: FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueArrowsFunctor = (CGMorphism a b
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\CGMorphism a b
morph FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct -> (CompositionGraph a b
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
CompositionGraph a b
-> Set (CGMorphism a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueMorphisms (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) [(FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
diag) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CGMorphism a b -> CGMorphism a b
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ CGMorphism a b
morph| FinFunctor (CompositionGraph a b) (CGMorphism a b) a
diag <- Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
diags]) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ FinFunctor (CompositionGraph a b) (CGMorphism a b) a
funct) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
glueObjectsFunctor Set (CGMorphism a b)
selectingArrows
            
    
    -- | Takes a diagram of compositions graphs, a function to combine an object of the indexing category with an object of a composition graph, a function to combine an object of the indexing category with a morphism of a composition graph and return the colimit cocone with the constructed composition graph as nadir. Note that the functions to combine objects and morphisms should be injective. The base should not be empty.

    colimitOfCompositionGraphs :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, Eq a, Eq b) =>
        Diagram c1 m1 o1 (FinCat (CompositionGraph a b) (CGMorphism a b) a) (FinFunctor (CompositionGraph a b) (CGMorphism a b) a) (CompositionGraph a b) -> (o1 -> a -> a) -> (o1 -> b -> b) -> Cocone c1 m1 o1 (FinCat (CompositionGraph a b) (CGMorphism a b) a) (FinFunctor (CompositionGraph a b) (CGMorphism a b) a) (CompositionGraph a b)
    colimitOfCompositionGraphs :: forall c1 m1 o1 a b.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1,
 Eq a, Eq b) =>
Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> (o1 -> a -> a)
-> (o1 -> b -> b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
colimitOfCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG o1 -> a -> a
combObj o1 -> b -> b
combMorph 
        | Set o1 -> Bool
forall a. Set a -> Bool
Set.null (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory) = String
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall a. HasCallStack => String -> a
error String
"The base should not be empty."
        | Bool
otherwise =  One
-> CompositionGraph a b
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall o1 o2 m3. o1 -> o2 -> m3 -> CommaObject o1 o2 m3
unsafeCommaObject One
One (FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> CompositionGraph a b
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt (NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coequalizedNat NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> o1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (Set o1 -> o1
forall a. Set a -> a
anElement(Set o1 -> o1) -> (c1 -> Set o1) -> c1 -> o1
forall b c a. (b -> c) -> (a -> b) -> a -> c
.c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob (c1 -> o1) -> c1 -> o1
forall a b. (a -> b) -> a -> b
$ c1
indexingCategory))) NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coequalizedNat
        where
            indexingCategory :: c1
indexingCategory = Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG
            coproductCocone :: Cocone
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coproductCocone = Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> (o1 -> a -> a)
-> (o1 -> b -> b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall c1 m1 o1 a b.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq o1, Eq a, Eq b) =>
Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> (o1 -> a -> a)
-> (o1 -> b -> b)
-> Cocone
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
coproductOfCompositionGraphs Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG o1 -> a -> a
combObj o1 -> b -> b
combMorph
            coproductNat :: NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coproductNat = Cocone
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall c1 m1 o1 c2 m2 o2.
Cocone c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2
legsCocone Cocone
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coproductCocone
            functorToNat :: Diagram c1 m1 o1 c1 m1 o1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
functorToNat Diagram c1 m1 o1 c1 m1 o1
funct = Diagram c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
-> Diagram
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
-> Map o1 (Diagram c1 m1 o1 c1 m1 o1)
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2
-> Diagram c1 m1 o1 c2 m2 o2
-> Map o1 m2
-> NaturalTransformation c1 m1 o1 c2 m2 o2
unsafeNaturalTransformation (c1
-> FinCat c1 m1 o1
-> c1
-> Diagram
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
indexingCategory FinCat c1 m1 o1
forall c m o. FinCat c m o
FinCat (Diagram c1 m1 o1 c1 m1 o1 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src Diagram c1 m1 o1 c1 m1 o1
funct)) (c1
-> FinCat c1 m1 o1
-> c1
-> Diagram
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
forall c1 m1 o1 c2 m2 o2.
(FiniteCategory c1 m1 o1, Morphism m1 o1, Category c2 m2 o2,
 Morphism m2 o2) =>
c1 -> c2 -> o2 -> Diagram c1 m1 o1 c2 m2 o2
constantDiagram c1
indexingCategory FinCat c1 m1 o1
forall c m o. FinCat c m o
FinCat (Diagram c1 m1 o1 c1 m1 o1 -> c1
forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt Diagram c1 m1 o1 c1 m1 o1
funct)) ((o1 -> Diagram c1 m1 o1 c1 m1 o1)
-> Set o1 -> Map o1 (Diagram c1 m1 o1 c1 m1 o1)
forall k v. (k -> v) -> Set k -> Map k v
memorizeFunction (Diagram c1 m1 o1 c1 m1 o1 -> o1 -> Diagram c1 m1 o1 c1 m1 o1
forall a b. a -> b -> a
const Diagram c1 m1 o1 c1 m1 o1
funct) (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory))
            composeNatWithFunctor :: NaturalTransformation
  c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
-> Diagram c1 m1 o1 c1 m1 o1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
composeNatWithFunctor NaturalTransformation
  c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
nat Diagram c1 m1 o1 c1 m1 o1
funct = (Diagram c1 m1 o1 c1 m1 o1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
forall {o1} {m1} {c1}.
(Eq o1, Eq m1, Eq c1, Morphism m1 o1, FiniteCategory c1 m1 o1) =>
Diagram c1 m1 o1 c1 m1 o1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
functorToNat Diagram c1 m1 o1 c1 m1 o1
funct) NaturalTransformation
  c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
forall m o. Morphism m o => m -> m -> m
@ NaturalTransformation
  c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
nat
            notBottomObjects :: Set o1
notBottomObjects = (o1 -> Bool) -> Set o1 -> Set o1
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not(Bool -> Bool) -> (o1 -> Bool) -> o1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Set m1 -> Bool
forall a. Set a -> Bool
Set.null)(Set m1 -> Bool) -> (o1 -> Set m1) -> o1 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o) =>
c -> o -> Set m
arFromWithoutId c1
indexingCategory)) (c1 -> Set o1
forall c m o. FiniteCategory c m o => c -> Set o
ob c1
indexingCategory)
            indexingFunctToLeg :: NaturalTransformation
  c1
  m1
  o1
  c2
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  o2
-> m1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
indexingFunctToLeg NaturalTransformation
  c1
  m1
  o1
  c2
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  o2
nat m1
indexingFunct = (NaturalTransformation
  c1
  m1
  o1
  c2
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  o2
nat NaturalTransformation
  c1
  m1
  o1
  c2
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  o2
-> o1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall o1 c1 m1 c2 m2 o2.
Eq o1 =>
NaturalTransformation c1 m1 o1 c2 m2 o2 -> o1 -> m2
=>$ (m1 -> o1
forall m o. Morphism m o => m -> o
target m1
indexingFunct)) FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m o. Morphism m o => m -> m -> m
@ (Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
diagOfCG Diagram
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> m1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall m1 c1 o1 c2 m2 o2.
Eq m1 =>
Diagram c1 m1 o1 c2 m2 o2 -> m1 -> m2
->£ m1
indexingFunct)
            coequalizedNat :: NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coequalizedNat = (o1
 -> NaturalTransformation
      c1
      m1
      o1
      (FinCat (CompositionGraph a b) (CGMorphism a b) a)
      (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
      (CompositionGraph a b)
 -> NaturalTransformation
      c1
      m1
      o1
      (FinCat (CompositionGraph a b) (CGMorphism a b) a)
      (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
      (CompositionGraph a b))
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
-> Set o1
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall a b. Eq a => (a -> b -> b) -> b -> Set a -> b
Set.foldr (\o1
indexingObj NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
nat -> NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
-> NaturalTransformation
     c1
     m1
     o1
     (FinCat (CompositionGraph a b) (CGMorphism a b) a)
     (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
     (CompositionGraph a b)
forall {o1} {m1} {c1}.
(Eq o1, Eq m1, Eq c1, Morphism m1 o1, FiniteCategory c1 m1 o1) =>
NaturalTransformation
  c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
-> Diagram c1 m1 o1 c1 m1 o1
-> NaturalTransformation
     c1 m1 o1 (FinCat c1 m1 o1) (Diagram c1 m1 o1 c1 m1 o1) c1
composeNatWithFunctor NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
nat (Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall a b.
(Eq a, Eq b) =>
Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
coequalizeCompositionGraphDiagrams (NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
-> m1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
forall {c1} {m1} {c2} {o2}.
NaturalTransformation
  c1
  m1
  o1
  c2
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  o2
-> m1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a
indexingFunctToLeg NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
nat (m1 -> FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
-> Set m1
-> Set (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (c1 -> o1 -> Set m1
forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> o -> Set m
genArFrom c1
indexingCategory o1
indexingObj)))) NaturalTransformation
  c1
  m1
  o1
  (FinCat (CompositionGraph a b) (CGMorphism a b) a)
  (FinFunctor (CompositionGraph a b) (CGMorphism a b) a)
  (CompositionGraph a b)
coproductNat Set o1
notBottomObjects