{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Structure.Ability.Comprehension where

import Pandora.Core.Functor (type (:=))
import Pandora.Core.Morphism ((%))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Bindable (Bindable ((>>=)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))

newtype Comprehension t a = Comprehension (t <:.> Construction t := a)

instance Interpreted (Comprehension t) where
	type Primary (Comprehension t) a = t <:.> Construction t := a
	run :: Comprehension t a -> Primary (Comprehension t) a
run ~(Comprehension (t <:.> Construction t) := a
x) = Primary (Comprehension t) a
(t <:.> Construction t) := a
x
	unite :: Primary (Comprehension t) a -> Comprehension t a
unite = Primary (Comprehension t) a -> Comprehension t a
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension

instance Covariant (t <:.> Construction t) => Covariant (Comprehension t) where
	a -> b
f <$> :: (a -> b) -> Comprehension t a -> Comprehension t b
<$> Comprehension (t <:.> Construction t) := a
x = ((t <:.> Construction t) := b) -> Comprehension t b
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (((t <:.> Construction t) := b) -> Comprehension t b)
-> ((t <:.> Construction t) := b) -> Comprehension t b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> b
f (a -> b)
-> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (t <:.> Construction t) := a
x

instance (Avoidable t, Pointable t) => Pointable (Comprehension t) where
	point :: a |-> Comprehension t
point = ((t <:.> Construction t) := a) -> Comprehension t a
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (((t <:.> Construction t) := a) -> Comprehension t a)
-> (a -> (t <:.> Construction t) := a) -> a |-> Comprehension t
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((t :. Construction t) := a) -> (t <:.> Construction t) := a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((t :. Construction t) := a) -> (t <:.> Construction t) := a)
-> (a -> (t :. Construction t) := a)
-> a
-> (t <:.> Construction t) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction t a |-> t
forall (t :: * -> *) a. Pointable t => a |-> t
point (Construction t a |-> t)
-> (a -> Construction t a) -> a -> (t :. Construction t) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((t :. Construction t) := a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((t :. Construction t) := a) -> Construction t a)
-> ((t :. Construction t) := a) -> a -> Construction t a
forall a b c. (a -> b -> c) -> b -> a -> c
% (t :. Construction t) := a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Traversable (t <:.> Construction t) => Traversable (Comprehension t) where
	Comprehension (t <:.> Construction t) := a
x ->> :: Comprehension t a -> (a -> u b) -> (u :. Comprehension t) := b
->> a -> u b
f = ((t <:.> Construction t) := b) -> Comprehension t b
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (((t <:.> Construction t) := b) -> Comprehension t b)
-> u ((t <:.> Construction t) := b) -> (u :. Comprehension t) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> ((t <:.> Construction t) := a
x ((t <:.> Construction t) := a)
-> (a -> u b) -> u ((t <:.> Construction t) := b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f)

instance (forall a . Semigroup (t <:.> Construction t := a), Bindable t, Pointable t, Avoidable t) => Applicative (Comprehension t) where
	Comprehension t (a -> b)
fs <*> :: Comprehension t (a -> b) -> Comprehension t a -> Comprehension t b
<*> Comprehension t a
xs = Comprehension t (a -> b)
fs Comprehension t (a -> b)
-> ((a -> b) -> Comprehension t b) -> Comprehension t b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= \a -> b
f -> Comprehension t a
xs Comprehension t a -> (a -> Comprehension t b) -> Comprehension t b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= ((t <:.> Construction t) := b) -> Comprehension t b
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (((t <:.> Construction t) := b) -> Comprehension t b)
-> (a -> (t <:.> Construction t) := b) -> a -> Comprehension t b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((t :. Construction t) := b) -> (t <:.> Construction t) := b
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((t :. Construction t) := b) -> (t <:.> Construction t) := b)
-> (a -> (t :. Construction t) := b)
-> a
-> (t <:.> Construction t) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction t b |-> t
forall (t :: * -> *) a. Pointable t => a |-> t
point (Construction t b |-> t)
-> (a -> Construction t b) -> a -> (t :. Construction t) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. b |-> Construction t
forall (t :: * -> *) a. Pointable t => a |-> t
point (b |-> Construction t) -> (a -> b) -> a -> Construction t b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> b
f

instance (forall a . Semigroup (t <:.> Construction t := a), Bindable t) => Bindable (Comprehension t) where
	Comprehension (TU (t :. Construction t) := a
t) >>= :: Comprehension t a -> (a -> Comprehension t b) -> Comprehension t b
>>= a -> Comprehension t b
f = ((t <:.> Construction t) := b) -> Comprehension t b
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (((t <:.> Construction t) := b) -> Comprehension t b)
-> (((t :. Construction t) := b) -> (t <:.> Construction t) := b)
-> ((t :. Construction t) := b)
-> Comprehension t b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((t :. Construction t) := b) -> (t <:.> Construction t) := b
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((t :. Construction t) := b) -> Comprehension t b)
-> ((t :. Construction t) := b) -> Comprehension t b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (t :. Construction t) := a
t ((t :. Construction t) := a)
-> (Construction t a -> (t :. Construction t) := b)
-> (t :. Construction t) := b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= \(Construct a
x (t :. Construction t) := a
xs) -> ((t <:.> Construction t) := b) -> (t :. Construction t) := b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (((t <:.> Construction t) := b) -> (t :. Construction t) := b)
-> ((t <:.> Construction t) := b) -> (t :. Construction t) := b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ Comprehension t b -> Primary (Comprehension t) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (a -> Comprehension t b
f a
x) ((t <:.> Construction t) := b)
-> ((t <:.> Construction t) := b) -> (t <:.> Construction t) := b
forall a. Semigroup a => a -> a -> a
+ Comprehension t b -> Primary (Comprehension t) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant t (Construction t) a -> Comprehension t a
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (((t :. Construction t) := a)
-> TU Covariant Covariant t (Construction t) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (t :. Construction t) := a
xs) Comprehension t a -> (a -> Comprehension t b) -> Comprehension t b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= a -> Comprehension t b
f)