module UVMHS.Core.Data.Set where

import UVMHS.Core.Init

import UVMHS.Core.Classes

import UVMHS.Core.Data.Iter
import UVMHS.Core.Data.Pair
import UVMHS.Core.Data.String

import qualified Data.Set as Set

infix 4 ⊆,⊇,∈,∉
infixl 5 ∪,∖
infixl 6 ∩

-------------------
-- GENERIC CLASS --
-------------------

class
  ( CSized s
  , Ord s
  , ToIter e s
  , Single e s
  , Monoid s
  , POrd s
  , JoinLattice s
  , Meet s
  , Difference s
  ) ⇒ Set e s | s→e
  where
    pø ∷ s
    pø = s
forall a. Null a => a
null
    psingle ∷ e → s
    psingle = e -> s
forall a t. Single a t => a -> t
single
    padd ∷ e → s → s
    padd e
e s
s = e -> s
forall a t. Single a t => a -> t
single e
e s -> s -> s
forall e s. Set e s => s -> s -> s
∪ s
s
    prem ∷ e → s → s
    prem e
e s
s = s
s s -> s -> s
forall e s. Set e s => s -> s -> s
∖ e -> s
forall a t. Single a t => a -> t
single e
e
    (∈) ∷ e → s → 𝔹
    (∈) e
e = s -> s -> 𝔹
forall e s. Set e s => s -> s -> 𝔹
(⊆) (s -> s -> 𝔹) -> s -> s -> 𝔹
forall a b. (a -> b) -> a -> b
$ e -> s
forall a t. Single a t => a -> t
single e
e
    (⊆) ∷ s → s → 𝔹
    (⊆) = s -> s -> 𝔹
forall a. POrd a => a -> a -> 𝔹
(⊑)
    (∪) ∷ s → s → s
    (∪) = s -> s -> s
forall a. Join a => a -> a -> a
(⊔)
    (∩) ∷ s → s → s
    (∩) = s -> s -> s
forall a. Meet a => a -> a -> a
(⊓)
    (∖) ∷ s → s → s
    (∖) = s -> s -> s
forall a. Difference a => a -> a -> a
(⊟)
    pminView ∷ s → 𝑂 (e ∧ s) -- NO DEFAULT
    pmaxView ∷ s → 𝑂 (e ∧ s) -- NO DEFAULT
    pminElem ∷ s → 𝑂 e
    pminElem = ((e ∧ s) -> e) -> 𝑂 (e ∧ s) -> 𝑂 e
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (e ∧ s) -> e
forall a b. (a ∧ b) -> a
fst (𝑂 (e ∧ s) -> 𝑂 e) -> (s -> 𝑂 (e ∧ s)) -> s -> 𝑂 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ s -> 𝑂 (e ∧ s)
forall e s. Set e s => s -> 𝑂 (e ∧ s)
pminView
    pmaxElem ∷ s → 𝑂 e
    pmaxElem = ((e ∧ s) -> e) -> 𝑂 (e ∧ s) -> 𝑂 e
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (e ∧ s) -> e
forall a b. (a ∧ b) -> a
fst (𝑂 (e ∧ s) -> 𝑂 e) -> (s -> 𝑂 (e ∧ s)) -> s -> 𝑂 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ s -> 𝑂 (e ∧ s)
forall e s. Set e s => s -> 𝑂 (e ∧ s)
pmaxView
    pow𝐼 ∷ 𝐼 e → s
    pow𝐼 = s -> (s -> s -> s) -> 𝐼 s -> s
forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
fold𝐼 s
forall e s. Set e s => s
pø s -> s -> s
forall e s. Set e s => s -> s -> s
(∪) (𝐼 s -> s) -> (𝐼 e -> 𝐼 s) -> 𝐼 e -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (e -> s) -> 𝐼 e -> 𝐼 s
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map e -> s
forall a t. Single a t => a -> t
single
    pvals ∷ s → 𝐼 e
    pvals = s -> 𝐼 e
forall a t. ToIter a t => t -> 𝐼 a
iter

(⊇) ∷ (Set e s) ⇒ s → s → 𝔹
⊇ :: forall e s. Set e s => s -> s -> 𝔹
(⊇) = (s -> s -> 𝔹) -> s -> s -> 𝔹
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> s -> 𝔹
forall e s. Set e s => s -> s -> 𝔹
(⊆)

