{-| Module  : FiniteCategories
Description : An example of set cat completion.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An example of set cat completion.
-}
module ExampleSet.ExampleCompletion
(
    main
)
where
    import              Set.FinSet
    import              ConeCategory.ConeCategory
    import              ExportGraphViz.ExportGraphViz
    import              Diagram.Diagram

    -- | Constructs the limit of an arbitrary diagram in a set category.
    main = do
        putStrLn "Start of ExampleCompletion"
        let set = Collection $ [singleton 1, singleton 2] :: FinSet Int
        let c = FinSetCat $ toList set
        
        let Just diag = mkDiscreteDiagram c [singleton 1, singleton 2]
        diagToPdf2 diag "OutputGraphViz/Examples/Set/diag"
        
        let coneCat = mkConeCategory diag
        catToPdf coneCat "OutputGraphViz/Examples/Set/Completion/coneCat"
        let (insertionFunctor, newDiag, newLimit) = constructLimit diag
        diagToPdf2 newDiag "OutputGraphViz/Examples/Set/Completion/newDiag"
        let newConeCat = mkConeCategory newDiag
        catToPdf newConeCat "OutputGraphViz/Examples/Set/Completion/newConeCat"
        let lim = limits newDiag
        sequence $ (uncurry coneToPdf) <$> zip (coneToNaturalTransformation <$> lim) (("OutputGraphViz/Examples/Set/Completion/limit"++).show <$> [1..(length lim)])
        putStrLn "End of ExampleCompletion"