module Pandora.Paradigm.Controlflow.Effect.Interpreted where

import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)), (<$$>), (<$$$>), (<$$$$>))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Paradigm.Primary.Algebraic.Exponential ()

infixr 2 ||=, =||

type family Schematic (c :: (* -> * -> *) -> (* -> *) -> k) (t :: * -> *) = (r :: (* -> *) -> * -> *) | r -> t

class Interpreted m t where
	{-# MINIMAL run, unite #-}
	type Primary t a :: *
	run :: m (t a) (Primary t a)
	unite :: m (Primary t a) (t a)

	(||=) :: (Semigroupoid m, Interpreted m u) => m (Primary t a) (Primary u b) -> m (t a) (u b)
	(||=) m (Primary t a) (Primary u b)
f = m (Primary u b) (u b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (Primary t a) (t a)
unite m (Primary u b) (u b) -> m (t a) (Primary u b) -> m (t a) (u b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. m (Primary t a) (Primary u b)
f m (Primary t a) (Primary u b)
-> m (t a) (Primary t a) -> m (t a) (Primary u b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. m (t a) (Primary t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run

	(=||) :: (Semigroupoid m, Interpreted m u) => m (t a) (u b) -> m (Primary t a) (Primary u b)
	(=||) m (t a) (u b)
f = m (u b) (Primary u b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run m (u b) (Primary u b)
-> m (Primary t a) (u b) -> m (Primary t a) (Primary u b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. m (t a) (u b)
f m (t a) (u b) -> m (Primary t a) (t a) -> m (Primary t a) (u b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. m (Primary t a) (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (Primary t a) (t a)
unite

	(<$||=) :: (Semigroupoid m, Covariant m m j, Interpreted m u)
                => m (Primary t a) (Primary u b) -> m (j := t a) (j := u b)
	(<$||=) m (Primary t a) (Primary u b)
f = m (t a) (u b) -> m (j := t a) (j := u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<$>) (m (Primary t a) (Primary u b) -> m (t a) (u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(||=) m (Primary t a) (Primary u b)
f)

	(<$$||=) :: (Semigroupoid m, Covariant m m j, Covariant m m k, Interpreted m u)
		=> m (Primary t a) (Primary u b) -> m (j :. k := t a) (j :. k := u b)
	(<$$||=) m (Primary t a) (Primary u b)
f = m (t a) (u b) -> m ((j :. k) := t a) ((j :. k) := u 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))
(<$$>) @m @m (m (Primary t a) (Primary u b) -> m (t a) (u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(||=) m (Primary t a) (Primary u b)
f)

	(<$$$||=) :: (Semigroupoid m, Covariant m m j, Covariant m m k, Covariant m m l, Interpreted m u)
		=> m (Primary t a) (Primary u b) -> m (j :. k :. l := t a) (j :. k :. l := u b)
	(<$$$||=) m (Primary t a) (Primary u b)
f = m (t a) (u b)
-> m ((j :. (k :. l)) := t a) ((j :. (k :. l)) := u b)
forall (source :: * -> * -> *) (between1 :: * -> * -> *)
       (between2 :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *)
       (u :: * -> *) (v :: * -> *) a b.
(Covariant source between1 v, Covariant between1 between2 u,
 Covariant between2 target t) =>
source a b -> target (t (u (v a))) (t (u (v b)))
(<$$$>) @m @m @m (m (Primary t a) (Primary u b) -> m (t a) (u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(||=) m (Primary t a) (Primary u b)
f)

	(<$$$$||=) :: (Semigroupoid m, Covariant m m j, Covariant m m k, Covariant m m l, Covariant m m n, Interpreted m u)
		=> m (Primary t a) (Primary u b) -> m (j :. k :. l :. n := t a) (j :. k :. l :. n := u b)
	(<$$$$||=) m (Primary t a) (Primary u b)
f = m (t a) (u b)
-> m ((j :. (k :. (l :. n))) := t a)
     ((j :. (k :. (l :. n))) := u b)
forall (source :: * -> * -> *) (between1 :: * -> * -> *)
       (between2 :: * -> * -> *) (between3 :: * -> * -> *)
       (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (w :: * -> *) a b.
(Covariant source between1 w, Covariant between1 between2 v,
 Covariant between2 between3 u, Covariant between3 target t) =>
source a b -> target (t (u (v (w a)))) (t (u (v (w b))))
(<$$$$>) @m @m @m @m (m (Primary t a) (Primary u b) -> m (t a) (u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(||=) m (Primary t a) (Primary u b)
f)

	(=||$>) :: (Covariant m m j, Interpreted m u)
		=> m (t a) (u b) -> m (j := Primary t a) (j := Primary u b)
	(=||$>) m (t a) (u b)
f = m (Primary t a) (Primary u b)
-> m (j := Primary t a) (j := Primary u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
(<$>) (m (t a) (u b) -> m (Primary t a) (Primary u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) m (t a) (u b)
f)

	(=||$$>) :: (Covariant m m j, Covariant m m k, Interpreted m u)
		=> m (t a) (u b) -> m (j :. k := Primary t a) (j :. k := Primary u b)
	(=||$$>) m (t a) (u b)
f = m (Primary t a) (Primary u b)
-> m ((j :. k) := Primary t a) ((j :. k) := Primary u 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))
(<$$>) @m @m (m (t a) (u b) -> m (Primary t a) (Primary u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) m (t a) (u b)
f)

	(=||$$$>) :: (Covariant m m j, Covariant m m k, Covariant m m l, Interpreted m u)
		=> m (t a) (u b) -> m (j :. k :. l := Primary t a) (j :. k :. l := Primary u b)
	(=||$$$>) m (t a) (u b)
f = m (Primary t a) (Primary u b)
-> m ((j :. (k :. l)) := Primary t a)
     ((j :. (k :. l)) := Primary u b)
forall (source :: * -> * -> *) (between1 :: * -> * -> *)
       (between2 :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *)
       (u :: * -> *) (v :: * -> *) a b.
(Covariant source between1 v, Covariant between1 between2 u,
 Covariant between2 target t) =>
source a b -> target (t (u (v a))) (t (u (v b)))
(<$$$>) @m @m @m (m (t a) (u b) -> m (Primary t a) (Primary u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) m (t a) (u b)
f)

	(=||$$$$>) :: (Covariant m m j, Covariant m m k, Covariant m m l, Covariant m m n, Interpreted m u)
		=> m (t a) (u b) -> m (j :. k :. l :. n := Primary t a) (j :. k :. l :. n := Primary u b)
	(=||$$$$>) m (t a) (u b)
f = m (Primary t a) (Primary u b)
-> m ((j :. (k :. (l :. n))) := Primary t a)
     ((j :. (k :. (l :. n))) := Primary u b)
forall (source :: * -> * -> *) (between1 :: * -> * -> *)
       (between2 :: * -> * -> *) (between3 :: * -> * -> *)
       (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (w :: * -> *) a b.
(Covariant source between1 w, Covariant between1 between2 v,
 Covariant between2 between3 u, Covariant between3 target t) =>
source a b -> target (t (u (v (w a)))) (t (u (v (w b))))
(<$$$$>) @m @m @m @m (m (t a) (u b) -> m (Primary t a) (Primary u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (t a) (u b) -> m (Primary t a) (Primary u b)
(=||) m (t a) (u b)
f)

(-=:) :: (Liftable m t, Interpreted m (t u), Interpreted m (t v), Covariant m m u)
	=> m (t u a) (t v b) -> m (u a) (Primary (t v) b)
-=: :: m (t u a) (t v b) -> m (u a) (Primary (t v) b)
(-=:) m (t u a) (t v b)
f = m (t v b) (Primary (t v) b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run m (t v b) (Primary (t v) b)
-> m (u a) (t v b) -> m (u a) (Primary (t v) b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. m (t u a) (t v b)
f m (t u a) (t v b) -> m (u a) (t u a) -> m (u a) (t v b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. m (u a) (t u a)
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift

instance Interpreted (->) (Flip v a) where
	type Primary (Flip v a) e = v e a
	run :: Flip v a a -> Primary (Flip v a) a
run ~(Flip v a a
x) = v a a
Primary (Flip v a) a
x
	unite :: Primary (Flip v a) a -> Flip v a a
unite = Primary (Flip v a) a -> Flip v a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip

instance Interpreted (->) (Straight v e) where
	type Primary (Straight v e) a = v e a
	run :: Straight v e a -> Primary (Straight v e) a
run ~(Straight v e a
x) = v e a
Primary (Straight v e) a
x
	unite :: Primary (Straight v e) a -> Straight v e a
unite = Primary (Straight v e) a -> Straight v e a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight