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

module Pandora.Paradigm.Structure.Modification.Prefixed where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)), (-<$$>-))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)), (-<<-<<-))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Algebraic ()
import Pandora.Paradigm.Primary.Algebraic.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 :. (:*:) k := a)

instance Interpreted (Prefixed t k) where
	type Primary (Prefixed t k) a = t :. (:*:) k := a
	run :: Prefixed t k a -> Primary (Prefixed t k) a
run ~(Prefixed (t :. (:*:) k) := a
x) = (t :. (:*:) 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 :. (:*:) 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 :. (:*:) k) := a
x = ((t :. (:*:) k) := b) -> Prefixed t k b
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (((t :. (:*:) k) := b) -> Prefixed t k b)
-> ((t :. (:*:) 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 :. (:*:) k) := a) -> (t :. (:*:) 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 :. (:*:) k) := a
x

instance Traversable t (->) (->) => Traversable (Prefixed t k) (->) (->) where
	a -> u b
f <<- :: (a -> u b) -> Prefixed t k a -> u (Prefixed t k b)
<<- Prefixed (t :. (:*:) k) := a
x = ((t :. (:*:) k) := b) -> Prefixed t k b
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (((t :. (:*:) k) := b) -> Prefixed t k b)
-> u ((t :. (:*:) k) := b) -> u (Prefixed t k b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f (a -> u b) -> ((t :. (:*:) k) := a) -> u ((t :. (:*:) k) := 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 :. (:*:) k) := a
x

instance (Monoid k, Pointable t (->)) => Pointable (Prefixed t k) (->) where
	point :: a -> Prefixed t k a
point = ((t :. (:*:) k) := a) -> Prefixed t k a
forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a
Prefixed (((t :. (:*:) k) := a) -> Prefixed t k a)
-> (a -> (t :. (:*:) k) := a) -> a -> Prefixed t k a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (k :*: a) -> (t :. (:*:) k) := a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point ((k :*: a) -> (t :. (:*:) k) := a)
-> (a -> k :*: a) -> a -> (t :. (:*:) k) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. k -> a -> k :*: a
forall s a. s -> a -> s :*: a
(:*:) k
forall a. Monoid a => a
zero

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 (k :*: a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed t k a -> t (k :*: a))
-> ((<:.>) (Tagged ('Into t)) (Prefixed t k) a -> Prefixed t k a)
-> (<:.>) (Tagged ('Into t)) (Prefixed t k) a
-> t (k :*: a)
forall (m :: * -> * -> *) b c a.
Semigroupoid 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 (k :*: a)
prefixed) = forall a. Extractable ((:*:) k) (->) => (k :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract @_ @(->) ((k :*: a) -> a) -> t (k :*: a) -> t a
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- t (k :*: a)
prefixed

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