{-| Module  : FiniteCategories
Description : Functions to convert all functor types.
Copyright   : Guillaume Sabbagh 2021
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Functions to convert all functor types.
-}

module Diagram.Conversion
(
    -- * Diagram to something

    diagramToFinFunctor,
    diagramToPartialFunctor,
    -- * FinFunctor to something

    finFunctorToDiagram,
    finFunctorToPartialFunctor,
    -- * PartialFunctor to something

    partialFunctorToDiagram,
    partialFunctorToFinFunctor
)
where
    import FiniteCategory.FiniteCategory
    import Diagram.Diagram
    import Cat.FinCat
    import Cat.PartialFinCat
    import Utils.SetList
    import Utils.AssociationList
    
    -- | Converts a homogeneous `Diagram` to a `FinFunctor`.

    diagramToFinFunctor :: (FiniteCategory c m o, Morphism m o) => Diagram c m o c m o -> FinFunctor c m o
    diagramToFinFunctor :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
Diagram c m o c m o -> FinFunctor c m o
diagramToFinFunctor Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c
t,omap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap=AssociationList o o
om,mmap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap=AssociationList m m
fm} = FinFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> FinFunctor c m o
FinFunctor{srcF :: c
srcF=c
s,tgtF :: c
tgtF=c
t,omapF :: AssociationList o o
omapF=AssociationList o o
om,mmapF :: AssociationList m m
mmapF=AssociationList m m
fm}
    
    -- | Converts a homogeneous `Diagram` to a `PartialFunctor`

    diagramToPartialFunctor :: (FiniteCategory c m o, Morphism m o) => Diagram c m o c m o -> PartialFunctor c m o
    diagramToPartialFunctor :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
Diagram c m o c m o -> PartialFunctor c m o
diagramToPartialFunctor Diagram{src :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c1
src=c
s,tgt :: forall c1 m1 o1 c2 m2 o2. Diagram c1 m1 o1 c2 m2 o2 -> c2
tgt=c
t,omap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList o1 o2
omap=AssociationList o o
om,mmap :: forall c1 m1 o1 c2 m2 o2.
Diagram c1 m1 o1 c2 m2 o2 -> AssociationList m1 m2
mmap=AssociationList m m
fm} = PartialFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> PartialFunctor c m o
PartialFunctor{srcPF :: c
srcPF=c
s,tgtPF :: c
tgtPF=c
t,omapPF :: AssociationList o o
omapPF=AssociationList o o
om,mmapPF :: AssociationList m m
mmapPF=AssociationList m m
fm}
    
    -- | Converts a `FinFunctor` into a `Diagram`.

    --

    -- A `FinFunctor` is a morphism of the `FinCat` category, it is a homogeneous FinFunctor. This functions casts it to a heterogeneous FinFunctor (i.e. a `Diagram`).

    finFunctorToDiagram :: FinFunctor c m o -> Diagram c m o c m o
    finFunctorToDiagram :: forall c m o. FinFunctor c m o -> Diagram c m o c m o
finFunctorToDiagram FinFunctor{srcF :: forall c m o. FinFunctor c m o -> c
srcF=c
s,tgtF :: forall c m o. FinFunctor c m o -> c
tgtF=c
t,omapF :: forall c m o. FinFunctor c m o -> AssociationList o o
omapF=AssociationList o o
om,mmapF :: forall c m o. FinFunctor c m o -> AssociationList m m
mmapF=AssociationList m m
fm} = Diagram :: forall c1 m1 o1 c2 m2 o2.
c1
-> c2
-> AssociationList o1 o2
-> AssociationList m1 m2
-> Diagram c1 m1 o1 c2 m2 o2
Diagram {src :: c
src=c
s,tgt :: c
tgt=c
t,omap :: AssociationList o o
omap=AssociationList o o
om,mmap :: AssociationList m m
mmap=AssociationList m m
fm}
    
    -- | Converts a total functor to a partial functor.

    finFunctorToPartialFunctor :: (FiniteCategory c m o, Morphism m o) => (FinFunctor c m o) -> (PartialFunctor c m o)
    finFunctorToPartialFunctor :: forall c m o.
