{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
module Data.Profunctor.Day(
  Day(..),
  promap1, promap2,
  swapDay, assocDay, unassocDay
) where

import Data.Profunctor (Profunctor (..), (:->))
import Data.Profunctor.Monad (ProfunctorFunctor (..))
import Data.Bifunctor.Assoc (Assoc(..))
import Data.Bifunctor (Bifunctor(..))
import Data.Bifunctor.Swap (Swap (..))

data Day t p q a b where
  Day :: p a1 b1 -> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b

deriving instance Functor (Day t p q a)

instance Profunctor (Day t p q) where
    dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Day t p q b c -> Day t p q a d
dimap a -> b
f c -> d
g (Day p a1 b1
p q a2 b2
q b -> t a1 a2
opA t b1 b2 -> c
opB) = p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> d) -> Day t p q a d
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day p a1 b1
p q a2 b2
q (b -> t a1 a2
opA (b -> t a1 a2) -> (a -> b) -> a -> t a1 a2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) (c -> d
g (c -> d) -> (t b1 b2 -> c) -> t b1 b2 -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t b1 b2 -> c
opB)

instance ProfunctorFunctor (Day t p) where
    promap :: forall (p :: * -> * -> *) (q :: * -> * -> *).
Profunctor p =>
(p :-> q) -> Day t p p :-> Day t p q
promap = (p :-> q) -> Day t p p a b -> Day t p q a b
(p :-> q) -> Day t p p :-> Day t p q
forall (q :: * -> * -> *) (q' :: * -> * -> *) (t :: * -> * -> *)
       (p :: * -> * -> *).
(q :-> q') -> Day t p q :-> Day t p q'
promap2

promap1 :: (p :-> p') -> Day t p q :-> Day t p' q
promap1 :: forall (p :: * -> * -> *) (p' :: * -> * -> *) (t :: * -> * -> *)
       (q :: * -> * -> *).
(p :-> p') -> Day t p q :-> Day t p' q
promap1 p :-> p'
h (Day p a1 b1
p q a2 b2
q a -> t a1 a2
opA t b1 b2 -> b
opB) = p' a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p' q a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day (p a1 b1 -> p' a1 b1
p :-> p'
h p a1 b1
p) q a2 b2
q a -> t a1 a2
opA t b1 b2 -> b
opB

promap2 :: (q :-> q') -> Day t p q :-> Day t p q'
promap2 :: forall (q :: * -> * -> *) (q' :: * -> * -> *) (t :: * -> * -> *)
       (p :: * -> * -> *).
(q :-> q') -> Day t p q :-> Day t p q'
promap2 q :-> q'
h (Day p a1 b1
p q a2 b2
q a -> t a1 a2
opA t b1 b2 -> b
opB) = p a1 b1
-> q' a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q' a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day p a1 b1
p (q a2 b2 -> q' a2 b2
q :-> q'
h q a2 b2
q) a -> t a1 a2
opA t b1 b2 -> b
opB

swapDay :: Swap t => Day t p q :-> Day t q p
swapDay :: forall (t :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
Swap t =>
Day t p q :-> Day t q p
swapDay (Day p a1 b1
p q a2 b2
q a -> t a1 a2
opA t b1 b2 -> b
opB) = q a2 b2
-> p a1 b1 -> (a -> t a2 a1) -> (t b2 b1 -> b) -> Day t q p a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day q a2 b2
q p a1 b1
p (t a1 a2 -> t a2 a1
forall a b. t a b -> t b a
forall (p :: * -> * -> *) a b. Swap p => p a b -> p b a
swap (t a1 a2 -> t a2 a1) -> (a -> t a1 a2) -> a -> t a2 a1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t a1 a2
opA) (t b1 b2 -> b
opB (t b1 b2 -> b) -> (t b2 b1 -> t b1 b2) -> t b2 b1 -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t b2 b1 -> t b1 b2
forall a b. t a b -> t b a
forall (p :: * -> * -> *) a b. Swap p => p a b -> p b a
swap)

assocDay :: Assoc t => Day t (Day t p q) r :-> Day t p (Day t q r)
assocDay :: forall (t :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *)
       (r :: * -> * -> *).
Assoc t =>
Day t (Day t p q) r :-> Day t p (Day t q r)
assocDay (Day (Day p a1 b1
p q a2 b2
q a1 -> t a1 a2
opA t b1 b2 -> b1
opB) r a2 b2
r a -> t a1 a2
opC t b1 b2 -> b
opD) = p a1 b1
-> Day t q r (t a2 a2) (t b2 b2)
-> (a -> t a1 (t a2 a2))
-> (t b1 (t b2 b2) -> b)
-> Day t p (Day t q r) a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day p a1 b1
p (q a2 b2
-> r a2 b2
-> (t a2 a2 -> t a2 a2)
-> (t b2 b2 -> t b2 b2)
-> Day t q r (t a2 a2) (t b2 b2)
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day q a2 b2
q r a2 b2
r t a2 a2 -> t a2 a2
forall a. a -> a
id t b2 b2 -> t b2 b2
forall a. a -> a
id) (t (t a1 a2) a2 -> t a1 (t a2 a2)
forall a b c. t (t a b) c -> t a (t b c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
assoc (t (t a1 a2) a2 -> t a1 (t a2 a2))
-> (a -> t (t a1 a2) a2) -> a -> t a1 (t a2 a2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a1 -> t a1 a2) -> t a1 a2 -> t (t a1 a2) a2
forall a b c. (a -> b) -> t a c -> t b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a1 -> t a1 a2
opA (t a1 a2 -> t (t a1 a2) a2)
-> (a -> t a1 a2) -> a -> t (t a1 a2) a2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t a1 a2
opC) (t b1 b2 -> b
opD (t b1 b2 -> b)
-> (t b1 (t b2 b2) -> t b1 b2) -> t b1 (t b2 b2) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t b1 b2 -> b1) -> t (t b1 b2) b2 -> t b1 b2
forall a b c. (a -> b) -> t a c -> t b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first t b1 b2 -> b1
opB (t (t b1 b2) b2 -> t b1 b2)
-> (t b1 (t b2 b2) -> t (t b1 b2) b2) -> t b1 (t b2 b2) -> t b1 b2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t b1 (t b2 b2) -> t (t b1 b2) b2
forall a b c. t a (t b c) -> t (t a b) c
forall (p :: * -> * -> *) a b c.
Assoc p =>
p a (p b c) -> p (p a b) c
unassoc)

unassocDay :: Assoc t => Day t p (Day t q r) :-> Day t (Day t p q) r 
unassocDay :: forall (t :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *)
       (r :: * -> * -> *).
Assoc t =>
Day t p (Day t q r) :-> Day t (Day t p q) r
unassocDay (Day p a1 b1
p (Day q a1 b1
q r a2 b2
r a2 -> t a1 a2
opA t b1 b2 -> b2
opB) a -> t a1 a2
opC t b1 b2 -> b
opD) = Day t p q (t a1 a1) (t b1 b1)
-> r a2 b2
-> (a -> t (t a1 a1) a2)
-> (t (t b1 b1) b2 -> b)
-> Day t (Day t p q) r a b
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day (p a1 b1
-> q a1 b1
-> (t a1 a1 -> t a1 a1)
-> (t b1 b1 -> t b1 b1)
-> Day t p q (t a1 a1) (t b1 b1)
forall (p :: * -> * -> *) a1 b1 (q :: * -> * -> *) a2 b2 a
       (t :: * -> * -> *) b.
p a1 b1
-> q a2 b2 -> (a -> t a1 a2) -> (t b1 b2 -> b) -> Day t p q a b
Day p a1 b1
p q a1 b1
q t a1 a1 -> t a1 a1
forall a. a -> a
id t b1 b1 -> t b1 b1
forall a. a -> a
id) r a2 b2
r (t a1 (t a1 a2) -> t (t a1 a1) a2
forall a b c. t a (t b c) -> t (t a b) c
forall (p :: * -> * -> *) a b c.
Assoc p =>
p a (p b c) -> p (p a b) c
unassoc (t a1 (t a1 a2) -> t (t a1 a1) a2)
-> (a -> t a1 (t a1 a2)) -> a -> t (t a1 a1) a2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a2 -> t a1 a2) -> t a1 a2 -> t a1 (t a1 a2)
forall b c a. (b -> c) -> t a b -> t a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second a2 -> t a1 a2
opA (t a1 a2 -> t a1 (t a1 a2))
-> (a -> t a1 a2) -> a -> t a1 (t a1 a2)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> t a1 a2
opC) (t b1 b2 -> b
opD (t b1 b2 -> b)
-> (t (t b1 b1) b2 -> t b1 b2) -> t (t b1 b1) b2 -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t b1 b2 -> b2) -> t b1 (t b1 b2) -> t b1 b2
forall b c a. (b -> c) -> t a b -> t a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second t b1 b2 -> b2
opB (t b1 (t b1 b2) -> t b1 b2)
-> (t (t b1 b1) b2 -> t b1 (t b1 b2)) -> t (t b1 b1) b2 -> t b1 b2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (t b1 b1) b2 -> t b1 (t b1 b2)
forall a b c. t (t a b) c -> t a (t b c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
assoc)