module Pandora.Paradigm.Structure.Interface.Set where

import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Object.Setoid (Setoid ((!=)))
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Pattern.Object.Quasiring (one)
import Pandora.Paradigm.Primary.Functor.Function ((!), (!!), (%))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (equate)
import Pandora.Paradigm.Primary.Functor.Product (attached)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Zero))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce), find)
import Pandora.Paradigm.Inventory.State (State, modify)
import Pandora.Paradigm.Controlflow.Effect (run)

member :: forall e a . (Setoid a, Monotonic a e) => a -> e -> Boolean
member :: a -> e -> Boolean
member a
x = (a -> Boolean -> Boolean) -> Boolean -> Maybe a -> Boolean
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce @a @(Maybe a) (Boolean
True Boolean -> a -> Boolean -> Boolean
forall a b c. a -> b -> c -> a
!!) Boolean
False (Maybe a -> Boolean) -> (e -> Maybe a) -> e -> Boolean
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Predicate a -> e -> Maybe a
forall a e (t :: * -> *).
(Monotonic a e, Pointable t, Avoidable t) =>
Predicate a -> e -> t a
find (a :=> Predicate
forall a. Setoid a => a :=> Predicate
equate a
x)

subset :: (Monotonic a (t a), Traversable t, Setoid a, Setoid (t a)) => t a -> t a -> Boolean
subset :: t a -> t a -> Boolean
subset t a
ss t a
s = Maybe (t a)
forall a. Maybe a
Nothing Maybe (t a) -> Maybe (t a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
!= t a
ss t a -> (a -> Maybe a) -> Maybe (t a)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> Predicate a -> t a -> Maybe a
forall a e (t :: * -> *).
(Monotonic a e, Pointable t, Avoidable t) =>
Predicate a -> e -> t a
find (Predicate a -> t a -> Maybe a) -> t a -> Predicate a -> Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
s (Predicate a -> Maybe a) -> (a -> Predicate a) -> a -> Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Predicate a
forall a. Setoid a => a :=> Predicate
equate

cardinality :: Traversable t => t a -> Numerator
cardinality :: t a -> Numerator
cardinality t a
s = (Numerator :*: t Numerator) -> Numerator
forall a b. (a :*: b) -> a
attached ((Numerator :*: t Numerator) -> Numerator)
-> (State Numerator (t Numerator) -> Numerator :*: t Numerator)
-> State Numerator (t Numerator)
-> Numerator
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State Numerator) =>
State Numerator a -> Primary (State Numerator) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _) (State Numerator (t Numerator)
 -> ((->) Numerator :. (:*:) Numerator) := t Numerator)
-> Numerator
-> State Numerator (t Numerator)
-> Numerator :*: t Numerator
forall a b c. (a -> b -> c) -> b -> a -> c
% Numerator
Zero (State Numerator (t Numerator) -> Numerator)
-> State Numerator (t Numerator) -> Numerator
forall (m :: * -> * -> *). Category m => m ~~> m
$ t a
s t a
-> (a -> State Numerator Numerator)
-> State Numerator (t Numerator)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> ((Numerator -> Numerator) -> State Numerator Numerator
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify @Numerator (Numerator -> Numerator -> Numerator
forall a. Semigroup a => a -> a -> a
+ Numerator
forall a. Quasiring a => a
one) State Numerator Numerator -> a -> State Numerator Numerator
forall a b. a -> b -> a
!)