{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Structure.Modification.Comprehension where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)), Covariant_ ((-<$>-)))
import Pandora.Pattern.Functor.Contravariant ((>$<))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Alternative (Alternative ((<+>)))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Push), premorph)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))

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 (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 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 (m a b) (m a b)
$ a -> b
f (a -> b)
-> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := b
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
-<$>- (t <:.> Construction t) := a
x

instance (Avoidable t, Pointable t (->)) => Pointable (Comprehension t) (->) where
	point :: a -> Comprehension t a
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 a
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 :. Construction t) := a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (Construction t a -> (t :. Construction t) := a)
-> (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 Alternative t => Alternative (Comprehension t) where
	Comprehension (t <:.> Construction t) := a
x <+> :: Comprehension t a -> Comprehension t a -> Comprehension t a
<+> Comprehension (t <:.> Construction t) := a
y = ((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)
-> ((t <:.> Construction t) := a) -> Comprehension t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t <:.> Construction t) := a
x ((t <:.> Construction t) := a)
-> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := a
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> (t <:.> Construction t) := a
y

instance (Avoidable t, Alternative t) => Avoidable (Comprehension t) where
	empty :: Comprehension t a
empty = ((t <:.> Construction t) := a) -> Comprehension t a
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (t <:.> Construction t) := a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Traversable (t <:.> Construction t) (->) (->) => Traversable (Comprehension t) (->) (->) where
	a -> u b
f <<- :: (a -> u b) -> Comprehension t a -> u (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)
-> u ((t <:.> Construction t) := b) -> u (Comprehension t b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f (a -> u b)
-> ((t <:.> Construction t) := a)
-> u ((t <:.> Construction t) := b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) (u :: * -> *) a b.
(Traversable t source target, Covariant_ u source target,
 Pointable u target, Semimonoidal u (:*:) source target) =>
source a (u b) -> target (t a) (u (t b))
<<- (t <:.> Construction t) := a
x

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 = (\a -> 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)
-> (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 :. Construction t) := b
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (Construction t b -> (t :. Construction t) := b)
-> (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 b
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (b -> Construction t b) -> (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 (a -> Comprehension t b) -> Comprehension t a -> Comprehension t b
forall (t :: * -> *) (source :: * -> * -> *) a b.
Bindable t source =>
source a (t b) -> source (t a) (t b)
=<< Comprehension t a
xs) ((a -> b) -> Comprehension t b)
-> Comprehension t (a -> b) -> Comprehension t b
forall (t :: * -> *) (source :: * -> * -> *) a b.
Bindable t source =>
source a (t b) -> source (t a) (t b)
=<< Comprehension t (a -> b)
fs

instance (forall a . Semigroup (t <:.> Construction t := a), Bindable t (->)) => Bindable (Comprehension t) (->) where
	a -> Comprehension t b
f =<< :: (a -> Comprehension t b) -> Comprehension t a -> Comprehension t b
=<< Comprehension (TU (t :. Construction t) := a
t) = ((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 (m a b) (m a 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)
-> (Comprehension t b -> (t <:.> Construction t) := b)
-> Comprehension t b
-> (t :. Construction t) := b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Comprehension t b -> (t <:.> Construction t) := b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Comprehension t b -> (t :. Construction t) := b)
-> Comprehension t b -> (t :. Construction t) := b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> Comprehension t b
f a
x Comprehension t b -> Comprehension t b -> Comprehension t b
forall a. Semigroup a => a -> a -> a
+ (a -> Comprehension t b
f (a -> Comprehension t b) -> Comprehension t a -> Comprehension t b
forall (t :: * -> *) (source :: * -> * -> *) a b.
Bindable t source =>
source a (t b) -> source (t a) (t b)
=<< 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))) (Construction t a -> (t :. Construction t) := b)
-> ((t :. Construction t) := a) -> (t :. Construction t) := b
forall (t :: * -> *) (source :: * -> * -> *) a b.
Bindable t source =>
source a (t b) -> source (t a) (t b)
=<< (t :. Construction t) := a
t
		-- t >>= \(Construct x xs) -> run . run $ f x + (Comprehension (TU xs) >>= f)

instance (forall a . Semigroup (t <:.> Construction t := a), Pointable t (->), Avoidable t, Bindable t (->)) => Monad (Comprehension t) where

instance Setoid (t <:.> Construction t := a) => Setoid (Comprehension t a) where
	Comprehension (t <:.> Construction t) := a
ls == :: Comprehension t a -> Comprehension t a -> Boolean
== Comprehension (t <:.> Construction t) := a
rs = (t <:.> Construction t) := a
ls ((t <:.> Construction t) := a)
-> ((t <:.> Construction t) := a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (t <:.> Construction t) := a
rs

instance Semigroup (t <:.> Construction t := a) => Semigroup (Comprehension t a) where
	Comprehension (t <:.> Construction t) := a
x + :: Comprehension t a -> Comprehension t a -> Comprehension t a
+ Comprehension (t <:.> Construction t) := a
y = ((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)
-> ((t <:.> Construction t) := a) -> Comprehension t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t <:.> Construction t) := a
x ((t <:.> Construction t) := a)
-> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := a
forall a. Semigroup a => a -> a -> a
+ (t <:.> Construction t) := a
y

instance Monoid (t <:.> Construction t := a) => Monoid (Comprehension t a) where
	zero :: Comprehension t a
zero = ((t <:.> Construction t) := a) -> Comprehension t a
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (t <:.> Construction t) := a
forall a. Monoid a => a
zero

instance (Covariant t, Covariant_ t (->) (->), Pointable t (->)) => Morphable Push (Comprehension t) where
	type Morphing Push (Comprehension t) = Identity <:.:> Comprehension t := (->)
	morphing :: (<:.>) (Tagged 'Push) (Comprehension t) a
-> Morphing 'Push (Comprehension t) a
morphing (Comprehension t a -> TU Covariant Covariant t (Construction t) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Comprehension t a -> TU Covariant Covariant t (Construction t) a)
-> ((<:.>) (Tagged 'Push) (Comprehension t) a -> Comprehension t a)
-> (<:.>) (Tagged 'Push) (Comprehension t) a
-> TU Covariant Covariant t (Construction t) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Push) (Comprehension t) a -> Comprehension t a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU Covariant Covariant t (Construction t) a
xs) = (Identity a -> Comprehension t a)
-> T_U Covariant Covariant (->) Identity (Comprehension t) a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Identity a -> Comprehension t a)
 -> T_U Covariant Covariant (->) Identity (Comprehension t) a)
-> (Identity a -> Comprehension t a)
-> T_U Covariant Covariant (->) Identity (Comprehension t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(Identity a
x) -> TU Covariant Covariant t (Construction t) a -> Comprehension t a
forall (t :: * -> *) a.
((t <:.> Construction t) := a) -> Comprehension t a
Comprehension (TU Covariant Covariant t (Construction t) a -> Comprehension t a)
-> (TU Covariant Covariant t (Construction t) a
    -> TU Covariant Covariant t (Construction t) a)
-> TU Covariant Covariant t (Construction t) a
-> Comprehension t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction t a -> TU Covariant Covariant t (Construction t) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction t a -> TU Covariant Covariant t (Construction t) a)
-> (TU Covariant Covariant t (Construction t) a
    -> Construction t a)
-> TU Covariant Covariant t (Construction t) a
-> TU Covariant Covariant 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
x (((t :. Construction t) := a) -> Construction t a)
-> (TU Covariant Covariant t (Construction t) a
    -> (t :. Construction t) := a)
-> TU Covariant Covariant t (Construction t) a
-> Construction t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant t (Construction t) a
-> (t :. Construction t) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant t (Construction t) a -> Comprehension t a)
-> TU Covariant Covariant t (Construction t) a -> Comprehension t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant t (Construction t) a
xs

instance Nullable (t <:.> Construction t) => Nullable (Comprehension t) where
	null :: (Predicate :. Comprehension t) := a
null = Comprehension t a -> (t <:.> Construction t) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Comprehension t a -> (t <:.> Construction t) := a)
-> Predicate ((t <:.> Construction t) := a)
-> (Predicate :. Comprehension t) := a
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$< Predicate ((t <:.> Construction t) := a)
forall k (t :: k -> *) (a :: k).
Nullable t =>
(Predicate :. t) := a
null