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

{-| Module  : FiniteCategories
Description : The __'FinGrph'__ category has finite multidigraphs as objects and multidigraph homomorphisms as morphisms.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

The __'FinGrph'__ category has finite multidigraphs as objects and multidigraph homomorphisms as morphisms.
-}

module Math.Categories.FinGrph
(
    -- * Graph

    Arrow(..),
    Graph,
    -- ** Getters

    nodes,
    edges,
    -- ** Smart constructors

    graph,
    unsafeGraph,
    -- * Graph homomorphism

    GraphHomomorphism,
    -- ** Getters

    nodeMap,
    edgeMap,
    -- ** Smart constructor

    checkGraphHomomorphism,
    graphHomomorphism,
    unsafeGraphHomomorphism,
    -- * FinGrph

    FinGrph(..),
    underlyingGraph,
    underlyingGraphFormat,
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.IO.PrettyPrint
    
    import              Data.WeakSet        (Set)
    import qualified    Data.WeakSet    as  Set
    import              Data.WeakSet.Safe
    import              Data.WeakMap        (Map)
    import qualified    Data.WeakMap    as  Map
    import              Data.WeakMap.Safe
    
    -- | An 'Arrow' is composed of a source node, a target node and a label.

    data Arrow n e = Arrow{
                            forall n e. Arrow n e -> n
sourceArrow :: n,
                            forall n e. Arrow n e -> n
targetArrow :: n,
                            forall n e. Arrow n e -> e
labelArrow :: e
                          }
                          deriving (Arrow n e -> Arrow n e -> Bool
(Arrow n e -> Arrow n e -> Bool)
-> (Arrow n e -> Arrow n e -> Bool) -> Eq (Arrow n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq n, Eq e) => Arrow n e -> Arrow n e -> Bool
/= :: Arrow n e -> Arrow n e -> Bool
$c/= :: forall n e. (Eq n, Eq e) => Arrow n e -> Arrow n e -> Bool
== :: Arrow n e -> Arrow n e -> Bool
$c== :: forall n e. (Eq n, Eq e) => Arrow n e -> Arrow n e -> Bool
Eq, Int -> Arrow n e -> ShowS
[Arrow n e] -> ShowS
Arrow n e -> String
(Int -> Arrow n e -> ShowS)
-> (Arrow n e -> String)
-> ([Arrow n e] -> ShowS)
-> Show (Arrow n e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. (Show n, Show e) => Int -> Arrow n e -> ShowS
forall n e. (Show n, Show e) => [Arrow n e] -> ShowS
forall n e. (Show n, Show e) => Arrow n e -> String
showList :: [Arrow n e] -> ShowS
$cshowList :: forall n e. (Show n, Show e) => [Arrow n e] -> ShowS
show :: Arrow n e -> String
$cshow :: forall n e. (Show n, Show e) => Arrow n e -> String
showsPrec :: Int -> Arrow n e -> ShowS
$cshowsPrec :: forall n e. (Show n, Show e) => Int -> Arrow n e -> ShowS
Show)
    
    instance (PrettyPrint n, PrettyPrint e) => PrettyPrint (Arrow n e) where
        pprint :: Arrow n e -> String
pprint Arrow n e
a = (n -> String
forall a. PrettyPrint a => a -> String
pprint (n -> String) -> n -> String
forall a b. (a -> b) -> a -> b
$ Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"-"String -> ShowS
forall a. [a] -> [a] -> [a]
++(e -> String
forall a. PrettyPrint a => a -> String
pprint (e -> String) -> e -> String
forall a b. (a -> b) -> a -> b
$ Arrow n e -> e
forall n e. Arrow n e -> e
labelArrow Arrow n e
a)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
"->"String -> ShowS
forall a. [a] -> [a] -> [a]
++(n -> String
forall a. PrettyPrint a => a -> String
pprint (n -> String) -> n -> String
forall a b. (a -> b) -> a -> b
$ Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a)
    
    -- | A 'Graph' is a set of nodes and a set of 'Arrow's.

    -- 

    -- 'Graph' is private, use smart constructor 'graph'.

    data Graph n e = Graph {
                        forall n e. Graph n e -> Set n
nodes :: Set n, -- ^ The set of nodes of the graph.

                        forall n e. Graph n e -> Set (Arrow n e)
edges :: Set (Arrow n e) -- ^ The set of arrows of the graph.

                        } deriving (Graph n e -> Graph n e -> Bool
(Graph n e -> Graph n e -> Bool)
-> (Graph n e -> Graph n e -> Bool) -> Eq (Graph n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq n, Eq e) => Graph n e -> Graph n e -> Bool
/= :: Graph n e -> Graph n e -> Bool
$c/= :: forall n e. (Eq n, Eq e) => Graph n e -> Graph n e -> Bool
== :: Graph n e -> Graph n e -> Bool
$c== :: forall n e. (Eq n, Eq e) => Graph n e -> Graph n e -> Bool
Eq)
    
    instance (Show n, Show e) => Show (Graph n e) where
        show :: Graph n e -> String
show Graph n e
g = String
"(unsafeGraph "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Set n -> String
forall a. Show a => a -> String
show (Set n -> String) -> Set n -> String
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Set (Arrow n e) -> String
forall a. Show a => a -> String
show (Set (Arrow n e) -> String) -> Set (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    -- | Smart constructor of 'Graph'.

    graph :: (Eq n) => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
    graph :: forall n e. Eq n => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
graph Set n
ns Set (Arrow n e)
es
        | (Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow (Arrow n e -> n) -> Set (Arrow n e) -> Set n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Arrow n e)
es) Set n -> Set n -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` Set n
ns Bool -> Bool -> Bool
&& (Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow (Arrow n e -> n) -> Set (Arrow n e) -> Set n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Arrow n e)
es) Set n -> Set n -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` Set n
ns = Graph n e -> Maybe (Graph n e)
forall a. a -> Maybe a
Just Graph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
Graph{nodes :: Set n
nodes=Set n
ns, edges :: Set (Arrow n e)
edges=Set (Arrow n e)
es}
        | Bool
otherwise = Maybe (Graph n e)
forall a. Maybe a
Nothing
        
    -- | Unsafe constructor of 'Graph', does not check the 'Graph' structure.

    unsafeGraph :: Set n -> Set (Arrow n e) -> Graph n e
    unsafeGraph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
unsafeGraph Set n
n Set (Arrow n e)
e = Graph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
Graph{nodes :: Set n
nodes=Set n
n, edges :: Set (Arrow n e)
edges=Set (Arrow n e)
e}
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (Graph n e) where
        pprint :: Graph n e -> String
pprint Graph n e
g = String
"Graph ("String -> ShowS
forall a. [a] -> [a] -> [a]
++(Set n -> String
forall a. PrettyPrint a => a -> String
pprint (Set n -> String) -> Set n -> String
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Set (Arrow n e) -> String
forall a. PrettyPrint a => a -> String
pprint (Set (Arrow n e) -> String) -> Set (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
g)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    -- | A 'GraphHomomorphism' is composed of a map between the nodes of the graphs, a map between the edges of the graphs, and the target 'Graph' so that we can recover it from the morphism.

    --

    -- It must follow axioms such that the image of an arrow is not torn appart, that is why the constructor is private. Use the smart constructor 'graphHomomorphism' instead.

    data GraphHomomorphism n e = GraphHomomorphism {
                                    forall n e. GraphHomomorphism n e -> Map n n
nodeMap :: Map n n, -- ^ The mapping of nodes.

                                    forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap :: Map (Arrow n e) (Arrow n e), -- ^ The mapping of edges.

                                    forall n e. GraphHomomorphism n e -> Graph n e
targetGraph :: Graph n e -- ^ The target graph.

                                    } deriving (GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
(GraphHomomorphism n e -> GraphHomomorphism n e -> Bool)
-> (GraphHomomorphism n e -> GraphHomomorphism n e -> Bool)
-> Eq (GraphHomomorphism n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e.
(Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
/= :: GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
$c/= :: forall n e.
(Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
== :: GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
$c== :: forall n e.
(Eq n, Eq e) =>
GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
Eq)
    
    -- | Check wether the structure of 'GraphHomomorphism' is respected or not.

    checkGraphHomomorphism :: (Eq n, Eq e) => GraphHomomorphism n e -> Bool
    checkGraphHomomorphism :: forall n e. (Eq n, Eq e) => GraphHomomorphism n e -> Bool
checkGraphHomomorphism GraphHomomorphism n e
gh = Bool
imageInTarget Bool -> Bool -> Bool
&& Set Bool -> Bool
Set.and Set Bool
noTear
        where
            noTear :: Set Bool
noTear = [(GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| (Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
arr) n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow ((GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
arr) Bool -> Bool -> Bool
&& (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh) Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| (Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
arr) n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow ((GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh) Map (Arrow n e) (Arrow n e) -> Arrow n e -> Arrow n e
forall k v. Eq k => Map k v -> k -> v
|!| Arrow n e
arr)| Arrow n e
arr <- (Map (Arrow n e) (Arrow n e) -> Set (Arrow n e)
forall k a. Map k a -> Set k
domain(Map (Arrow n e) (Arrow n e) -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e))
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap) GraphHomomorphism n e
gh]
            imageInTarget :: Bool
imageInTarget = (Map n n -> Set n
forall k a. Eq k => Map k a -> Set a
image(Map n n -> Set n)
-> (GraphHomomorphism n e -> Map n n)
-> GraphHomomorphism n e
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap) GraphHomomorphism n e
gh Set n -> Set n -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes(Graph n e -> Set n)
-> (GraphHomomorphism n e -> Graph n e)
-> GraphHomomorphism n e
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph) GraphHomomorphism n e
gh Bool -> Bool -> Bool
&& (Map (Arrow n e) (Arrow n e) -> Set (Arrow n e)
forall k a. Eq k => Map k a -> Set a
image(Map (Arrow n e) (Arrow n e) -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e))
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap) GraphHomomorphism n e
gh Set (Arrow n e) -> Set (Arrow n e) -> Bool
forall a. Eq a => Set a -> Set a -> Bool
`isIncludedIn` (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges(Graph n e -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Graph n e)
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph) GraphHomomorphism n e
gh
    
    -- | The smart constructor of 'GraphHomomorphism'.

    graphHomomorphism :: (Eq n, Eq e) => Map n n -> Map (Arrow n e) (Arrow n e) -> Graph n e -> Maybe (GraphHomomorphism n e)
    graphHomomorphism :: forall n e.
(Eq n, Eq e) =>
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> Maybe (GraphHomomorphism n e)
graphHomomorphism Map n n
nm Map (Arrow n e) (Arrow n e)
em Graph n e
tg
        | GraphHomomorphism n e -> Bool
forall n e. (Eq n, Eq e) => GraphHomomorphism n e -> Bool
checkGraphHomomorphism GraphHomomorphism n e
gh = GraphHomomorphism n e -> Maybe (GraphHomomorphism n e)
forall a. a -> Maybe a
Just GraphHomomorphism n e
gh
        | Bool
otherwise = Maybe (GraphHomomorphism n e)
forall a. Maybe a
Nothing
        where
            gh :: GraphHomomorphism n e
gh = GraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
GraphHomomorphism{nodeMap :: Map n n
nodeMap=Map n n
nm, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap=Map (Arrow n e) (Arrow n e)
em, targetGraph :: Graph n e
targetGraph=Graph n e
tg}
    
    -- | Unsafe constructor of 'GraphHomomorphism' which does not check the structure of the 'GraphHomomorphism'.

    unsafeGraphHomomorphism :: Map n n -> Map (Arrow n e) (Arrow n e) -> Graph n e -> GraphHomomorphism n e
    unsafeGraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
unsafeGraphHomomorphism Map n n
nm Map (Arrow n e) (Arrow n e)
em Graph n e
tg = GraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
GraphHomomorphism{nodeMap :: Map n n
nodeMap=Map n n
nm, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap=Map (Arrow n e) (Arrow n e)
em, targetGraph :: Graph n e
targetGraph=Graph n e
tg}
    
    instance (Show n, Show e) => Show (GraphHomomorphism n e) where
        show :: GraphHomomorphism n e -> String
show GraphHomomorphism n e
gh = String
"(unsafeGraphHomomorphism "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Map n n -> String
forall a. Show a => a -> String
show (Map n n -> String) -> Map n n -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Map (Arrow n e) (Arrow n e) -> String
forall a. Show a => a -> String
show (Map (Arrow n e) (Arrow n e) -> String)
-> Map (Arrow n e) (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Graph n e -> String
forall a. Show a => a -> String
show (Graph n e -> String) -> Graph n e -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph GraphHomomorphism n e
gh) String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (GraphHomomorphism n e) where
        pprint :: GraphHomomorphism n e -> String
pprint GraphHomomorphism n e
gh = String
"("String -> ShowS
forall a. [a] -> [a] -> [a]
++(Map n n -> String
forall a. PrettyPrint a => a -> String
pprint (Map n n -> String) -> Map n n -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", "String -> ShowS
forall a. [a] -> [a] -> [a]
++(Map (Arrow n e) (Arrow n e) -> String
forall a. PrettyPrint a => a -> String
pprint (Map (Arrow n e) (Arrow n e) -> String)
-> Map (Arrow n e) (Arrow n e) -> String
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh)String -> ShowS
forall a. [a] -> [a] -> [a]
++String
")"
        
    instance (Eq n, Eq e) => Morphism (GraphHomomorphism n e) (Graph n e) where
        source :: GraphHomomorphism n e -> Graph n e
source GraphHomomorphism n e
gh = Graph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
Graph {nodes :: Set n
nodes = (Map n n -> Set n
forall k a. Map k a -> Set k
domain(Map n n -> Set n)
-> (GraphHomomorphism n e -> Map n n)
-> GraphHomomorphism n e
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap) GraphHomomorphism n e
gh, edges :: Set (Arrow n e)
edges = (Map (Arrow n e) (Arrow n e) -> Set (Arrow n e)
forall k a. Map k a -> Set k
domain(Map (Arrow n e) (Arrow n e) -> Set (Arrow n e))
-> (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e))
-> GraphHomomorphism n e
-> Set (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap) GraphHomomorphism n e
gh}
        target :: GraphHomomorphism n e -> Graph n e
target = GraphHomomorphism n e -> Graph n e
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph
        @? :: GraphHomomorphism n e
-> GraphHomomorphism n e -> Maybe (GraphHomomorphism n e)
(@?) GraphHomomorphism n e
gh2 GraphHomomorphism n e
gh1
            | GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh1 Graph n e -> Graph n e -> Bool
forall a. Eq a => a -> a -> Bool
== GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
source GraphHomomorphism n e
gh2 = GraphHomomorphism n e -> Maybe (GraphHomomorphism n e)
forall a. a -> Maybe a
Just (GraphHomomorphism n e -> Maybe (GraphHomomorphism n e))
-> GraphHomomorphism n e -> Maybe (GraphHomomorphism n e)
forall a b. (a -> b) -> a -> b
$ GraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
GraphHomomorphism {nodeMap :: Map n n
nodeMap = (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh2) Map n n -> Map n n -> Map n n
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (GraphHomomorphism n e -> Map n n
forall n e. GraphHomomorphism n e -> Map n n
nodeMap GraphHomomorphism n e
gh1), edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh2) Map (Arrow n e) (Arrow n e)
-> Map (Arrow n e) (Arrow n e) -> Map (Arrow n e) (Arrow n e)
forall b c a. Eq b => Map b c -> Map a b -> Map a c
|.| (GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap GraphHomomorphism n e
gh1), targetGraph :: Graph n e
targetGraph = GraphHomomorphism n e -> Graph n e
forall m o. Morphism m o => m -> o
target GraphHomomorphism n e
gh2}
            | Bool
otherwise = Maybe (GraphHomomorphism n e)
forall a. Maybe a
Nothing
    
    -- | The category of finite graphs.

    data FinGrph n e = FinGrph deriving (FinGrph n e -> FinGrph n e -> Bool
(FinGrph n e -> FinGrph n e -> Bool)
-> (FinGrph n e -> FinGrph n e -> Bool) -> Eq (FinGrph n e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. FinGrph n e -> FinGrph n e -> Bool
/= :: FinGrph n e -> FinGrph n e -> Bool
$c/= :: forall n e. FinGrph n e -> FinGrph n e -> Bool
== :: FinGrph n e -> FinGrph n e -> Bool
$c== :: forall n e. FinGrph n e -> FinGrph n e -> Bool
Eq, Int -> FinGrph n e -> ShowS
[FinGrph n e] -> ShowS
FinGrph n e -> String
(Int -> FinGrph n e -> ShowS)
-> (FinGrph n e -> String)
-> ([FinGrph n e] -> ShowS)
-> Show (FinGrph n e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. Int -> FinGrph n e -> ShowS
forall n e. [FinGrph n e] -> ShowS
forall n e. FinGrph n e -> String
showList :: [FinGrph n e] -> ShowS
$cshowList :: forall n e. [FinGrph n e] -> ShowS
show :: FinGrph n e -> String
$cshow :: forall n e. FinGrph n e -> String
showsPrec :: Int -> FinGrph n e -> ShowS
$cshowsPrec :: forall n e. Int -> FinGrph n e -> ShowS
Show)
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (FinGrph n e) where
        pprint :: FinGrph n e -> String
pprint = FinGrph n e -> String
forall a. Show a => a -> String
show
        
    instance (Eq n, Eq e, Show n ,Show e) => Category (FinGrph n e) (GraphHomomorphism n e) (Graph n e) where
        identity :: Morphism (GraphHomomorphism n e) (Graph n e) =>
FinGrph n e -> Graph n e -> GraphHomomorphism n e
identity FinGrph n e
_ Graph n e
g = GraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
GraphHomomorphism {nodeMap :: Map n n
nodeMap = (Set n -> Map n n
forall a. Set a -> Map a a
idFromSet(Set n -> Map n n) -> (Graph n e -> Set n) -> Graph n e -> Map n n
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes) Graph n e
g, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = (Set (Arrow n e) -> Map (Arrow n e) (Arrow n e)
forall a. Set a -> Map a a
idFromSet(Set (Arrow n e) -> Map (Arrow n e) (Arrow n e))
-> (Graph n e -> Set (Arrow n e))
-> Graph n e
-> Map (Arrow n e) (Arrow n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges) Graph n e
g, targetGraph :: Graph n e
targetGraph = Graph n e
g}
        ar :: Morphism (GraphHomomorphism n e) (Graph n e) =>
FinGrph n e
-> Graph n e -> Graph n e -> Set (GraphHomomorphism n e)
ar FinGrph n e
_ Graph n e
s Graph n e
t = [GraphHomomorphism :: forall n e.
Map n n
-> Map (Arrow n e) (Arrow n e)
-> Graph n e
-> GraphHomomorphism n e
GraphHomomorphism
            {
                nodeMap :: Map n n
nodeMap = Map n n
appO, edgeMap :: Map (Arrow n e) (Arrow n e)
edgeMap = Map (Arrow n e) (Arrow n e)
appF, targetGraph :: Graph n e
targetGraph = Graph n e
t
            } | Map n n
appO <- Set (Map n n)
appObj, Map (Arrow n e) (Arrow n e)
appF <- ((([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e))
-> Set [Map (Arrow n e) (Arrow n e)]
-> Set (Map (Arrow n e) (Arrow n e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e))
 -> Set [Map (Arrow n e) (Arrow n e)]
 -> Set (Map (Arrow n e) (Arrow n e)))
-> ([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e))
-> Set [Map (Arrow n e) (Arrow n e)]
-> Set (Map (Arrow n e) (Arrow n e))
forall a b. (a -> b) -> a -> b
$ ([Map (Arrow n e) (Arrow n e)] -> Map (Arrow n e) (Arrow n e)
forall k a. Eq k => [Map k a] -> Map k a
Map.unions))(Set [Map (Arrow n e) (Arrow n e)]
 -> Set (Map (Arrow n e) (Arrow n e)))
-> ([Set (Map (Arrow n e) (Arrow n e))]
    -> Set [Map (Arrow n e) (Arrow n e)])
-> [Set (Map (Arrow n e) (Arrow n e))]
-> Set (Map (Arrow n e) (Arrow n e))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[Set (Map (Arrow n e) (Arrow n e))]
-> Set [Map (Arrow n e) (Arrow n e)]
forall (m :: * -> *) a.
(Monoid (m a), Monad m, Foldable m, Eq a) =>
m (Set a) -> Set (m a)
cartesianProductOfSets ([Set (Map (Arrow n e) (Arrow n e))]
 -> Set (Map (Arrow n e) (Arrow n e)))
-> [Set (Map (Arrow n e) (Arrow n e))]
-> Set (Map (Arrow n e) (Arrow n e))
forall a b. (a -> b) -> a -> b
$ [n -> n -> Map n n -> Set (Map (Arrow n e) (Arrow n e))
twoObjToEdgeMaps n
x n
y Map n n
appO | n
x <- (Set n -> [n]
forall a. Eq a => Set a -> [a]
setToList (Set n -> [n]) -> Set n -> [n]
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
s), n
y <- (Set n -> [n]
forall a. Eq a => Set a -> [a]
setToList (Set n -> [n]) -> Set n -> [n]
forall a b. (a -> b) -> a -> b
$ Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
s)])]
            where
                appObj :: Set (Map n n)
appObj = Set n -> Set n -> Set (Map n n)
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
s) (Graph n e -> Set n
forall n e. Graph n e -> Set n
nodes Graph n e
t)
                twoObjToEdgeMaps :: n -> n -> Map n n -> Set (Map (Arrow n e) (Arrow n e))
twoObjToEdgeMaps n
n1 n
n2 Map n n
nMap = Set (Arrow n e)
-> Set (Arrow n e) -> Set (Map (Arrow n e) (Arrow n e))
forall a b. (Eq a, Eq b) => Set a -> Set b -> Set (Map a b)
Map.enumerateMaps ((Arrow n e -> Bool) -> Set (Arrow n e) -> Set (Arrow n e)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow n e
a -> Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
n1 Bool -> Bool -> Bool
&& Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
n2) (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
s)) ((Arrow n e -> Bool) -> Set (Arrow n e) -> Set (Arrow n e)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Arrow n e
a -> Arrow n e -> n
forall n e. Arrow n e -> n
sourceArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Map n n
nMap Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
n1 Bool -> Bool -> Bool
&& Arrow n e -> n
forall n e. Arrow n e -> n
targetArrow Arrow n e
a n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== Map n n
nMap Map n n -> n -> n
forall k v. Eq k => Map k v -> k -> v
|!| n
n2) (Graph n e -> Set (Arrow n e)
forall n e. Graph n e -> Set (Arrow n e)
edges Graph n e
t))
    
    -- | Return the underlying graph of a 'FiniteCategory'.

    underlyingGraph :: (FiniteCategory c m o, Morphism m o) => c -> Graph o m
    underlyingGraph :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
c -> Graph o m
underlyingGraph c
c = Graph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
Graph{
                                nodes :: Set o
nodes = c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c,
                                edges :: Set (Arrow o m)
edges = (\m
m -> Arrow :: forall n e. n -> n -> e -> Arrow n e
Arrow{sourceArrow :: o
sourceArrow=m -> o
forall m o. Morphism m o => m -> o
source m
m, targetArrow :: o
targetArrow=m -> o
forall m o. Morphism m o => m -> o
target m
m, labelArrow :: m
labelArrow=m
m}) (m -> Arrow o m) -> Set m -> Set (Arrow o m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c
                            }
                            
    -- | Return the underlying graph of a 'FiniteCategory' and apply formatting functions on objects and arrows.

    underlyingGraphFormat :: (FiniteCategory c m o, Morphism m o) => (o -> a) -> (m -> b) -> c -> Graph a b
    underlyingGraphFormat :: forall c m o a b.
(FiniteCategory c m o, Morphism m o) =>
(o -> a) -> (m -> b) -> c -> Graph a b
underlyingGraphFormat o -> a
formatObj m -> b
formatAr c
c = Graph :: forall n e. Set n -> Set (Arrow n e) -> Graph n e
Graph{
                                                        nodes :: Set a
nodes = o -> a
formatObj (o -> a) -> Set o -> Set a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set o
forall c m o. FiniteCategory c m o => c -> Set o
ob c
c,
                                                        edges :: Set (Arrow a b)
edges = (\m
m -> Arrow :: forall n e. n -> n -> e -> Arrow n e
Arrow{sourceArrow :: a
sourceArrow=o -> a
formatObj(o -> a) -> (m -> o) -> m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.m -> o
forall m o. Morphism m o => m -> o
source (m -> a) -> m -> a
forall a b. (a -> b) -> a -> b
$ m
m, targetArrow :: a
targetArrow=o -> a
formatObj(o -> a) -> (m -> o) -> m -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.m -> o
forall m o. Morphism m o => m -> o
target (m -> a) -> m -> a
forall a b. (a -> b) -> a -> b
$ m
m, labelArrow :: b
labelArrow=m -> b
formatAr m
m}) (m -> Arrow a b) -> Set m -> Set (Arrow a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> c -> Set m
forall c m o. (FiniteCategory c m o, Morphism m o) => c -> Set m
arrows c
c
                                                    }