{-| Module  : WeakSets
Description : Pure sets are nested sets which only contain other sets all the way down. They allow to explore basic set theory.
Copyright   : Guillaume Sabbagh 2022
License     : GPL-3
Maintainer  : guillaumesabbagh@protonmail.com
Stability   : experimental
Portability : portable

Pure sets are nested sets which only contain other sets all the way down. They allow to explore basic set theory.

Every mathematical object is a set, usual constructions such as Von Neumann numbers and Kuratowski pairs are implemented.

It is a tree where the order of the branches does not matter.

Functions with the same name as pure set functions are suffixed with the letter 'P' for pure to avoid name collision.
-}

module Math.PureSet 
(
    -- * `PureSet` datatype
    PureSet(..),
    pureSet,
    -- * Mathematical constructions using sets
    emptySet,
    singleton,
    pair,
    cartesianProduct,
    numberToSet,
    (||||),
    (&&&&),
    isInP,
    isIncludedInP,
    card,
    powerSetP,
    -- * Formatting functions
    prettify,
    formatPureSet,
)
where
    import Data.WeakSet (Set)
    import Data.WeakSet.Safe
    import qualified Data.WeakSet as S
    import Data.List    (intersect, nub, intercalate, subsequences)
    import Data.Maybe   (fromJust, catMaybes)
    
    -- | A `PureSet` is a `Set` of other pure sets.
    data PureSet = PureSet (Set PureSet) deriving (Eq)
    
    instance Show PureSet where
        show (PureSet xs) = "(pureSet "++ show (setToList xs) ++")"
    
    -- | Construct a `PureSet` from a list of pure sets.
    pureSet :: [PureSet] -> PureSet
    pureSet = (PureSet).set
    
    -- | Peel a `PureSet` into a `Set`.
    pureSetToSet :: PureSet -> Set PureSet
    pureSetToSet (PureSet xs) = xs
    
    -- | Construct the empty set.
    emptySet :: PureSet
    emptySet = pureSet []
  
    -- | Construct the singleton containing a given set.
    singleton :: PureSet -> PureSet
    singleton x = pureSet $ [x]
    
    -- | Construct an ordered pair from two sets according to Kuratowski's definition of a tuple.
    pair :: PureSet -> PureSet -> PureSet
    pair x y = PureSet $ set [singleton x, pureSet $ [x,y]]
    
    -- | Construct the cartesian product of two sets.
    cartesianProduct :: PureSet -> PureSet -> PureSet
    cartesianProduct (PureSet xs) (PureSet ys) = pureSet $ [pair x y | x <- setToList xs, y <- setToList ys]
    
    -- | Union of two pure sets.
    (||||) :: PureSet -> PureSet -> PureSet
    (||||) (PureSet xs) (PureSet ys) = PureSet $ xs ||| ys
    
    -- | Intersection of two pure sets.
    (&&&&) :: PureSet -> PureSet -> PureSet
    (&&&&) (PureSet xs) (PureSet ys) = PureSet $ xs |&| ys
    
    -- | Difference of two pure sets.
    (\\\\) :: PureSet -> PureSet -> PureSet
    (\\\\) (PureSet xs) (PureSet ys) = PureSet $ xs |-| ys
   
    -- | Transform a number into its Von Neumann construction
    numberToSet :: (Num a, Eq a) => a -> PureSet
    numberToSet 0 = emptySet
    numberToSet n = (numberToSet (n-1)) |||| (singleton (numberToSet (n-1)))
    
    -- | Return wether a pure set is in another one.
    isInP :: PureSet -> PureSet -> Bool
    isInP x (PureSet xs) = x `isIn` xs
    
    -- | Return wether a pure set is included in another one.
    isIncludedInP :: PureSet -> PureSet -> Bool
    isIncludedInP (PureSet xs) (PureSet ys) = xs `isIncludedIn` ys
    
    -- | Return the size of a pure set.
    card :: PureSet -> Int
    card (PureSet xs) = cardinal xs
    
    -- | Return the set of subsets of a given set.
    powerSetP :: PureSet -> PureSet
    powerSetP (PureSet xs) = PureSet $ PureSet <$> S.powerSet xs
    
    -- | Prettify a pure set according to usual mathematical notation.
    prettify :: PureSet -> String
    prettify (PureSet xs)
        | cardinal xs == 0 = "{}"
        | otherwise = "{" ++ (intercalate ", " $ prettify <$> setToList xs) ++ "}"
        
    -- | Format pure sets such that if numbers are recognized, they are transformed into integer and if pairs are recognized, they are transformed into pairs.
    formatPureSet :: PureSet -> String
    formatPureSet x
        | (not.null) $ toNumber x = show.fromJust $ toNumber x
        | (not.null) $ toPair x = fromJust.toPair $ x
        | otherwise = "{"++intercalate "," (formatPureSet <$> (setToList.pureSetToSet $ x))++"}"
            where
                toNumber s@(PureSet xs)
                    | s == emptySet = Just 0
                    | otherwise =   let
                                        numbers = setToList $ toNumber <$> xs
                                        anyMissing = null $ foldr1 (>>) numbers
                                        maxNb = maximum $ catMaybes numbers
                                    in 
                                        if (not anyMissing) && (set (Just <$> [0..maxNb])) == (set numbers) then Just (maxNb + 1) else Nothing
                toPair (PureSet xs)
                    | cardinal xs == 2 = 
                        case () of
                         () | ((card $ (setToList xs) !! 0) == 1 && (card $ (setToList xs) !! 1) == 2) && ((setToList xs) !! 0) `isInP` ((setToList xs) !! 1) -> Just $ "(" ++ (formatPureSet.head.setToList.pureSetToSet $ ((setToList xs) !! 0)) ++ "," ++ (formatPureSet.head.setToList.pureSetToSet $ (((setToList xs) !! 1) \\\\ ((setToList xs) !! 0))) ++ ")"
                            | ((card $ (setToList xs) !! 1) == 1 && (card $ (setToList xs) !! 0) == 2) && ((setToList xs) !! 1) `isInP` ((setToList xs) !! 0) -> Just $ "(" ++ (formatPureSet.head.setToList.pureSetToSet $ ((setToList xs) !! 1)) ++ "," ++ (formatPureSet.head.setToList.pureSetToSet $ (((setToList xs) !! 0) \\\\ ((setToList xs) !! 1))) ++ ")"
                            | otherwise -> Nothing
                    | otherwise = Nothing