{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, MonadComprehensions #-}
module Math.Categories.FinGrph
(
Arrow(..),
Graph,
nodes,
edges,
graph,
unsafeGraph,
GraphHomomorphism,
nodeMap,
edgeMap,
checkGraphHomomorphism,
graphHomomorphism,
unsafeGraphHomomorphism,
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
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
$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
/= :: 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
$cshowsPrec :: forall n e. (Show n, Show e) => Int -> Arrow n e -> ShowS
showsPrec :: Int -> Arrow n e -> ShowS
$cshow :: forall n e. (Show n, Show e) => Arrow n e -> String
show :: Arrow n e -> String
$cshowList :: forall n e. (Show n, Show e) => [Arrow n e] -> ShowS
showList :: [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)
data Graph n e = Graph {
forall n e. Graph n e -> Set n
nodes :: Set n,
forall n e. Graph n e -> Set (Arrow n e)
edges :: Set (Arrow n e)
} 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
$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
/= :: 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
")"
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{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
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{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
")"
data GraphHomomorphism n e = GraphHomomorphism {
forall n e. GraphHomomorphism n e -> Map n n
nodeMap :: Map n n,
forall n e. GraphHomomorphism n e -> Map (Arrow n e) (Arrow n e)
edgeMap :: Map (Arrow n e) (Arrow n e),
forall n e. GraphHomomorphism n e -> Graph n e
targetGraph :: Graph n e
} 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
$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
/= :: GraphHomomorphism n e -> GraphHomomorphism n e -> Bool
Eq)
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
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{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}
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{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 {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 {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
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
$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
/= :: 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
$cshowsPrec :: forall n e. Int -> FinGrph n e -> ShowS
showsPrec :: Int -> FinGrph n e -> ShowS
$cshow :: forall n e. FinGrph n e -> String
show :: FinGrph n e -> String
$cshowList :: forall n e. [FinGrph n e] -> ShowS
showList :: [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 {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
{
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 a b. (a -> b) -> Set a -> Set b
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))
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{
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{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
}
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{
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{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
}