(∉) ∷ (Set e s) ⇒ e → s → 𝔹
∉ :: forall e s. Set e s => e -> s -> 𝔹
(∉) = 𝔹 -> 𝔹
not (𝔹 -> 𝔹) -> (e -> s -> 𝔹) -> e -> s -> 𝔹
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
∘∘ e -> s -> 𝔹
forall e s. Set e s => e -> s -> 𝔹
(∈)

pow ∷ ∀ s t e. (ToIter e t,Set e s) ⇒ t → s
pow :: forall s t e. (ToIter e t, Set e s) => t -> s
pow = 𝐼 e -> s
forall e s. Set e s => 𝐼 e -> s
pow𝐼 (𝐼 e -> s) -> (t -> 𝐼 e) -> t -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 e
forall a t. ToIter a t => t -> 𝐼 a
iter

unions ∷ (Set e s,ToIter s t) ⇒ t → s
unions :: forall e s t. (Set e s, ToIter s t) => t -> s
unions t
ss = t -> s -> (s -> s -> s) -> s
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom t
ss s
forall e s. Set e s => s
pø s -> s -> s
forall e s. Set e s => s -> s -> s
(∪)

intersFrom ∷ (Set e s,ToIter s t) ⇒ s → t → s
intersFrom :: forall e s t. (Set e s, ToIter s t) => s -> t -> s
intersFrom s
s t
ss = t -> s -> (s -> s -> s) -> s
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom t
ss s
s s -> s -> s
forall e s. Set e s => s -> s -> s
(∩)

sdiffsFrom ∷ (Set e s,ToIter s t) ⇒ s → t → s
sdiffsFrom :: forall e s t. (Set e s, ToIter s t) => s -> t -> s
sdiffsFrom s
s t
ss = t -> s -> (s -> s -> s) -> s
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom t
ss s
s s -> s -> s
forall e s. Set e s => s -> s -> s
(∖)

---------------------------
-- STANDARD SET DATATYPE --
---------------------------

-- CLASS DEFINITIONS: Set --

pø𝑃 ∷ 𝑃 a
pø𝑃 :: forall a. 𝑃 a
pø𝑃 = Set a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce Set a
forall a. Set a
Set.empty

psingle𝑃 ∷ a → 𝑃 a
psingle𝑃 :: forall a. a -> 𝑃 a
psingle𝑃 = (a -> Set a) -> a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce a -> Set a
forall a. a -> Set a
Set.singleton

padd𝑃 ∷ (Ord a) ⇒ a → 𝑃 a → 𝑃 a
padd𝑃 :: forall a. Ord a => a -> 𝑃 a -> 𝑃 a
padd𝑃 = (a -> Set a -> Set a) -> a -> 𝑃 a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert

prem𝑃 ∷ (Ord a) ⇒ a → 𝑃 a → 𝑃 a
prem𝑃 :: forall a. Ord a => a -> 𝑃 a -> 𝑃 a
prem𝑃 = (a -> Set a -> Set a) -> a -> 𝑃 a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.delete

(∈♭) ∷ (Ord a) ⇒ a → 𝑃 a → 𝔹
∈♭ :: forall a. Ord a => a -> 𝑃 a -> 𝔹
(∈♭) = (a -> Set a -> 𝔹) -> a -> 𝑃 a -> 𝔹
forall a b. Coercible a b => a -> b
coerce a -> Set a -> 𝔹
forall a. Ord a => a -> Set a -> 𝔹
Set.member

(⊆♭) ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝔹
⊆♭ :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝔹
(⊆♭) = (Set a -> Set a -> 𝔹) -> 𝑃 a -> 𝑃 a -> 𝔹
forall a b. Coercible a b => a -> b
coerce Set a -> Set a -> 𝔹
forall a. Ord a => Set a -> Set a -> 𝔹
Set.isSubsetOf

(∪♭) ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
∪♭ :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∪♭) = (Set a -> Set a -> Set a) -> 𝑃 a -> 𝑃 a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union

(∩♭) ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
∩♭ :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∩♭) = (Set a -> Set a -> Set a) -> 𝑃 a -> 𝑃 a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection

(∖♭) ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
∖♭ :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∖♭) = (Set a -> Set a -> Set a) -> 𝑃 a -> 𝑃 a -> 𝑃 a
forall a b. Coercible a b => a -> b
coerce Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.difference