(FiniteCategory c m o, Morphism m o) =>
FinFunctor c m o -> PartialFunctor c m o
finFunctorToPartialFunctor FinFunctor{srcF :: forall c m o. FinFunctor c m o -> c
srcF=c
s,tgtF :: forall c m o. FinFunctor c m o -> c
tgtF=c
t,omapF :: forall c m o. FinFunctor c m o -> AssociationList o o
omapF=AssociationList o o
om,mmapF :: forall c m o. FinFunctor c m o -> AssociationList m m
mmapF=AssociationList m m
fm} = PartialFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> PartialFunctor c m o
PartialFunctor{srcPF :: c
srcPF=c
s,tgtPF :: c
tgtPF=c
t,omapPF :: AssociationList o o
omapPF=AssociationList o o
om,mmapPF :: AssociationList m m
mmapPF=AssociationList m m
fm}
    
    -- | Try to convert a `PartialFunctor` into a `Diagram` if it can (if it is total).

    partialFunctorToDiagram :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o, Show o, Show m) => PartialFunctor c m o -> Maybe (Diagram c m o c m o)
    partialFunctorToDiagram :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o, Show o, Show m) =>
PartialFunctor c m o -> Maybe (Diagram c m o c m o)
partialFunctorToDiagram PartialFunctor c m o
x = FinFunctor c m o -> Diagram c m o c m o
forall c m o. FinFunctor c m o -> Diagram c m o c m o
finFunctorToDiagram (FinFunctor c m o -> Diagram c m o c m o)
-> Maybe (FinFunctor c m o) -> Maybe (Diagram c m o c m o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PartialFunctor c m o -> Maybe (FinFunctor c m o)
forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o, Show o, Show m) =>
PartialFunctor c m o -> Maybe (FinFunctor c m o)
partialFunctorToFinFunctor PartialFunctor c m o
x
    
    -- | Try to convert a partial functor to a total functor if it is possible.

    partialFunctorToFinFunctor :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o, Show o, Show m) => (PartialFunctor c m o) -> Maybe (FinFunctor c m o)
    partialFunctorToFinFunctor :: forall c m o.
(FiniteCategory c m o, Morphism m o, Eq m, Eq o, Show o, Show m) =>
PartialFunctor c m o -> Maybe (FinFunctor c m o)
partialFunctorToFinFunctor PartialFunctor{srcPF :: forall c m o. PartialFunctor c m o -> c
srcPF=c
s,tgtPF :: forall c m o. PartialFunctor c m o -> c
tgtPF=c
t,omapPF :: forall c m o. PartialFunctor c m o -> AssociationList o o
omapPF=AssociationList o o
om,mmapPF :: forall c m o. PartialFunctor c m o -> AssociationList m m
mmapPF=AssociationList m m
fm}
        | Bool -> Bool
not ((AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om) [o] -> [o] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`doubleInclusion` (c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
s)) = [Char] -> Maybe (FinFunctor c m o)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe (FinFunctor c m o))
-> [Char] -> Maybe (FinFunctor c m o)
forall a b. (a -> b) -> a -> b
$ ([o] -> [Char]
forall a. Show a => a -> [Char]
show ([o] -> [Char]) -> [o] -> [Char]
forall a b. (a -> b) -> a -> b
$ c -> [o]
forall c m o. FiniteCategory c m o => c -> [o]
ob c
s) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
"," [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([o] -> [Char]
forall a. Show a => a -> [Char]
show ([o] -> [Char]) -> [o] -> [Char]
forall a b. (a -> b) -> a -> b
$ AssociationList o o -> [o]
forall a b. AssociationList a b -> [a]
keys AssociationList o o
om)--Nothing

        | Bool -> Bool
not ((AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm) [m] -> [m] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`doubleInclusion` (c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
s)) = [Char] -> Maybe (FinFunctor c m o)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe (FinFunctor c m o))
-> [Char] -> Maybe (FinFunctor c m o)
forall a b. (a -> b) -> a -> b
$ ([m] -> [Char]
forall a. Show a => a -> [Char]
show ([m] -> [Char]) -> [m] -> [Char]
forall a b. (a -> b) -> a -> b
$ c -> [m]
forall c m o.
(FiniteCategory c m o, FiniteCategory c m o, Morphism m o) =>
c -> [m]
arrows c
s) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
"," [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([m] -> [Char]
forall a. Show a => a -> [Char]
show ([m] -> [Char]) -> [m] -> [Char]
forall a b. (a -> b) -> a -> b
$ AssociationList m m -> [m]
forall a b. AssociationList a b -> [a]
keys AssociationList m m
fm)--Nothing

        | Bool
otherwise = FinFunctor c m o -> Maybe (FinFunctor c m o)
forall a. a -> Maybe a
Just FinFunctor :: forall c m o.
c
-> c
-> AssociationList o o
-> AssociationList m m
-> FinFunctor c m o
FinFunctor{srcF :: c
srcF=c
s,tgtF :: c
tgtF=c
t,omapF :: AssociationList o o
omapF=AssociationList o o
om,mmapF :: AssociationList m m
mmapF=AssociationList m m
fm}