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

Examples of Kan extensions.


-}
module Math.Functors.KanExtension.Examples
(
    exampleLeftKanExtension,
    exampleRightKanExtension,
)
where
    import              Math.FiniteCategory
    import              Math.FiniteCategories
    import              Math.Functors.KanExtension

    import              Data.Text                (Text)
    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 example of left Kan Extension which computes the sum (disjunction) of two booleans variables.
    exampleLeftKanExtension :: Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (CompositionGraph Text Text) (CGMorphism Text Text) Text
    exampleLeftKanExtension = lk
        where
            a = unsafeReadCGString "A\nB\n"
            b = unsafeReadCGString "A -q1-> C\nB -q2-> C\n"
            c = unsafeReadCGString "0 -abs-> 1\n"
            f = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nA -q1-> C\nB -q2-> C\n</TGT>\nA => A\nB => B\n"
            x = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -abs-> 1\n</TGT>\nA => 0\nB => 1"
            Just (lk,lknat) = (leftKan f x)
        
    -- | An example of right Kan Extension which computes the product (conjonction) of two booleans variables.
    exampleRightKanExtension :: Diagram (CompositionGraph Text Text) (CGMorphism Text Text) Text (CompositionGraph Text Text) (CGMorphism Text Text) Text
    exampleRightKanExtension = rk
        where
            a = unsafeReadCGString "A\nB\n"
            b = unsafeReadCGString "C -p1-> A\nC -p2-> B\n"
            c = unsafeReadCGString "0 -abs-> 1\n"
            f = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\nC -p1-> A\nC -p2-> B\n</TGT>\nA => A\nB => B\n"
            x = unsafeReadCGDString "<SRC>\nA\nB\n</SRC>\n<TGT>\n0 -abs-> 1\n</TGT>\nA => 0\nB => 1"
            Just (rk,rknat) = (rightKan f x)