pminView𝑃 ∷ ∀ a. 𝑃 a → 𝑂 (a ∧ 𝑃 a)
pminView𝑃 :: forall a. 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
pminView𝑃 = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(Set.Set a → 𝑂 (a ∧ Set.Set a)) ((Set a -> 𝑂 (a ∧ Set a)) -> 𝑃 a -> 𝑂 (a ∧ 𝑃 a))
-> (Set a -> 𝑂 (a ∧ Set a)) -> 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
forall a b. (a -> b) -> a -> b
$ Maybe (a, Set a) -> 𝑂 (a ∧ Set a)
forall a b. CHS a b => b -> a
frhs (Maybe (a, Set a) -> 𝑂 (a ∧ Set a))
-> (Set a -> Maybe (a, Set a)) -> Set a -> 𝑂 (a ∧ Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.minView

pmaxView𝑃 ∷ ∀ a. 𝑃 a → 𝑂 (a ∧ 𝑃 a)
pmaxView𝑃 :: forall a. 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
pmaxView𝑃 = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(Set.Set a → 𝑂 (a ∧ Set.Set a)) ((Set a -> 𝑂 (a ∧ Set a)) -> 𝑃 a -> 𝑂 (a ∧ 𝑃 a))
-> (Set a -> 𝑂 (a ∧ Set a)) -> 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
forall a b. (a -> b) -> a -> b
$ Maybe (a, Set a) -> 𝑂 (a ∧ Set a)
forall a b. CHS a b => b -> a
frhs (Maybe (a, Set a) -> 𝑂 (a ∧ Set a))
-> (Set a -> Maybe (a, Set a)) -> Set a -> 𝑂 (a ∧ Set a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.maxView

pminElem𝑃 ∷ ∀ a. 𝑃 a → 𝑂 a
pminElem𝑃 :: forall a. 𝑃 a -> 𝑂 a
pminElem𝑃 = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(Set.Set a → 𝑂 a) ((Set a -> 𝑂 a) -> 𝑃 a -> 𝑂 a) -> (Set a -> 𝑂 a) -> 𝑃 a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ Maybe a -> 𝑂 a
forall a b. CHS a b => b -> a
frhs (Maybe a -> 𝑂 a) -> (Set a -> Maybe a) -> Set a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Set a -> Maybe a
forall a. Set a -> Maybe a
Set.lookupMin

pmaxElem𝑃 ∷ ∀ a. 𝑃 a → 𝑂 a
pmaxElem𝑃 :: forall a. 𝑃 a -> 𝑂 a
pmaxElem𝑃 = forall a b. Coercible a b => a -> b
forall a b. Coercible a b => a -> b
coerce @(Set.Set a → 𝑂 a) ((Set a -> 𝑂 a) -> 𝑃 a -> 𝑂 a) -> (Set a -> 𝑂 a) -> 𝑃 a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ Maybe a -> 𝑂 a
forall a b. CHS a b => b -> a
frhs (Maybe a -> 𝑂 a) -> (Set a -> Maybe a) -> Set a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Set a -> Maybe a
forall a. Set a -> Maybe a
Set.lookupMax

pow𝐼𝑃 ∷ (Ord a) ⇒ 𝐼 a → 𝑃 a
pow𝐼𝑃 :: forall a. Ord a => 𝐼 a -> 𝑃 a
pow𝐼𝑃 = Set a -> 𝑃 a
forall a. Set a -> 𝑃 a
𝑃 (Set a -> 𝑃 a) -> ([a] -> Set a) -> [a] -> 𝑃 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> 𝑃 a) -> (𝐼 a -> [a]) -> 𝐼 a -> 𝑃 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 a -> [a]
forall a t. ToIter a t => t -> [a]
lazyList

pvals𝑃 ∷ ∀ a. 𝑃 a → 𝐼 a
pvals𝑃 :: forall a. 𝑃 a -> 𝐼 a
pvals𝑃 = (Set a -> 𝐼 a) -> 𝑃 a -> 𝐼 a
forall a b. Coercible a b => a -> b
coerce ((Set a -> 𝐼 a) -> 𝑃 a -> 𝐼 a) -> (Set a -> 𝐼 a) -> 𝑃 a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ [a] -> 𝐼 a
forall a. [a] -> 𝐼 a
iterLL ([a] -> 𝐼 a) -> (Set a -> [a]) -> Set a -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Set a -> [a]
forall a. Set a -> [a]
Set.toList

-- CLASS DEFINITIONS: CSized --

csize𝑃 ∷ 𝑃 a → ℕ64
csize𝑃 :: forall a. 𝑃 a -> ℕ64
csize𝑃 = (Set a -> ℕ64) -> 𝑃 a -> ℕ64
forall a b. Coercible a b => a -> b
coerce ((Set a -> ℕ64) -> 𝑃 a -> ℕ64) -> (Set a -> ℕ64) -> 𝑃 a -> ℕ64
forall a b. (a -> b) -> a -> b
$ ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64 -> ℕ64) -> (Int -> ℤ64) -> Int -> ℕ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Int -> ℤ64
forall a b. CHS a b => b -> a
frhs (Int -> ℕ64) -> (Set a -> Int) -> Set a -> ℕ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Set a -> Int
forall a. Set a -> Int
Set.size

