{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Primary.Transformer.Tap where

import Pandora.Core.Functor (type (>>>>>>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<------))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=), (<<==)))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Core.Interpreted ((<~), (<~~~))
import Pandora.Paradigm.Algebraic ((<-*--), (<-||--), extract)
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), (<:*:>))
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))

data Tap t a = Tap a (t a)

instance Covariant (->) (->) t => Covariant (->) (->) (Tap t) where
	a -> b
f <-|- :: (a -> b) -> Tap t a -> Tap t b
<-|- Tap a
x t a
xs = b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> t b -> Tap t b) -> b -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> b
f a
x (t b -> Tap t b) -> t b -> Tap 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
xs

instance Semimonoidal (-->) (:*:) (:*:) t => Semimonoidal (-->) (:*:) (:*:) (Tap t) where
	mult :: (Tap t a :*: Tap t b) --> Tap t (a :*: b)
mult = ((Tap t a :*: Tap t b) -> Tap t (a :*: b))
-> (Tap t a :*: Tap t b) --> Tap t (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Tap t a :*: Tap t b) -> Tap t (a :*: b))
 -> (Tap t a :*: Tap t b) --> Tap t (a :*: b))
-> ((Tap t a :*: Tap t b) -> Tap t (a :*: b))
-> (Tap t a :*: Tap t b) --> Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Tap a
x t a
xs :*: Tap b
y t b
ys) -> (a :*: b) -> t (a :*: b) -> Tap t (a :*: b)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap ((a :*: b) -> t (a :*: b) -> Tap t (a :*: b))
-> (a :*: b) -> t (a :*: b) -> Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y (t (a :*: b) -> Tap t (a :*: b)) -> t (a :*: b) -> Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- 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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
xs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
ys

instance Semimonoidal (<--) (:*:) (:*:) t => Semimonoidal (<--) (:*:) (:*:) (Tap t) where
	mult :: (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
mult = (Tap t (a :*: b) -> Tap t a :*: Tap t b)
-> (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Tap t (a :*: b) -> Tap t a :*: Tap t b)
 -> (Tap t a :*: Tap t b) <-- Tap t (a :*: b))
-> (Tap t (a :*: b) -> Tap t a :*: Tap t b)
-> (Tap t a :*: Tap t b) <-- Tap t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Tap (a
x :*: b
y) t (a :*: b)
xys) -> a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (t a -> Tap t a) -> (t a :*: Tap t b) -> Tap t a :*: Tap t b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-- b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
y (t b -> Tap t b) -> (t a :*: t b) -> t a :*: Tap t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- 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 :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ t (a :*: b)
xys

instance Semimonoidal (<--) (:*:) (:*:) t => Monoidal (<--) (-->) (:*:) (:*:) (Tap t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Tap t a
unit Proxy (:*:)
_ = (Tap t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Tap t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Tap t a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Tap t a))
-> (Tap t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Tap t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Tap a
x t a
_) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

instance Traversable (->) (->) t => Traversable (->) (->) (Tap t) where
	a -> u b
f <-/- :: (a -> u b) -> Tap t a -> u (Tap t b)
<-/- Tap a
x t a
xs = b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> t b -> Tap t b) -> u b -> u (t b -> Tap t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- a -> u b
f a
x u (t b -> Tap t b) -> u (t b) -> u (Tap t b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<-/- t a
xs

instance (Semimonoidal (<--) (:*:) (:*:) t, Extendable (->) t, Covariant (->) (->) t) => Extendable (->) (Tap t) where
	Tap t a -> b
f <<= :: (Tap t a -> b) -> Tap t a -> Tap t b
<<= Tap t a
x = b -> t b -> Tap t b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b -> t b -> Tap t b) -> b -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Tap t a -> b
f Tap t a
x (t b -> Tap t b) -> t b -> Tap t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Tap t a -> b
f (Tap t a -> b) -> (t a -> Tap t a) -> t a -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (Tap t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Tap t a
x) (t a -> b) -> t a -> t b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Extendable source t =>
source (t a) b -> source (t a) (t b)
<<= Tap t a -> t a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower Tap t a
x

instance Lowerable (->) Tap where
	lower :: Tap u a -> u a
lower (Tap a
_ u a
xs) = u a
xs

instance Hoistable (->) Tap where
	forall a. u a -> v a
f /|\ :: (forall a. u a -> v a) -> forall a. Tap u a -> Tap v a
/|\ Tap a
x u a
xs = a -> v a -> Tap v a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (v a -> Tap v a) -> v a -> Tap v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- u a -> v a
forall a. u a -> v a
f u a
xs

instance {-# OVERLAPS #-} Semimonoidal (-->) (:*:) (:*:) t => Semimonoidal (-->) (:*:) (:*:) (Tap (t <:.:> t >>>>>> (:*:))) where
	mult :: (Tap ((t <:.:> t) >>>>>> (:*:)) a
 :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
--> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)
mult = ((Tap ((t <:.:> t) >>>>>> (:*:)) a
  :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
 -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b))
-> (Tap ((t <:.:> t) >>>>>> (:*:)) a
    :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
   --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Tap ((t <:.:> t) >>>>>> (:*:)) a
   :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
  -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b))
 -> (Tap ((t <:.:> t) >>>>>> (:*:)) a
     :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
    --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b))
-> ((Tap ((t <:.:> t) >>>>>> (:*:)) a
     :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
    -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b))
-> (Tap ((t <:.:> t) >>>>>> (:*:)) a
    :*: Tap ((t <:.:> t) >>>>>> (:*:)) b)
   --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Tap a
x (T_U (t a
xls :*: t a
xrs)) :*: Tap b
y (T_U (t b
yls :*: t b
yrs))) ->
		(a :*: b)
-> (>>>>>>) (t <:.:> t) (:*:) (a :*: b)
-> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y) ((>>>>>>) (t <:.:> t) (:*:) (a :*: b)
 -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b))
-> (>>>>>>) (t <:.:> t) (:*:) (a :*: b)
-> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ (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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
xls t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yls) t (a :*: b) -> t (a :*: b) -> (>>>>>>) (t <:.:> t) (:*:) (a :*: b)
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ t a
xrs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yrs)