{-# 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{
                            sourceArrow :: n,
                            targetArrow :: n,
                            labelArrow :: e
                          }
                          deriving (Eq, Show)
    
    instance (PrettyPrint n, PrettyPrint e) => PrettyPrint (Arrow n e) where
        pprint a = (pprint $ sourceArrow a)++"-"++(pprint $ labelArrow a)++"->"++(pprint $ targetArrow 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 {
                        nodes :: Set n, -- ^ The set of nodes of the graph.
                        edges :: Set (Arrow n e) -- ^ The set of arrows of the graph.
                        } deriving (Eq)
    
    instance (Show n, Show e) => Show (Graph n e) where
        show g = "(unsafeGraph "++(show $ nodes g)++" "++(show $ edges g)++")"
    
    -- | Smart constructor of 'Graph'.
    graph :: (Eq n) => Set n -> Set (Arrow n e) -> Maybe (Graph n e)
    graph ns es
        | (sourceArrow <$> es) `isIncludedIn` ns && (targetArrow <$> es) `isIncludedIn` ns = Just Graph{nodes=ns, edges=es}
        | otherwise = Nothing
        
    -- | Unsafe constructor of 'Graph', does not check the 'Graph' structure.
    unsafeGraph :: Set n -> Set (Arrow n e) -> Graph n e
    unsafeGraph n e = Graph{nodes=n, edges=e}
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (Graph n e) where
        pprint g = "Graph ("++(pprint $ nodes g)++", "++(pprint $ edges g)++")"
    
    -- | 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 {
                                    nodeMap :: Map n n, -- ^ The mapping of nodes.
                                    edgeMap :: Map (Arrow n e) (Arrow n e), -- ^ The mapping of edges.
                                    targetGraph :: Graph n e -- ^ The target graph.
                                    } deriving (Eq)
    
    -- | Check wether the structure of 'GraphHomomorphism' is respected or not.
    checkGraphHomomorphism :: (Eq n, Eq e) => GraphHomomorphism n e -> Bool
    checkGraphHomomorphism gh = imageInTarget && Set.and noTear
        where
            noTear = [(nodeMap gh) |!| (sourceArrow arr) == sourceArrow ((edgeMap gh) |!| arr) && (nodeMap gh) |!| (targetArrow arr) == targetArrow ((edgeMap gh) |!| arr)| arr <- (domain.edgeMap) gh]
            imageInTarget = (image.nodeMap) gh `isIncludedIn` (nodes.targetGraph) gh && (image.edgeMap) gh `isIncludedIn` (edges.targetGraph) 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 nm em tg
        | checkGraphHomomorphism gh = Just gh
        | otherwise = Nothing
        where
            gh = GraphHomomorphism{nodeMap=nm, edgeMap=em, targetGraph=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 nm em tg = GraphHomomorphism{nodeMap=nm, edgeMap=em, targetGraph=tg}
    
    instance (Show n, Show e) => Show (GraphHomomorphism n e) where
        show gh = "(unsafeGraphHomomorphism "++(show $ nodeMap gh)++" "++(show $ edgeMap gh)++ " " ++ (show $ targetGraph gh) ++")"
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (GraphHomomorphism n e) where
        pprint gh = "("++(pprint $ nodeMap gh)++", "++(pprint $ edgeMap gh)++")"
        
    instance (Eq n, Eq e) => Morphism (GraphHomomorphism n e) (Graph n e) where
        source gh = Graph {nodes = (domain.nodeMap) gh, edges = (domain.edgeMap) gh}
        target = targetGraph
        (@?) gh2 gh1
            | target gh1 == source gh2 = Just $ GraphHomomorphism {nodeMap = (nodeMap gh2) |.| (nodeMap gh1), edgeMap = (edgeMap gh2) |.| (edgeMap gh1), targetGraph = target gh2}
            | otherwise = Nothing
    
    -- | The category of finite graphs.
    data FinGrph n e = FinGrph deriving (Eq, Show)
    
    instance (PrettyPrint n, PrettyPrint e, Eq n, Eq e) => PrettyPrint (FinGrph n e) where
        pprint = show
        
    instance (Eq n, Eq e, Show n ,Show e) => Category (FinGrph n e) (GraphHomomorphism n e) (Graph n e) where
        identity _ g = GraphHomomorphism {nodeMap = (idFromSet.nodes) g, edgeMap = (idFromSet.edges) g, targetGraph = g}
        ar _ s t = [GraphHomomorphism
            {
                nodeMap = appO, edgeMap = appF, targetGraph = t
            } | appO <- appObj, appF <- ((fmap $ (Map.unions)).cartesianProductOfSets $ [twoObjToEdgeMaps x y appO | x <- (setToList $ nodes s), y <- (setToList $ nodes s)])]
            where
                appObj = Map.enumerateMaps (nodes s) (nodes t)
                twoObjToEdgeMaps n1 n2 nMap = Map.enumerateMaps (Set.filter (\a -> sourceArrow a == n1 && targetArrow a == n2) (edges s)) (Set.filter (\a -> sourceArrow a == nMap |!| n1 && targetArrow a == nMap |!| n2) (edges t))
    
    -- | Return the underlying graph of a 'FiniteCategory'.
    underlyingGraph :: (FiniteCategory c m o, Morphism m o) => c -> Graph o m
    underlyingGraph c = Graph{
                                nodes = ob c,
                                edges = (\m -> Arrow{sourceArrow=source m, targetArrow=target m, labelArrow=m}) <$> arrows 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 formatObj formatAr c = Graph{
                                                        nodes = formatObj <$> ob c,
                                                        edges = (\m -> Arrow{sourceArrow=formatObj.source $ m, targetArrow=formatObj.target $ m, labelArrow=formatAr m}) <$> arrows c
                                                    }