-- CLASS DEFINITIONS: Show --

show𝑃 ∷ (Show a) ⇒ 𝑃 a → 𝕊
show𝑃 :: forall a. Show a => 𝑃 a -> 𝕊
show𝑃 = 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝑃 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"{" 𝕊
"}" 𝕊
"," a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊

-- CLASS DEFINITIONS: ToIter --

iter𝑃 ∷ 𝑃 a → 𝐼 a
iter𝑃 :: forall a. 𝑃 a -> 𝐼 a
iter𝑃 = 𝑃 a -> 𝐼 a
forall a. 𝑃 a -> 𝐼 a
pvals𝑃

-- CLASS DEFINITIONS: Single --

single𝑃 ∷ a → 𝑃 a
single𝑃 :: forall a. a -> 𝑃 a
single𝑃 = a -> 𝑃 a
forall a. a -> 𝑃 a
psingle𝑃

-- CLASS DEFINITIONS: Monoid --

null𝑃 ∷ 𝑃 a
null𝑃 :: forall a. 𝑃 a
null𝑃 = 𝑃 a
forall a. 𝑃 a
pø𝑃

append𝑃 ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
append𝑃 :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
append𝑃 = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∪♭)

-- CLASS DEFINITIONS: Prodoid --

unit𝑃 ∷ (Ord a,Null a) ⇒ 𝑃 a
unit𝑃 :: forall a. (Ord a, Null a) => 𝑃 a
unit𝑃 = a -> 𝑃 a
forall a. a -> 𝑃 a
single𝑃 a
forall a. Null a => a
null

cross𝑃 ∷ (Ord a,Append a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
cross𝑃 :: forall a. (Ord a, Append a) => 𝑃 a -> 𝑃 a -> 𝑃 a
cross𝑃 𝑃 a
xs 𝑃 a
ys = 𝐼 a -> 𝑃 a
forall a. Ord a => 𝐼 a -> 𝑃 a
pow𝐼𝑃 (𝐼 a -> 𝑃 a) -> 𝐼 a -> 𝑃 a
forall a b. (a -> b) -> a -> b
$ do
  a
x ← 𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
xs
  a
y ← 𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
ys
  a -> 𝐼 a
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> 𝐼 a) -> a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
y

-- CLASS DEFINITIONS: Additive --

zero𝑃 ∷ 𝑃 a
zero𝑃 :: forall a. 𝑃 a
zero𝑃 = 𝑃 a
forall a. 𝑃 a
pø𝑃

plus𝑃 ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
plus𝑃 :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
plus𝑃 = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∪♭)

-- CLASS DEFINITIONS: Multiplicative --

one𝑃 ∷ (Ord a,Zero a) ⇒ 𝑃 a
one𝑃 :: forall a. (Ord a, Zero a) => 𝑃 a
one𝑃 = a -> 𝑃 a
forall a. a -> 𝑃 a
single𝑃 a
forall a. Zero a => a
zero

times𝑃 ∷ (Ord a,Plus a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
times𝑃 :: forall a. (Ord a, Plus a) => 𝑃 a -> 𝑃 a -> 𝑃 a
times𝑃 𝑃 a
xs 𝑃 a
ys = 𝐼 a -> 𝑃 a
forall a. Ord a => 𝐼 a -> 𝑃 a
pow𝐼𝑃 (𝐼 a -> 𝑃 a) -> 𝐼 a -> 𝑃 a
forall a b. (a -> b) -> a -> b
$ do
  a
x ← 𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
xs
  a
y ← 𝑃 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 a
ys
  a -> 𝐼 a
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> 𝐼 a) -> a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Plus a => a -> a -> a
+ a
y

