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

import Pandora.Core.Functor (type (:.), type (>>>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), (<------))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
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.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Paradigm.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:)((:*:)))
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (point)
import Pandora.Core.Interpreted ((<~), (<~~~))

data Instruction t a = Enter a | Instruct (t :. Instruction t >>> a)

instance Covariant (->) (->) t => Covariant (->) (->) (Instruction t) where
	a -> b
f <-|- :: (a -> b) -> Instruction t a -> Instruction t b
<-|- Enter a
x = b -> Instruction t b
forall (t :: * -> *) a. a -> Instruction t a
Enter (b -> Instruction t b) -> b -> Instruction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
x
	a -> b
f <-|- Instruct (t :. Instruction t) >>> a
xs = ((t :. Instruction t) >>> b) -> Instruction t b
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (((t :. Instruction t) >>> b) -> Instruction t b)
-> ((t :. Instruction t) >>> b) -> Instruction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<------ a -> b
f (a -> b)
-> ((t :. Instruction t) >>> a) -> (t :. Instruction t) >>> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
<-|-|- (t :. Instruction t) >>> a
xs

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Semimonoidal (-->) (:*:) (:*:) (Instruction t) where
	mult :: (Instruction t a :*: Instruction t b) --> Instruction t (a :*: b)
mult = ((Instruction t a :*: Instruction t b) -> Instruction t (a :*: b))
-> (Instruction t a :*: Instruction t b)
   --> Instruction t (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Instruction t a :*: Instruction t b) -> Instruction t (a :*: b))
 -> (Instruction t a :*: Instruction t b)
    --> Instruction t (a :*: b))
-> ((Instruction t a :*: Instruction t b)
    -> Instruction t (a :*: b))
-> (Instruction t a :*: Instruction t b)
   --> Instruction t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \case
		Enter a
x :*: Enter b
y -> (a :*: b) -> Instruction t (a :*: b)
forall (t :: * -> *) a. a -> Instruction t a
Enter ((a :*: b) -> Instruction t (a :*: b))
-> (a :*: b) -> Instruction 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
		Enter a
x :*: Instruct (t :. Instruction t) >>> b
y -> (a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*:) (b -> a :*: b) -> Instruction t b -> Instruction t (a :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- ((t :. Instruction t) >>> b) -> Instruction t b
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (t :. Instruction t) >>> b
y
		Instruct (t :. Instruction t) >>> a
x :*: Enter b
y -> (a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y) (a -> a :*: b) -> Instruction t a -> Instruction t (a :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- ((t :. Instruction t) >>> a) -> Instruction t a
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (t :. Instruction t) >>> a
x
		Instruct (t :. Instruction t) >>> a
x :*: Instruct (t :. Instruction t) >>> b
y -> ((t :. Instruction t) >>> (a :*: b)) -> Instruction t (a :*: b)
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (((t :. Instruction t) >>> (a :*: b)) -> Instruction t (a :*: b))
-> ((t :. Instruction t) >>> (a :*: b)) -> Instruction 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 @(-->) ((Instruction t a :*: Instruction t b) --> Instruction t (a :*: b))
-> (Instruction t a :*: Instruction t b) -> Instruction t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) ((Instruction t a :*: Instruction t b) -> Instruction t (a :*: b))
-> t (Instruction t a :*: Instruction t b)
-> (t :. Instruction t) >>> (a :*: 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 :. Instruction t) >>> a) :*: ((t :. Instruction t) >>> b))
 --> t (Instruction t a :*: Instruction t b))
