module Pandora.Paradigm.Primary.Transformer.Day where

import Pandora.Pattern ((.|..))
import Pandora.Pattern.Category (($), (/))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable (hoist))
import Pandora.Paradigm.Primary.Functor.Function ((!!))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))

data Day t u a = forall b c . Day (t b) (u c) (b -> c -> a)

instance Covariant (Day t u) where
	a -> b
f <$> :: (a -> b) -> Day t u a -> Day t u b
<$> Day t b
tb u c
uc b -> c -> a
g = t b -> u c -> (b -> c -> b) -> Day t u b
forall (t :: * -> *) (u :: * -> *) a b c.
t b -> u c -> (b -> c -> a) -> Day t u a
Day t b
tb u c
uc ((b -> c -> b) -> Day t u b) -> (b -> c -> b) -> Day t u b
forall (m :: * -> * -> *). Category m => m ~~> m
/ a -> b
f (a -> b) -> (b -> c -> a) -> b -> c -> b
forall (v :: * -> * -> *) a c d b.
(Category v, Covariant (v a)) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.|.. b -> c -> a
g

instance (Pointable t, Pointable u) => Pointable (Day t u) where
	point :: a :=> Day t u
point a
x = t () -> u () -> (() -> () -> a) -> Day t u a
forall (t :: * -> *) (u :: * -> *) a b c.
t b -> u c -> (b -> c -> a) -> Day t u a
Day (t () -> u () -> (() -> () -> a) -> Day t u a)
-> t () -> u () -> (() -> () -> a) -> Day t u a
forall (m :: * -> * -> *). Category m => m ~~> m
/ () :=> t
forall (t :: * -> *) a. Pointable t => a :=> t
point () (u () -> (() -> () -> a) -> Day t u a)
-> u () -> (() -> () -> a) -> Day t u a
forall (m :: * -> * -> *). Category m => m ~~> m
/ () :=> u
forall (t :: * -> *) a. Pointable t => a :=> t
point () ((() -> () -> a) -> Day t u a) -> (() -> () -> a) -> Day t u a
forall (m :: * -> * -> *). Category m => m ~~> m
/ (a
x a -> () -> () -> a
forall a b c. a -> b -> c -> a
!!)

instance (Applicative t, Applicative u) => Applicative (Day t u) where
	Day t b
tb u c
uc b -> c -> a -> b
bcad <*> :: Day t u (a -> b) -> Day t u a -> Day t u b
<*> Day t b
vb u c
wc b -> c -> a
bca = t (Product b b)
-> u (Product c c)
-> (Product b b -> Product c c -> b)
-> Day t u b
forall (t :: * -> *) (u :: * -> *) a b c.
t b -> u c -> (b -> c -> a) -> Day t u a
Day (t (Product b b)
 -> u (Product c c)
 -> (Product b b -> Product c c -> b)
 -> Day t u b)
-> t (Product b b)
-> u (Product c c)
-> (Product b b -> Product c c -> b)
-> Day t u b
forall (m :: * -> * -> *). Category m => m ~~> m
/ b -> b -> Product b b
forall s a. s -> a -> Product s a
(:*:) (b -> b -> Product b b) -> t b -> t (b -> Product b b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t b
tb t (b -> Product b b) -> t b -> t (Product b b)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> t b
vb (u (Product c c) -> (Product b b -> Product c c -> b) -> Day t u b)
-> u (Product c c)
-> (Product b b -> Product c c -> b)
-> Day t u b
forall (m :: * -> * -> *). Category m => m ~~> m
/ c -> c -> Product c c
forall s a. s -> a -> Product s a
(:*:) (c -> c -> Product c c) -> u c -> u (c -> Product c c)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> u c
uc u (c -> Product c c) -> u c -> u (Product c c)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> u c
wc
		((Product b b -> Product c c -> b) -> Day t u b)
-> (Product b b -> Product c c -> b) -> Day t u b
forall (m :: * -> * -> *). Category m => m ~~> m
$ \(b
b :*: b
b') (c
c :*: c
c') -> b -> c -> a -> b
bcad b
b c
c (a -> b) -> a -> b
forall (m :: * -> * -> *). Category m => m ~~> m
$ b -> c -> a
bca b
b' c
c'

instance (Extractable t, Extractable u) => Extractable (Day t u) where
	extract :: a <:= Day t u
extract (Day t b
tb u c
uc b -> c -> a
bcad) = b -> c -> a
bcad (b -> c -> a) -> b -> c -> a
forall (m :: * -> * -> *). Category m => m ~~> m
/ b <:= t
forall (t :: * -> *) a. Extractable t => a <:= t
extract t b
tb (c -> a) -> c -> a
forall (m :: * -> * -> *). Category m => m ~~> m
/ c <:= u
forall (t :: * -> *) a. Extractable t => a <:= t
extract u c
uc

instance (Extendable t, Extendable u) => Extendable (Day t u) where
	day :: Day t u a
day@(Day t b
tb u c
uc b -> c -> a
_) =>> :: Day t u a -> (Day t u a -> b) -> Day t u b
=>> Day t u a -> b
f = t b -> u c -> (b -> c -> b) -> Day t u b
forall (t :: * -> *) (u :: * -> *) a b c.
t b -> u c -> (b -> c -> a) -> Day t u a
Day t b
tb u c
uc (Day t u a -> b
f Day t u a
day b -> b -> c -> b
forall a b c. a -> b -> c -> a
!!)

instance Extractable t => Lowerable (Day t) where
	lower :: Day t u ~> u
lower (Day t b
tb u c
uc b -> c -> a
bca) = b -> c -> a
bca (b <:= t
forall (t :: * -> *) a. Extractable t => a <:= t
extract t b
tb) (c -> a) -> u c -> u a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> u c
uc

instance Hoistable (Day t) where
	hoist :: (u ~> v) -> Day t u ~> Day t v
hoist u ~> v
g (Day t b
tb u c
uc b -> c -> a
bca) = t b -> v c -> (b -> c -> a) -> Day t v a
forall (t :: * -> *) (u :: * -> *) a b c.
t b -> u c -> (b -> c -> a) -> Day t u a
Day t b
tb (v c -> (b -> c -> a) -> Day t v a)
-> v c -> (b -> c -> a) -> Day t v a
forall (m :: * -> * -> *). Category m => m ~~> m
/ u c -> v c
u ~> v
g u c
uc ((b -> c -> a) -> Day t v a) -> (b -> c -> a) -> Day t v a
forall (m :: * -> * -> *). Category m => m ~~> m
/ b -> c -> a
bca