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

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid ((.))
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.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (!)))
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.Primary.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:))
import Pandora.Paradigm.Primary.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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! ((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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (\(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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! 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 (((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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! (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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! TT Covariant Covariant t (Construction t) a
xs