module Fuzzy.Sets.Properties (
    -- * Standard predicates 

    isEmpty,
    isSingleton,
    isCrisp,
    isUniversal,
    strictSubsethood,
    strictEquality,
    -- * Graded predicates

    gradedSubsethood,
    gradedEquality,
) where

import FuzzySet
import Fuzzy.Sets.LSet
import Lattices.ResiduatedLattice 
import FuzzySet

{- | True if 'fuzzySet' is empty, meaning for each `u` in 'universe', 
'member' u == 'bot'.

==== __Examples__

>>> let emptySet = mkEmptySet :: LSet Int UILukasiewicz
>>> isEmpty emptySet
True

>>> let nonEmptySet = fromPairs [(1, 0.2), (2, 0.0)] :: LSet Int UILukasiewicz
>>> isEmpty nonEmptySet
False
-}
isEmpty :: (FuzzySet set a l) => set -> Bool
isEmpty :: forall set a l. FuzzySet set a l => set -> Bool
isEmpty set
set = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== forall l. BoundedLattice l => l
bot) (forall set a l. FuzzySet set a l => set -> [l]
truthDegrees set
set)


{- | 'fuzzySet' is a singleton if and only if there is exactly 
one `u` in 'universe' for which 'member' u is greater than 'bot'.

==== __Examples__

>>> let singletonSet = mkSingletonSet [1, 2, 3] (2, 0.8) :: LSet Int UILukasiewicz
>>> isSingleton singletonSet
True

>>> let nonSingletonSet = fromPairs [(1, 0.2), (2, 0.7)] :: LSet Int UILukasiewicz
>>> isSingleton nonSingletonSet
False
-}
isSingleton :: (FuzzySet set a l) => set -> Bool
isSingleton :: forall set a l. FuzzySet set a l => set -> Bool
isSingleton set
set = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
> forall l. BoundedLattice l => l
bot) (forall set a l. FuzzySet set a l => set -> [l]
truthDegrees set
set)) forall a. Eq a => a -> a -> Bool
== Int
1


{- | Check if fuzzy set is a crisp set (Truth value structure contains only two values: 0 and 1).

==== __Examples__

>>> let crispSet = fromPairs [(1, 1.0), (2, 0.0)] :: LSet Int UILukasiewicz
>>> isCrisp crispSet
True

>>> let nonCrispSet = fromPairs [(1, 0.5), (2, 0.7)] :: LSet Int UILukasiewicz
>>> isCrisp nonCrispSet
False
-}
isCrisp :: (FuzzySet set a l) => set -> Bool
isCrisp :: forall set a l. FuzzySet set a l => set -> Bool
isCrisp set
set = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\l
x -> l
x forall a. Eq a => a -> a -> Bool
== forall l. BoundedLattice l => l
top Bool -> Bool -> Bool
|| l
x forall a. Eq a => a -> a -> Bool
== forall l. BoundedLattice l => l
bot) [a -> l
f a
x | a
x <- [a]
u]
    where
        f :: a -> l
f = forall set a l. FuzzySet set a l => set -> a -> l
member set
set
        u :: [a]
u = forall set a l. FuzzySet set a l => set -> [a]
universe set
set

{- | Fuzzy set is universal if it returns 'top' for every value in its universe. 
This means that the fuzzy set equals its universe.

==== __Examples__

>>> let universalSet = mkUniversalSet [1, 2, 3] :: LSet Int UILukasiewicz
>>> isUniversal universalSet
True

>>> let nonUniversalSet = fromPairs [(1, 1.0), (2, 0.8)] :: LSet Int UILukasiewicz
>>> isUniversal nonUniversalSet
False
-} 
isUniversal :: (FuzzySet set a l) => set -> Bool
isUniversal :: forall set a l. FuzzySet set a l => set -> Bool
isUniversal set
set = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== forall l. BoundedLattice l => l
top) [a -> l
f a
x | a
x <- [a]
u]
    where 
        u :: [a]
u = forall set a l. FuzzySet set a l => set -> [a]
universe set
set
        f :: a -> l
f = forall set a l. FuzzySet set a l => set -> a -> l
member set
set


-- | Highest possible membership of a functions. 

-- It is always bound by the 'top' of the defining lattice.

height :: (FuzzySet set a l) => set -> l
height :: forall set a l. FuzzySet set a l => set -> l
height set
_ = forall l. BoundedLattice l => l
top


{- | Support is a list of all elements with non 'bot' 'member' 

>>> let set = fromPairs [(1, 0), (2, 0.8), (3, 0), (4, 0.5), (6, 0)]
[2, 4] 
-}
support :: (FuzzySet set a l) => set -> [a]
support :: forall set a l. FuzzySet set a l => set -> [a]
support set
set = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/=forall l. BoundedLattice l => l
bot) forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> l
f) [a]
u
    where f :: a -> l
f = forall set a l. FuzzySet set a l => set -> a -> l
member set
set
          u :: [a]
u = forall set a l. FuzzySet set a l => set -> [a]
universe set
set 


