{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Structure.Modification.Comprehension where

import Pandora.Core.Functor (type (>), type (>>>>>), type (>>>>>>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~)))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<), (==<<)))
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.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Schemes.TT (TT (TT), 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.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Sum ((:+:))
import Pandora.Paradigm.Algebraic (empty, (<-|-<-|-))

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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (t <::> Construction t) >>>>> a
x

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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<-/- (t <::> Construction t) >>>>> a
x

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) right t, Semimonoidal (-->) (:*:) right (t <::> Construction t)) => Semimonoidal (-->) (:*:) right (Comprehension t) where
	mult :: (Comprehension t a :*: Comprehension t b)
--> Comprehension t (right a b)
mult = ((Comprehension t a :*: Comprehension t b)
 -> Comprehension t (right a b))
-> (Comprehension t a :*: Comprehension t b)
   --> Comprehension t (right a b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Comprehension t a :*: Comprehension t b)
  -> Comprehension t (right a b))
 -> (Comprehension t a :*: Comprehension t b)
    --> Comprehension t (right a b))
-> ((Comprehension t a :*: Comprehension t b)
    -> Comprehension t (right a b))
-> (Comprehension t a :*: Comprehension t b)
   --> Comprehension t (right a b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((t <::> Construction t) >>>>> right a b)
-> Comprehension t (right a b)
forall (t :: * -> *) a.
((t <::> Construction t) >>>>> a) -> Comprehension t a
Comprehension (((t <::> Construction t) >>>>> right a b)
 -> Comprehension t (right a b))
-> ((Comprehension t a :*: Comprehension t b)
    -> (t <::> Construction t) >>>>> right a b)
-> (Comprehension t a :*: Comprehension t b)
-> Comprehension t (right a b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (t :: * -> *) a b.
Semimonoidal (Straight (->)) (:*:) right t =>
(t a :*: t b) --> t (right a b)
mult @(-->) @(:*:) @right ((TT Covariant Covariant t (Construction t) a
  :*: TT Covariant Covariant t (Construction t) b)
 --> ((t <::> Construction t) >>>>> right a b))
-> (TT Covariant Covariant t (Construction t) a
    :*: TT Covariant Covariant t (Construction t) b)
-> (t <::> Construction t) >>>>> right a b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) ((TT Covariant Covariant t (Construction t) a
  :*: TT Covariant Covariant t (Construction t) b)
 -> (t <::> Construction t) >>>>> right a b)
-> ((Comprehension t a :*: Comprehension t b)
    -> TT Covariant Covariant t (Construction t) a
       :*: TT Covariant Covariant t (Construction t) b)
-> (Comprehension t a :*: Comprehension t b)
-> (t <::> Construction t) >>>>> right a b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((Comprehension t a -> TT Covariant Covariant t (Construction t) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Comprehension t a -> TT Covariant Covariant t (Construction t) a)
-> (Comprehension t b
    -> TT Covariant Covariant t (Construction t) b)
-> (Comprehension t a
    -> TT Covariant Covariant t (Construction t) a)
   :*: (Comprehension t b
        -> TT Covariant Covariant t (Construction t) b)
forall s a. s -> a -> s :*: a
:*: Comprehension t b -> TT Covariant Covariant t (Construction t) b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run) ((Comprehension t a -> TT Covariant Covariant t (Construction t) a)
 :*: (Comprehension t b
      -> TT Covariant Covariant t (Construction t) b))
-> (Comprehension t a :*: Comprehension t b)
-> TT Covariant Covariant t (Construction t) a
   :*: TT Covariant Covariant t (Construction t) b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d.
(Covariant m m (p a), Covariant m m (Flip p d),
 Interpreted m (Flip p d)) =>
(m a b :*: m c d) -> m (p a c) (p b d)
<-|-<-|-)

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) (Construction t), Semimonoidal (-->) (:*:) (:+:) t, Semimonoidal (-->) (:*:) (:+:) (Construction t), Monoidal (-->) (-->) (:*:) (:+:) t) => Monoidal (-->) (-->) (:*:) (:+:) (Comprehension t) where
	unit :: Proxy (:*:) -> (Unit (:+:) --> a) --> Comprehension t a
unit Proxy (:*:)
_ = ((Zero --> a) -> Comprehension t a)
-> Straight (->) (Zero --> a) (Comprehension t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Zero --> a) -> Comprehension t a)
 -> Straight (->) (Zero --> a) (Comprehension t a))
-> ((Zero --> a) -> Comprehension t a)
-> Straight (->) (Zero --> a) (Comprehension t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Zero --> a
_ -> ((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. Emptiable t => t a
empty

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 (TT (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.
Semigroupoid 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) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') >>> a) -> TT ct ct' t t' a
TT (((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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall (t :: * -> *) a.
Interpreted (->) t =>
((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < 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 (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< TT Covariant Covariant t (Construction t) a -> Comprehension t a
forall (t :: * -> *) a.
((t <::> Construction t) >>>>> a) -> Comprehension t a
Comprehension (TT Covariant Covariant t (Construction t) a -> Comprehension t a)
-> TT Covariant Covariant t (Construction t) a -> Comprehension t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((t :. Construction t) >>> a)
-> TT Covariant Covariant t (Construction t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') >>> a) -> TT ct ct' t t' a
TT (t :. Construction t) >>> a
xs)) (Construction t a -> (t :. Construction t) >>> b)
-> ((t :. Construction t) >>> a) -> (t :. Construction t) >>> b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (t :. Construction t) >>> a
t

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, Monoidal (-->) (-->) (:*:) (:*:) t) => Morphable Push (Comprehension t) where
	type Morphing Push (Comprehension t) = Exactly <:.:> Comprehension t >>>>>> (->)
	morphing :: (<::>) (Tagged 'Push) (Comprehension t) a
-> Morphing 'Push (Comprehension t) a
morphing (Comprehension t a -> TT Covariant Covariant t (Construction t) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Comprehension t a -> TT Covariant Covariant t (Construction t) a)
-> ((<::>) (Tagged 'Push) (Comprehension t) a -> Comprehension t a)
-> (<::>) (Tagged 'Push) (Comprehension t) a
-> TT Covariant Covariant t (Construction t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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 -> TT Covariant Covariant t (Construction t) a
xs) = (Exactly a -> Comprehension t a)
-> T_U Covariant Covariant (->) Exactly (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 ((Exactly a -> Comprehension t a)
 -> T_U Covariant Covariant (->) Exactly (Comprehension t) a)
-> (Exactly a -> Comprehension t a)
-> T_U Covariant Covariant (->) Exactly (Comprehension t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Exactly a
x) -> TT Covariant Covariant t (Construction t) a -> Comprehension t a
forall (t :: * -> *) a.
((t <::> Construction t) >>>>> a) -> Comprehension t a
Comprehension (TT Covariant Covariant t (Construction t) a -> Comprehension t a)
-> (TT Covariant Covariant t (Construction t) a
    -> TT Covariant Covariant t (Construction t) a)
-> TT Covariant Covariant t (Construction t) a
-> Comprehension t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction t a -> TT Covariant Covariant t (Construction t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction t a -> TT Covariant Covariant t (Construction t) a)
-> (TT Covariant Covariant t (Construction t) a
    -> Construction t a)
-> TT Covariant Covariant t (Construction t) a
-> TT Covariant Covariant t (Construction t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid 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)
-> (TT Covariant Covariant t (Construction t) a
    -> (t :. Construction t) >>> a)
-> TT Covariant Covariant t (Construction t) a
-> Construction t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant t (Construction t) a
-> (t :. Construction t) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant t (Construction t) a -> Comprehension t a)
-> TT Covariant Covariant t (Construction t) a -> Comprehension t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- TT Covariant Covariant t (Construction t) a
xs