{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE MultiParamTypeClasses #-}

{-| Module  : FiniteCategories
Description : An 'OrdinalCategory' is a 'TotalOrder' category where the total order is an order induced by ordinal numbers. 
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

An 'OrdinalCategory' is a 'TotalOrder' category where the total order is an order induced by ordinal numbers. 

Concretely the type parameter must implement the Enum typeclass.

For example, the 'TotalOrder' category induced by (R,<=) is not an 'OrdinalCategory' whereas (N,<=) is.

It induces a non trivial generating set of arrows thanks to the 'succ' function.
-}

module Math.Categories.OrdinalCategory
(
    OrdinalCategory(..),
    module Math.Categories.TotalOrder
    
)
where
    import              Math.Category
    import              Math.FiniteCategory
    import              Math.CompleteCategory
    import              Math.CocompleteCategory
    import              Math.Categories.FunctorCategory
    import              Math.Categories.ConeCategory
    import              Math.Categories.TotalOrder
    import              Math.FiniteCategories.Parallel
    import              Math.IO.PrettyPrint
    
    import qualified    Data.WeakSet          as Set
    import              Data.WeakSet.Safe
    import qualified    Data.WeakMap          as Map
    import              Data.WeakMap.Safe
    import              Data.Simplifiable
    
    import              GHC.Generics
    
    -- | An 'OrdinalCategory' is a 'TotalOrder' where the type /a/ follows the Enum typeclass.
    newtype OrdinalCategory a = OrdinalCategory (TotalOrder a) deriving (Eq, Show, Generic, PrettyPrint, Simplifiable)
    
    instance (Enum a, Ord a) => Category (OrdinalCategory a) (IsSmallerThan a) a where
        ar _ x y
            | x <= y = set [IsSmallerThan x y]
            | otherwise = set []
            
        identity _ x = IsSmallerThan x x
        
        -- | An 'OrdinalCategory' is generated by morphisms from a number to its successor.
        genAr _ x y
            | x == y = set [IsSmallerThan x x]
            | (succ x) == y = set [IsSmallerThan x y]
            | otherwise = set []
  
        decompose _ (IsSmallerThan x y)
            | x == y = [IsSmallerThan x y]
            | otherwise = reverse $ (\n -> IsSmallerThan n (succ n)) <$> [x..(pred y)]
    
    instance (Enum a, Ord a, Eq oIndex) => HasProducts (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a oIndex where
        product diag = unsafeCone apexProduct nat
            where
                apexProduct = Set.minimum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation (constantDiagram (src diag) (OrdinalCategory TotalOrder) apexProduct) diag $ Map.weakMapFromSet [(i,IsSmallerThan apexProduct (diag ->$ i)) | i <- ob $ src diag]
                
    instance (Enum a, Ord a) => HasEqualizers (OrdinalCategory a) (IsSmallerThan a) a where
        equalize parallelDiag = unsafeCone apexEq nat
            where
                apexEq = parallelDiag ->$ ParallelA
                nat = unsafeNaturalTransformation (constantDiagram Parallel (OrdinalCategory TotalOrder) apexEq) parallelDiag (weakMap [(ParallelA, IsSmallerThan apexEq apexEq),(ParallelB, IsSmallerThan (parallelDiag ->$ ParallelB) (parallelDiag ->$ ParallelB))])
                
    instance (Enum a, Ord a, Eq mIndex, Eq oIndex) => CompleteCategory (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a cIndex mIndex oIndex where
        limit diag = unsafeCone apexLimit nat
            where
                apexLimit = Set.minimum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation (constantDiagram (src diag) (OrdinalCategory TotalOrder) apexLimit) diag $ Map.weakMapFromSet [(i,IsSmallerThan apexLimit (diag ->$ i)) | i <- ob $ src diag]
                
        projectBase diag = Diagram{src = tgt diag, tgt = tgt diag, omap = memorizeFunction id (Map.values (omap diag)), mmap = memorizeFunction id (Map.values (mmap diag))}
                
    instance (Enum a, Ord a, Eq oIndex) => HasCoproducts (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a oIndex where
        coproduct diag = unsafeCocone nadirCoproduct nat
            where
                nadirCoproduct = Set.maximum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation diag (constantDiagram (src diag) (OrdinalCategory TotalOrder) nadirCoproduct) $ Map.weakMapFromSet [(i,IsSmallerThan (diag ->$ i) nadirCoproduct) | i <- ob $ src diag]
                
    instance (Enum a, Ord a) => HasCoequalizers (OrdinalCategory a) (IsSmallerThan a) a where
        coequalize parallelDiag = unsafeCocone nadirCoeq nat
            where
                nadirCoeq = parallelDiag ->$ ParallelB
                nat = unsafeNaturalTransformation parallelDiag (constantDiagram Parallel (OrdinalCategory TotalOrder) nadirCoeq) (weakMap [(ParallelA, IsSmallerThan (parallelDiag ->$ ParallelA) (parallelDiag ->$ ParallelA)),(ParallelB, IsSmallerThan nadirCoeq nadirCoeq)])
                
    instance (Enum a, Ord a, Eq mIndex, Eq oIndex) => CocompleteCategory (OrdinalCategory a) (IsSmallerThan a) a (OrdinalCategory a) (IsSmallerThan a) a cIndex mIndex oIndex where
        colimit diag = unsafeCocone nadirColimit nat
            where
                nadirColimit = Set.maximum $ Map.values $ omap diag
                nat = unsafeNaturalTransformation diag (constantDiagram (src diag) (OrdinalCategory TotalOrder) nadirColimit) $ Map.weakMapFromSet [(i,IsSmallerThan (diag ->$ i) nadirColimit) | i <- ob $ src diag]
                
        coprojectBase diag = Diagram{src = tgt diag, tgt = tgt diag, omap = memorizeFunction id (Map.values (omap diag)), mmap = memorizeFunction id (Map.values (mmap diag))}