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))

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
<$> 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

-- 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 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
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