{-# LANGUAGE DeriveFunctor #-}
module Data.Profunctor.Exhaust(
  Exhaust(..)
) where

import Data.Void

import Data.Profunctor
import Data.Profunctor.Cartesian

data Exhaust a b = Absurd (a -> Void)
                 | Exhaust ((b -> Bool) -> b)
  deriving ((forall a b. (a -> b) -> Exhaust a a -> Exhaust a b)
-> (forall a b. a -> Exhaust a b -> Exhaust a a)
-> Functor (Exhaust a)
forall a b. a -> Exhaust a b -> Exhaust a a
forall a b. (a -> b) -> Exhaust a a -> Exhaust a b
forall a a b. a -> Exhaust a b -> Exhaust a a
forall a a b. (a -> b) -> Exhaust a a -> Exhaust a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a a b. (a -> b) -> Exhaust a a -> Exhaust a b
fmap :: forall a b. (a -> b) -> Exhaust a a -> Exhaust a b
$c<$ :: forall a a b. a -> Exhaust a b -> Exhaust a a
<$ :: forall a b. a -> Exhaust a b -> Exhaust a a
Functor)

instance Profunctor Exhaust where
  lmap :: forall a b c. (a -> b) -> Exhaust b c -> Exhaust a c
lmap a -> b
l (Absurd b -> Void
f)  = (a -> Void) -> Exhaust a c
forall a b. (a -> Void) -> Exhaust a b
Absurd (b -> Void
f (b -> Void) -> (a -> b) -> a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
l)
  lmap a -> b
_ (Exhaust (c -> Bool) -> c
g) = ((c -> Bool) -> c) -> Exhaust a c
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust (c -> Bool) -> c
g
  
  rmap :: forall b c a. (b -> c) -> Exhaust a b -> Exhaust a c
rmap b -> c
_ (Absurd a -> Void
f)  = (a -> Void) -> Exhaust a c
forall a b. (a -> Void) -> Exhaust a b
Absurd a -> Void
f
  rmap b -> c
r (Exhaust (b -> Bool) -> b
s) = ((c -> Bool) -> c) -> Exhaust a c
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust (((c -> Bool) -> c) -> Exhaust a c)
-> ((c -> Bool) -> c) -> Exhaust a c
forall a b. (a -> b) -> a -> b
$ \c -> Bool
cond -> b -> c
r (b -> c) -> b -> c
forall a b. (a -> b) -> a -> b
$ (b -> Bool) -> b
s (c -> Bool
cond (c -> Bool) -> (b -> c) -> b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
r)

instance Cartesian Exhaust where
  proUnit :: forall a. Exhaust a ()
proUnit = ((() -> Bool) -> ()) -> Exhaust a ()
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust (\() -> Bool
_ -> ())
  Absurd a -> Void
p  *** :: forall a b a' b'.
Exhaust a b -> Exhaust a' b' -> Exhaust (a, a') (b, b')
*** Exhaust a' b'
_         = ((a, a') -> Void) -> Exhaust (a, a') (b, b')
forall a b. (a -> Void) -> Exhaust a b
Absurd (\(a
a,a'
_) -> a -> Void
p a
a)
  Exhaust (b -> Bool) -> b
_ *** Absurd a' -> Void
q  = ((a, a') -> Void) -> Exhaust (a, a') (b, b')
forall a b. (a -> Void) -> Exhaust a b
Absurd (\(a
_,a'
a') -> a' -> Void
q a'
a')
  Exhaust (b -> Bool) -> b
p *** Exhaust (b' -> Bool) -> b'
q = (((b, b') -> Bool) -> (b, b')) -> Exhaust (a, a') (b, b')
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust ((b, b') -> Bool) -> (b, b')
pq
    where
      pq :: ((b, b') -> Bool) -> (b, b')
pq (b, b') -> Bool
cond =
        let subQuery :: b -> b'
subQuery b
b = (b' -> Bool) -> b'
q ((b' -> Bool) -> b') -> (b' -> Bool) -> b'
forall a b. (a -> b) -> a -> b
$ \b'
b' -> (b, b') -> Bool
cond (b
b, b'
b')
            bGot :: b
bGot = (b -> Bool) -> b
p ((b -> Bool) -> b) -> (b -> Bool) -> b
forall a b. (a -> b) -> a -> b
$ \b
b -> (b, b') -> Bool
cond (b
b, b -> b'
subQuery b
b)
        in (b
bGot, b -> b'
subQuery b
bGot)

instance Cocartesian Exhaust where
  proEmpty :: forall b. Exhaust Void b
proEmpty = (Void -> Void) -> Exhaust Void b
forall a b. (a -> Void) -> Exhaust a b
Absurd Void -> Void
forall a. a -> a
id
  Absurd a -> Void
p  +++ :: forall a b a' b'.
Exhaust a b -> Exhaust a' b' -> Exhaust (Either a a') (Either b b')
+++ Absurd a' -> Void
q  = (Either a a' -> Void) -> Exhaust (Either a a') (Either b b')
forall a b. (a -> Void) -> Exhaust a b
Absurd ((Either a a' -> Void) -> Exhaust (Either a a') (Either b b'))
-> (Either a a' -> Void) -> Exhaust (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ (a -> Void) -> (a' -> Void) -> Either a a' -> Void
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Void
p a' -> Void
q
  Absurd a -> Void
_  +++ Exhaust (b' -> Bool) -> b'
q = ((Either b b' -> Bool) -> Either b b')
-> Exhaust (Either a a') (Either b b')
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust (((Either b b' -> Bool) -> Either b b')
 -> Exhaust (Either a a') (Either b b'))
-> ((Either b b' -> Bool) -> Either b b')
-> Exhaust (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ \Either b b' -> Bool
cond -> b' -> Either b b'
forall a b. b -> Either a b
Right (b' -> Either b b') -> b' -> Either b b'
forall a b. (a -> b) -> a -> b
$ (b' -> Bool) -> b'
q (Either b b' -> Bool
cond (Either b b' -> Bool) -> (b' -> Either b b') -> b' -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b' -> Either b b'
forall a b. b -> Either a b
Right)
  Exhaust (b -> Bool) -> b
p +++ Absurd a' -> Void
_  = ((Either b b' -> Bool) -> Either b b')
-> Exhaust (Either a a') (Either b b')
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust (((Either b b' -> Bool) -> Either b b')
 -> Exhaust (Either a a') (Either b b'))
-> ((Either b b' -> Bool) -> Either b b')
-> Exhaust (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ \Either b b' -> Bool
cond -> b -> Either b b'
forall a b. a -> Either a b
Left (b -> Either b b') -> b -> Either b b'
forall a b. (a -> b) -> a -> b
$ (b -> Bool) -> b
p (Either b b' -> Bool
cond (Either b b' -> Bool) -> (b -> Either b b') -> b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either b b'
forall a b. a -> Either a b
Left)
  Exhaust (b -> Bool) -> b
p +++ Exhaust (b' -> Bool) -> b'
q = ((Either b b' -> Bool) -> Either b b')
-> Exhaust (Either a a') (Either b b')
forall a b. ((b -> Bool) -> b) -> Exhaust a b
Exhaust (((Either b b' -> Bool) -> Either b b')
 -> Exhaust (Either a a') (Either b b'))
-> ((Either b b' -> Bool) -> Either b b')
-> Exhaust (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ \Either b b' -> Bool
cond ->
    let x :: Either b b
x = b -> Either b b
forall a b. a -> Either a b
Left (b -> Either b b) -> b -> Either b b
forall a b. (a -> b) -> a -> b
$ (b -> Bool) -> b
p (Either b b' -> Bool
cond (Either b b' -> Bool) -> (b -> Either b b') -> b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either b b'
forall a b. a -> Either a b
Left)
        y :: Either a b'
y = b' -> Either a b'
forall a b. b -> Either a b
Right (b' -> Either a b') -> b' -> Either a b'
forall a b. (a -> b) -> a -> b
$ (b' -> Bool) -> b'
q (Either b b' -> Bool
cond (Either b b' -> Bool) -> (b' -> Either b b') -> b' -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b' -> Either b b'
forall a b. b -> Either a b
Right)
    in if Either b b' -> Bool
cond Either b b'
forall {b}. Either b b
x then Either b b'
forall {b}. Either b b
x else Either b b'
forall {a}. Either a b'
y