{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Construction where

import Pandora.Core.Functor (type (:.), type (:=), type (:=>), type (~>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)), (-<$$>-))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply_))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)), (-<<-<<-))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\), hoist))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Ringoid ((*))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Algebraic ((-<*>-))
import Pandora.Paradigm.Primary.Algebraic.Exponential ()
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:)((:*:)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce))
import Pandora.Paradigm.Schemes (type (<:.>))

infixr 7 .-+

data Construction t a = Construct a (t :. Construction t := a)

instance Covariant t (->) (->) => Covariant (Construction t) (->) (->) where
	a -> b
f -<$>- :: (a -> b) -> Construction t a -> Construction t b
-<$>- ~(Construct a
x (t :. Construction t) := a
xs) = b -> ((t :. Construction t) := b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((t :. Construction t) := b) -> Construction t b)
-> b -> ((t :. Construction t) := b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a -> b
f a
x (((t :. Construction t) := b) -> Construction t b)
-> ((t :. Construction t) := b) -> Construction 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 :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant u category category, Covariant t category category) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- (t :. Construction t) := a
xs

instance Covariant t (->) (->) => Extractable (Construction t) (->) where
	extract :: Construction t a -> a
extract ~(Construct a
x (t :. Construction t) := a
_) = a
x

instance (Covariant t (->) (->), Semimonoidal t (->) (:*:) (:*:)) => Semimonoidal (Construction t) (->) (:*:) (:*:) where
	multiply_ :: (Construction t a :*: Construction t b) -> Construction t (a :*: b)