-- CLASS DEFINITIONS: POrd --

plte𝑃 ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝔹
plte𝑃 :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝔹
plte𝑃 = 𝑃 a -> 𝑃 a -> 𝔹
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝔹
(⊆♭)

-- CLASS DEFINITIONS: Lattice

bot𝑃 ∷ 𝑃 a
bot𝑃 :: forall a. 𝑃 a
bot𝑃 = 𝑃 a
forall a. 𝑃 a
pø𝑃

join𝑃 ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
join𝑃 :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
join𝑃 = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∪♭)

meet𝑃 ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
meet𝑃 :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
meet𝑃 = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∩♭)

diff𝑃 ∷ (Ord a) ⇒ 𝑃 a → 𝑃 a → 𝑃 a
diff𝑃 :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
diff𝑃 = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∖♭)

-- CLASS DEFINITIONS: All --

all𝑃 ∷ (Ord a,All a) ⇒ 𝐼 (𝑃 a)
all𝑃 :: forall a. (Ord a, All a) => 𝐼 (𝑃 a)
all𝑃 = 𝐼 a -> 𝐼 (𝑃 a) -> (a -> 𝐼 (𝑃 a) -> 𝐼 (𝑃 a)) -> 𝐼 (𝑃 a)
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldrOnFrom 𝐼 a
forall a. All a => 𝐼 a
all (𝑃 a -> 𝐼 (𝑃 a)
forall a t. Single a t => a -> t
single 𝑃 a
forall a. 𝑃 a
pø𝑃) ((a -> 𝐼 (𝑃 a) -> 𝐼 (𝑃 a)) -> 𝐼 (𝑃 a))
-> (a -> 𝐼 (𝑃 a) -> 𝐼 (𝑃 a)) -> 𝐼 (𝑃 a)
forall a b. (a -> b) -> a -> b
$ \ a
x 𝐼 (𝑃 a)
xssᵢ → do
  𝑃 a
xs ← 𝐼 (𝑃 a)
xssᵢ
  [𝑃 a] -> 𝐼 (𝑃 a)
forall a t. ToIter a t => t -> 𝐼 a
iter ([𝑃 a] -> 𝐼 (𝑃 a)) -> [𝑃 a] -> 𝐼 (𝑃 a)
forall a b. (a -> b) -> a -> b
$ [ 𝑃 a
xs , a -> 𝑃 a
forall a t. Single a t => a -> t
single a
x 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
∪♭ 𝑃 a
xs ]

-- OTHER DEFINITIONS --

pow𝑃 ∷ (Ord a,ToIter a t) ⇒ t → 𝑃 a
pow𝑃 :: forall a t. (Ord a, ToIter a t) => t -> 𝑃 a
pow𝑃 = 𝐼 a -> 𝑃 a
forall a. Ord a => 𝐼 a -> 𝑃 a
pow𝐼𝑃 (𝐼 a -> 𝑃 a) -> (t -> 𝐼 a) -> t -> 𝑃 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

map𝑃 ∷ (Ord b) ⇒ (a → b) → 𝑃 a → 𝑃 b
map𝑃 :: forall b a. Ord b => (a -> b) -> 𝑃 a -> 𝑃 b
map𝑃 = ((a -> b) -> Set a -> Set b) -> (a -> b) -> 𝑃 a -> 𝑃 b
forall a b. Coercible a b => a -> b
coerce (a -> b) -> Set a -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map

