{-# 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.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

-- TODO: Try to generalize (->) here
instance Covariant (->) (->) t => Covariant (->) (->) (Prefixed t k) where
	<$> :: (a -> b) -> Prefixed t k a -> Prefixed t k b
(<$>) a -> b
f = (Primary (Prefixed t k) a -> Primary (Prefixed t k) b)
-> Prefixed t k a -> Prefixed t k b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(||=) ((a -> b) -> t (k :*: a) -> t (k :*: b)
forall (source :: * -> * -> *) (between :: * -> * -> *)
       (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Covariant source between u, Covariant between target t) =>
source a b -> target (t (u a)) (t (u b))
(<$$>) @(->) @(->) a -> b
f)

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 (Straight 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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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