{-# LANGUAGE NoImplicitPrelude #-}

module Set (
  Set
, empty, singleton
, findMin, deleteMin, findMax, deleteMax
, succ, pred, zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven, twelve
, false, true, iif, not, (||), (&&)
, (==), (/=)
, lt, eq, gt, compare, (>=)
, (∪), union, (∩), intersection, (⊕), symmetricDifference, (\\), difference
, (<<), insert, (>>), delete
, (∈), member, (∉), notMember, (⊆), isSubsetOf, disjoint
, filter, map, flatmap, any, all, unions
, size, take, drop, range, powerSet
, (+), (-), (*), (/), (%), mod
, pair, fst, snd, (×), cartesianProduct, partition
) where

import Prelude (Show(show), (++))

infixl 9 *
infixl 9 /
infixl 9 %
infixl 9 `mod`
infixl 9 ×
infixl `cartesianProduct`
infixl 8 +
infixl 8 -
infixl 8 \\
infixl 8 `difference`
infixl 8 <<
infixl 8 >>
infixl 7 ∩
infixl 7 `intersection`
infixl 6 ⊕
infixl 6 `symmetricDifference`
infixl 5 ∪
infixl 5 `union`
infix  4 ==
infix  4 /=
infix  4 >=
infix  4 ∈
infix  4 `member`
infix  4 ∉
infix  4 `notMember`
infix  4 ⊆
infix  4 `isSubsetOf`
infixl 3 &&
infixl 2 ||

data Set = Nil | Cons Set Set

empty = Nil
singleton a = Cons a Nil

-- Min/Max
findMin (Cons a _) = a

deleteMin Nil        = empty
deleteMin (Cons _ a) = a

findMax (Cons a Nil) = a
findMax (Cons _ a  ) = findMax a

deleteMax Nil          = empty
deleteMax (Cons a Nil) = empty
deleteMax (Cons a b  ) = Cons a (deleteMax b)

-- Zermelo ordinals
succ = singleton
pred (Cons a Nil) = a

zero   = empty
one    = succ zero
two    = succ one
three  = succ two
four   = succ three
five   = succ four
six    = succ five
seven  = succ six
eight  = succ seven
nine   = succ eight
ten    = succ nine
eleven = succ ten
twelve = succ eleven

-- Logic
false = zero
true  = one

iif Nil _ a = a
iif _   a _ = a

not a  = iif a false true
a || b = iif a a b
a && b = iif a b a

-- Equality
Nil == Nil = true
Nil == _   = false
_   == Nil = false
(Cons a as) == (Cons b bs) = a == b && as == bs

a /= b = not (a == b)

-- Comparison
lt = zero
eq = one
gt = two
compare Nil Nil = eq
compare Nil _   = lt
compare _   Nil = gt
compare (Cons a as) (Cons b bs) = iif (a == b) (compare as bs) (compare a b)
(>=) = compare

-- Set operations
Nil ∪ a   = a
a   ∪ Nil = a
(Cons a as) ∪ (Cons b bs) = case compare a b of
  Nil          -> Cons a (as ∪ Cons b bs)
  Cons Nil Nil -> Cons a (as ∪ bs)
  _            -> Cons b (Cons a as ∪ bs)
union = (∪)

Nil ∩ _   = empty
_   ∩ Nil = empty
(Cons a as) ∩ (Cons b bs) = case compare a b of
  Nil          -> as ∩ Cons b bs
  Cons Nil Nil -> Cons a (as ∩ bs)
  _            -> Cons a as ∩ bs
intersection = (∩)

Nil ⊕ a   = a
a   ⊕ Nil = a
(Cons a as) ⊕ (Cons b bs) = case compare a b of
  Nil          -> Cons a (as ⊕ Cons b bs)
  Cons Nil Nil -> as ⊕ bs
  _            -> Cons b (Cons a as ⊕ bs)
symmetricDifference = (⊕)

Nil \\ _   = empty
a   \\ Nil = a
(Cons a as) \\ (Cons b bs) = case compare a b of
  Nil          -> Cons a (as \\ Cons b bs)
  Cons Nil Nil -> as \\ bs
  _            -> Cons a as \\ bs
difference = (\\)

a << b = a ∪ singleton b -- ruby <3
insert a b = b << a
a >> b = a \\ singleton b
delete a b = b >> a

_ ∈ Nil         = false
a ∈ (Cons b bs) = a == b || a ∈ bs
member = (∈)
a ∉ b = not (a ∈ b)
notMember = (∉)

Nil ⊆ _   = true
_   ⊆ Nil = false
(Cons a as) ⊆ (Cons b bs) = case compare a b of
  Nil          -> false
  Cons Nil Nil -> as ⊆ bs
  _            -> Cons a as ⊆ bs
isSubsetOf = (⊆)

disjoint a b = not (a ∩ b)

filter _ Nil         = empty
filter f (Cons a as) = iif (f a) (Cons a t) t
  where t = filter f as

map _ Nil         = empty
map f (Cons a as) = map f as << f a

flatmap _ Nil         = empty
flatmap f (Cons a as) = flatmap f as ∪ f a

any _ Nil         = false
any p (Cons a as) = p a || any p as

all _ Nil         = true
all p (Cons a as) = p a && all p as

unions Nil         = empty
unions (Cons a as) = a ∪ unions as

size Nil        = zero
size (Cons _ a) = succ (size a)

take _   Nil         = empty
take Nil _           = empty
take n   (Cons a as) = Cons a (take (pred n) as)

drop Nil a           = a
drop _   Nil         = empty
drop n   (Cons a as) = drop (pred n) as

nats = go zero
  where go n = Cons n (go (succ n))

range n = take n nats

powerSet Nil         = singleton empty
powerSet (Cons a as) = p ∪ map (<< a) p
  where p = powerSet as

-- Arithmetic
a + b = iif b (succ a + pred b) a
a - b = iif b (pred a - pred b) a
a * b = iif b (a + a * pred b) zero
a / b = iif (a >= b) (succ ((a - b) / b)) zero
a % b = iif (a >= b) (mod (a - b) b) a
mod = (%)

-- Tuples
-- Wiener construction:
-- (a,b) = {     {    { }  ,     {    a   }    }    ,     {     {    b   }    }    }
pair a b = Cons (Cons Nil (Cons (Cons a Nil) Nil)) (Cons (Cons (Cons b Nil) Nil) Nil)

fst (Cons (Cons Nil (Cons (Cons a Nil) Nil)) _) = a
snd (Cons _ (Cons (Cons (Cons a Nil) Nil) Nil)) = a

as × bs = flatmap (\a -> map (pair a) bs) as
cartesianProduct = (×)

partition _ Nil         = pair Nil Nil
partition p (Cons a as) = iif (p a) (pair (Cons a f) s) (pair f (Cons a s))
  where t = partition p as
        f = fst t
        s = snd t

-- Debugging
valid Nil                  = true
valid (Cons a Nil)         = valid a
valid (Cons a (Cons b bs)) = valid a && not (a >= b) && valid (Cons b bs)

instance Show Set where
  show Nil = "{}"
  show a   = "{" ++ show' a
    where show' (Cons a as) = show a ++ iif as ("," ++ show' as) "}"