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 ((<$>), (<$$>)))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Functor.Pointable (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 ((>>=)))
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.Controlflow (run)
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))

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
<$> Construction t a
x = b -> ((t :. Construction t) := b) -> Construction t b
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> b
f (a -> b) -> a -> b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract 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 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
<$$> 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 => Pointable (Construction t) where
	point :: a |-> Construction t
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 :: a <-| Construction t
extract ~(Construct a
x (t :. Construction t) := a
_) = a
x

instance Applicative t => Applicative (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 ((a -> b) <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction t (a -> b)
f (a -> b) -> a -> b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract 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 a b -> m a b
$ Construction t (a -> b) -> (:.) t (Construction t) (a -> b)
forall (t :: * -> *) a.
Construction t a -> (:.) t (Construction t) a
deconstruct Construction t (a -> b)
f (:.) 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
<**> Construction t a -> (t :. Construction t) := a
forall (t :: * -> *) a.
Construction t a -> (:.) t (Construction t) a
deconstruct Construction t a
x

instance Traversable t => Traversable (Construction t) where
	Construction t a
x ->> :: 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 <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction t 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
<*> 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
-> (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 => Bindable (Construction t) where
	Construction t a
x >>= :: 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 <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract (b <-| Construction t) -> (a -> Construction t b) -> a -> b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Construction t b
f (a -> b) -> a -> b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract 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 a b -> m a b
$ (Construction t b -> (t :. Construction t) := b
forall (t :: * -> *) a.
Construction t a -> (:.) t (Construction t) a
deconstruct (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
. a -> Construction t b
f (a -> (t :. Construction t) := b)
-> a -> (t :. Construction t) := b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction t 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
<+> (Construction t a -> (a -> Construction t b) -> Construction t b
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= a -> Construction t 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 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 (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 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) => Monad (Construction t) where

instance Covariant t => Comonad (Construction t) where

instance Lowerable Construction where
	lower :: Construction u ~> u
lower Construction u a
x = a <-| Construction u
forall (t :: * -> *) a. Extractable t => a <-| t
extract (a <-| Construction u) -> u (Construction u a) -> u a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> 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
	hoist :: (u ~> v) -> Construction u ~> Construction v
hoist u ~> v
f 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 <-| Construction u
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction u a
x) (((v :. Construction v) := a) -> Construction v a)
-> (u (Construction v a) -> (v :. Construction v) := a)
-> u (Construction v a)
-> Construction v a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. u (Construction v a) -> (v :. Construction v) := a
u ~> v
f (u (Construction v a) -> Construction v a)
-> u (Construction v a) -> Construction v a
forall (m :: * -> * -> *) a b. Category 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 :: * -> *) a b. Covariant t => (a -> b) -> 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 = (a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction t a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
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 <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
extract Construction t a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ a <-| Construction t
forall (t :: * -> *) a. Extractable t => a <-| t
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 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

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

iterate :: Covariant t => (a |-> t) -> (a |-> Construction t)
iterate :: (a |-> t) -> a |-> Construction t
iterate a |-> t
f 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 a b -> m a b
$ (a |-> t) -> a |-> Construction t
forall (t :: * -> *) a.
Covariant t =>
(a |-> t) -> a |-> Construction t
iterate a |-> t
f (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
forall (t :: * -> *) a. Extractable t => a <-| t
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 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

instance (Covariant u, Covariant t) => Covariant (t <:.> Construction u) where
	a -> b
f <$> :: (a -> b)
-> (<:.>) t (Construction u) a -> (<:.>) t (Construction u) b
<$> (<:.>) t (Construction u) a
g = ((t :. Construction u) := b) -> (<:.>) t (Construction u) 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 u) := b) -> (<:.>) t (Construction u) b)
-> ((t :. Construction u) := b) -> (<:.>) t (Construction u) b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> b
f (a -> b)
-> ((t :. Construction u) := a) -> (t :. Construction u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) t (Construction u) a
g

instance (Avoidable u, Pointable t) => Pointable (t <:.> Construction u) where
	point :: a |-> (t <:.> Construction u)
point a
x = ((t :. Construction u) := a)
-> TU Covariant Covariant t (Construction u) 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 u) := a)
 -> TU Covariant Covariant t (Construction u) a)
-> (((u :. Construction u) := a) -> (t :. Construction u) := a)
-> ((u :. Construction u) := a)
-> TU Covariant Covariant t (Construction u) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction u a |-> t
forall (t :: * -> *) a. Pointable t => a |-> t
point (Construction u a |-> t)
-> (((u :. Construction u) := a) -> Construction u a)
-> ((u :. Construction u) := a)
-> (t :. Construction u) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((u :. Construction u) := a) -> Construction u a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((u :. Construction u) := a)
 -> TU Covariant Covariant t (Construction u) a)
-> ((u :. Construction u) := a)
-> TU Covariant Covariant t (Construction u) a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (u :. Construction u) := a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance (Applicative u, Applicative t) => Applicative (t <:.> Construction u) where
	(<:.>) t (Construction u) (a -> b)
f <*> :: (<:.>) t (Construction u) (a -> b)
-> (<:.>) t (Construction u) a -> (<:.>) t (Construction u) b
<*> (<:.>) t (Construction u) a
x = ((t :. Construction u) := b) -> (<:.>) t (Construction u) 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 u) := b) -> (<:.>) t (Construction u) b)
-> ((t :. Construction u) := b) -> (<:.>) t (Construction u) b
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (<:.>) t (Construction u) (a -> b)
-> Primary (t <:.> Construction u) (a -> b)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) t (Construction u) (a -> b)
f ((t :. Construction u) := (a -> b))
-> ((t :. Construction u) := a) -> (t :. Construction u) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Applicative t, Applicative u) =>
((t :. u) := (a -> b)) -> ((t :. u) := a) -> (t :. u) := b
<**> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) t (Construction u) a
x

instance (Covariant u, Alternative t) => Alternative (t <:.> Construction u) where
	(<:.>) t (Construction u) a
x <+> :: (<:.>) t (Construction u) a
-> (<:.>) t (Construction u) a -> (<:.>) t (Construction u) a
<+> (<:.>) t (Construction u) a
y = ((t :. Construction u) := a) -> (<:.>) t (Construction u) 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 u) := a) -> (<:.>) t (Construction u) a)
-> ((t :. Construction u) := a) -> (<:.>) t (Construction u) a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) t (Construction u) a
x ((t :. Construction u) := a)
-> ((t :. Construction u) := a) -> (t :. Construction u) := a
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) t (Construction u) a
y

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

instance (Traversable u, Traversable t) => Traversable (t <:.> Construction u) where
	(<:.>) t (Construction u) a
g ->> :: (<:.>) t (Construction u) a
-> (a -> u b) -> (u :. (t <:.> Construction u)) := b
->> a -> u b
f = ((t :. Construction u) := b)
-> TU Covariant Covariant t (Construction u) 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 u) := b)
 -> TU Covariant Covariant t (Construction u) b)
-> u ((t :. Construction u) := b)
-> (u :. (t <:.> Construction u)) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) t (Construction u) a
g ((t :. Construction u) := a)
-> (a -> u b) -> u ((t :. Construction u) := 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