{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Structure.Modification.Prefixed where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Contravariant ((>$<))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Bindable (Bindable ((>>=)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Pattern.Object.Setoid (Setoid)
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), attached)
import Pandora.Paradigm.Primary.Functor.Predicate (equate)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic, find)
import Pandora.Paradigm.Structure.Interface.Dictionary (Dictionary ((?=)))

type Keyed k = Product k <:.> Maybe

newtype Prefixed t k a = Prefixed (t <:.> Keyed k := a)

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

instance Traversable t => Traversable (Prefixed t k) where
	Prefixed (t <:.> Keyed k) := a
x ->> :: Prefixed t k a -> (a -> u b) -> (u :. Prefixed t k) := b
->> a -> u b
f = ((t <:.> Keyed k) := b) -> Prefixed t k b
forall (t :: * -> *) k a. ((t <:.> Keyed k) := a) -> Prefixed t k a
Prefixed (((t <:.> Keyed k) := b) -> Prefixed t k b)
-> u ((t <:.> Keyed k) := b) -> (u :. Prefixed t k) := b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (t <:.> Keyed k) := a
x ((t <:.> Keyed k) := a) -> (a -> u b) -> u ((t <:.> Keyed k) := b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance (Monoid k, Pointable t) => Pointable (Prefixed t k) where
	point :: a :=> Prefixed t k
point = ((t <:.> Keyed k) := a) -> Prefixed t k a
forall (t :: * -> *) k a. ((t <:.> Keyed k) := a) -> Prefixed t k a
Prefixed (((t <:.> Keyed k) := a) -> Prefixed t k a)
-> (a -> (t <:.> Keyed k) := a) -> a :=> Prefixed t k
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Keyed k a -> (t <:.> Keyed k) := a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Keyed k a -> (t <:.> Keyed k) := a)
-> (a -> Keyed k a) -> a -> (t <:.> Keyed k) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Product k :. Maybe) := a) -> Keyed k a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Product k :. Maybe) := a) -> Keyed k a)
-> (a -> (Product k :. Maybe) := a) -> a -> Keyed k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. k -> Maybe a -> (Product k :. Maybe) := a
forall s a. s -> a -> Product s a
(:*:) k
forall a. Monoid a => a
zero (Maybe a -> (Product k :. Maybe) := a)
-> (a -> Maybe a) -> a -> (Product k :. Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Maybe a
forall a. a -> Maybe a
Just

instance (Monotonic (Keyed k a) (t (Keyed k a)), Setoid k) => Dictionary a k (Prefixed t k) where
	k
k ?= :: k -> Prefixed t k a -> Maybe a
?= Prefixed (t <:.> Keyed k) := a
x = Predicate (Keyed k a) -> t (Keyed k a) -> Maybe (Keyed k a)
forall a e (t :: * -> *).
(Monotonic a e, Pointable t, Avoidable t) =>
Predicate a -> e -> t a
find @(Keyed k a) ((k :*: Maybe a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: Maybe a) -> k)
-> (Keyed k a -> k :*: Maybe a) -> Keyed k a -> k
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Keyed k a -> k :*: Maybe a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Keyed k a -> k) -> Predicate k -> Predicate (Keyed k a)
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$< k :=> Predicate
forall a. Setoid a => a :=> Predicate
equate k
k) (((t <:.> Keyed k) := a) -> Primary (t <:.> Keyed k) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (t <:.> Keyed k) := a
x) Maybe (Keyed k a) -> (Keyed k a -> Maybe a) -> Maybe a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= Maybe a <:= Product k
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Maybe a <:= Product k)
-> (Keyed k a -> k :*: Maybe a) -> Keyed k a -> Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Keyed k a -> k :*: Maybe a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run