module Proarrow.Promonad.Collage where

import Proarrow.Core (PRO, CategoryOf(..), Promonad(..), Profunctor(..), lmap, rmap)
import Proarrow.Category.Instance.Prof (Prof(..))
import Proarrow.Category.Instance.Coproduct (COPRODUCT(..), (:++:)(..), coproductId)
import Proarrow.Functor (Functor(..))

type Collage :: PRO j k -> PRO (COPRODUCT j k) (COPRODUCT j k)
data Collage p a b where
  InL :: (a ~> b) -> Collage p (L a) (L b)
  InR :: (a ~> b) -> Collage p (R a) (R b)
  L2R :: p a b -> Collage p (L a) (R b)

instance Profunctor p => Profunctor (Collage p) where
  dimap :: forall (c :: COPRODUCT j k) (a :: COPRODUCT j k)
       (b :: COPRODUCT j k) (d :: COPRODUCT j k).
(c ~> a) -> (b ~> d) -> Collage p a b -> Collage p c d
dimap (InjL a1 ~> b1
l) (InjL a1 ~> b1
r) (InL a ~> b
f) = (a1 ~> b1) -> Collage p ('L a1) ('L b1)
forall {k} {k} (a :: k) (b :: k) (p :: PRO k k).
(a ~> b) -> Collage p ('L a) ('L b)
InL ((a1 ~> b1) -> (a1 ~> b1) -> (b1 ~> a1) -> a1 ~> b1
forall (c :: j) (a :: j) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a1 ~> b1
l a1 ~> b1
r b1 ~> a1
a ~> b
f)
  dimap (InjR a1 ~> b1
l) (InjR a1 ~> b1
r) (InR a ~> b
f) = (a1 ~> b1) -> Collage p ('R a1) ('R b1)
forall {k} {j} (a :: k) (b :: k) (p :: PRO j k).
(a ~> b) -> Collage p ('R a) ('R b)
InR ((a1 ~> b1) -> (a1 ~> b1) -> (b1 ~> a1) -> a1 ~> b1
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> (a ~> b) -> c ~> d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a1 ~> b1
l a1 ~> b1
r b1 ~> a1
a ~> b
f)
  dimap (InjL a1 ~> b1
l) (InjR a1 ~> b1
r) (L2R p a b
p) = p a1 b1 -> Collage p ('L a1) ('R b1)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Collage p ('L a) ('R b)
L2R ((a1 ~> a) -> (b ~> b1) -> p a b -> p a1 b1
forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a1 ~> b1
a1 ~> a
l a1 ~> b1
b ~> b1
r p a b
p)
  dimap (InjR a1 ~> b1
_) (InjL a1 ~> b1
_) Collage p a b
f = case Collage p a b
f of
  (Ob a, Ob b) => r
r \\ :: forall (a :: COPRODUCT j k) (b :: COPRODUCT j k) r.
((Ob a, Ob b) => r) -> Collage p a b -> r
\\ InL a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  (Ob a, Ob b) => r
r \\ InR a ~> b
f = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
f
  (Ob a, Ob b) => r
r \\ L2R p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance Profunctor p => Promonad (Collage p) where
  id :: forall a. Ob a => Collage p a a
  id :: forall (a :: COPRODUCT j k). Ob a => Collage p a a
id = case forall {j} {k} (a :: COPRODUCT j k).
IsCoproduct a =>
(:++:) (~>) (~>) a a
forall (a :: COPRODUCT j k). IsCoproduct a => (:++:) (~>) (~>) a a
coproductId @a of
    InjL a1 ~> b1
f -> (b1 ~> b1) -> Collage p ('L b1) ('L b1)
forall {k} {k} (a :: k) (b :: k) (p :: PRO k k).
(a ~> b) -> Collage p ('L a) ('L b)
InL a1 ~> b1
b1 ~> b1
f
    InjR a1 ~> b1
f -> (b1 ~> b1) -> Collage p ('R b1) ('R b1)
forall {k} {j} (a :: k) (b :: k) (p :: PRO j k).
(a ~> b) -> Collage p ('R a) ('R b)
InR a1 ~> b1
b1 ~> b1
f
  InL a ~> b
g . :: forall (b :: COPRODUCT j k) (c :: COPRODUCT j k)
       (a :: COPRODUCT j k).
Collage p b c -> Collage p a b -> Collage p a c
. InL a ~> b
f = (a ~> b) -> Collage p ('L a) ('L b)
forall {k} {k} (a :: k) (b :: k) (p :: PRO k k).
(a ~> b) -> Collage p ('L a) ('L b)
InL (a ~> b
g (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: j) (c :: j) (a :: j). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
a ~> b
f)
  InR a ~> b
g . L2R p a b
p = p a b -> Collage p ('L a) ('R b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Collage p ('L a) ('R b)
L2R ((b ~> b) -> p a b -> p a b
forall {j} {k} (p :: PRO j k) (b :: k) (d :: k) (a :: j).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
b ~> b
g p a b
p)
  L2R p a b
p . InL a ~> b
f = p a b -> Collage p ('L a) ('R b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Collage p ('L a) ('R b)
L2R ((a ~> a) -> p a b -> p a b
forall {j} {k} (p :: PRO j k) (c :: j) (a :: j) (b :: k).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> a
a ~> b
f p a b
p)
  InR a ~> b
g . InR a ~> b
f = (a ~> b) -> Collage p ('R a) ('R b)
forall {k} {j} (a :: k) (b :: k) (p :: PRO j k).
(a ~> b) -> Collage p ('R a) ('R b)
InR (a ~> b
g (a ~> b) -> (a ~> a) -> a ~> b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> a
a ~> b
f)

instance Functor Collage where
  map :: forall (a :: PRO j k) (b :: PRO j k).
(a ~> b) -> Collage a ~> Collage b
map (Prof a :~> b
n) = (Collage a :~> Collage b) -> Prof (Collage a) (Collage b)
forall {j} {k} (p :: PRO j k) (q :: PRO j k).
(Profunctor p, Profunctor q) =>
(p :~> q) -> Prof p q
Prof \case
    InL a ~> b
l -> (a ~> b) -> Collage b ('L a) ('L b)
forall {k} {k} (a :: k) (b :: k) (p :: PRO k k).
(a ~> b) -> Collage p ('L a) ('L b)
InL a ~> b
l
    InR a ~> b
r -> (a ~> b) -> Collage b ('R a) ('R b)
forall {k} {j} (a :: k) (b :: k) (p :: PRO j k).
(a ~> b) -> Collage p ('R a) ('R b)
InR a ~> b
r
    L2R a a b
p -> b a b -> Collage b ('L a) ('R b)
forall {j} {k} (p :: PRO j k) (a :: j) (b :: k).
p a b -> Collage p ('L a) ('R b)
L2R (a a b -> b a b
a :~> b
n a a b
p)