uniques𝑃 ∷ (Ord a,ToIter a t) ⇒ t → 𝐼 a
uniques𝑃 :: forall a t. (Ord a, ToIter a t) => t -> 𝐼 a
uniques𝑃 t
xs = (𝑂 a -> 𝑂 a) -> 𝐼 (𝑂 a) -> 𝐼 a
forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap 𝑂 a -> 𝑂 a
forall a. a -> a
id (𝐼 (𝑂 a) -> 𝐼 a) -> 𝐼 (𝑂 a) -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> (𝐼 a -> 𝐼 (𝑂 a)) -> 𝐼 (𝑂 a)
forall a b. a -> (a -> b) -> b
appto (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) ((𝐼 a -> 𝐼 (𝑂 a)) -> 𝐼 (𝑂 a)) -> (𝐼 a -> 𝐼 (𝑂 a)) -> 𝐼 (𝑂 a)
forall a b. (a -> b) -> a -> b
$ 𝑃 a -> (a -> 𝑃 a -> 𝑃 a ∧ 𝑂 a) -> 𝐼 a -> 𝐼 (𝑂 a)
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter 𝑃 a
forall a. 𝑃 a
pø𝑃 ((a -> 𝑃 a -> 𝑃 a ∧ 𝑂 a) -> 𝐼 a -> 𝐼 (𝑂 a))
-> (a -> 𝑃 a -> 𝑃 a ∧ 𝑂 a) -> 𝐼 a -> 𝐼 (𝑂 a)
forall a b. (a -> b) -> a -> b
$ \ a
x 𝑃 a
seen →
  if a
x a -> 𝑃 a -> 𝔹
forall a. Ord a => a -> 𝑃 a -> 𝔹
∈♭ 𝑃 a
seen 
  then 𝑃 a
seen 𝑃 a -> 𝑂 a -> 𝑃 a ∧ 𝑂 a
forall a b. a -> b -> a ∧ b
:* 𝑂 a
forall a. 𝑂 a
None 
  else (a -> 𝑃 a
forall a. a -> 𝑃 a
single𝑃 a
x 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
∪♭ 𝑃 a
seen) 𝑃 a -> 𝑂 a -> 𝑃 a ∧ 𝑂 a
forall a b. a -> b -> a ∧ b
:* a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x

---------------
-- INSTANCES --
---------------

instance                    CSized      (𝑃 a) where csize :: 𝑃 a -> ℕ64
csize  = 𝑃 a -> ℕ64
forall a. 𝑃 a -> ℕ64
csize𝑃
instance (Show a)         ⇒ Show        (𝑃 a) where show :: 𝑃 a -> String
show   = 𝕊 -> String
tohsChars (𝕊 -> String) -> (𝑃 a -> 𝕊) -> 𝑃 a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 a -> 𝕊
forall a. Show a => 𝑃 a -> 𝕊
show𝑃
instance                    ToIter a    (𝑃 a) where iter :: 𝑃 a -> 𝐼 a
iter   = 𝑃 a -> 𝐼 a
forall a. 𝑃 a -> 𝐼 a
iter𝑃
instance (Ord a)          ⇒ Single a    (𝑃 a) where single :: a -> 𝑃 a
single = a -> 𝑃 a
forall a. a -> 𝑃 a
single𝑃
instance                    Null        (𝑃 a) where null :: 𝑃 a
null   = 𝑃 a
forall a. 𝑃 a
null𝑃
instance (Ord a)          ⇒ Append      (𝑃 a) where ⧺ :: 𝑃 a -> 𝑃 a -> 𝑃 a
(⧺)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
append𝑃
instance (Ord a)          ⇒ Monoid      (𝑃 a)
instance (Ord a,Null a)   ⇒ Unit        (𝑃 a) where unit :: 𝑃 a
unit   = 𝑃 a
forall a. (Ord a, Null a) => 𝑃 a
unit𝑃
instance (Ord a,Append a) ⇒ Cross       (𝑃 a) where ⨳ :: 𝑃 a -> 𝑃 a -> 𝑃 a
(⨳)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. (Ord a, Append a) => 𝑃 a -> 𝑃 a -> 𝑃 a
cross𝑃
instance (Ord a,Monoid a) ⇒ Prodoid     (𝑃 a)
instance                    Zero        (𝑃 a) where zero :: 𝑃 a
zero   = 𝑃 a
forall a. 𝑃 a
zero𝑃
instance (Ord a)          ⇒ Plus        (𝑃 a) where + :: 𝑃 a -> 𝑃 a -> 𝑃 a
(+)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
plus𝑃
instance (Ord a)          ⇒ Additive    (𝑃 a)
instance (Ord a,Zero a)   ⇒ One         (𝑃 a) where one :: 𝑃 a
one    = 𝑃 a
forall a. (Ord a, Zero a) => 𝑃 a
one𝑃
instance (Ord a,Plus a)   ⇒ Times       (𝑃 a) where × :: 𝑃 a -> 𝑃 a -> 𝑃 a
(×)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. (Ord a, Plus a) => 𝑃 a -> 𝑃 a -> 𝑃 a
times𝑃
instance (Ord a)          ⇒ POrd        (𝑃 a) where ⊑ :: 𝑃 a -> 𝑃 a -> 𝔹
(⊑)    = 𝑃 a -> 𝑃 a -> 𝔹
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝔹
plte𝑃
instance                    Bot         (𝑃 a) where bot :: 𝑃 a
bot    = 𝑃 a
forall a. 𝑃 a
bot𝑃
instance (Ord a)          ⇒ Join        (𝑃 a) where ⊔ :: 𝑃 a -> 𝑃 a -> 𝑃 a
(⊔)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
join𝑃
instance (Ord a)          ⇒ JoinLattice (𝑃 a)
instance (Ord a)          ⇒ Meet        (𝑃 a) where ⊓ :: 𝑃 a -> 𝑃 a -> 𝑃 a
(⊓)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
meet𝑃
instance (Ord a)          ⇒ Difference  (𝑃 a) where ⊟ :: 𝑃 a -> 𝑃 a -> 𝑃 a
(⊟)    = 𝑃 a -> 𝑃 a -> 𝑃 a
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
diff𝑃
instance (Ord a,All a)    ⇒ All         (𝑃 a) where all :: 𝐼 (𝑃 a)
all    = 𝐼 (𝑃 a)
forall a. (Ord a, All a) => 𝐼 (𝑃 a)
all𝑃

