{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Reverse where

import Pandora.Core.Appliable ((!))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Distributive (Distributive ((-<<)))
import Pandora.Pattern.Functor.Bivariant ((<->))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Paradigm.Primary.Transformer.Backwards (Backwards (Backwards))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (point, extract)
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))

newtype Reverse t a = Reverse (t a)

instance Covariant (->) (->) t => Covariant (->) (->) (Reverse t) where
	a -> b
f <$> :: (a -> b) -> Reverse t a -> Reverse t b
<$> Reverse t a
x = t b -> Reverse t b
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t b -> Reverse t b) -> t b -> Reverse t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f (a -> b) -> t a -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> t a
x

instance (Semimonoidal (-->) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (-->) (:*:) (:*:) (Reverse t) where
	mult :: (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b)
mult = ((Reverse t a :*: Reverse t b) -> Reverse t (a :*: b))
-> (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Reverse t a :*: Reverse t b) -> Reverse t (a :*: b))
 -> (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b))
-> ((Reverse t a :*: Reverse t b) -> Reverse t (a :*: b))
-> (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Reverse t a
x :*: Reverse t b
y) -> t (a :*: b) -> Reverse t (a :*: b)
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t (a :*: b) -> Reverse t (a :*: b))
-> t (a :*: b) -> Reverse t (a :*: b)
forall k k k k (m :: k -> k -> *) (a :: k) (b :: k)
       (n :: k -> k -> *) (c :: k) (d :: k).
Appliable m a b n c d =>
m a b -> n c d
! forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall k k k k (m :: k -> k -> *) (a :: k) (b :: k)
       (n :: k -> k -> *) (c :: k) (d :: k).
Appliable m a b n c d =>
m a b -> n c d
! (t a
x t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
y)

instance (Covariant (->) (->) t, Monoidal (-->) (->) (:*:) (:*:) t) => Monoidal (-->) (->) (:*:) (:*:) (Reverse t) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) --> Reverse t a
unit Proxy (:*:)
_ = ((One -> a) -> Reverse t a)
-> Straight (->) (One -> a) (Reverse t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One -> a) -> Reverse t a)
 -> Straight (->) (One -> a) (Reverse t a))
-> ((One -> a) -> Reverse t a)
-> Straight (->) (One -> a) (Reverse t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t a -> Reverse t a)
-> ((One -> a) -> t a) -> (One -> a) -> Reverse t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> t a) -> ((One -> a) -> a) -> (One -> a) -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One -> a) -> One -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ One
One)

instance (Semimonoidal (<--) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (<--) (:*:) (:*:) (Reverse t) where
	mult :: (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b)
mult = (Reverse t (a :*: b) -> Reverse t a :*: Reverse t b)
-> (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Reverse t (a :*: b) -> Reverse t a :*: Reverse t b)
 -> (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b))
-> (Reverse t (a :*: b) -> Reverse t a :*: Reverse t b)
-> (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t a -> Reverse t a)
-> (t b -> Reverse t b)
-> (t a :*: t b)
-> Reverse t a :*: Reverse t b
forall (left :: * -> * -> *) (right :: * -> * -> *)
       (target :: * -> * -> *) (v :: * -> * -> *) a b c d.
Bivariant left right target v =>
left a b -> right c d -> target (v a c) (v b d)
<-> t b -> Reverse t b
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse) ((t a :*: t b) -> Reverse t a :*: Reverse t b)
-> (Reverse t (a :*: b) -> t a :*: t b)
-> Reverse t (a :*: b)
-> Reverse t a :*: Reverse t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Flip (->) (t a :*: t b) (t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--)) (t (a :*: b) -> t a :*: t b)
-> (Reverse t (a :*: b) -> t (a :*: b))
-> Reverse t (a :*: b)
-> t a :*: t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Reverse t (a :*: b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run

instance (Covariant (->) (->) t, Monoidal (<--) (->) (:*:) (:*:) t) => Monoidal (<--) (->) (:*:) (:*:) (Reverse t) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- Reverse t a
unit Proxy (:*:)
_ = (Reverse t a -> One -> a) -> Flip (->) (One -> a) (Reverse t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Reverse t a -> One -> a) -> Flip (->) (One -> a) (Reverse t a))
-> (Reverse t a -> One -> a) -> Flip (->) (One -> a) (Reverse t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Reverse t a
x) -> (\One
_ -> t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract t a
x)

instance Traversable (->) (->) t => Traversable (->) (->) (Reverse t) where
	a -> u b
f <<- :: (a -> u b) -> Reverse t a -> u (Reverse t b)
<<- Reverse t a
x = t b -> Reverse t b
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t b -> Reverse t b) -> u (t b) -> u (Reverse t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<$> Backwards u (t b) -> u (t b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (u b -> Backwards u b
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (u b -> Backwards u b) -> (a -> u b) -> a -> Backwards u b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> u b
f (a -> Backwards u b) -> t a -> Backwards u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- t a
x)

instance Distributive (->) (->) t => Distributive (->) (->) (Reverse t) where
	a -> Reverse t b
f -<< :: (a -> Reverse t b) -> u a -> Reverse t (u b)
-<< u a
x = t (u b) -> Reverse t (u b)
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t (u b) -> Reverse t (u b)) -> t (u b) -> Reverse t (u b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Reverse t b -> t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Reverse t b -> t b) -> (a -> Reverse t b) -> a -> t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Reverse t b
f (a -> t b) -> u a -> t (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Distributive source target t, Covariant source target u) =>
source a (t b) -> target (u a) (t (u b))
-<< u a
x

instance Contravariant (->) (->) t => Contravariant (->) (->) (Reverse t) where
	a -> b
f >$< :: (a -> b) -> Reverse t b -> Reverse t a
>$< Reverse t b
x = t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (t a -> Reverse t a) -> t a -> Reverse t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f (a -> b) -> t b -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
>$< t b
x

instance Interpreted (->) (Reverse t) where
	type Primary (Reverse t) a = t a
	run :: Reverse t a -> Primary (Reverse t) a
run ~(Reverse t a
x) = t a
Primary (Reverse t) a
x
	unite :: Primary (Reverse t) a -> Reverse t a
unite = Primary (Reverse t) a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse

instance Liftable (->) Reverse where
	lift :: u a -> Reverse u a
lift = u a -> Reverse u a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse

instance Lowerable (->) Reverse where
	lower :: Reverse u a -> u a
lower = Reverse u a -> u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run

instance Hoistable Reverse where
	u ~> v
f /|\ :: (u ~> v) -> Reverse u ~> Reverse v
/|\ Reverse u a
x = v a -> Reverse v a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (v a -> Reverse v a) -> v a -> Reverse v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# u a -> v a
u ~> v
f u a
x