multiply_ (Construct a
x (t :. Construction t) := a
xs :*: Construct b
y (t :. Construction t) := b
ys) = (a :*: b)
-> ((t :. Construction t) := (a :*: b)) -> Construction t (a :*: b)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a
x a -> b -> a :*: b
forall s a. s -> a -> s :*: a
:*: b
y) (forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
p (source (t a) (t b)) (t (target a b))
forall (target :: * -> * -> *) a b.
Semimonoidal (Construction t) (->) (:*:) target =>
(Construction t a :*: Construction t b)
-> Construction t (target a b)
multiply_ @_ @(->) @(:*:) ((Construction t a :*: Construction t b)
 -> Construction t (a :*: b))
-> t (Construction t a :*: Construction t b)
-> (t :. Construction t) := (a :*: b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- (((t :. Construction t) := a) :*: ((t :. Construction t) := b))
-> t (Construction t a :*: Construction t b)
forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
p (source (t a) (t b)) (t (target a b))
multiply_ ((t :. Construction t) := a
xs ((t :. Construction t) := a)
-> ((t :. Construction t) := b)
-> ((t :. Construction t) := a) :*: ((t :. Construction t) := b)
forall s a. s -> a -> s :*: a
:*: (t :. Construction t) := b
ys))

instance Traversable t (->) (->) => Traversable (Construction t) (->) (->) where
	a -> u b
f <<- :: (a -> u b) -> Construction t a -> u (Construction t b)
<<- ~(Construct a
x (t :. Construction t) := a
xs) = b -> ((t :. Construction t) := b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((t :. Construction t) := b) -> Construction t b)
-> u b -> u (((t :. Construction t) := b) -> Construction 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
x u (((t :. Construction t) := b) -> Construction t b)
-> u ((t :. Construction t) := b) -> u (Construction t b)
forall (t :: * -> *) a b.
Applicative_ t =>
t (a -> b) -> t a -> t b
-<*>- a -> u b
f (a -> u b)
-> ((t :. Construction t) := a) -> u ((t :. Construction t) := b)
forall (t :: * -> *) (u :: * -> *) (v :: * -> *)
       (category :: * -> * -> *) a b.
(Traversable t category category, Covariant u category category,
 Pointable u category, Semimonoidal u category (:*:) (:*:),
 Traversable v category category) =>
category a (u b) -> category (v (t a)) (u (v (t b)))
-<<-<<- (t :. Construction t) := a
xs

instance Covariant t (->) (->) => Extendable (Construction t) (->) where
	Construction t a -> b
f <<= :: (Construction t a -> b) -> Construction t a -> Construction t b
<<= Construction t a
x = b -> ((t :. Construction t) := b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (b -> ((t :. Construction t) := b) -> Construction t b)
-> b -> ((t :. Construction t) := b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction t a -> b
f Construction t a
x (((t :. Construction t) := b) -> Construction t b)
-> ((t :. Construction t) := b) -> Construction t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (Construction t a -> b
f (Construction t a -> b) -> Construction t a -> Construction t b
forall (t :: * -> *) (source :: * -> * -> *) a b.
Extendable t source =>
source (t a) b -> source (t a) (t b)
<<=) (Construction t a -> Construction t 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)
-<$>- Construction t a -> t (Construction t a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction t a
x

instance (Covariant t (->) (->)) => Comonad (Construction t) (->) where

instance Lowerable Construction where
	lower :: Construction u ~> u
lower Construction u a
x = forall a.
Extractable (Construction u) (->) =>
Construction u a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract @_ @(->) (Construction u a -> a) -> u (Construction u a) -> u a
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- Construction u a -> u (Construction u a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction u a
x

instance Hoistable Construction where
	u ~> v
f /|\ :: (u ~> v) -> Construction u ~> Construction v
/|\ Construction u a
x = a -> ((v :. Construction v) := a) -> Construction v a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((v :. Construction v) := a) -> Construction v a)
-> a -> ((v :. Construction v) := a) -> Construction v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction u a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction u a
x (((v :. Construction v) := a) -> Construction v a)
-> ((v :. Construction v) := a) -> Construction v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ u (Construction v a) -> (v :. Construction v) := a
u ~> v
f (u (Construction v a) -> (v :. Construction v) := a)
-> u (Construction v a) -> (v :. Construction v) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (u ~> v) -> Construction u ~> Construction v
forall k (t :: (* -> *) -> k -> *) (u :: * -> *) (v :: * -> *).
(Hoistable t, Covariant u (->) (->)) =>
(u ~> v) -> t u ~> t v
hoist u ~> v
f (Construction u a -> Construction v a)
-> u (Construction u a) -> u (Construction v a)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- Construction u a -> u (Construction u a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction u a
x

instance (Setoid a, forall b . Setoid b => Setoid (t b), Covariant t (->) (->)) => Setoid (Construction t a) where
	Construction t a
x == :: Construction t a -> Construction t a -> Boolean
== Construction t a
y = (Construction t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction t a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== Construction t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction t a
y) Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* (Construction t a -> (t :. Construction t) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction t a
x ((t :. Construction t) := a)
-> ((t :. Construction t) := a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== Construction t a -> (t :. Construction t) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction t a
y)

instance (Semigroup a, forall b . Semigroup b => Semigroup (t b), Covariant t (->) (->)) => Semigroup (Construction t a) where
	Construction t a
x + :: Construction t a -> Construction t a -> Construction t a
+ Construction t a
y = 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)
-> a -> ((t :. Construction t) := a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction t a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ Construction t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction t a
y (((t :. Construction t) := a) -> Construction t a)
-> ((t :. Construction t) := a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction t a -> (t :. Construction t) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction t a
x ((t :. Construction t) := a)
-> ((t :. Construction t) := a) -> (t :. Construction t) := a
forall a. Semigroup a => a -> a -> a
+ Construction t a -> (t :. Construction t) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction t a
y

instance (Monoid a, forall b . Semigroup b => Monoid (t b), Covariant t (->) (->)) => Monoid (Construction t a) where
	zero :: Construction t a
zero = a -> ((t :. Construction t) := a) -> Construction t a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
forall a. Monoid a => a
zero (t :. Construction t) := a
forall a. Monoid a => a
zero

instance Monotonic a (t :. Construction t := a) => Monotonic a (Construction t a) where
	reduce :: (a -> r -> r) -> r -> Construction t a -> r
reduce a -> r -> r
f r
r ~(Construct a
x (t :. Construction t) := a
xs) = a -> r -> r
f a
x (r -> r) -> r -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (a -> r -> r) -> r -> ((t :. Construction t) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (t :. Construction t) := a
xs

instance Monotonic a (t :. Construction t := a) => Monotonic a (t <:.> Construction t := a) where
	reduce :: (a -> r -> r) -> r -> ((t <:.> Construction t) := a) -> r
reduce a -> r -> r
f r
r = (a -> r -> r) -> r -> ((t :. Construction t) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (((t :. Construction t) := a) -> r)
-> (((t <:.> Construction t) := a) -> (t :. Construction t) := a)
-> ((t <:.> Construction t) := a)
-> r
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((t <:.> Construction t) := a) -> (t :. Construction t) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

deconstruct :: Construction t a -> t :. Construction t := a
deconstruct :: Construction t a -> (t :. Construction t) := a
deconstruct ~(Construct a
_ (t :. Construction t) := a
xs) = (t :. Construction t) := a
xs

-- Generate a construction from seed using effectful computation
(.-+) :: Covariant t (->) (->) => a :=> t -> a :=> Construction t
a :=> t
f .-+ :: (a :=> t) -> a :=> Construction t
.-+ a
x = 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)
-> ((t :. Construction t) := a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (a :=> t
f (a :=> t) -> a :=> Construction t
forall (t :: * -> *) a.
Covariant t (->) (->) =>
(a :=> t) -> a :=> Construction t
.-+) (a :=> Construction t) -> t a -> (t :. Construction t) := a
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- a :=> t
f a
x

section :: Comonad t (->) => t ~> Construction t
section :: t ~> Construction t
section t a
xs = 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)
-> a -> ((t :. Construction t) := a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract t a
xs (((t :. Construction t) := a) -> Construction t a)
-> ((t :. Construction t) := a) -> Construction t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a -> Construction t a
forall (t :: * -> *). Comonad t (->) => t ~> Construction t
section (t a -> Construction t a) -> t a -> (t :. Construction t) := a
forall (t :: * -> *) (source :: * -> * -> *) a b.
Extendable t source =>
source (t a) b -> source (t a) (t b)
<<= t a
xs