instance (Ord e) ⇒ Set e (𝑃 e) where
  pø :: 𝑃 e
pø       = 𝑃 e
forall a. 𝑃 a
pø𝑃
  psingle :: e -> 𝑃 e
psingle  = e -> 𝑃 e
forall a. a -> 𝑃 a
psingle𝑃
  padd :: e -> 𝑃 e -> 𝑃 e
padd     = e -> 𝑃 e -> 𝑃 e
forall a. Ord a => a -> 𝑃 a -> 𝑃 a
padd𝑃
  prem :: e -> 𝑃 e -> 𝑃 e
prem     = e -> 𝑃 e -> 𝑃 e
forall a. Ord a => a -> 𝑃 a -> 𝑃 a
prem𝑃
  ∈ :: e -> 𝑃 e -> 𝔹
(∈)      = e -> 𝑃 e -> 𝔹
forall a. Ord a => a -> 𝑃 a -> 𝔹
(∈♭) 
  ⊆ :: 𝑃 e -> 𝑃 e -> 𝔹
(⊆)      = 𝑃 e -> 𝑃 e -> 𝔹
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝔹
(⊆♭)
  ∪ :: 𝑃 e -> 𝑃 e -> 𝑃 e
(∪)      = 𝑃 e -> 𝑃 e -> 𝑃 e
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∪♭)
  ∩ :: 𝑃 e -> 𝑃 e -> 𝑃 e
(∩)      = 𝑃 e -> 𝑃 e -> 𝑃 e
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∩♭)
  ∖ :: 𝑃 e -> 𝑃 e -> 𝑃 e
(∖)      = 𝑃 e -> 𝑃 e -> 𝑃 e
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
(∖♭)
  pminView :: 𝑃 e -> 𝑂 (e ∧ 𝑃 e)
pminView = 𝑃 e -> 𝑂 (e ∧ 𝑃 e)
forall a. 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
pminView𝑃
  pmaxView :: 𝑃 e -> 𝑂 (e ∧ 𝑃 e)
pmaxView = 𝑃 e -> 𝑂 (e ∧ 𝑃 e)
forall a. 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
pmaxView𝑃
  pminElem :: 𝑃 e -> 𝑂 e
pminElem = 𝑃 e -> 𝑂 e
forall a. 𝑃 a -> 𝑂 a
pminElem𝑃
  pmaxElem :: 𝑃 e -> 𝑂 e
pmaxElem = 𝑃 e -> 𝑂 e
forall a. 𝑃 a -> 𝑂 a
pmaxElem𝑃
  pow𝐼 :: 𝐼 e -> 𝑃 e
pow𝐼     = 𝐼 e -> 𝑃 e
forall a. Ord a => 𝐼 a -> 𝑃 a
pow𝐼𝑃
  pvals :: 𝑃 e -> 𝐼 e
pvals    = 𝑃 e -> 𝐼 e
forall a. 𝑃 a -> 𝐼 a
pvals𝑃