{-| Module  : FiniteCategories
Description : Examples of 'LimitCategory'.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of 'LimitCategory'.
-}
module Math.FiniteCategories.LimitCategory.Examples
(
    exampleDiagramVToFinCat,
    exampleLimitCategoryOfCompositionGraphs,
    exampleLimitOfCompositionGraphs,
)
where
    import Data.WeakSet.Safe
    import Data.WeakMap.Safe
    import Data.Text (pack, Text)
    
    import Math.CompleteCategory
    import Math.Categories.FunctorCategory
    import Math.Categories.ConeCategory
    import Math.Categories.FinCat
    import Math.FiniteCategories.LimitCategory
    import Math.FiniteCategories.V
    import Math.FiniteCategories.CompositionGraph
    
    -- | An example of 'Diagram' from 'V' to 'FinCat'.
    exampleDiagramVToFinCat :: Diagram V VAr VOb (FinCat (CompositionGraph Text Text) (CGMorphism Text Text) Text) (FinFunctor (CompositionGraph Text Text) (CGMorphism Text Text) Text) (CompositionGraph Text Text)
    exampleDiagramVToFinCat = completeDiagram diag
        where
            Right cg1 = readCGString "A -f-> B\nB -i-> D\nA -g-> C\nC -h-> D"
            Right cg2 = readCGString "F -j-> G"
            Right cg3 = readCGString "H -k-> I\nH -l-> I"
            Right diag1 = readCGDString "<SRC>\nA -f-> B\nB -i-> D\nA -g-> C\nC -h-> D\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nB => H\nC => H\nA -f-> B => <ID>\nA -g-> C => <ID>\nB -i-> D => H -k-> I\nC -h-> D => H -l-> I\nA => H\n"
            Right diag2 = readCGDString "<SRC>\nF -j-> G\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nF -j-> G => H -k-> I\n"
            diag = Diagram {src = V, tgt = FinCat, omap = weakMap [(VA,cg3),(VB,cg1),(VC,cg2)], mmap = weakMap [(VF, diag1),(VG, diag2)]}
    
    -- | An example of 'LimitCategory' of 'CompositionGraph's.
    exampleLimitCategoryOfCompositionGraphs :: LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text
    exampleLimitCategoryOfCompositionGraphs = LimitCategory $ completeDiagram diag
        where
            Right cg1 = readCGString "A -f-> B\nB -i-> D\nA -g-> C\nC -h-> D"
            Right cg2 = readCGString "F -j-> G"
            Right cg3 = readCGString "H -k-> I\nH -l-> I"
            Right diag1 = readCGDString "<SRC>\nA -f-> B\nB -i-> D\nA -g-> C\nC -h-> D\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nB => H\nC => H\nA -f-> B => <ID>\nA -g-> C => <ID>\nB -i-> D => H -k-> I\nC -h-> D => H -l-> I\nA => H\n"
            Right diag2 = readCGDString "<SRC>\nF -j-> G\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nF -j-> G => H -k-> I\n"
            diag = Diagram {src = V, tgt = FinCat, omap = weakMap [(VA,cg3),(VB,cg1),(VC,cg2)], mmap = weakMap [(VF, diag1),(VG, diag2)]}
            
    -- | Same example as 'exampleLimitCategoryOfCompositionGraphs' but the complete 'Cone'.
    exampleLimitOfCompositionGraphs :: Cone V VAr VOb (FinCat (LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text) (Limit VOb (CGMorphism Text Text)) (Limit VOb Text)) (FinFunctor (LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text) (Limit VOb (CGMorphism Text Text)) (Limit VOb Text)) (LimitCategory V VAr VOb (CompositionGraph Text Text) (CGMorphism Text Text) Text)
    exampleLimitOfCompositionGraphs = limit $ completeDiagram diag
        where
            Right cg1 = readCGString "A -f-> B\nB -i-> D\nA -g-> C\nC -h-> D"
            Right cg2 = readCGString "F -j-> G"
            Right cg3 = readCGString "H -k-> I\nH -l-> I"
            Right diag1 = readCGDString "<SRC>\nA -f-> B\nB -i-> D\nA -g-> C\nC -h-> D\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nB => H\nC => H\nA -f-> B => <ID>\nA -g-> C => <ID>\nB -i-> D => H -k-> I\nC -h-> D => H -l-> I\nA => H\n"
            Right diag2 = readCGDString "<SRC>\nF -j-> G\n</SRC>\n<TGT>\nH -k-> I\nH -l-> I\n</TGT>\nF -j-> G => H -k-> I\n"
            diag = Diagram {src = V, tgt = FinCat, omap = weakMap [(VA,cg3),(VB,cg1),(VC,cg2)], mmap = weakMap [(VF, diag1),(VG, diag2)]}