{-| Module  : FiniteCategories
Description : Examples of Kan extensions pretty printed.
Copyright   : Guillaume Sabbagh 2023
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Examples of Kan extensions pretty printed.


-}
module Math.Functors.KanExtension.Example
(
    main
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategories
    import              Math.Functors.KanExtension
    import              Math.IO.PrettyPrint
    import              Math.FiniteCategory

    
    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
    
    -- | Examples of Kan extensions pretty printed.
    main :: IO ()
    main = do
        putStrLn "Start of Math.Functors.KanExtension.Example"
        let d1 = (setToList $ ob (FunctorCategory (numberCategory 2) (numberCategory 4)))!! 3
        let d2 = (setToList $ ob (FunctorCategory (numberCategory 2) (numberCategory 3)))!! 2
        putStrLn $ pprint d1 
        putStrLn $ pprint d2 
        let Just (lk,lknat) = (leftKan d1 d2)
        putStrLn $ pprint lk 
        putStrLn $ pprint lknat 
        let Just (rk,rknat) = (rightKan d1 d2)
        putStrLn $ pprint rk 
        putStrLn $ pprint rknat 
        
        let a = unsafeReadSCGString "2\nA\n"
        putStrLn $ pprintFiniteCategory a 
        let b = unsafeReadSCGString "2\nA -f-> B\n"
        putStrLn $ pprintFiniteCategory b 
        let c = unsafeReadSCGString "2\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n"
        putStrLn $ pprintFiniteCategory c 
        let f = unsafeReadSCGDString "<SRC>\n2\nA\n</SRC>\n<TGT>\n2\nA -f-> B -g-> A = <ID>\nB -g-> A -f-> B = <ID>\n</TGT>\nA => A"
        putStrLn $ pprint f 
        let g = unsafeReadSCGDString "<SRC>\n2\nA\n</SRC>\n<TGT>\n2\nA -f-> B\n</TGT>\nA => A"
        putStrLn $ pprint g 
        
        let Just (lk,lknat) = (leftKan f g)
        putStrLn $ pprint lk 
        putStrLn $ pprint lknat 
        
        let Just (rk,rknat) = (rightKan f g)
        putStrLn $ pprint rk 
        putStrLn $ pprint rknat 
        
        
        let a = unsafeReadSCGString "2\nA\nB\n"
        putStrLn $ pprintFiniteCategory a 
        let b = unsafeReadSCGString "2\nC -p1-> A\nC -p2-> B\n"
        putStrLn $ pprintFiniteCategory b 
        let c = unsafeReadSCGString "2\n0 -abs-> 1\n"
        putStrLn $ pprintFiniteCategory c 
        let f = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nC -p1-> A\nC -p2-> B\n</TGT>\nA => A\nB => B\n"
        putStrLn $ pprint f 
        let x = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -abs-> 1\n</TGT>\nA => 1\nB => 1"
        putStrLn $ pprint x 
        
        -- let Just (lk,lknat) = (leftKan f x)
        -- putStrLn $ pprint lk 
        -- putStrLn $ pprint lknat 
        
        let Just (rk,rknat) = (rightKan f x)
        putStrLn $ pprint rk 
        putStrLn $ pprint rknat 
        
        
        let a = unsafeReadSCGString "2\nA\nB\n"
        putStrLn $ pprintFiniteCategory a 
        let b = unsafeReadSCGString "2\nA -q1-> C\nB -q2-> C\n"
        putStrLn $ pprintFiniteCategory b 
        let c = unsafeReadSCGString "2\n0 -abs-> 1\n"
        putStrLn $ pprintFiniteCategory c 
        let f = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nA -q1-> C\nB -q2-> C\n</TGT>\nA => A\nB => B\n"
        putStrLn $ pprint f 
        let x = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -abs-> 1\n</TGT>\nA => 1\nB => 1"
        putStrLn $ pprint x 
        
        let Just (lk,lknat) = (leftKan f x)
        putStrLn $ pprint lk 
        putStrLn $ pprint lknat 
        
        -- let Just (rk,rknat) = (rightKan f x)
        -- putStrLn $ pprint rk 
        -- putStrLn $ pprint rknat 
        
        
        let a = unsafeReadSCGString "2\nA\nB\n"
        putStrLn $ pprintFiniteCategory a 
        let b = unsafeReadSCGString "2\nA -f-> C\nB -g-> C\n"
        putStrLn $ pprintFiniteCategory b 
        let c = unsafeReadSCGString "2\n0 -f-> 1\n1 -g-> 2\n"
        putStrLn $ pprintFiniteCategory c 
        let f = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nA -f-> C\nB -g-> C\n</TGT>\nA => A\nB => B\n"
        putStrLn $ pprint f 
        let x = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -f-> 1\n1 -g-> 2\n</TGT>\nA => 1\nB => 1"
        putStrLn $ pprint x 
        
        let Just (lk,lknat) = (leftKan f x)
        putStrLn $ pprint lk 
        putStrLn $ pprint lknat 
        
        let Just (rk,rknat) = (rightKan f x)
        putStrLn $ pprint rk 
        putStrLn $ pprint rknat 
        
        -- let a = unsafeReadSCGString "2\nA\nB\n"
        -- putStrLn $ pprintFiniteCategory a 
        -- let b = unsafeReadSCGString "2\nA -q1-> C\nB -q2-> C\n"
        -- putStrLn $ pprintFiniteCategory b 
        -- let c = unsafeReadSCGString "2\n0 -abs-> 1\n"
        -- putStrLn $ pprintFiniteCategory c 
        -- let f = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\nA -q1-> C\nB -q2-> C\n</TGT>\nA => A\nB => B\n"
        -- putStrLn $ pprint f 
        -- let x = unsafeReadSCGDString "<SRC>\n2\nA\nB\n</SRC>\n<TGT>\n2\n0 -abs-> 1\n</TGT>\nA => 0\nB => 1"
        -- putStrLn $ pprint x 
        
        -- let Just (lk,lknat) = (leftKan f x)
        -- putStrLn $ pprint lk 
        -- putStrLn $ pprint lknat 
        
        -- let Just (rk,rknat) = (rightKan f x)
        -- putStrLn $ pprint rk 
        -- putStrLn $ pprint rknat 
        
        putStrLn "End of Math.Functors.KanExtension.Example"