module Pandora.Paradigm.Controlflow.Effect.Interpreted where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.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 t where
	{-# MINIMAL run, unite #-}
	type Primary t a :: *
	run :: t a -> Primary t a
	unite :: Primary t a -> t a

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

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

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

	(<$$||=) :: (Covariant (->) (->) j, Covariant (->) (->) k, Interpreted u)
		=> (Primary t a -> Primary u b) -> j :. k := t a -> j :. k := u b
	Primary t a -> Primary u b
f <$$||= (j :. k) := t a
x = (Primary t a -> Primary u b
f (Primary t a -> Primary u b) -> t a -> u b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||=) (t a -> u b) -> ((j :. k) := t a) -> (j :. k) := u b
forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant category category u, Covariant category category t) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- (j :. k) := t a
x

	(<$$$||=) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted u)
		=> (Primary t a -> Primary u b) -> j :. k :. l := t a -> j :. k :. l := u b
	Primary t a -> Primary u b
f <$$$||= (j :. (k :. l)) := t a
x = (Primary t a -> Primary u b
f (Primary t a -> Primary u b) -> t a -> u b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||=) (t a -> u b) -> ((j :. (k :. l)) := t a) -> (j :. (k :. l)) := u b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Covariant category category t, Covariant category category u,
 Covariant category category v) =>
category a b -> category (t (u (v a))) (t (u (v b)))
-<$$$>- (j :. (k :. l)) := t a
x

	(<$$$$||=) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) m, Interpreted u)
		=> (Primary t a -> Primary u b) -> j :. k :. l :. m := t a -> j :. k :. l :. m := u b
	Primary t a -> Primary u b
f <$$$$||= (j :. (k :. (l :. m))) := t a
x = (Primary t a -> Primary u b
f (Primary t a -> Primary u b) -> t a -> u b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||=) (t a -> u b)
-> ((j :. (k :. (l :. m))) := t a) -> (j :. (k :. (l :. m))) := u b
forall (category :: * -> * -> *) (t :: * -> *) (u :: * -> *)
       (v :: * -> *) (w :: * -> *) a b.
(Covariant category category t, Covariant category category u,
 Covariant category category v, Covariant category category w) =>
category a b -> category (t (u (v (w a)))) (t (u (v (w b))))
-<$$$$>- (j :. (k :. (l :. m))) := t a
x

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

	(=||$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Interpreted u)
		=> (t a -> u b) -> j :. k := Primary t a -> j :. k := Primary u b
	t a -> u b
f =||$$> (j :. k) := Primary t a
x = (t a -> u b
f (t a -> u b) -> Primary t a -> Primary u b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(t a -> u b) -> Primary t a -> Primary u b
=||) (Primary t a -> Primary u b)
-> ((j :. k) := Primary t a) -> (j :. k) := Primary u b
forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant category category u, Covariant category category t) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- (j :. k) := Primary t a
x

	(=||$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted u)
		=> (t a -> u b) -> j :. k :. l := Primary t a -> j :. k :. l := Primary u b
	t a -> u b
f =||$$$> (j :. (k :. l)) := Primary t a
x = (t a -> u b
f (t a -> u b) -> Primary t a -> Primary u b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(t a -> u b) -> Primary t a -> Primary u b
=||) (Primary t a -> Primary u b)
-> ((j :. (k :. l)) := Primary t a)
-> (j :. (k :. l)) := Primary u b
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Covariant category category t, Covariant category category u,
 Covariant category category v) =>
category a b -> category (t (u (v a))) (t (u (v b)))
-<$$$>- (j :. (k :. l)) := Primary t a
x

	(=||$$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) m, Interpreted u)
		=> (t a -> u b) -> j :. k :. l :. m := Primary t a -> j :. k :. l :. m := Primary u b
	t a -> u b
f =||$$$$> (j :. (k :. (l :. m))) := Primary t a
x = (t a -> u b
f (t a -> u b) -> Primary t a -> Primary u b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(t a -> u b) -> Primary t a -> Primary u b
=||) (Primary t a -> Primary u b)
-> ((j :. (k :. (l :. m))) := Primary t a)
-> (j :. (k :. (l :. m))) := Primary u b
forall (category :: * -> * -> *) (t :: * -> *) (u :: * -> *)
       (v :: * -> *) (w :: * -> *) a b.
(Covariant category category t, Covariant category category u,
 Covariant category category v, Covariant category category w) =>
category a b -> category (t (u (v (w a)))) (t (u (v (w b))))
-<$$$$>- (j :. (k :. (l :. m))) := Primary t a
x

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