{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Instruction where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Appliable ((!))
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.Primary.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:)((:*:)))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic (point)

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)
-> ((t :. Instruction t) := a) -> (t :. Instruction t) := b
forall (source :: * -> * -> *) (between :: * -> * -> *)
       (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Covariant source between u, Covariant between target t) =>
source a b -> target (t (u a)) (t (u b))
(<$$>) @(->) @(->) a -> b
f (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 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
!) ((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 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 :. 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 (:*:)
_ = ((One -> a) -> Instruction t a)
-> Straight (->) (One -> a) (Instruction t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One -> a) -> Instruction t a)
 -> Straight (->) (One -> a) (Instruction t a))
-> ((One -> a) -> Instruction t a)
-> 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)
-> ((One -> a) -> a) -> (One -> a) -> Instruction 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 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) 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
	u ~> v
_ /|\ :: (u ~> v) -> Instruction u ~> Instruction v
/|\ Enter a
x = a -> Instruction v a
forall (t :: * -> *) a. a -> Instruction t a
Enter a
x
	u ~> v
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)
$ (u ~> v
f (u ~> v) -> Instruction u a -> Instruction v a
forall k (t :: (* -> *) -> k -> *) (u :: * -> *) (v :: * -> *).
(Hoistable t, Covariant (->) (->) u) =>
(u ~> v) -> t u ~> t v
/|\) (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)
u ~> v
f (u :. Instruction u) := a
xs