module Pandora.Paradigm.Structure.Interface.Set where

import Pandora.Core.Morphism ((!), (%))
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.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.Natural (Natural (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 e a) => a -> e -> Boolean
member :: a -> e -> Boolean
member a
x = (a -> Boolean -> Boolean) -> Boolean -> Maybe a -> Boolean
forall e a r. Monotonic e a => (a -> r -> r) -> r -> e -> r
reduce @(Maybe a) @a (\a
_ Boolean
_ -> Boolean
True) 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 e a (t :: * -> *).
(Monotonic e a, Pointable t, Avoidable t) =>
Predicate a -> e -> t a
find (a |-> Predicate
forall a. Setoid a => a |-> Predicate
equate a
x)

subset :: (Monotonic (t a) 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 e a (t :: * -> *).
(Monotonic e a, 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 -> Natural
cardinality :: t a -> Natural
cardinality t a
s = (Natural :*: t ()) -> Natural
forall a b. (a :*: b) -> a
attached ((Natural :*: t ()) -> Natural)
-> (State Natural (t ()) -> Natural :*: t ())
-> State Natural (t ())
-> Natural
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State Natural) =>
State Natural a -> Primary (State Natural) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _) (State Natural (t ()) -> ((->) Natural :. (:*:) Natural) := t ())
-> Natural -> State Natural (t ()) -> Natural :*: t ()
forall a b c. (a -> b -> c) -> b -> a -> c
% Natural
Zero (State Natural (t ()) -> Natural)
-> State Natural (t ()) -> Natural
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ t a
s t a -> (a -> State Natural ()) -> State Natural (t ())
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> (!) ((Natural -> Natural) -> State Natural ()
forall s (t :: * -> *). Stateful s t => (s -> s) -> t ()
modify @Natural (Natural -> Natural -> Natural
forall a. Semigroup a => a -> a -> a
+ Natural
forall a. Quasiring a => a
one))