{-# 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.Traversable (Traversable ((<<-)), (-<<-<<-))
import Pandora.Paradigm.Primary.Algebraic (extract)
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 category category u, Covariant category category t) =>
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 (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
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 category category t, Covariant category category u,
 Monoidal category category (:*:) (:*:) u,
 Traversable category category v) =>
category a (u b) -> category (v (t a)) (u (v (t b)))
-<<-<<- (t :. (:*:) k) := a
x

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) = (k :*: a) -> a
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract ((k :*: a) -> a) -> t (k :*: a) -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- t (k :*: a)
prefixed

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