{- | Core of a fuzzy set is 'alphaCut' where alpha = 'top'. 
In other words it's a list of items with 'member' equal to 'top'

==== __Examples__

>>> let set = fromPairs [(1, 1:0), (2, 0.8), (3, 1.0), (4, 0.5), (6, 1.0)]
>>> core set
[1, 3, 6]

>>> alphaCut 1.0 set == core set
True
-}
core :: (FuzzySet set a l) => set -> [a]
core :: forall set a l. FuzzySet set a l => set -> [a]
core = forall set a l. FuzzySet set a l => l -> set -> [a]
alphaCut forall l. BoundedLattice l => l
top

{- | Is 'FuzzySet' A a strict subset of 'FuzzySet' B?
Membership of values from A is smaller than B for every item of universe

==== __Examples__

>>> let setA = fromPairs [(1, 0.2), (2, 0.5)] :: LSet Int UILukasiewicz
>>> let setB = fromPairs [(1, 0.3), (2, 0.7)] :: LSet Int UILukasiewicz
>>> strictSubsethood setA setB
True

>>> strictSubsethood setB setA
False
-}
strictSubsethood :: (FuzzySet set a l) => set -> set -> Bool
strictSubsethood :: forall set a l. FuzzySet set a l => set -> set -> Bool
strictSubsethood set
set1 set
set2 = forall l. BoundedLattice l => l
top forall a. Eq a => a -> a -> Bool
== forall set a l. FuzzySet set a l => set -> set -> l
gradedSubsethood set
set1 set
set2


{- | Is 'FuzzySet' A strictly equal to 'FuzzySet' B? 
Member of all values from universe in set A is equal to member of all values in set B.

==== __Examples__

>>> let setA = fromPairs [(1, 0.2), (2, 0.5)] :: LSet Int UILukasiewicz
>>> let setB = fromPairs [(1, 0.2), (2, 0.5)] :: LSet Int UILukasiewicz
>>> strictEquality setA setB
True

>>> let setC = fromPairs [(1, 0.3), (2, 0.5)] :: LSet Int UILukasiewicz
>>> strictEquality setA setC
False
-}
strictEquality :: (FuzzySet set a l) => set -> set -> Bool
strictEquality :: forall set a l. FuzzySet set a l => set -> set -> Bool
strictEquality set
set1 set
set2 = forall l. BoundedLattice l => l
top forall a. Eq a => a -> a -> Bool
== forall set a l. FuzzySet set a l => set -> set -> l
gradedEquality set
set1 set
set2 


{- | Degree to which set A is a subset of B.
If the result is 1, we can conclude that A ⊆ B.

==== __Examples__

>>> let setA = fromPairs [(1, 0.2), (2, 0.5)] :: LSet Int UILukasiewicz
>>> let setB = fromPairs [(1, 0.3), (2, 0.7)] :: LSet Int UILukasiewicz
>>> gradedSubsethood setA setB
1.0

>>> gradedSubsethood setB setA
0.8
-}
gradedSubsethood :: (FuzzySet set a l) => set -> set -> l
gradedSubsethood :: forall set a l. FuzzySet set a l => set -> set -> l
gradedSubsethood set
set1 set
set2 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall l. BoundedLattice l => l -> l -> l
(/\) forall l. BoundedLattice l => l
top forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall l. ResiduatedLattice l => l -> l -> l
(-->) (forall a b. (a -> b) -> [a] -> [b]
map a -> l
f [a]
u) (forall a b. (a -> b) -> [a] -> [b]
map a -> l
g [a]
u)
        where 
            f :: a -> l
f = forall set a l. FuzzySet set a l => set -> a -> l
member set
set1
            g :: a -> l
g = forall set a l. FuzzySet set a l => set -> a -> l
member set
set2
            u :: [a]
u = forall set a l. FuzzySet set a l => set -> [a]
universe set
set1


{- | Degree to which set A is equal to set B.
If the result is 1, the fuzzy sets are equal.

==== __Examples__

>>> let setA = fromPairs [(1, 0.2), (2, 0.5)] :: LSet Int UILukasiewicz
>>> let setB = fromPairs [(1, 0.2), (2, 0.5)] :: LSet Int UILukasiewicz
>>> gradedEquality setA setB
1.0

>>> let setC = fromPairs [(1, 0.3), (2, 0.5)] :: LSet Int UILukasiewicz
>>> gradedEquality setA setC
0.9
-}
gradedEquality :: (FuzzySet set a l) => set -> set -> l
gradedEquality :: forall set a l. FuzzySet set a l => set -> set -> l
gradedEquality set
set1 set
set2 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall l. BoundedLattice l => l -> l -> l
(/\) forall l. BoundedLattice l => l
top forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall l. ResiduatedLattice l => l -> l -> l
(<-->) (forall a b. (a -> b) -> [a] -> [b]
map a -> l
f [a]
u) (forall a b. (a -> b) -> [a] -> [b]
map a -> l
g [a]
u)
        where 
            f :: a -> l
f = forall set a l. FuzzySet set a l => set -> a -> l
member set
set1
            g :: a -> l
g = forall set a l. FuzzySet set a l => set -> a -> l
member set
set2
            u :: [a]
u = forall set a l. FuzzySet set a l => set -> [a]
universe set
set1


{- $Standard predicates
Predicate functions that take a fuzzy set and return true if fuzzy set has some property (crisp, empty...)
-}

{- $Graded Predicates determining if two Fuzzy sets are equal can be... well, fuzzy. 
in this section we introduce predicates that return graded values from 'ResiduatedLattice'
-}