module Pandora.Core.Interpreted where

import Pandora.Core.Functor (type (<), type (>))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Trip (Trip (Trip))
import Pandora.Pattern.Semigroupoid (Semigroupoid ((.)))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))

infixr 2 =#-, -#=

infixl 1 <~~~~~~~~
infixl 2 <~~~~~~~
infixl 3 <~~~~~~
infixl 4 <~~~~~
infixl 5 <~~~~
infixl 6 <~~~
infixl 7 <~~
infixl 8 <~

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

	(<~~~~~~~~), (<~~~~~~~), (<~~~~~~), (<~~~~~), (<~~~~), (<~~~), (<~~), (<~) :: m < t a < Primary t a
	(<~~~~~~~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~~~~~~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~~~~~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~~~~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~~~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~~) = (m < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
	(<~) = (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 < 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)
	--(<$$=#-) f = (<$$>) @m @m ((=#-) 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)
	--(-<$$$=#-) f = (<$$$>) @m @m @m ((=#-) 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)
	--(-#=$$>) f = (<$$>) @m @m ((-#=) 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)
	--(-#=$$$>) f = (<$$$>) @m @m @m ((-#=) 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 (->) (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

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 (->) (Trip v a b) where
	type Primary (Trip v a b) e = v e b a
	run :: ((->) < Trip v a b a) < Primary (Trip v a b) a
run ~(Trip v a b a
x) = v a b a
Primary (Trip v a b) a
x
	unite :: ((->) < Primary (Trip v a b) a) < Trip v a b a
unite = ((->) < Primary (Trip v a b) a) < Trip v a b a
forall (v :: * -> * -> * -> *) a b c. v c b a -> Trip v a b c
Trip