{-# LANGUAGE MultiParamTypeClasses  #-}

{-| Module  : FiniteCategories
Description : Check the 'FiniteCategory' structure.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Provide a function to test the structure of a 'FiniteCategory'.
-}

module Math.FiniteCategoryError
(
    -- * Check structure
    FiniteCategoryError,
    checkFiniteCategory
)
where
    import              Data.WeakSet               (Set)
    import qualified    Data.WeakSet           as  Set
    import              Data.WeakSet.Safe
    
    import              Math.FiniteCategory

    -- | A data type to represent an incoherence inside a finite category.
    data FiniteCategoryError m o =
         CompositionNotAssociative {f :: m, g :: m, h :: m, fg_h :: m, f_gh :: m} -- ^ @(h\@g)\@f /= h\@(g\@f)@
       | WrongSource {f :: m, realSource :: o} -- ^ `f` was found by using @'ar' c s t@ where @s /= 'source' f@.
       | WrongTarget {f :: m, realTarget :: o} -- ^ `f` was found by using @'ar' c s t@ where @t /= 'target' f@.
       | IdentityNotLeftNeutral {idL :: m, f :: m, foidL :: m} -- ^ `idL` is not a valid identity : @f \@ idL /= f@.
       | IdentityNotRightNeutral {f :: m, idR :: m, idRof :: m} -- ^ `idR` is not a valid identity : @idR \@ f /= f@.
       | MorphismsShouldNotBeEqual {f :: m, g :: m} -- ^ @f == g@ even though they don'y share the same source or target.
       | NotTransitive {f :: m, g :: m} -- ^ @f\@g@ is not an element of @ar c (source g) (target g)@.
       | GeneratorIsNotAMorphism {f :: m} -- ^ `f` is a generator but not a morphism.
       | MorphismDoesntDecomposesIntoGenerators {f :: m, decomp :: [m], notGen :: m} -- ^ The morphism `f` decomposes into `decomp` where `notGen` is a non generating morphism.
       | WrongDecomposition {f :: m, decomp :: [m], comp :: m} -- ^ @compose (decompose c f) /= f@.
       deriving (Eq, Show)

    -- | Checks the category axioms for a 'FiniteCategory'.
    --
    -- If an error is found in the category, 'Just' a `FiniteCategoryError` is returned.
    -- Otherwise, 'Nothing' is returned.
    checkFiniteCategory :: (FiniteCategory c m o, Morphism m o, Eq m, Eq o) => c -> Maybe (FiniteCategoryError m o)
    checkFiniteCategory c
        | (not.null) incoherentEq = Just MorphismsShouldNotBeEqual {f=(fst.head) incoherentEq, g=(snd.head) incoherentEq}
        | (not.null) wrongSource = Just WrongSource {f = (fst.head) wrongSource, realSource = (snd.head) wrongSource}
        | (not.null) wrongTarget = Just WrongTarget {f = (fst.head) wrongTarget, realTarget = (snd.head) wrongTarget}
        | (not.null) idNotLNeutral = Just IdentityNotLeftNeutral {idL=(fst3.head) idNotLNeutral, f=(snd3.head) idNotLNeutral,foidL=(trd3.head) idNotLNeutral} 
        | (not.null) idNotRNeutral = Just IdentityNotRightNeutral {f=(fst3.head) idNotRNeutral, idR=(snd3.head) idNotRNeutral,idRof=(trd3.head) idNotRNeutral} 
        | (not.null) notAssociative = Just CompositionNotAssociative {f=(fst3.head) notAssociative,g=(snd3.head) notAssociative,h=(trd3.head) notAssociative, fg_h=(((fst3.head)notAssociative) @ ((snd3.head)notAssociative)) @ ((trd3.head)notAssociative),
                        f_gh=((fst3.head)notAssociative) @ (((snd3.head)notAssociative) @ ((trd3.head)notAssociative))}
        | (not.null) notTransitive = Just NotTransitive {f=(fst.head) notTransitive, g=(snd.head) notTransitive}
        | (not.(Set.null)) genNotMorph = Just GeneratorIsNotAMorphism {f=head.setToList $ genNotMorph}
        | (not.null) decompIntoComposite = Just MorphismDoesntDecomposesIntoGenerators {f=(fst3.head) decompIntoComposite, decomp=(snd3.head) decompIntoComposite, notGen=(trd3.head) decompIntoComposite}
        | (not.null) wrongDecomp = Just WrongDecomposition {f=(fst3.head) wrongDecomp, decomp=(snd3.head) wrongDecomp, comp=(trd3.head) wrongDecomp}
        | otherwise = Nothing
        where
            incoherentEq = setToList $ Set.filter (\(f,g) -> f == g && (source f /= source g || target f /= target g)) (arrows c |*| arrows c)
            wrongSource = [(f,s) | s <- setToList $ ob c, t <- setToList $ ob c, f <- setToList $ ar c s t, source f /= s]
            wrongTarget = [(f,t) | s <- setToList $ ob c, t <- setToList $ ob c, f <- setToList $ ar c s t, target f /= t]
            idNotLNeutral = [(identity c (source f),f,f @ identity c (source f)) | f <- setToList $ arrows c, f @ identity c (source f) /= f]
            idNotRNeutral = [(f,identity c (target f), identity c (target f) @ f) | f <- setToList $ arrows c, identity c (target f) @ f /= f]
            notAssociative = [(x,y,z) | z <- setToList $ arrows c, y <- setToList $ arFrom c (target z), x <- setToList $ arFrom c (target y), (x @ y) @ z /= x @ (y @ z)]
            notTransitive = [(f,g) | g <- setToList $ arrows c, f <- setToList $ arFrom c (target g), not ((f @ g) `isIn` (ar c (source g) (target f)))]
            genNotMorph = genArrows c |-| arrows c
            decompIntoComposite = [(m,decompose c m,f) | m <- setToList $ arrows c, f <- decompose c m, not (f `isIn` (genAr c (source f) (target f)))]
            wrongDecomp = [(f,decompose c f, compose (decompose c f)) | f <- setToList $ arrows c, compose (decompose c f) /= f]
            fst3 (x,_,_) = x
            snd3 (_,x,_) = x
            trd3 (_,_,x) = x