-> (((t :. Instruction t) >>> a) :*: ((t :. Instruction t) >>> b))
-> t (Instruction t a :*: Instruction t b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~~~ (t :. Instruction t) >>> a
x ((t :. Instruction t) >>> a)
-> ((t :. Instruction t) >>> b)
-> ((t :. Instruction t) >>> a) :*: ((t :. Instruction t) >>> b)
forall s a. s -> a -> s :*: a
:*: (t :. Instruction t) >>> b
y

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Monoidal (-->) (-->) (:*:) (:*:) (Instruction t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Instruction t a
unit Proxy (:*:)
_ = (Straight (->) One a -> Instruction t a)
-> Straight (->) (Straight (->) One a) (Instruction t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> Instruction t a)
 -> Straight (->) (Straight (->) One a) (Instruction t a))
-> (Straight (->) One a -> Instruction t a)
-> Straight (->) (Straight (->) One a) (Instruction t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> Instruction t a
forall (t :: * -> *) a. a -> Instruction t a
Enter (a -> Instruction t a)
-> (Straight (->) One a -> a)
-> Straight (->) One a
-> Instruction t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

instance Covariant (->) (->) t => Bindable (->) (Instruction t) where
	a -> Instruction t b
f =<< :: (a -> Instruction t b) -> Instruction t a -> Instruction t b
=<< Enter a
x = a -> Instruction t b
f a
x
	a -> Instruction t b
f =<< Instruct (t :. Instruction t) >>> a
xs = ((t :. Instruction t) >>> b) -> Instruction t b
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (((t :. Instruction t) >>> b) -> Instruction t b)
-> ((t :. Instruction t) >>> b) -> Instruction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (a -> Instruction t b
f (a -> Instruction t b) -> Instruction t a -> Instruction t b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<<) (Instruction t a -> Instruction t b)
-> ((t :. Instruction t) >>> a) -> (t :. Instruction t) >>> b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (t :. Instruction t) >>> a
xs

instance Monad (->) t => Monad (->) (Instruction t) where

instance Traversable (->) (->) t => Traversable (->) (->) (Instruction t) where
	a -> u b
f <-/- :: (a -> u b) -> Instruction t a -> u (Instruction t b)
<-/- Enter a
x = b -> Instruction t b
forall (t :: * -> *) a. a -> Instruction t a
Enter (b -> Instruction t b) -> u b -> u (Instruction 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
	a -> u b
f <-/- Instruct (t :. Instruction t) >>> a
xs = ((t :. Instruction t) >>> b) -> Instruction t b
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (((t :. Instruction t) >>> b) -> Instruction t b)
-> u ((t :. Instruction t) >>> b) -> u (Instruction 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 -> u b)
-> ((t :. Instruction t) >>> a) -> u ((t :. Instruction t) >>> b)
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Traversable category category t, Covariant category category u,
 Monoidal (Straight category) (Straight category) (:*:) (:*:) u,
 Traversable category category v) =>
category a (u b) -> category (v (t a)) (u (v (t b)))
<-/-/- (t :. Instruction t) >>> a
xs)

instance Liftable (->) Instruction where
	lift :: u a -> Instruction u a
lift u a
x = ((u :. Instruction u) >>> a) -> Instruction u a
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (((u :. Instruction u) >>> a) -> Instruction u a)
-> ((u :. Instruction u) >>> a) -> Instruction u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> Instruction u a
forall (t :: * -> *) a. a -> Instruction t a
Enter (a -> Instruction u a) -> u a -> (u :. Instruction u) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- u a
x

instance (forall t . Bindable (->) t, forall t . Monoidal (-->) (-->) (:*:) (:*:) t) => Lowerable (->) Instruction where
	lower :: Instruction u a -> u a
lower (Enter a
x) = a -> u a
forall (t :: * -> *) a. Pointable t => a -> t a
point a
x
	lower (Instruct (u :. Instruction u) >>> a
xs) = Instruction u a -> u a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (Instruction u a -> u a) -> ((u :. Instruction u) >>> a) -> u a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (u :. Instruction u) >>> a
xs

instance (forall v . Covariant (->) (->) v) => Hoistable (->) Instruction where
	forall a. u a -> v a
_ /|\ :: (forall a. u a -> v a)
-> forall a. Instruction u a -> Instruction v a
/|\ Enter a
x = a -> Instruction v a
forall (t :: * -> *) a. a -> Instruction t a
Enter a
x
	forall a. u a -> v a
f /|\ Instruct (u :. Instruction u) >>> a
xs = ((v :. Instruction v) >>> a) -> Instruction v a
forall (t :: * -> *) a.
((t :. Instruction t) >>> a) -> Instruction t a
Instruct (((v :. Instruction v) >>> a) -> Instruction v a)
-> ((v :. Instruction v) >>> a) -> Instruction v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (forall a. u a -> v a
f (forall a. u a -> v a) -> Instruction u a -> Instruction v a
forall k (m :: * -> * -> *) (t :: (* -> *) -> k -> *) (u :: * -> *)
       (v :: * -> *).
(Hoistable m t, Covariant m m u) =>
(forall a. m (u a) (v a)) -> forall (a :: k). m (t u a) (t v a)
/|\) (Instruction u a -> Instruction v a)
-> v (Instruction u a) -> (v :. Instruction v) >>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- ((u :. Instruction u) >>> a) -> v (Instruction u a)
forall a. u a -> v a
f (u :. Instruction u) >>> a
xs