{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Construction where

import Pandora.Core.Functor (type (:.), type (:=), type (:=>), type (~>))
import Pandora.Pattern.Category ((.), ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>)), Covariant_ ((-<$>-)), (-<$$>-))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Functor.Pointable (Pointable (point), Pointable_ (point_))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Alternative (Alternative ((<+>)))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>), (<**>)))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>), (->>>)))
import Pandora.Pattern.Functor.Bindable (Bindable ((>>=), ($>>=)) , Bindable_ (join_))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>), extend))
import Pandora.Pattern.Functor.Monad (Monad)
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.Functor.Function ()
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 :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (t :. Construction t) := a
xs

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 (Avoidable t, Covariant_ t (->) (->)) => Pointable (Construction t) (->) where
	point :: a -> Construction t a
point 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
forall (t :: * -> *) a. Avoidable t => t a
empty

instance (Avoidable t, Covariant_ t (->) (->)) => Pointable_ (Construction t) (->) where
	point_ :: a -> Construction t a
point_ 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
forall (t :: * -> *) a. Avoidable t => t a
empty

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

instance Applicative t => Applicative (Construction t) where
	~(Construct a -> b
f (t :. Construction t) := (a -> b)
fs) <*> :: Construction t (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)
# (t :. Construction t) := (a -> b)
fs ((t :. Construction t) := (a -> b))
-> ((t :. Construction t) := a) -> (t :. Construction t) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Applicative t, Applicative u) =>
((t :. u) := (a -> b)) -> ((t :. u) := a) -> (t :. u) := b
<**> (t :. Construction t) := a
xs

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

instance (Alternative t, Covariant_ t (->) (->)) => Bindable (Construction t) where
	~(Construct a
x (t :. Construction t) := a
xs) >>= :: Construction t a -> (a -> Construction t b) -> Construction t b
>>= a -> Construction t b
f = 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 b -> b
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (a -> Construction t 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)
# Construction t b -> (t :. Construction t) := b
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (a -> Construction t b
f a
x) ((t :. Construction t) := b)
-> ((t :. Construction t) := b) -> (t :. Construction t) := b
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> (t :. Construction t) := a
xs ((t :. Construction t) := a)
-> (a -> Construction t b) -> (t :. Construction t) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Bindable t, Covariant u) =>
((u :. t) := a) -> (a -> t b) -> (u :. t) := b
$>>= a -> Construction t b
f

instance (Covariant_ t (->) (->), Alternative t) => Bindable_ (Construction t) (->) where
	join_ :: Construction t (Construction t a) -> Construction t a
join_ (Construct Construction t a
x (t :. Construction t) := Construction 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)
# Construction t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction t 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)
# 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 (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> (forall a.
Bindable_ (Construction t) (->) =>
Construction t (Construction t a) -> Construction t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Bindable_ t source =>
source (t (t a)) (t a)
join_ @_ @(->) (Construction t (Construction t a) -> Construction t a)
-> ((t :. Construction t) := Construction t a)
-> (t :. Construction t) := a
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
-<$>- (t :. Construction t) := Construction t a
xs)

instance Covariant t => Extendable (Construction t) where
	Construction t a
x =>> :: Construction t a -> (Construction t a -> b) -> Construction t b
=>> Construction t a -> b
f = 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) -> Construction t a -> Construction t b
forall (t :: * -> *) a b. Extendable t => (t a -> b) -> t a -> t b
extend Construction t a -> b
f (Construction t a -> Construction t b)
-> t (Construction t a) -> (t :. Construction t) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> 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 (Avoidable t, Alternative t, Covariant_ t (->) (->)) => Monad (Construction t) where

instance (Covariant t, 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, 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, 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, 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.
Category 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 :: * -> *) a b. Covariant t => (a -> b) -> 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
xs t a -> (t a -> Construction t a) -> (t :. Construction t) := a
forall (t :: * -> *) a b. Extendable t => t a -> (t a -> b) -> t b
=>> t a -> Construction t a
forall (t :: * -> *). Comonad t (->) => t ~> Construction t
section