{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Structure.Modification.Prefixed where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>)), Covariant_ ((-<$>-)), (-<$$>-))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>), (->>>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Alternative (Alternative ((<+>)))
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Into), premorph)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)

newtype Prefixed t k a = Prefixed (t :. Product k := a)

instance Interpreted (Prefixed t k) where
	type Primary (Prefixed t k) a = t :. Product k := a
	run :: Prefixed t k a -> Primary (Prefixed t k) a
run ~(Prefixed (t :. Product k) := a
x) = (t :. Product k) := a
Primary (Prefixed t k) a
x
	unite :: Primary (Prefixed t k) a -> Prefixed t k a
unite = Primary (Prefixed t k) a -> Prefixed t k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed

instance Covariant t => Covariant (Prefixed t k) where
	a -> b
f <$> :: (a -> b) -> Prefixed t k a -> Prefixed t k b
<$> Prefixed (t :. Product k) := a
x = ((t :. Product k) := b) -> Prefixed t k b
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (((t :. Product k) := b) -> Prefixed t k b)
-> ((t :. Product k) := b) -> Prefixed t k b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f (a -> b) -> ((t :. Product k) := a) -> (t :. Product k) := b
forall (t :: * -> *) (u :: * -> *) a b.
(Covariant t, Covariant u) =>
(a -> b) -> ((t :. u) := a) -> (t :. u) := b
<$$> (t :. Product k) := a
x

instance Covariant_ t (->) (->) => Covariant_ (Prefixed t k) (->) (->) where
	a -> b
f -<$>- :: (a -> b) -> Prefixed t k a -> Prefixed t k b
-<$>- Prefixed (t :. Product k) := a
x = ((t :. Product k) := b) -> Prefixed t k b
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (((t :. Product k) := b) -> Prefixed t k b)
-> ((t :. Product k) := b) -> Prefixed t k b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f (a -> b) -> ((t :. Product k) := a) -> (t :. Product k) := 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 :. Product k) := a
x

instance Traversable t => Traversable (Prefixed t k) where
	Prefixed (t :. Product k) := a
x ->> :: Prefixed t k a -> (a -> u b) -> (u :. Prefixed t k) := b
->> a -> u b
f = ((t :. Product k) := b) -> Prefixed t k b
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (((t :. Product k) := b) -> Prefixed t k b)
-> u ((t :. Product k) := b) -> (u :. Prefixed t k) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (t :. Product k) := a
x ((t :. Product k) := a) -> (a -> u b) -> u ((t :. Product k) := 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 (Monoid k, Pointable t (->)) => Pointable (Prefixed t k) (->) where
	point :: a -> Prefixed t k a
point = ((t :. Product k) := a) -> Prefixed t k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (((t :. Product k) := a) -> Prefixed t k a)
-> (a -> (t :. Product k) := a) -> a -> Prefixed t k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product k a -> (t :. Product k) := a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (Product k a -> (t :. Product k) := a)
-> (a -> Product k a) -> a -> (t :. Product k) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. k -> a -> Product k a
forall s a. s -> a -> Product s a
(:*:) k
forall a. Monoid a => a
zero

instance Alternative t => Alternative (Prefixed t k) where
	Prefixed t k a
x <+> :: Prefixed t k a -> Prefixed t k a -> Prefixed t k a
<+> Prefixed t k a
y = ((t :. Product k) := a) -> Prefixed t k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (((t :. Product k) := a) -> Prefixed t k a)
-> ((t :. Product k) := a) -> Prefixed t k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Prefixed t k a -> Primary (Prefixed t k) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Prefixed t k a
x ((t :. Product k) := a)
-> ((t :. Product k) := a) -> (t :. Product k) := a
forall (t :: * -> *) a. Alternative t => t a -> t a -> t a
<+> Prefixed t k a -> Primary (Prefixed t k) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Prefixed t k a
y

instance Avoidable t => Avoidable (Prefixed t k) where
	empty :: Prefixed t k a
empty = ((t :. Product k) := a) -> Prefixed t k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (t :. Product k) := a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Covariant t => Morphable (Into t) (Prefixed t k) where
	type Morphing (Into t) (Prefixed t k) = t
	morphing :: (<:.>) (Tagged ('Into t)) (Prefixed t k) a
-> Morphing ('Into t) (Prefixed t k) a
morphing (Prefixed t k a -> t (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed t k a -> t (Product k a))
-> ((<:.>) (Tagged ('Into t)) (Prefixed t k) a -> Prefixed t k a)
-> (<:.>) (Tagged ('Into t)) (Prefixed t k) a
-> t (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Into t)) (Prefixed t k) a -> Prefixed t k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> t (Product k a)
prefixed) = Product k a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Product k a -> a) -> t (Product k a) -> t a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t (Product k a)
prefixed

type instance Nonempty (Prefixed t k) = Prefixed (Nonempty t) k